Projection mismatch when declaring array-based SIMD

[matthiaskrgr]

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 https://github.com/model-checking/kani/issues/277

[celinval]

Thanks @matthiaskrgr, I believe this is related to https://github.com/model-checking/kani/issues/1926. We don't really support portable_simd yet. We should make this error at least more specific until we properly fix it.

[celinval]

BTW, we have fixed the original projection mismatch, but the given test still fails due to unsupported simd_as intrinsic.

[matthiaskrgr]

Right this no longer ICEs with 0.40, renders this fixed in my eyes, but we can also leave this open to track intrinsic stuff