ICE: Intrinsic simd_add crashes when using float vector

[celinval]

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>>