Fix spurious overflow counter examples. (#558)

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());
+}