Repository navigation
SIMD codegen: invalid splat/extract/insert/shuffle instantiations abort the whole crate #4952
Description
Kani's SIMD codegen stands in for rustc's E0511 monomorphization checks, because under Kani rustc's own codegen backend never runs. #4951 turned the comparison checks into a reported unsupported construct, so an invalid instantiation fails only the harnesses that reach it. These still report a compile error and call abort_if_errors(), so one bad instantiation stops codegen of the whole crate:
| Intrinsic | Check | intrinsic.rs |
|---|---|---|
simd_splat |
argument type must be the output's element type | Intrinsic::SimdSplat arm |
simd_extract |
return type must be the input's element type | codegen_intrinsic_simd_extract |
simd_insert |
inserted type must be the input's element type | codegen_intrinsic_simd_insert |
simd_shuffle |
index vector must be u32 lanes; result length and element type must match |
simd_shuffle_length, codegen_intrinsic_simd_shuffle |
Nothing in the standard library reaches these through autoharness today. But they have the same shape as #4950: a generic helper whose type parameters are independent (simd_splat<T, U>, simd_extract<T, U>) can be instantiated by autoharness with types no caller uses, and then the whole run aborts.
Suggested fix, matching #4951:
- turn each check into
codegen_unimplemented_stmt; - where cheap, have
invalid_simd_instantiation(kani_middle/codegen_units.rs) reject such candidates up front, so autoharness picks a valid instantiation instead.
The existing tests simd-splat-wrong-type, simd-extract-wrong-type, simd-insert-wrong-type, simd-shuffle-result-type-is-diff-type and simd-shuffle-result-type-is-diff-size pin the current compile errors and would move with the change.
Activity
Stop a SIMD comparison with float mask lanes from aborting the crate (m…
Report invalid SIMD splat/extract/insert/shuffle instantiations as un…