Invalid projection on firecracker regression with the 2022-11-20 rust toolchain

[zhassan-aws]

With the update to the 2022-11-20 rust toolchain, a debug assert is hit on the firecracker regression.
Command to run:

./scripts/codegen-firecracker.sh

Crash:

WARN kani_compiler::codegen_cprover_gotoc::codegen::place Unexpected type mismatch in projection:
Expr { value: Index { array: Expr { value: Symbol { identifier: "_RNvXsb_NtNtCs731DbSNn5GY_4core9core_simd6vectorINtB5_4SimdhKj1_EINtNtB9_7convert4FromAhBW_E4fromCsb5cH7nQNIBq_10micro_http::1::var_0" }, typ: Vector { typ: Unsignedbv { width: 8 }, size: 1 }, location: None }, index: Expr { value: IntConstant(0), typ: CInteger(SizeT), location: None } }, typ: Unsignedbv { width: 8 }, location: None }
Expr type
Unsignedbv { width: 8 }
Type from MIR
StructTag("tag-[_13358953601680865708; 1]")
thread '<unnamed>' panicked at 'Unexpected type mismatch in projection:
Expr { value: Index { array: Expr { value: Symbol { identifier: "_RNvXsb_NtNtCs731DbSNn5GY_4core9core_simd6vectorINtB5_4SimdhKj1_EINtNtB9_7convert4FromAhBW_E4fromCsb5cH7nQNIBq_10micro_http::1::var_0" }, typ: Vector { typ: Unsignedbv { width: 8 }, size: 1 }, location: None }, index: Expr { value: IntConstant(0), typ: CInteger(SizeT), location: None } }, typ: Unsignedbv { width: 8 }, location: None }
Expr type
Unsignedbv { width: 8 }
Type from MIR
StructTag("tag-[_13358953601680865708; 1]")', kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs:179:13
stack backtrace:
   0: rust_begin_unwind
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/std/src/panicking.rs:575:5
   1: core::panicking::panic_fmt
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/panicking.rs:65:14
   2: core::panicking::panic_display
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/panicking.rs:138:5
   3: kani_compiler::codegen_cprover_gotoc::codegen::place::ProjectedPlace::try_new
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs:179:13
   4: kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_projection
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs:422:17
   5: kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place::{{closure}}
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs:579:53
   6: core::iter::adapters::copied::copy_fold::{{closure}}
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/iter/adapters/copied.rs:31:22
   7: core::iter::traits::iterator::Iterator::fold
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/iter/traits/iterator.rs:2414:21
   8: <core::iter::adapters::copied::Copied<I> as core::iter::traits::iterator::Iterator>::fold
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/iter/adapters/copied.rs:76:9
   9: kani_compiler::codegen_cprover_gotoc::codegen::place::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_place
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs:576:22
  10: kani_compiler::codegen_cprover_gotoc::codegen::statement::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_statement
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs:54:72
  11: kani_compiler::codegen_cprover_gotoc::codegen::block::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_block
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs:31:32
  12: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function::{{closure}}
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:85:69
  13: core::iter::traits::iterator::Iterator::for_each::call::{{closure}}
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/iter/traits/iterator.rs:828:29
  14: core::iter::adapters::map::map_fold::{{closure}}
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/iter/adapters/map.rs:84:21
  15: <core::iter::adapters::enumerate::Enumerate<I> as core::iter::traits::iterator::Iterator>::fold::enumerate::{{closure}}
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/iter/adapters/enumerate.rs:106:27
  16: core::iter::traits::iterator::Iterator::fold
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/iter/traits/iterator.rs:2414:21
  17: <core::iter::adapters::enumerate::Enumerate<I> as core::iter::traits::iterator::Iterator>::fold
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/iter/adapters/enumerate.rs:112:9
  18: <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::fold
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/iter/adapters/map.rs:124:9
  19: core::iter::traits::iterator::Iterator::for_each
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/core/src/iter/traits/iterator.rs:831:9
  20: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::codegen_function
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs:85:13
  21: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{{closure}}
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:116:31
  22: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info::{{closure}}
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:68:13
  23: std::thread::local::LocalKey<T>::try_with
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/std/src/thread/local.rs:446:16
  24: std::thread::local::LocalKey<T>::with
             at /rustc/c5d82ed7a4ad94a538bb87e5016e7d5ce0bd434b/library/std/src/thread/local.rs:422:9
  25: kani_compiler::codegen_cprover_gotoc::utils::debug::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs:65:9
  26: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
             at /home/ubuntu/git/kani/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs:115:21
  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_interface::passes::QueryContext>::enter::<<rustc_interface::queries::Queries>::ongoing_codegen::{closure#0}::{closure#0}, core::result::Result<alloc::boxed::Box<dyn core::any::Any>, rustc_errors::ErrorGuaranteed>>
  30: <rustc_interface::queries::Queries>::ongoing_codegen
  31: <rustc_interface::interface::Compiler>::enter::<rustc_driver::run_compiler::{closure#1}::{closure#2}, core::result::Result<core::option::Option<rustc_interface::queries::Linker>, rustc_errors::ErrorGuaranteed>>
  32: rustc_span::with_source_map::<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>::{closure#0}::{closure#1}>
  33: <scoped_tls::ScopedKey<rustc_span::SessionGlobals>>::set::<rustc_interface::interface::run_compiler<core::result::Result<(), rustc_errors::ErrorGuaranteed>, rustc_driver::run_compiler::{closure#1}>::{closure#0}, core::result::Result<(), rustc_errors::ErrorGuaranteed>>
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

Kani unexpectedly panicked during compilation.
If you are seeing this message, 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: <std::simd::Simd<u8, 1> as std::convert::From<[u8; 1]>>::from
_RNvXsb_NtNtCs731DbSNn5GY_4core9core_simd6vectorINtB5_4SimdhKj1_EINtNtB9_7convert4FromAhBW_E4fromCsb5cH7nQNIBq_10micro_http
[Kani] current codegen location: Loc { file: "/home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/portable-simd/crates/core_simd/src/vector.rs", function: None, start_line: 627, start_col: Some(5), end_line: 627, end_col: Some(39) }

[zhassan-aws]

Here's a minimal reproducer for the crash:

#[kani::proof]
fn main() {
    let _ = "abc".contains("a");
}

$ kani test.rs 
 WARN kani_compiler::codegen_cprover_gotoc::codegen::place Unexpected type mismatch in projection:
Expr { value: Index { array: Expr { value: Symbol { identifier: "_ZN116_$LT$core..core_simd..vector..Simd$LT$T$C$_$GT$$u20$as$u20$core..convert..From$LT$$u5b$T$u3b$$u20$LANES$u5d$$GT$$GT$4from17h25a1cc2542720844E::1::var_0" }, typ: Vector { typ: Unsignedbv { width: 8 }, size: 1 }, location: None }, index: Expr { value: IntConstant(0), typ: CInteger(SizeT), location: None } }, typ: Unsignedbv { width: 8 }, location: None }
Expr type
Unsignedbv { width: 8 }
Type from MIR
StructTag("tag-[_13358953601680865708; 1]")
thread '<unnamed>' panicked at 'Unexpected type mismatch in projection:
Expr { value: Index { array: Expr { value: Symbol { identifier: "_ZN116_$LT$core..core_simd..vector..Simd$LT$T$C$_$GT$$u20$as$u20$core..convert..From$LT$$u5b$T$u3b$$u20$LANES$u5d$$GT$$GT$4from17h25a1cc2542720844E::1::var_0" }, typ: Vector { typ: Unsignedbv { width: 8 }, size: 1 }, location: None }, index: Expr { value: IntConstant(0), typ: CInteger(SizeT), location: None } }, typ: Unsignedbv { width: 8 }, location: None }
Expr type
Unsignedbv { width: 8 }
Type from MIR
StructTag("tag-[_13358953601680865708; 1]")', kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs:181:13
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
If you are seeing this message, 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: <std::simd::Simd<u8, 1> as std::convert::From<[u8; 1]>>::from
_ZN116_$LT$core..core_simd..vector..Simd$LT$T$C$_$GT$$u20$as$u20$core..convert..From$LT$$u5b$T$u3b$$u20$LANES$u5d$$GT$$GT$4from17h25a1cc2542720844E
[Kani] current codegen location: Loc { file: "/home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/portable-simd/crates/core_simd/src/vector.rs", function: None, start_line: 627, start_col: Some(5), end_line: 627, end_col: Some(39) }
Error: /home/ubuntu/git/kani/target/kani/bin/kani-compiler exited with status exit status: 101

[zhassan-aws]

A minimal example that uses the culprit simd instruction directly:

#![feature(portable_simd)]

#[kani::proof]
fn main() {
    let x = "a".as_bytes();
    std::simd::u8x16::splat(x[0]);
}

[celinval]

I am relabeling this since this looks like an issue with SIMD support and @zhassan-aws has mitigated the crash seeing initially.

[zhassan-aws]

Some more information from debugging. The issue arises during codegen of the line involving move in this MIR function:

fn <std::simd::Simd<T, LANES> as std::convert::From<[T; LANES]>>::from(_1: [T; LANES]) -> std::simd::Simd<T, LANES> {
    debug array => _1;                   // in scope 0 at /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/../../portable-simd/crates/core_simd/src/vector.rs:627:13: 627:18
    let mut _0: std::simd::Simd<T, LANES>; // return place in scope 0 at /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/../../portable-simd/crates/core_simd/src/vector.rs:627:35: 627:39
    let mut _2: [T; LANES];              // in scope 0 at /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/../../portable-simd/crates/core_simd/src/vector.rs:628:14: 628:19

    bb0: {
        _2 = _1;                         // scope 0 at /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/../../portable-simd/crates/core_simd/src/vector.rs:628:14: 628:19
        Deinit(_0);                      // scope 0 at /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/../../portable-simd/crates/core_simd/src/vector.rs:628:9: 628:20
        (_0.0: [T; LANES]) = move _2;    // scope 0 at /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/../../portable-simd/crates/core_simd/src/vector.rs:628:9: 628:20
        return;                          // scope 0 at /home/ubuntu/.rustup/toolchains/nightly-2022-11-20-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/../../portable-simd/crates/core_simd/src/vector.rs:629:6: 629:6
    }
}

The MIR involves a field projection operation (ProjectionElem::Field) (handled here) where the type before projection is std::simd::Simd<u8, 1> and the field type is [T; LANES]. The Simd type is codegen as a vector here and the field projection is codegen as an array indexing operation here. However, the field type ([T; LANES]) is codegen as an array. This results in a mismatch in the result type: array index (from codegen of the field projection operation) vs. array (from codegen of the field MIR type).

[tedinski]

I find this MIR syntax inscrutable FWIW (_0.0: [T; LANES]) = move _2;

I think I can guess what that's saying, but since we're getting something slightly wrong here, I think getting pedantic here about what that syntax tree looks like will probably point to which way our translation is broken. I'm also not sure where the "coercion" is happening...

Because we're treating Simd<T, LANES> and [T; LANES] as equivalent in our back-end, but I think that MIR is saying "the .0 element of Simd<T, LANES> should have type [T; LANES]" which is either:

1. We're mistranslating simd types in our backend because they should be a struct of array, not just directly an array. That way .0 is the internal array of the struct (as opposed to "this first element of the vector" as it is translated now)
2. Is the 1 significant here? Maybe Rust is just like "[T; 1] is T no problem there"
3. We're supposed to spot some coercion that we're not seeing??