search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.21k stars 89 forks source link

`simd_shuffle*` doesn't check that `indexes` contains constant values which are within expected bounds #1960

Open adpaco-aws opened 1 year ago

adpaco-aws commented 1 year ago

The LLVM backend checks that all indexes supplied via the 3rd argument to simd_shuffle are:

  1. Constant values.
  2. Within bounds for the simd_shuffle operation (i.e., 2x the length of one of the first arguments).

At present, we do not perform this type check because we don't have access to the Builder type they use for constant evaluation. But we can probably do it some other way, or just use cprover types for it.

adpaco-aws commented 1 year ago

Actually, this would be more of an enhancement than unsupported UB. As discussed in #1961, verification shows an out-of-bounds failure because we don't check these indexes at compile time. It would be better to bring this check into the compilation stage, which is what this task would be about.