Projection mismatch when declaring array-based SIMD #2264
Description
I tried this code:
#![feature(repr_simd, platform_intrinsics)]
extern "platform-intrinsic" {
fn simd_as<T, U>(x: T) -> U;
}
#[derive(Copy, Clone)]
#[repr(simd)]
struct V<T>([T; 2]);
#[kani::proof]
fn main() {
unsafe {
let u = V::<u32>([u32::MIN, u32::MAX]);
let i: V<i16> = simd_as(u);
}
}using the following command line invocation:
with Kani version: 0.22.0
I expected to see this happen: explanation
Instead, this happened: explanation
warning: unused variable: `i`
--> generic-as.rs:15:13
|
15 | let i: V<i16> = simd_as(u);
| ^ help: if this is intentional, prefix it with an underscore: `_i`
|
= note: `#[warn(unused_variables)]` on by default
WARN kani_compiler::codegen_cprover_gotoc::codegen::place Unexpected type mismatch in projection:
Expr { value: Index { array: Expr { value: Symbol { identifier: "main::1::var_1::u" }, typ: Vector { typ: Unsignedbv { width: 32 }, size: 2 }, location: None }, index: Expr { value: IntConstant(0), typ: CInteger(SizeT), location: None } }, typ: Unsignedbv { width: 32 }, location: None }
Expr type
Unsignedbv { width: 32 }
Type from MIR
StructTag("tag-[_18349839772473174998; 2]")
warning: Found the following unsupported constructs:
- Projection mismatch (1)
- simd_as (1)
Verification will fail if one or more of these constructs is reachable.
See https://model-checking.github.io/kani/rust-feature-support.html for more details.
warning: 2 warnings emitted
Checking harness main...
CBMC 5.77.0 (cbmc-5.77.0)
CBMC version 5.77.0 (cbmc-5.77.0) 64-bit x86_64 linux
Reading GOTO program from file /tmp/kani/generic_as.for-main.out
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
aborting path on assume(false) at thread 0
aborting path on assume(false) at file /tmp/kani/generic-as.rs line 15 column 25 function main thread 0
Runtime Symex: 0.000472428s
size of program expression: 29 steps
slicing removed 19 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.8535e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 1.3595e-05s
Running propositional reduction
Post-processing
Runtime Post-process: 3.617e-06s
Solving with MiniSAT 2.2.1 with simplifier
0 variables, 0 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 2.2102e-05s
Runtime decision procedure: 5.4061e-05s
RESULTS:
Check 1: unsupported_construct.1
- Status: FAILURE
- Description: "Projection mismatch is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/277"
Check 2: main.unsupported_construct.1
- Status: UNDETERMINED
- Description: "simd_as is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/new/choose"
- Location: generic-as.rs:15:25 in function main
SUMMARY:
** 1 of 2 failed (1 undetermined)
Failed Checks: Projection mismatch is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/277
VERIFICATION:- FAILED
** WARNING: A Rust construct that is not currently supported by Kani was found to be reachable. Check the results for more details.Verification Time: 0.01263466s
cc #277