Fix spurious overflow counter examples. (rust-lang#558) (rust-lang#647)

We cannot easily specify which arithmetic operations are wrapping ones to CBMC. Thus, CBMC was generating overflow checks for wrapping operations which were generating spurious failures. This change disables some of those CBMC checks. We replace them by using rustc overflow checks for regular operations and by explicitly adding checks to unchecked operations.

compiler/cbmc/src/goto_program/expr.rs

@@ -225,7 +225,7 @@ pub enum UnaryOperand {
     UnaryMinus,
 }
 
-/// The return type for `__builtin_op_overflow` operations
+/// The return type for `__CPROVER_overflow_op` operations
 pub struct ArithmeticOverflowResult {
     /// If overflow did not occur, the result of the operation. Otherwise undefined.
     pub result: Expr,
@@ -849,8 +849,13 @@ impl Expr {
             // Floating Point Equalities
             IeeeFloatEqual | IeeeFloatNotequal => lhs.typ == rhs.typ && lhs.typ.is_floating_point(),
             // Overflow flags
-            OverflowMinus | OverflowMult | OverflowPlus => {
-                lhs.typ == rhs.typ && lhs.typ.is_integer()
+            OverflowMinus => {
+                (lhs.typ == rhs.typ && (lhs.typ.is_pointer() || lhs.typ.is_numeric()))
+                    || (lhs.typ.is_pointer() && rhs.typ.is_integer())
+            }
+            OverflowMult | OverflowPlus => {
+                (lhs.typ == rhs.typ && lhs.typ.is_integer())
+                    || (lhs.typ.is_pointer() && rhs.typ.is_integer())
             }
         }
     }

compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs

@@ -130,6 +130,60 @@ impl<'tcx> GotocCtx<'tcx> {
             }};
         }
 
