ICE: Kani compiler crashes when initializing a SIMD struct

[celinval]

I tried this code:

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

#[derive(Clone, Debug)]
#[repr(simd)]
struct CustomSimd<T, const LANES: usize>([T; LANES]);

#[kani::proof]
fn simd_vec() {
    std::hint::black_box(CustomSimd([0u8; 10]));
}

using the following command line invocation:

kani simd.rs

with Kani version: 0.31.0 (dev)

I expected to see this happen: Harness should succeed

Instead, this happened: Kani failed to compile the code due to an ICE.

Stack backtrace:

thread 'rustc' panicked at 'assertion failed: `(left == right)`
  left: `80`,
 right: `8`', cprover_bindings/src/goto_program/expr.rs:880:9
stack backtrace:
   0: rust_begin_unwind
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/std/src/panicking.rs:593:5
   1: core::panicking::panic_fmt
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/panicking.rs:67:14
   2: core::panicking::assert_failed_inner
   3: core::panicking::assert_failed
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/panicking.rs:229:5
   4: cprover_bindings::goto_program::expr::Expr::transmute_to
             at /kani/cprover_bindings/src/goto_program/expr.rs:880:9
   5: kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue_aggregate::{{closure}}
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:598:33
   6: core::iter::adapters::map::map_fold::{{closure}}
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/iter/adapters/map.rs:84:28
   7: core::iter::adapters::map::map_fold::{{closure}}
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/iter/adapters/map.rs:84:21
   8: core::iter::traits::iterator::Iterator::fold
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/iter/traits/iterator.rs:2481:21
   9: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/iter/adapters/map.rs:124:9
  10: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/iter/adapters/map.rs:124:9
  11: core::iter::traits::iterator::Iterator::for_each
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/iter/traits/iterator.rs:856:9
  12: alloc::vec::Vec<T,A>::extend_trusted
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/alloc/src/vec/mod.rs:2827:17
  13: <alloc::vec::Vec<T,A> as alloc::vec::spec_extend::SpecExtend<T,I>>::spec_extend
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/alloc/src/vec/spec_extend.rs:26:9
  14: <alloc::vec::Vec<T> as alloc::vec::spec_from_iter_nested::SpecFromIterNested<T,I>>::from_iter
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/alloc/src/vec/spec_from_iter_nested.rs:62:9
  15: <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/alloc/src/vec/spec_from_iter.rs:33:9
  16: <alloc::vec::Vec<T> as core::iter::traits::collect::FromIterator<T>>::from_iter
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/alloc/src/vec/mod.rs:2695:9
  17: core::iter::traits::iterator::Iterator::collect
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/iter/traits/iterator.rs:1895:9
  18: kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue_aggregate
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:588:21
  19: kani_compiler::codegen_cprover_gotoc::codegen::rvalue::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_rvalue
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs:716:17
  20: kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:54:33
  21: kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs:33:32
  22: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::{{closure}}
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:84:57
  23: core::iter::traits::iterator::Iterator::for_each::call::{{closure}}
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/iter/traits/iterator.rs:853:29
  24: core::iter::adapters::map::map_fold::{{closure}}
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/iter/adapters/map.rs:84:21
  25: <core::slice::iter::Iter<T> as core::iter::traits::iterator::Iterator>::fold
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/slice/iter/macros.rs:215:27
  26: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/iter/adapters/map.rs:124:9
  27: core::iter::traits::iterator::Iterator::for_each
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/core/src/iter/traits/iterator.rs:856:9
  28: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function
             at /kani/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:84:13
  29: 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
  30: 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/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:68:13
  31: std::thread::local::LocalKey<T>::try_with
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/std/src/thread/local.rs:270:16
  32: std::thread::local::LocalKey<T>::with
             at /rustc/fe7454bf439c93cbe9ac8a8f7fcfacd5a40244c2/library/std/src/thread/local.rs:246:9
  33: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info
             at /kani/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:65:9
  34: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items::{{closure}}
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:126:29
  35: kani_compiler::codegen_cprover_gotoc::compiler_interface::with_timer
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:738:15
  36: kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend::codegen_items
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:96:9
  37: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
             at /kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:242:25
  38: <rustc_session::session::Session>::time::<alloc::boxed::Box<dyn core::any::Any>, rustc_interface::passes::start_codegen::{closure#0}>
  39: rustc_interface::passes::start_codegen
  40: <rustc_middle::ty::context::GlobalCtxt>::enter::<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_span::ErrorGuaranteed>>
  41: <rustc_interface::queries::Queries>::ongoing_codegen
  42: 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}>
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: simd_vec
_RNvCsda83y15ZBjb_4simd8simd_vec
[Kani] current codegen location: Loc { file: "/kani/tests/kani/Intrinsics/SIMD/Operators/simd.rs", function: None, start_line: 16, start_col: Some(1), end_line: 16, end_col: Some(14) }
error: /kani/target/kani/bin/kani-compiler exited with status exit status: 101

It seems that inside codegen_rvalue_aggregate we are assuming that the SIMD structure has LANES elements of type T. However, it is legal for the type to have an array [T; LANES].

For example, that is how portable-simd uses the SIMD representation:

#[repr(simd)]
pub struct Simd<T, const N: usize>([T; N])
where
    LaneCount<N>: SupportedLaneCount,
    T: SimdElement;

[workingjubilee]

It seems that inside codegen_rvalue_aggregate we are assuming that the SIMD structure has LANES elements of type T. However, it is legal for the type to have an array [T; LANES].

We will be moving exclusively to the arrays in the future as our internal representation of these types, per this accepted MCP:

• Remove multi-field repr(simd) rust-lang/compiler-team#621

Just a bit of work to do to make that actually happen.

[celinval]

It seems that inside codegen_rvalue_aggregate we are assuming that the SIMD structure has LANES elements of type T. However, it is legal for the type to have an array [T; LANES].

We will be moving exclusively to the arrays in the future as our internal representation of these types, per this accepted MCP:

* [Remove multi-field `repr(simd)` rust-lang/compiler-team#621](https://github.com/rust-lang/compiler-team/issues/621)

Just a bit of work to do to make that actually happen.

That's good to know. I have to say, it is much cleaner. Thanks @workingjubilee for the heads up!

[scottmcm]

We've also discussed (rust-lang/stdarch#1422 (comment)) disallowing field projections into SIMD entirely, thus requiring it to go through CastKind::Transmute (or similar) to create these values.

If you think that would be good or bad for you, please let us know.

[celinval]

Hi @scottmcm, from our tool perspective, this will simplify our code generation. From a Rust user perspective, I'm curious to see how this restriction will look like, but I also think it's probably for the best since it will forbid a bunch of invalid usages that we've seen so far.