ICE: Simd operations crashes when using input that is not `repr(simd)`

I tried this code:

// simd.rs
#![feature(platform_intrinsics)]

extern "platform-intrinsic" {
    fn simd_add<T>(x: T, y: T) -> T;
    fn simd_eq<T, U>(x: T, y: T) -> U;
}

#[kani::proof]
fn check_invalid_sum() {
    let a = 'a';
    let b = 'b';
    let sum = unsafe { simd_add(a, b) };
    assert!(sum.is_lowercase());
}

using the following command line invocation:

kani simd.rs

with Kani version: 0.34.0 (dev)

I expected to see this happen: The code above shouldn't compile.

Note that the different simd operations display the same problem, there is no validation that the type representation is simd.

Instead, this happened: Kani's compiler crashed.

Backtrace:

``` Kani Rust Verifier 0.34.0 (standalone) warning: function `simd_eq` is never used --> non_simd.rs:12:8 | 12 | fn simd_eq(x: T, y: T) -> U; | ^^^^^^^ | = note: `#[warn(dead_code)]` on by default thread 'rustc' panicked at kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:1532:36: called `Option::unwrap()` on a `None` value stack backtrace: 0: rust_begin_unwind at /rustc/f3623871cfa0763c95ebd6ceafaa6dc2e44ca68f/library/std/src/panicking.rs:617:5 1: core::panicking::panic_fmt at /rustc/f3623871cfa0763c95ebd6ceafaa6dc2e44ca68f/library/core/src/panicking.rs:67:14 2: core::panicking::panic at /rustc/f3623871cfa0763c95ebd6ceafaa6dc2e44ca68f/library/core/src/panicking.rs:117:5 3: core::option::Option::unwrap at /rustc/f3623871cfa0763c95ebd6ceafaa6dc2e44ca68f/library/core/src/option.rs:935:21 4: kani_compiler::codegen_cprover_gotoc::codegen::intrinsic::::codegen_simd_op_with_overflow at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:1532:22 5: kani_compiler::codegen_cprover_gotoc::codegen::intrinsic::::codegen_intrinsic at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:503:27 6: kani_compiler::codegen_cprover_gotoc::codegen::intrinsic::::codegen_funcall_of_intrinsic at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs:58:21 7: kani_compiler::codegen_cprover_gotoc::codegen::statement::::codegen_funcall at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:516:20 8: kani_compiler::codegen_cprover_gotoc::codegen::statement::::codegen_terminator at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:156:17 9: kani_compiler::codegen_cprover_gotoc::codegen::block::::codegen_block at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs:66:29 10: kani_compiler::codegen_cprover_gotoc::codegen::function::::codegen_function::{{closure}} at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:84:57 11: core::iter::traits::iterator::Iterator::for_each::call::{{closure}} at /rustc/f3623871cfa0763c95ebd6ceafaa6dc2e44ca68f/library/core/src/iter/traits/iterator.rs:853:29 12: core::iter::adapters::map::map_fold::{{closure}} at /rustc/f3623871cfa0763c95ebd6ceafaa6dc2e44ca68f/library/core/src/iter/adapters/map.rs:84:21 13: as core::iter::traits::iterator::Iterator>::fold at /rustc/f3623871cfa0763c95ebd6ceafaa6dc2e44ca68f/library/core/src/slice/iter/macros.rs:232:27 14: as core::iter::traits::iterator::Iterator>::fold at /rustc/f3623871cfa0763c95ebd6ceafaa6dc2e44ca68f/library/core/src/iter/adapters/map.rs:124:9 15: core::iter::traits::iterator::Iterator::for_each at /rustc/f3623871cfa0763c95ebd6ceafaa6dc2e44ca68f/library/core/src/iter/traits/iterator.rs:856:9 16: kani_compiler::codegen_cprover_gotoc::codegen::function::::codegen_function at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:84:13 17: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::{{closure}}::{{closure}} at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:127:39 18: kani_compiler::codegen_cprover_gotoc::utils::debug::::call_with_panic_debug_info::{{closure}} at /kani/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:68:13 19: std::thread::local::LocalKey::try_with at /rustc/f3623871cfa0763c95ebd6ceafaa6dc2e44ca68f/library/std/src/thread/local.rs:270:16 20: std::thread::local::LocalKey::with at /rustc/f3623871cfa0763c95ebd6ceafaa6dc2e44ca68f/library/std/src/thread/local.rs:246:9 21: kani_compiler::codegen_cprover_gotoc::utils::debug::::call_with_panic_debug_info at /kani/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:65:9 22: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::{{closure}} at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:126:29 23: kani_compiler::codegen_cprover_gotoc::compiler_interface::with_timer at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:738:15 24: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:96:9 25: ::codegen_crate at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:242:25 26: ::time::, rustc_interface::passes::start_codegen::{closure#0}> 27: rustc_interface::passes::start_codegen 28: ::enter::<::ongoing_codegen::{closure#0}, core::result::Result, rustc_span::ErrorGuaranteed>> 29: rustc_span::set_source_map::, rustc_interface::interface::run_compiler, rustc_driver_impl::run_compiler::{closure#1}>::{closure#0}::{closure#0}> note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace. Kani unexpectedly panicked during compilation. Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md [Kani] current codegen item: codegen_function: check_invalid_sum _RNvCs9Irx7EepS4M_8non_simd17check_invalid_sum [Kani] current codegen location: Loc { file: "/kani/tests/expected/intrinsics/simd-compile-errors/non_simd.rs", function: None, start_line: 16, start_col: Some(1), end_line: 16, end_col: Some(23) } warning: 1 warning emitted ```

model-checking / kani

ICE: Simd operations crashes when using input that is not `repr(simd)` #2692