-
Notifications
You must be signed in to change notification settings - Fork 95
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Invalid projection on firecracker regression with the 2022-11-20 rust toolchain #1926
Comments
Here's a minimal reproducer for the crash: #[kani::proof]
fn main() {
let _ = "abc".contains("a");
}
|
A minimal example that uses the culprit #![feature(portable_simd)]
#[kani::proof]
fn main() {
let x = "a".as_bytes();
std::simd::u8x16::splat(x[0]);
} |
I am relabeling this since this looks like an issue with SIMD support and @zhassan-aws has mitigated the crash seeing initially. |
Some more information from debugging. The issue arises during codegen of the line involving 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 ( |
I find this MIR syntax inscrutable FWIW 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
|
ProjectPlace::try_new
on firecracker regression with the 2022-11-20 rust toolchain
Just wanted to give some additional context: At the moment there are a few efforts to bring SIMD intrinsics into Rust, and I'd say the two main ones are:
Note that both approaches are still gated (unstable) features in Rust. But |
Even though this is a gated feature, it is currently used to implement |
Bad news.. I tried disabling this feature by compiling the standard library with |
Note that after the mitigation for this issue, some
However, something like the harness bellow will fail to verify: #[kani::proof]
#[kani::unwind(5)]
fn check_contains() {
assert_eq!("Hello my good friend! How are you doing?".contains("good old friend"), false);
} The error is:
I also believe that after we fix this issue, we will bump into #2131 issue while trying to verify this harness. |
@tautschnig - would you mind helping with this one? Does CBMC have any support in this area? |
Disabling the feature doesn't seem the best option to me, as that'd basically mean that we avoid the problematic path for analysis, but the actual execution will still take it. Thus, Kani's analysis couldn't be trusted in that case. At present, we codegen a vector based on the If we removed this case, it's possible that |
I think I tried this and it didn't work. |
Do you recall what didn't work? |
|
Thanks, @zhassan-aws ! It doesn't look like a dead end to me, but of course we need to debug the example from here. |
With the update to the 2022-11-20 rust toolchain, a debug assert is hit on the firecracker regression.
Command to run:
Crash:
The text was updated successfully, but these errors were encountered: