search

model-checking / kani

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

Feature request: detect when Rustc hides UB (undefined behavior) when generating MIR #298

Open danielsn opened 3 years ago

danielsn commented 3 years ago

RMC operates at the MIR level. It is possible that the MIR generated by Rustc may make implementation decisions that hide UB.

Likelihood:

We do not have data on how often this occurs.

Mitigation:

We can disable some Rust optimizations on the command-line. We should test whether we get the same result given different optimization levels. By default, we should operate with all optimizations off.

Path to soundness:

Work with the compiler team to

Documentation:

zhassan-aws commented 2 years ago

Mitigate by documenting that Kani results are with respect to a specific compiler version and remove the soundness label.