+        // Intrinsics which encode a simple arithmetic operation with overflow check
+        macro_rules! codegen_op_with_overflow_check {
+            ($f:ident) => {{
+                let a = fargs.remove(0);
+                let b = fargs.remove(0);
+                let res = a.$f(b);
+                let check = Stmt::assert(
+                    res.overflowed.not(),
+                    format!("attempt to compute {} which would overflow", intrinsic).as_str(),
+                    loc,
+                );
+                let expr_place = self.codegen_expr_to_place(p, res.result);
+                Stmt::block(vec![expr_place, check], loc)
+            }};
+        }
+
+        // Intrinsics which encode a SIMD arithmetic operation with overflow check.
+        // We expand the overflow check because CBMC overflow operations don't accept array as
+        // argument.
+        macro_rules! codegen_simd_with_overflow_check {
+            ($op:ident, $overflow:ident) => {{
+                let a = fargs.remove(0);
+                let b = fargs.remove(0);
+                let mut check = Expr::bool_false();
+                if let Type::Vector { size, .. } = a.typ() {
+                    let a_size = size;
+                    if let Type::Vector { size, .. } = b.typ() {
+                        let b_size = size;
+                        assert_eq!(a_size, b_size, "Expected same length vectors",);
+                        for i in 0..*a_size {
+                            // create expression
+                            let index = Expr::int_constant(i, Type::ssize_t());
+                            let v_a = a.clone().index_array(index.clone());
+                            let v_b = b.clone().index_array(index);
+                            check = check.or(v_a.$overflow(v_b));
+                        }
+                    }
+                }
+                let check_stmt = Stmt::assert(
+                    check.not(),
+                    format!("attempt to compute {} which would overflow", intrinsic).as_str(),
+                    loc,
+                );
+                let res = a.$op(b);
+                let expr_place = self.codegen_expr_to_place(p, res);
+                Stmt::block(vec![expr_place, check_stmt], loc)
+            }};
+        }
+
+        // Intrinsics which encode a simple wrapping arithmetic operation
+        macro_rules! codegen_wrapping_op {
+            ($f:ident) => {{ codegen_intrinsic_binop!($f) }};
+        }
+
         // Intrinsics which encode a simple binary operation
         macro_rules! codegen_intrinsic_boolean_binop {
             ($f:ident) => {{ self.binop(p, fargs, |a, b| a.$f(b).cast_to(Type::c_bool())) }};
@@ -203,6 +257,7 @@ impl<'tcx> GotocCtx<'tcx> {
         // *var1 = op(*var1, var2);
         // var = tmp;
         // -------------------------
+        // Note: Atomic arithmetic operations wrap around on overflow.
         macro_rules! codegen_atomic_binop {
             ($op: ident) => {{
                 warn!("RMC does not support concurrency for now. {} treated as a sequential operation.", intrinsic);
@@ -227,7 +282,7 @@ impl<'tcx> GotocCtx<'tcx> {
         match intrinsic {
             "abort" => Stmt::assert_false("abort intrinsic", loc),
             "add_with_overflow" => codegen_op_with_overflow!(add_overflow),
-            "arith_offset" => codegen_intrinsic_binop!(plus),
+            "arith_offset" => codegen_wrapping_op!(plus),
             "assert_inhabited" => {
                 let ty = instance.substs.type_at(0);
                 let layout = self.layout_of(ty);
@@ -356,7 +411,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "nearbyintf32" => codegen_simple_intrinsic!(Nearbyintf),
             "nearbyintf64" => codegen_simple_intrinsic!(Nearbyint),
             "needs_drop" => codegen_intrinsic_const!(),
-            "offset" => codegen_intrinsic_binop!(plus),
+            "offset" => codegen_op_with_overflow_check!(add_overflow),
             "powf32" => codegen_simple_intrinsic!(Powf),
             "powf64" => codegen_simple_intrinsic!(Pow),
             "powif32" => codegen_simple_intrinsic!(Powif),
@@ -376,7 +431,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "saturating_sub" => codegen_intrinsic_binop_with_mm!(saturating_sub),
             "sinf32" => codegen_simple_intrinsic!(Sinf),
             "sinf64" => codegen_simple_intrinsic!(Sin),
-            "simd_add" => codegen_intrinsic_binop!(plus),
+            "simd_add" => codegen_simd_with_overflow_check!(plus, add_overflow_p),
             "simd_and" => codegen_intrinsic_binop!(bitand),
             "simd_div" => codegen_intrinsic_binop!(div),
             "simd_eq" => codegen_intrinsic_binop!(eq),
@@ -390,7 +445,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "simd_insert" => self.codegen_intrinsic_simd_insert(fargs, p, cbmc_ret_ty, loc),
             "simd_le" => codegen_intrinsic_binop!(le),
             "simd_lt" => codegen_intrinsic_binop!(lt),
-            "simd_mul" => codegen_intrinsic_binop!(mul),
+            "simd_mul" => codegen_simd_with_overflow_check!(mul, mul_overflow_p),
             "simd_ne" => codegen_intrinsic_binop!(neq),
             "simd_or" => codegen_intrinsic_binop!(bitor),
             "simd_rem" => codegen_intrinsic_binop!(rem),
@@ -404,7 +459,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 }
             }
             // "simd_shuffle#" => handled in an `if` preceding this match
-            "simd_sub" => codegen_intrinsic_binop!(sub),
+            "simd_sub" => codegen_simd_with_overflow_check!(sub, sub_overflow_p),
             "simd_xor" => codegen_intrinsic_binop!(bitxor),
             "size_of" => codegen_intrinsic_const!(),
             "size_of_val" => codegen_size_align!(size),
@@ -422,9 +477,9 @@ impl<'tcx> GotocCtx<'tcx> {
             "unaligned_volatile_load" => {
                 self.codegen_expr_to_place(p, fargs.remove(0).dereference())
             }
-            "unchecked_add" => codegen_intrinsic_binop!(plus),
+            "unchecked_add" => codegen_op_with_overflow_check!(add_overflow),
             "unchecked_div" => codegen_intrinsic_binop!(div),
-            "unchecked_mul" => codegen_intrinsic_binop!(mul),
+            "unchecked_mul" => codegen_op_with_overflow_check!(mul_overflow),
             "unchecked_rem" => codegen_intrinsic_binop!(rem),
             "unchecked_shl" => codegen_intrinsic_binop!(shl),
             "unchecked_shr" => {
@@ -434,15 +489,15 @@ impl<'tcx> GotocCtx<'tcx> {
                     codegen_intrinsic_binop!(lshr)
                 }
             }
-            "unchecked_sub" => codegen_intrinsic_binop!(sub),
+            "unchecked_sub" => codegen_op_with_overflow_check!(sub_overflow),
             "unlikely" => self.codegen_expr_to_place(p, fargs.remove(0)),
             "unreachable" => Stmt::assert_false("unreachable", loc),
             "volatile_copy_memory" => codegen_intrinsic_copy!(Memmove),
             "volatile_copy_nonoverlapping_memory" => codegen_intrinsic_copy!(Memcpy),
             "volatile_load" => self.codegen_expr_to_place(p, fargs.remove(0).dereference()),
-            "wrapping_add" => codegen_intrinsic_binop!(plus),
-            "wrapping_mul" => codegen_intrinsic_binop!(mul),
-            "wrapping_sub" => codegen_intrinsic_binop!(sub),
+            "wrapping_add" => codegen_wrapping_op!(plus),
+            "wrapping_mul" => codegen_wrapping_op!(mul),
+            "wrapping_sub" => codegen_wrapping_op!(sub),
             "write_bytes" => {
                 let dst = fargs.remove(0).cast_to(Type::void_pointer());
                 let val = fargs.remove(0).cast_to(Type::c_int());

compiler/rustc_codegen_rmc/src/codegen/rvalue.rs

@@ -470,6 +470,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     let relative_discr = if *niche_start == 0 {
                         niche_val
                     } else {
+                        // This should be a wrapping sub.
                         niche_val.sub(Expr::int_constant(*niche_start, discr_ty.clone()))
                     };
                     let relative_max =

compiler/rustc_codegen_rmc/src/compiler_interface.rs

@@ -58,6 +58,10 @@ impl CodegenBackend for GotocCodegenBackend {
     ) -> Box<dyn Any> {
         use rustc_hir::def_id::LOCAL_CRATE;
 
+        if !tcx.sess.overflow_checks() {
+            tcx.sess.err("RMC requires overflow checks in order to provide a sound analysis.")
+        }
+
         super::utils::init();
 
         let codegen_units: &'tcx [CodegenUnit<'_>] = tcx.collect_and_partition_mono_items(()).1;

scripts/rmc-rustc

@@ -54,6 +54,7 @@ then
 else
     set_rmc_lib_path
     RMC_FLAGS="-Z codegen-backend=gotoc \
+            -C overflow-checks=on \
             -Z trim-diagnostic-paths=no \
             -Z human_readable_cgu_names \
             --cfg=rmc \

scripts/rmc.py

@@ -21,14 +21,15 @@
 MEMORY_SAFETY_CHECKS = ["--bounds-check",
                         "--pointer-check",
                         "--pointer-primitive-check"]
+
+# We no longer use --(un)signed-overflow-check" by default since rust already add assertions for places where wrapping
+# is an error.
 OVERFLOW_CHECKS = ["--conversion-check",
                    "--div-by-zero-check",
                    "--float-overflow-check",
                    "--nan-check",
                    "--pointer-overflow-check",
-                   "--signed-overflow-check",
-                   "--undefined-shift-check",
-                   "--unsigned-overflow-check"]
+                   "--undefined-shift-check"]
 UNWINDING_CHECKS = ["--unwinding-assertions"]
 
 
@@ -172,6 +173,8 @@ def run_cmd(
 
         process = subprocess.CompletedProcess(None, EXIT_CODE_SUCCESS, stdout=cmd_line)
     else:
+        if verbose:
+            print(' '.join(cmd))
         process = subprocess.run(
             cmd, universal_newlines=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT,
             env=env, cwd=cwd)

src/test/expected/dry-run/expected

@@ -1,4 +1,4 @@
 rmc-rustc -Z symbol-mangling-version=v0 -Z symbol_table_passes=
 symtab2gb
 goto-cc --function main
-cbmc --bounds-check --pointer-check --pointer-primitive-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-overflow-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --object-bits 16 --function main
+cbmc --bounds-check --pointer-check --pointer-primitive-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-overflow-check --undefined-shift-check --unwinding-assertions --object-bits 16 --function main

src/test/firecracker/virtio-block-parse/main.rs

@@ -1,13 +1,6 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// rmc-flags: --no-overflow-checks
-
-// We use `--no-overflow-checks` in this test to avoid getting
-// a verification failure:
-// [overflow.1] arithmetic overflow on unsigned + in var_6 + var_7: FAILURE
-// Tracking issue: https://github.com/model-checking/rmc/issues/307
-
 // Example from Firecracker virtio block device
 // We test the parse function against an arbitrary guest memory
 

src/test/rmc/ArithOperators/unchecked.rs

@@ -0,0 +1,22 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check that none of these operations trigger spurious overflow checks.
+#![feature(unchecked_math)]
+
+macro_rules! verify_no_overflow {
+    ($cf: ident, $uf: ident) => {{
+        let a: u8 = rmc::nondet();
+        let b: u8 = rmc::nondet();
+        let checked = a.$cf(b);
+        rmc::assume(checked.is_some());
+        let unchecked = unsafe { a.$uf(b) };
+        assert!(checked.unwrap() == unchecked);
+    }};
+}
+
+fn main() {
+    verify_no_overflow!(checked_add, unchecked_add);
+    verify_no_overflow!(checked_sub, unchecked_sub);
+    verify_no_overflow!(checked_mul, unchecked_mul);
+}

src/test/rmc/ArithOperators/unchecked_add_fail.rs

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check that unchecked add trigger overflow checks.
+// rmc-verify-fail
+
+#![feature(unchecked_math)]
+
+pub fn main() {
+    let a: u8 = rmc::nondet();
+    let b: u8 = rmc::nondet();
+    unsafe { a.unchecked_add(b) };
+}

src/test/rmc/ArithOperators/unchecked_mul_fail.rs

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check that unchecked mul trigger overflow checks.
+// rmc-verify-fail
+
+#![feature(unchecked_math)]
+
+pub fn main() {
+    let a: u8 = rmc::nondet();
+    let b: u8 = rmc::nondet();
+    unsafe { a.unchecked_mul(b) };
+}

src/test/rmc/ArithOperators/unchecked_sub_fail.rs

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check that unchecked sub trigger overflow checks.
+// rmc-verify-fail
+
+#![feature(unchecked_math)]
+
+fn main() {
+    let a: u8 = rmc::nondet();
+    let b: u8 = rmc::nondet();
+    unsafe { a.unchecked_sub(b) };
+}

src/test/rmc/ArithOperators/unsafe.rs

@@ -0,0 +1,21 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check that none of these operations trigger spurious overflow checks.
+
+macro_rules! verify_no_overflow {
+    ($cf: ident, $uf: tt) => {{
+        let a: u8 = rmc::nondet();
+        let b: u8 = rmc::nondet();
+        let checked = a.$cf(b);
+        rmc::assume(checked.is_some());
+        let unchecked = unsafe { a $uf b };
+        assert!(checked.unwrap() == unchecked);
+    }};
+}
+
+fn main() {
+    verify_no_overflow!(checked_add, +);
+    verify_no_overflow!(checked_sub, -);
+    verify_no_overflow!(checked_mul, *);
+}

src/test/rmc/ArithOperators/unsafe_add_fail.rs

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check that regular arithmetic operations in unsafe blocks still trigger overflow checks.
+// rmc-verify-fail
+// rmc-flags: --function check_add
+// compile-flags: --crate-type lib
+
+pub fn check_add(a: u8, b: u8) {
+    unsafe {
+        a + b;
+    }
+}

src/test/rmc/ArithOperators/unsafe_mul_fail.rs

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check that regular arithmetic operations in unsafe blocks still trigger overflow checks.
+// rmc-verify-fail
+// rmc-flags: --function check_mul
+// compile-flags: --crate-type lib
+
+pub fn check_add(a: u8, b: u8) {
+    unsafe {
+        a * b;
+    }
+}

src/test/rmc/ArithOperators/unsafe_sub_fail.rs

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check that regular arithmetic operations in unsafe blocks still trigger overflow checks.
+// rmc-verify-fail
+// rmc-flags: --function check_sub
+// compile-flags: --crate-type lib
+
+pub fn check_sub(a: u8, b: u8) {
+    unsafe {
+        a - b;
+    }
+}

src/test/rmc/ArithOperators/wrapping.rs

@@ -0,0 +1,16 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Check that none of these operations trigger spurious overflow checks.
+#![feature(core_intrinsics)]
+
+fn main() {
+    let a: u8 = rmc::nondet();
+    let b: u8 = rmc::nondet();
+    let sum0 = core::intrinsics::wrapping_add(a, b);
+    let sum1 = a.wrapping_add(b);
+    let sum2 = a.checked_add(b);
+    assert!(sum0 == sum1);
+    assert!(sum1 >= b || sum2.is_none());
+    assert!(sum1 >= a || sum2.is_none());
+}