Command-line flag to change model target or environment

[DianaNites]

Requested feature: Command-line flag to change model target or environment

Use case: Proving certain errors don't happen on non-host targets

I have code that does some operations done that I believe could overflow, but only with a 16-bit usize. I wish to support this case, and use kani to check whether it does occur, and when I expect it to. The covered condition is reported UNREACHABLE on my 64-bit host, as expected.

Link to relevant documentation (Rust reference, Nomicon, RFC):

• https://doc.rust-lang.org/stable/reference/types/numeric.html?highlight=16-biit#machine-dependent-integer-types
• https://doc.rust-lang.org/stable/reference/conditional-compilation.html?highlight=target_poi#target_pointer_width
• The only 16-bit in-tree target, msp430-none-elf

[jswrenn]

Our use-cases:

Verifying Endian-Dependent Code

The zerocopy crate provides byte-order aware abstractions over the numeric types. Kani is used to prove that these abstractions are correct on little endian targets. With this feature, Kani could be used to verify that these abstractions are also correct for big endian targets.

Verify Complex Harnesses By Reducing Pointer Width

The zerocopy crate hopes to expand its use of Kani to verify the correctness of critical routines that operate over usizes. Unfortunately, the most natural ways to express proofs for these routines encounters catastrophically bad verification performance. However, these harnesses complete in reasonable time when usize is replaced with u16. Unfortunately, cannot make the routine-under-verification generic over numeric type (because these are const functions, and such functions cannot have bounded generics) --- we would need to duplicate-and-modify the routine-under-verification.

If Kani permitted verification on alternative targets, we could leave our routine and harness as-is, and merely run verification using a target with reduced pointer size.

[rahulku]

We need to update our documentation for supported architectures. Please see https://model-checking.github.io/kani/install-guide.html for a list of supported architectures.