Remove temporary variables from translating MIR assert instructions (r…

…ust-lang#884)

* Remove temporary variables from Assert instructions

Use description function to get the user friendly message instead of
using the debug display method.

* Update test expected output

* Enhanced test

docs/src/tutorial/kinds-of-failure/add_overflow.expected

@@ -1 +1 @@
-[overflow::simple_addition.assertion.1] line 7 attempt to compute `move _3 + move _4`, which would overflow: FAILURE
+[overflow::simple_addition.assertion.1] line 7 attempt to add with overflow: FAILURE

docs/src/tutorial/kinds-of-failure/bound_check.expected

@@ -1,3 +1,3 @@
-[bounds_check::get_wrapped.assertion.3] line 11 index out of bounds: the length is move _12 but the index is _5: FAILURE
-[bounds_check::get_wrapped.pointer_dereference.5] line 11 dereference failure: pointer outside object bounds in a.data[var_5]: FAILURE
+line 11 index out of bounds: the length is less than or equal to the given index
+line 11 dereference failure: pointer outside object bounds in a.data[var_5]: FAILURE
 VERIFICATION FAILED

docs/src/tutorial/kinds-of-failure/midpoint_overflow.expected

@@ -1,2 +1,2 @@
-[overflow_quicksort::find_midpoint.assertion.1] line 7 attempt to compute `move _4 + move _5`, which would overflow: FAILURE
+[overflow_quicksort::find_midpoint.assertion.1] line 7 attempt to add with overflow: FAILURE
 VERIFICATION FAILED

src/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

@@ -8,7 +8,8 @@ use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir;
 use rustc_middle::mir::{
-    BasicBlock, Operand, Place, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind,
+    AssertKind, BasicBlock, Operand, Place, Statement, StatementKind, SwitchTargets, Terminator,
+    TerminatorKind,
 };
 use rustc_middle::ty;
 use rustc_middle::ty::layout::LayoutOf;
@@ -78,14 +79,24 @@ impl<'tcx> GotocCtx<'tcx> {
                     if *expected { r } else { Expr::not(r) }
                 };
 
+                let msg = if let AssertKind::BoundsCheck { .. } = msg {
+                    // For bounds check the following panic message is generated at runtime:
+                    // "index out of bounds: the length is {len} but the index is {index}",
+                    // but CBMC only accepts static messages so we don't add values to the message.
+                    "index out of bounds: the length is less than or equal to the given index"
+                } else {
+                    // For all other assert kind we can get the static message.
+                    msg.description()
+                };
+
                 Stmt::block(
                     vec![
                         cond.cast_to(Type::bool()).if_then_else(
                             Stmt::goto(self.current_fn().find_label(target), loc.clone()),
                             None,
                             loc.clone(),
                         ),
-                        Stmt::assert_false(&format!("{:?}", msg), loc.clone()),
+                        Stmt::assert_false(msg, loc.clone()),
                         Stmt::goto(self.current_fn().find_label(target), loc.clone()),
                     ],
                     loc,

tests/expected/array/expected

@@ -5,5 +5,5 @@ array 'x'.0 upper bound in x.0[var_3]: SUCCESS
 array 'x'.0 upper bound in x.0[var_5]: SUCCESS
 line 14 assertion failed: y[0] == 1: SUCCESS
 line 15 assertion failed: y[1] == 2: SUCCESS
-line 16 index out of bounds: the length is move _17 but the index is _16: FAILURE
+line 16 index out of bounds: the length is less than or equal to the given index: FAILURE
 line 16 assertion failed: y[z] == 3: FAILURE

tests/expected/binop/expected

@@ -1,38 +1,38 @@
-line 6 attempt to compute `move _8 + move _9`, which would overflow: SUCCESS
+line 6 attempt to add with overflow: SUCCESS
 line 6 assertion failed: a + b == correct: SUCCESS
-line 7 attempt to compute `move _15 + move _16`, which would overflow: SUCCESS
+line 7 attempt to add with overflow: SUCCESS
 line 7 assertion failed: a + b == wrong: FAILURE
-line 11 attempt to compute `move _8 - move _9`, which would overflow: SUCCESS
+line 11 attempt to subtract with overflow: SUCCESS
 line 11 assertion failed: a - b == correct: SUCCESS
-line 12 attempt to compute `move _15 - move _16`, which would overflow: SUCCESS
+line 12 attempt to subtract with overflow: SUCCESS
 line 12 assertion failed: a - b == wrong: FAILURE
-line 16 attempt to compute `move _8 * move _9`, which would overflow: SUCCESS
+line 16 attempt to multiply with overflow: SUCCESS
 line 16 assertion failed: a * b == correct: SUCCESS
-line 17 attempt to compute `move _15 * move _16`, which would overflow: SUCCESS
+line 17 attempt to multiply with overflow: SUCCESS
 line 17 assertion failed: a * b == wrong: FAILURE
-line 21 attempt to divide `_8` by zero: SUCCESS
-line 21 attempt to compute `_8 / _9`, which would overflow: SUCCESS
+line 21 attempt to divide by zero: SUCCESS
+line 21 attempt to divide with overflow: SUCCESS
 line 21 assertion failed: a / b == correct: SUCCESS
-line 22 attempt to divide `_18` by zero: SUCCESS
-line 22 attempt to compute `_18 / _19`, which would overflow: SUCCESS
+line 22 attempt to divide by zero: SUCCESS
+line 22 attempt to divide with overflow: SUCCESS
 line 22 assertion failed: a / b == wrong: FAILURE
-line 26 attempt to calculate the remainder of `_8` with a divisor of zero: SUCCESS
-line 26 attempt to compute the remainder of `_8 % _9`, which would overflow: SUCCESS
+line 26 attempt to calculate the remainder with a divisor of zero: SUCCESS
+line 26 attempt to calculate the remainder with overflow: SUCCESS
 line 26 assertion failed: a % b == correct: SUCCESS
-line 27 attempt to calculate the remainder of `_18` with a divisor of zero: SUCCESS
-line 27 attempt to compute the remainder of `_18 % _19`, which would overflow: SUCCESS
+line 27 attempt to calculate the remainder with a divisor of zero: SUCCESS
+line 27 attempt to calculate the remainder with overflow: SUCCESS
 line 27 assertion failed: a % b == wrong: FAILURE
-line 31 attempt to shift left by `move _9`, which would overflow: SUCCESS
+line 31 attempt to shift left with overflow: SUCCESS
 line 31 assertion failed: a << b == correct: SUCCESS
-line 32 attempt to shift left by `move _16`, which would overflow: SUCCESS
+line 32 attempt to shift left with overflow: SUCCESS
 line 32 assertion failed: a << b == wrong: FAILURE
-line 36 attempt to shift right by `move _9`, which would overflow: SUCCESS
+line 36 attempt to shift right with overflow: SUCCESS
 line 36 assertion failed: a >> b == correct: SUCCESS
-line 37 attempt to shift right by `move _16`, which would overflow: SUCCESS
+line 37 attempt to shift right with overflow: SUCCESS
 line 37 assertion failed: a >> b == wrong: FAILURE
-line 41 attempt to shift right by `move _9`, which would overflow: SUCCESS
+line 41 attempt to shift right with overflow: SUCCESS
 line 41 assertion failed: a >> b == correct: SUCCESS
-line 42 attempt to shift right by `move _16`, which would overflow: SUCCESS
+line 42 attempt to shift right with overflow: SUCCESS
 line 42 assertion failed: a >> b == wrong: FAILURE
 line 46 assertion failed: a & b == correct: SUCCESS
 line 47 assertion failed: a & b == wrong: FAILURE

tests/expected/closure/expected

@@ -1,6 +1,5 @@
-line 20 attempt to compute `move _8 + move _9`, which would overflow: SUCCESS
-line 20 attempt to compute `move _5 + move _6`, which would overflow: SUCCESS
-line 20 attempt to compute `(*((*_1).0: &mut i32)) + move _4`, which would overflow: SUCCESS
-line 25 attempt to compute `move _18 + const 12_i32`, which would overflow: SUCCESS
-line 25 assertion failed: original_num + 12 == num: SUCCESS
-line 25 arithmetic overflow on signed + in var_18 + 12: SUCCESS
+attempt to add with overflow: SUCCESS
+attempt to add with overflow: SUCCESS
+attempt to add with overflow: SUCCESS
+attempt to add with overflow: SUCCESS
+assertion failed: original_num + 12 == num: SUCCESS

tests/expected/closure/main.rs

@@ -2,7 +2,6 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 // kani-flags: --output-format old
-// cbmc-flags: --signed-overflow-check
 fn call_with_one<F>(mut some_closure: F) -> ()
 where
     F: FnMut(i64, i64) -> (),

tests/expected/closure2/expected

@@ -1,4 +1,4 @@
-line 7 attempt to compute `move _3 + move _4`, which would overflow: SUCCESS
-line 9 attempt to compute `move _3 + move _4`, which would overflow: SUCCESS
+line 7 attempt to add with overflow: SUCCESS
+line 9 attempt to add with overflow: SUCCESS
 line 10 assertion failed: z == 102: SUCCESS
 line 11 assertion failed: g(z) == 206: SUCCESS

tests/expected/closure3/expected

@@ -1,3 +1,3 @@
-line 16 attempt to compute `move _3 + move _4`, which would overflow: SUCCESS
-line 17 attempt to compute `move _11 + const 10_i64`, which would overflow: SUCCESS
+line 16 attempt to add with overflow: SUCCESS
+line 17 attempt to add with overflow: SUCCESS
 line 17 assertion failed: num + 10 == y: SUCCESS

tests/expected/comp/expected

@@ -1,11 +1,11 @@
-line 7 attempt to compute `move _6 + move _7`, which would overflow: SUCCESS
-line 7 attempt to compute `move _10 + move _11`, which would overflow: SUCCESS
+line 7 attempt to add with overflow: SUCCESS
+line 7 attempt to add with overflow: SUCCESS
 line 7 assertion failed: a + b == b + a: SUCCESS
-line 8 attempt to compute `move _16 + move _17`, which would overflow: SUCCESS
-line 8 attempt to compute `move _21 + move _22`, which would overflow: SUCCESS
-line 8 attempt to compute `move _20 + const 1_i32`, which would overflow: SUCCESS
+line 8 attempt to add with overflow: SUCCESS
+line 8 attempt to add with overflow: SUCCESS
+line 8 attempt to add with overflow: SUCCESS
 line 8 assertion failed: a + b != a + b + 1: SUCCESS
-line 13 attempt to compute `move _6 + move _7`, which would overflow: SUCCESS
+line 13 attempt to add with overflow: SUCCESS
 line 13 assertion failed: a + b > a: SUCCESS
-line 14 attempt to compute `move _13 - move _14`, which would overflow: SUCCESS
+line 14 attempt to subtract with overflow: SUCCESS
 line 14 assertion failed: a - b < a: SUCCESS

tests/expected/dynamic-trait/expected

@@ -1,9 +1,9 @@
-line 25 attempt to compute `move _2 * move _3`, which would overflow: SUCCESS
-line 28 attempt to compute `move _4 * move _5`, which would overflow: SUCCESS
-line 28 attempt to compute `move _3 * move _7`, which would overflow: SUCCESS
-line 34 attempt to compute `move _2 * move _3`, which would overflow: SUCCESS
-line 37 attempt to compute `move _4 * move _5`, which would overflow: SUCCESS
-line 37 attempt to compute `move _3 * move _7`, which would overflow: SUCCESS
+line 25 attempt to multiply with overflow: SUCCESS
+line 28 attempt to multiply with overflow: SUCCESS
+line 28 attempt to multiply with overflow: SUCCESS
+line 34 attempt to multiply with overflow: SUCCESS
+line 37 attempt to multiply with overflow: SUCCESS
+line 37 attempt to multiply with overflow: SUCCESS
 line 54 assertion failed: rec.vol(3) == 150: SUCCESS
 line 55 assertion failed: impl_area(rec.clone()) == 50: SUCCESS
 line 58 assertion failed: vol == 100: SUCCESS

tests/expected/iterator/expected

@@ -1,3 +1,3 @@
 line 7 unreachable code: SUCCESS
-line 8 attempt to compute `_1 * move _10`, which would overflow: SUCCESS
+line 8 attempt to multiply with overflow: SUCCESS
 line 10 assertion failed: z == 6: SUCCESS

tests/expected/nondet/expected

@@ -1,5 +1,5 @@
-line 9 attempt to compute `move _12 * move _13`, which would overflow: SUCCESS
-line 9 attempt to compute `const 2_i32 * move _16`, which would overflow: SUCCESS
-line 9 attempt to compute `move _11 - move _15`, which would overflow: SUCCESS
-line 9 attempt to compute `move _10 + const 1_i32`, which would overflow: SUCCESS
+line 9 attempt to multiply with overflow: SUCCESS
+line 9 attempt to multiply with overflow: SUCCESS
+line 9 attempt to subtract with overflow: SUCCESS
+line 9 attempt to add with overflow: SUCCESS
 line 9 assertion failed: x * x - 2 * x + 1 != 4 || (x == -1 || x == 3): SUCCESS

tests/expected/slice/expected

@@ -1,4 +1,4 @@
 line 17 assertion failed: y.len() == 5: SUCCESS
-line 18 index out of bounds: the length is move _16 but the index is _15: SUCCESS
+line 18 index out of bounds: the length is less than or equal to the given index: SUCCESS
 line 18 assertion failed: y[1] == 2: SUCCESS
 line 19 assertion failed: z.len() == 3: SUCCESS

tests/expected/test1/expected

@@ -1,5 +1,5 @@
-line 9 attempt to compute `_1 + move _4`, which would overflow: SUCCESS
-line 10 attempt to compute `_2 - const 1_i32`, which would overflow: SUCCESS
+line 9 attempt to add with overflow: SUCCESS
+line 10 attempt to subtract with overflow: SUCCESS
 line 14 assertion failed: a == 54: FAILURE
 line 16 assertion failed: a == 55: SUCCESS
 line 18 assertion failed: a >= 55: SUCCESS

tests/expected/test2/expected

@@ -1,5 +1,5 @@
-line 9 attempt to shift right by `const 1_i32`, which would overflow: SUCCESS
-line 10 attempt to compute `_2 + const 1_i32`, which would overflow: SUCCESS
+line 9 attempt to shift right with overflow: SUCCESS
+line 10 attempt to add with overflow: SUCCESS
 line 15 assertion failed: i == 3: FAILURE
 line 17 assertion failed: i == 2: SUCCESS
 line 19 assertion failed: i == 2 || i == 3: SUCCESS

tests/expected/test3/expected

@@ -1,4 +1,4 @@
-line 11 attempt to compute `_2 - const 1_i32`, which would overflow: SUCCESS
+line 11 attempt to subtract with overflow: SUCCESS
 line 17 assertion failed: a == 10.0 && i == 1: FAILURE
 line 19 assertion failed: a == 9.0 && i == 0: FAILURE
 line 21 assertion failed: a == 9.0 && i == 1: FAILURE

tests/expected/test4/expected

@@ -1,6 +1,6 @@
-line 10 attempt to compute `_2 + const 1_i32`, which would overflow: SUCCESS
+line 10 attempt to add with overflow: SUCCESS
 line 15 assertion failed: i == 3: FAILURE
 line 17 assertion failed: i == 2: SUCCESS
 line 19 assertion failed: i == 2 || i == 3: SUCCESS
-line 23 attempt to divide `_3` by zero: SUCCESS
-line 23 attempt to compute `_3 / _4`, which would overflow: SUCCESS
+line 23 attempt to divide by zero: SUCCESS
+line 23 attempt to divide with overflow: SUCCESS

tests/expected/test5/expected

@@ -1,4 +1,4 @@
 line 7 assertion failed: div(4, 2) == 2: SUCCESS
 line 9 assertion failed: div(6, 2) == 2: FAILURE
-line 13 attempt to divide `_3` by zero: SUCCESS
-line 13 attempt to compute `_3 / _4`, which would overflow: SUCCESS
+line 13 attempt to divide by zero: SUCCESS
+line 13 attempt to divide with overflow: SUCCESS

tests/kani/ArithOperators/unsafe_add_fail.rs

@@ -5,7 +5,7 @@
 // kani-verify-fail
 // kani-flags: --function check_add
 // compile-flags: --crate-type lib
-
+#[kani::proof]
 pub fn check_add(a: u8, b: u8) {
     unsafe {
         a + b;

tests/kani/ArithOperators/unsafe_mul_fail.rs

@@ -6,6 +6,7 @@
 // kani-flags: --function check_mul
 // compile-flags: --crate-type lib
 
+#[kani::proof]
 pub fn check_mul(a: u8, b: u8) {
     unsafe {
         a * b;

tests/kani/ArithOperators/unsafe_sub_fail.rs

@@ -6,6 +6,7 @@
 // kani-flags: --function check_sub
 // compile-flags: --crate-type lib
 
+#[kani::proof]
 pub fn check_sub(a: u8, b: u8) {
     unsafe {
         a - b;

tests/ui/check_operations/expected

@@ -0,0 +1,9 @@
+Failed Checks: attempt to add with overflow
+Failed Checks: attempt to subtract with overflow
+Failed Checks: attempt to multiply with overflow
+Failed Checks: attempt to divide by zero
+Failed Checks: attempt to calculate the remainder with a divisor of zero
+Failed Checks: attempt to shift left with overflow
+Failed Checks: attempt to shift right with overflow
+Failed Checks: attempt to negate with overflow
+Failed Checks: index out of bounds: the length is less than or equal to the given index

tests/ui/check_operations/operations.rs

@@ -0,0 +1,21 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check the message printed when a checked operation fails.
+// kani-flags: --unwind 3
+extern crate kani;
+
+use kani::any;
+
+#[kani::proof]
+fn main() {
+    let _ = any::<u8>() + any::<u8>();
+    let _ = any::<u8>() - any::<u8>();
+    let _ = any::<u8>() * any::<u8>();
+    let _ = any::<u8>() / any::<u8>();
+    let _ = any::<u8>() % any::<u8>();
+    let _ = any::<u8>() << any::<u8>();
+    let _ = any::<u8>() >> any::<u8>();
+    let _ = -any::<i8>();
+    let _ = kani::any::<[u8; 2]>()[any::<usize>()];
+}