Add an option to skip codegen

[zhassan-aws]

This PR adds a new unstable option, --no-codegen, that can be used for running Kani, just to check if the code compiles, i.e. similar to running cargo check. This is useful as a lightweight check for compilation errors including code under #[cfg(kani)].

This is implemented through passing rustc's -Zno-codegen option, which is what cargo check passes to rustc.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

[carolynzech]

If I run kani src/lib.rs -Z function-contracts on the following:

// Error: not a boolean expression
#[kani::requires(x - 2)]
fn main(x: u32) {
    let x: i32 = 5;
    // Error: different types
    let y: u32 = x;
    assert_eq!(y, 5);
}

I get these error messages:

error[E0308]: mismatched types
  --> src/fail.rs:2:18
   |
2  | #[kani::requires(x - 2)]
   | -----------------^^^^^--
   | |                |
   | |                expected `bool`, found `u32`
   | arguments to this function are incorrect
   |
note: function defined here
  --> /Users/cmzech/kani/library/kani/src/lib.rs:54:1
   |
54 | kani_core::kani_lib!(kani);
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^
   = note: this error originates in the macro `kani_core::kani_intrinsics` which comes from the expansion of the macro `kani_core::kani_lib` (in Nightly builds, run with -Z macro-backtrace for more info)

error[E0308]: mismatched types
 --> src/fail.rs:6:18
  |
6 |     let y: u32 = x;
  |            ---   ^ expected `u32`, found `i32`
  |            |
  |            expected due to this
  |
help: you can convert an `i32` to a `u32` and panic if the converted value doesn't fit
  |
6 |     let y: u32 = x.try_into().unwrap();
  |                   ++++++++++++++++++++

So my question is: how is this option better than just running Kani and seeing what happens? These type errors will cause Kani to abort before codegen already.

[zhassan-aws]

Right, but the point is the behavior in the case where there are no errors. This option makes it terminate immediately without going through codegen (similar to cargo check).

[carolynzech]

Two documentation nits, take them or leave them. The changes in phrasing are meant to make clearer that this is more useful than the default in the success case.