ICE: Intrinsic simd_add crashes when using float vector #2631
Description
I tried this code:
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//! Ensure we can handle float vectors
#![allow(non_camel_case_types)]
#![feature(repr_simd, platform_intrinsics)]
extern "platform-intrinsic" {
fn simd_add<T>(x: T, y: T) -> T;
fn simd_eq<T, U>(x: T, y: T) -> U;
}
#[repr(simd)]
#[derive(Clone, PartialEq, kani::Arbitrary)]
pub struct f32x4(f32, f32);
impl f32x4 {
fn as_array(&self) -> &[f32; 2] {
unsafe { &*(self as *const f32x4 as *const [f32; 2]) }
}
}
#[kani::proof]
fn check_sum() {
let a = f32x4(0.0, 0.0);
let b = kani::any::<f32x4>();
let sum = unsafe { simd_add(a.clone(), b) };
assert_eq!(sum.as_array(), a.as_array());
}using the following command line invocation:
kani simd_float.rs
with Kani version: kani 0.33.0 (dev)
I expected to see this happen: Harness should verify correctly
Instead, this happened: Kani crashes
thread 'rustc' panicked at 'BinaryOperation Expression does not typecheck OverflowPlus Expr { value: Index { array: Expr { value: Symbol { identifier: "_RNvCs4OCrPoGFD1p_20simd_float_ops_fixme9check_sum::1::var_4" }, typ: Vector { typ: Float, size: 2 }, location: None, size_of_annotation: None }, index: Expr { value: IntConstant(0), typ: CInteger(SSizeT), location: None, size_of_annotation: None } }, typ: Float, location: None, size_of_annotation: None } Expr { value: Index { array: Expr { value: Symbol { identifier: "_RNvCs4OCrPoGFD1p_20simd_float_ops_fixme9check_sum::1::var_6" }, typ: Vector { typ: Float, size: 2 }, location: None, size_of_annotation: None }, index: Expr { value: IntConstant(0), typ: CInteger(SSizeT), location: None, size_of_annotation: None } }, typ: Float, location: None, size_of_annotation: None }', cprover_bindings/src/goto_program/expr.rs:1029:9
stack backtrace:
0: rust_begin_unwind
at /rustc/f4b80cacf93ca216c75f6ae12f4b9dec19eba42f/library/std/src/panicking.rs:593:5
1: core::panicking::panic_fmt
at /rustc/f4b80cacf93ca216c75f6ae12f4b9dec19eba42f/library/core/src/panicking.rs:67:14
2: cprover_bindings::goto_program::expr::Expr::binop
at /kani/cprover_bindings/src/goto_program/expr.rs:1029:9
3: cprover_bindings::goto_program::expr::Expr::add_overflow_p
at /kani/cprover_bindings/src/goto_program/expr.rs:1048:9
4: core::ops::function::Fn::call
at /rustc/f4b80cacf93ca216c75f6ae12f4b9dec19eba42f/library/core/src/ops/function.rs:79:5
5: kani_compiler::codegen_cprover_gotoc::codegen::intrinsic::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_simd_op_with_overflow
at /kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:1551:30
6: kani_compiler::codegen_cprover_gotoc::codegen::intrinsic::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_intrinsic
at /kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:503:27
7: kani_compiler::codegen_cprover_gotoc::codegen::intrinsic::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_funcall_of_intrinsic
at /kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:58:21
8: kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_funcall
at /kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:516:20
9: kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_terminator
at /kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:156:17
10: kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block
at /kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs:36:28
11: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::{{closure}}
at /kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:84:57
12: core::iter::traits::iterator::Iterator::for_each::call::{{closure}}
at /rustc/f4b80cacf93ca216c75f6ae12f4b9dec19eba42f/library/core/src/iter/traits/iterator.rs:853:29
13: core::iter::adapters::map::map_fold::{{closure}}
at /rustc/f4b80cacf93ca216c75f6ae12f4b9dec19eba42f/library/core/src/iter/adapters/map.rs:84:21
14: <core::slice::iter::Iter<T> as core::iter::traits::iterator::Iterator>::fold
at /rustc/f4b80cacf93ca216c75f6ae12f4b9dec19eba42f/library/core/src/slice/iter/macros.rs:215:27
15: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold
at /rustc/f4b80cacf93ca216c75f6ae12f4b9dec19eba42f/library/core/src/iter/adapters/map.rs:124:9
16: core::iter::traits::iterator::Iterator::for_each
at /rustc/f4b80cacf93ca216c75f6ae12f4b9dec19eba42f/library/core/src/iter/traits/iterator.rs:856:9
17: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function
at /kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:84:13
18: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::{{closure}}::{{closure}}
at /kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:127:39
19: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::{{closure}}
at /kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:68:13
20: std::thread::local::LocalKey<T>::try_with
at /rustc/f4b80cacf93ca216c75f6ae12f4b9dec19eba42f/library/std/src/thread/local.rs:270:16
21: std::thread::local::LocalKey<T>::with
at /rustc/f4b80cacf93ca216c75f6ae12f4b9dec19eba42f/library/std/src/thread/local.rs:246:9
22: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info
at /kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:65:9
23: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::{{closure}}
at /kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:126:29
24: kani_compiler::codegen_cprover_gotoc::compiler_interface::with_timer
at /kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:738:15
25: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
at /kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:96:9
26: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
at /kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:242:25
27: <rustc_session::session::Session>::time::<alloc::boxed::Box<dyn core::any::Any>, rustc_interface::passes::start_codegen::{closure#0}>
28: rustc_interface::passes::start_codegen
29: <rustc_middle::ty::context::GlobalCtxt>::enter::<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_span::ErrorGuaranteed>>
30: <rustc_interface::interface::Compiler>::enter::<rustc_driver_impl::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_span::ErrorGuaranteed>>
31: rustc_span::set_source_map::<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_interface::interface::run_compiler<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#1}>::{closure#0}::{closure#0}>
32: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_span::ErrorGuaranteed>, rustc_driver_impl::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_span::ErrorGuaranteed>>