Kani's assert macro implementation bypasses some compile-time checks

[zhassan-aws]

With PR #797, Kani's implementation of the assert macro's second form that accepts a custom message bypasses several compile-time checks.

For example, while rustc errors out on the following program:

fn main() {
    assert!(1 + 1 == 3, "Bad arithmetic: {}", foo);
}

output:

error[E0425]: cannot find value `foo` in this scope
 --> no_display.rs:2:47
  |
2 |     assert!(1 + 1 == 3, "Bad arithmetic: {}", foo);
  |                                               ^^^ not found in this scope

kani does not complain about the non-existence of the variable foo:

CBMC version 5.48.0 (cbmc-5.48.0) 64-bit x86_64 linux
Reading GOTO program from file no_display.goto
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 16 object bits, 48 offset bits (user-specified)
Starting Bounded Model Checking
Runtime Symex: 0.00102581s
size of program expression: 75 steps
simple slicing removed 3 assignments
Generated 3 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 7.25e-06s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000213004s
Running propositional reduction
Post-processing
Runtime Post-process: 2.594e-05s
Solving with MiniSAT 2.2.1 with simplifier
100 variables, 33 clauses
SAT checker: instance is SATISFIABLE
Runtime Solver: 9.1981e-05s
Runtime decision procedure: 0.000343287s

** Results:
[assertion.1] Code generation sanity check: Correct CBMC vtable size for StructTag("tag-_4317141983261250885") (MIR type Closure(DefId(2:9147 ~ std[2f3c]::rt::lang_start::{closure#0}), [(), i8, extern "rust-call" fn(()) -> i32, (fn(),)])). Please report failures:
https://github.com/model-checking/kani/issues/new?template=bug_report.md: SUCCESS
[pointer_primitives.1] dead object in OBJECT_SIZE(&temp_0): SUCCESS
/home/ubuntu/examples/no_display.rs function main
[main.assertion.1] line 2 assertion: "Bad arithmetic: {}", foo: FAILURE

** 1 of 3 failed (2 iterations)
VERIFICATION FAILED

Other checks that would be skipped by kani's assert macro are that the argument must implement the Display trait.

[celinval]

@zhassan-aws Haven't you fixed this yet?

[zhassan-aws]

No, this isn't fixed. I have an idea for fixing it, but I haven't had time for it.