From 9632276e4c27094541766c5f9d9fafe1cf24dc14 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 12 Nov 2021 19:15:00 -0800 Subject: [PATCH 1/5] Change overflow check to be generated by rmc (#558) --- compiler/cbmc/src/goto_program/expr.rs | 6 +- .../src/codegen/intrinsic.rs | 78 ++++++++++++++++--- .../rustc_codegen_rmc/src/codegen/rvalue.rs | 1 + scripts/rmc-rustc | 1 + scripts/rmc.py | 9 ++- src/test/expected/dry-run/expected | 2 +- src/test/rmc/ArithOperators/unchecked.rs | 22 ++++++ .../rmc/ArithOperators/unchecked_add_fail.rs | 13 ++++ .../rmc/ArithOperators/unchecked_mul_fail.rs | 13 ++++ .../rmc/ArithOperators/unchecked_sub_fail.rs | 13 ++++ src/test/rmc/ArithOperators/wrapping.rs | 15 ++++ src/test/rmc/Enum/discriminant.rs | 20 +++++ src/test/rmc/Enum/niche.rs | 22 ++++++ src/test/rmc/SIMD/Operators/overflow.rs | 39 ++++++++++ 14 files changed, 234 insertions(+), 20 deletions(-) create mode 100644 src/test/rmc/ArithOperators/unchecked.rs create mode 100644 src/test/rmc/ArithOperators/unchecked_add_fail.rs create mode 100644 src/test/rmc/ArithOperators/unchecked_mul_fail.rs create mode 100644 src/test/rmc/ArithOperators/unchecked_sub_fail.rs create mode 100644 src/test/rmc/ArithOperators/wrapping.rs create mode 100644 src/test/rmc/Enum/discriminant.rs create mode 100644 src/test/rmc/Enum/niche.rs create mode 100644 src/test/rmc/SIMD/Operators/overflow.rs diff --git a/compiler/cbmc/src/goto_program/expr.rs b/compiler/cbmc/src/goto_program/expr.rs index 6dafa01e3afd..2713452f349a 100644 --- a/compiler/cbmc/src/goto_program/expr.rs +++ b/compiler/cbmc/src/goto_program/expr.rs @@ -815,7 +815,7 @@ impl Expr { && (lhs.typ.is_pointer() || lhs.typ.is_numeric() || lhs.typ.is_vector()) || (lhs.typ.is_pointer() && rhs.typ.is_integer()) } - Plus => { + Plus | OverflowMinus | OverflowMult | OverflowPlus => { (lhs.typ == rhs.typ && (lhs.typ.is_numeric() || lhs.typ.is_vector())) || (lhs.typ.is_pointer() && rhs.typ.is_integer()) } @@ -848,10 +848,6 @@ 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() - } } } diff --git a/compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs b/compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs index 713aa55c3dc7..de5027feb18d 100644 --- a/compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs +++ b/compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs @@ -130,6 +130,61 @@ 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 + // RMC overflow operations accept SIMD vectors but the results are unsound. + // TODO: Create a CBMC issue. + // For now, we expand the overflow check. + 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) => {{ self.binop(p, fargs, |a, b| a.$f(b)) }}; + } + // 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 +258,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 +283,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 +412,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 +432,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 +446,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 +460,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 +478,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 +490,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()); diff --git a/compiler/rustc_codegen_rmc/src/codegen/rvalue.rs b/compiler/rustc_codegen_rmc/src/codegen/rvalue.rs index 268ac52f93c0..966f13223684 100644 --- a/compiler/rustc_codegen_rmc/src/codegen/rvalue.rs +++ b/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 = diff --git a/scripts/rmc-rustc b/scripts/rmc-rustc index 0069fa033f5f..8d981fed5dd2 100755 --- a/scripts/rmc-rustc +++ b/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 \ diff --git a/scripts/rmc.py b/scripts/rmc.py index 4317dbad6b59..964caf7ca7a3 100644 --- a/scripts/rmc.py +++ b/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) diff --git a/src/test/expected/dry-run/expected b/src/test/expected/dry-run/expected index ece530e0232a..cfc13d01ccb7 100644 --- a/src/test/expected/dry-run/expected +++ b/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 diff --git a/src/test/rmc/ArithOperators/unchecked.rs b/src/test/rmc/ArithOperators/unchecked.rs new file mode 100644 index 000000000000..e8bec8b24df8 --- /dev/null +++ b/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); + }}; +} + +pub fn main() { + verify_no_overflow!(checked_add, unchecked_add); + verify_no_overflow!(checked_sub, unchecked_sub); + verify_no_overflow!(checked_mul, unchecked_mul); +} diff --git a/src/test/rmc/ArithOperators/unchecked_add_fail.rs b/src/test/rmc/ArithOperators/unchecked_add_fail.rs new file mode 100644 index 000000000000..bfaf65e8def7 --- /dev/null +++ b/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) }; +} diff --git a/src/test/rmc/ArithOperators/unchecked_mul_fail.rs b/src/test/rmc/ArithOperators/unchecked_mul_fail.rs new file mode 100644 index 000000000000..c289667fe1a8 --- /dev/null +++ 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) }; +} diff --git a/src/test/rmc/ArithOperators/unchecked_sub_fail.rs b/src/test/rmc/ArithOperators/unchecked_sub_fail.rs new file mode 100644 index 000000000000..4372dfe3d754 --- /dev/null +++ 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)] + +pub fn main() { + let a: u8 = rmc::nondet(); + let b: u8 = rmc::nondet(); + unsafe { a.unchecked_sub(b) }; +} diff --git a/src/test/rmc/ArithOperators/wrapping.rs b/src/test/rmc/ArithOperators/wrapping.rs new file mode 100644 index 000000000000..bf1598f1f8d1 --- /dev/null +++ b/src/test/rmc/ArithOperators/wrapping.rs @@ -0,0 +1,15 @@ +// 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)] + +pub 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 >= a || sum2.is_none()); +} diff --git a/src/test/rmc/Enum/discriminant.rs b/src/test/rmc/Enum/discriminant.rs new file mode 100644 index 000000000000..3dcda4624610 --- /dev/null +++ b/src/test/rmc/Enum/discriminant.rs @@ -0,0 +1,20 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Testcase for https://github.com/model-checking/rmc/issues/558. +// See https://rust-lang.github.io/unsafe-code-guidelines/layout/enums.html for information on the +// layout. +pub enum MyEnum { + Val1, + Val2, +} + +fn foo(x: u32) -> Option { + // The math does overflow. Val1 == 0, Val2 == 1, None == 2. + // The discriminant logic is val - max == 0 ? <> : <>; where max is 2 + if x > 10 { Some(MyEnum::Val2) } else { None } +} + +pub fn main() { + let x = foo(15); + assert!(x.is_some(), "assert"); +} diff --git a/src/test/rmc/Enum/niche.rs b/src/test/rmc/Enum/niche.rs new file mode 100644 index 000000000000..804eb14bdfb4 --- /dev/null +++ b/src/test/rmc/Enum/niche.rs @@ -0,0 +1,22 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// Testcase for https://github.com/model-checking/rmc/issues/558. + +enum MyError { + Val1, + Val2, +} + +fn foo(x: u32) -> Result<(), MyError> { + if x > 10 { Err(MyError::Val2) } else { Ok(()) } +} + +fn bar() -> Result<(), MyError> { + let x = foo(15)?; + + Ok(x) +} + +pub fn main() { + bar(); +} diff --git a/src/test/rmc/SIMD/Operators/overflow.rs b/src/test/rmc/SIMD/Operators/overflow.rs new file mode 100644 index 000000000000..8570d6d1142b --- /dev/null +++ b/src/test/rmc/SIMD/Operators/overflow.rs @@ -0,0 +1,39 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// rmc-verify-fail +// +// This test ensures that overflow in SIMD operations are detected by RMC. +#![feature(repr_simd, platform_intrinsics)] + +#[repr(simd)] +#[allow(non_camel_case_types)] +#[derive(Clone, Copy, PartialEq, Eq, Debug)] +pub struct i8x2(i8, i8); + +extern "platform-intrinsic" { + fn simd_add(x: T, y: T) -> T; + fn simd_sub(x: T, y: T) -> T; + fn simd_mul(x: T, y: T) -> T; +} + +macro_rules! assert_op { + ($simd_op: ident, $wrap_op: ident, $x: expr, $y: expr) => { + let result = $simd_op($x, $y); + assert!(result.0 == $x.0.$wrap_op($y.0)); + assert!(result.1 == $x.1.$wrap_op($y.1)); + }; +} + +// Tests inspired by Rust's examples in +// https://github.com/rust-lang/rust/blob/0d97f7a96877a96015d70ece41ad08bb7af12377/src/test/ui/simd-intrinsic/simd-intrinsic-generic-arithmetic.rs +pub fn main() { + let v1 = i8x2(2, 2); + let max_min = i8x2(i8::MIN, i8::MAX); + + unsafe { + assert_op!(simd_add, wrapping_add, v1, max_min); + assert_op!(simd_sub, wrapping_sub, v1, max_min); + assert_op!(simd_mul, wrapping_mul, v1, max_min); + } +} From e67f604ac34b4f902f2944945f71f98b16899bae Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 15 Nov 2021 12:52:27 -0800 Subject: [PATCH 2/5] Remove flag from tests that had spurious counter examples (#307) --- src/test/firecracker/virtio-block-parse/main.rs | 7 ------- src/test/rmc/PointerOffset/Stable/main.rs | 8 -------- src/test/rmc/PointerOffset/Unstable/main.rs | 8 -------- src/test/rmc/Strings/main.rs | 11 ----------- src/test/rmc/SwitchInt/main.rs | 6 ------ src/test/rmc/Whitespace/main.rs | 7 ------- 6 files changed, 47 deletions(-) diff --git a/src/test/firecracker/virtio-block-parse/main.rs b/src/test/firecracker/virtio-block-parse/main.rs index c6384023786f..669866b59942 100644 --- a/src/test/firecracker/virtio-block-parse/main.rs +++ b/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 diff --git a/src/test/rmc/PointerOffset/Stable/main.rs b/src/test/rmc/PointerOffset/Stable/main.rs index 9d6ecad8d5a4..4d19fe8c1e47 100644 --- a/src/test/rmc/PointerOffset/Stable/main.rs +++ b/src/test/rmc/PointerOffset/Stable/main.rs @@ -1,14 +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 signed - in var_11 - var_12: FAILURE -// [overflow.2] arithmetic overflow on signed - in var_11 - var_12: FAILURE -// Tracking issue: https://github.com/model-checking/rmc/issues/307 - fn main() { // pub unsafe fn offset_from(self, origin: *const T) -> isize // Calculates the distance between two pointers. The returned value diff --git a/src/test/rmc/PointerOffset/Unstable/main.rs b/src/test/rmc/PointerOffset/Unstable/main.rs index 0ada27120326..87ae21b955ff 100644 --- a/src/test/rmc/PointerOffset/Unstable/main.rs +++ b/src/test/rmc/PointerOffset/Unstable/main.rs @@ -1,14 +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.2] arithmetic overflow on signed - in var_23 - var_24: FAILURE -// [overflow.4] arithmetic overflow on signed - in var_33 - var_34: FAILURE -// Tracking issue: https://github.com/model-checking/rmc/issues/307 - #![feature(core_intrinsics)] use std::intrinsics::ptr_offset_from; diff --git a/src/test/rmc/Strings/main.rs b/src/test/rmc/Strings/main.rs index c7cc4fc3193e..081b7357dd5b 100644 --- a/src/test/rmc/Strings/main.rs +++ b/src/test/rmc/Strings/main.rs @@ -1,17 +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: -// [_RINvMNtCs9Odk7Lrvgnw_4core6optionINtB3_6OptioncE5ok_orjECs21hi0yVfW1J_4main.overflow.1] line 569 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&self + 0)) - 1114112: FAILURE -// [_RNvXsG_NtCs9Odk7Lrvgnw_4core6optionINtB5_6OptioncENtNtB7_3cmp9PartialEq2eqCs21hi0yVfW1J_4main.overflow.1] line 160 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&(*var_4) + 0)) - 1114112: FAILURE -// [_RNvXsG_NtCs9Odk7Lrvgnw_4core6optionINtB5_6OptioncENtNtB7_3cmp9PartialEq2eqCs21hi0yVfW1J_4main.overflow.2] line 160 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&(*var_7) + 0)) - 1114112: FAILURE -// [_RNvXsG_NtCs9Odk7Lrvgnw_4core6optionINtB5_6OptioncENtNtB7_3cmp9PartialEq2eqCs21hi0yVfW1J_4main.overflow.3] line 160 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&(*var_13.0) + 0)) - 1114112: FAILURE -// [_RNvXsG_NtCs9Odk7Lrvgnw_4core6optionINtB5_6OptioncENtNtB7_3cmp9PartialEq2eqCs21hi0yVfW1J_4main.overflow.4] line 160 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&(*var_13.1) + 0)) - 1114112: FAILURE -// Tracking issue: https://github.com/model-checking/rmc/issues/307 - fn test1() { let str = "foo"; let string = str.to_string(); diff --git a/src/test/rmc/SwitchInt/main.rs b/src/test/rmc/SwitchInt/main.rs index 9c341457e204..7c99721c9f40 100644 --- a/src/test/rmc/SwitchInt/main.rs +++ b/src/test/rmc/SwitchInt/main.rs @@ -1,14 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// rmc-flags: --no-overflow-checks // cbmc-flags: --unwind 2 -// We use `--no-overflow-checks` in this test to avoid getting -// a verification failure: -// [_RNvCs21hi0yVfW1J_4main14doswitch_chars.overflow.1] line 17 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&var_7 + 0)) - 1114112: FAILURE -// Tracking issue: https://github.com/model-checking/rmc/issues/307 - fn doswitch_int() -> i32 { for i in [99].iter() { if *i == 99 { diff --git a/src/test/rmc/Whitespace/main.rs b/src/test/rmc/Whitespace/main.rs index 3e321e7a83b2..0faa4516797f 100644 --- a/src/test/rmc/Whitespace/main.rs +++ b/src/test/rmc/Whitespace/main.rs @@ -1,15 +1,8 @@ // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 OR MIT -// rmc-flags: --no-overflow-checks // cbmc-flags: --unwind 2 -// We use `--no-overflow-checks` in this test to avoid getting -// a verification failure: -// [_RNvXs3_NtNtCs9Odk7Lrvgnw_4core3str4iterNtB5_11CharIndicesNtNtNtNtB9_4iter6traits8iterator8Iterator4nextCs21hi0yVfW1J_4main.overflow.1] line 141 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&var_4 + 0)) - 1114112: FAILURE -// [_RNvXs5_NtNtCs9Odk7Lrvgnw_4core3str7patternINtB5_19MultiCharEqSearcherNtB7_12IsWhitespaceENtB5_8Searcher4nextCs21hi0yVfW1J_4main.overflow.1] line 641 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&var_5 + 8)) - 1114112: FAILURE -// Tracking issue: https://github.com/model-checking/rmc/issues/307 - fn main() { let mut iter = "A few words".split_whitespace(); match iter.next() { From 72f317dcc4da2f0e2d317ce071d1b62de5895f3f Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 16 Nov 2021 23:22:41 -0800 Subject: [PATCH 3/5] Address PR comments --- compiler/cbmc/src/goto_program/expr.rs | 13 +++++++++++-- compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs | 9 ++++----- .../rustc_codegen_rmc/src/compiler_interface.rs | 4 ++++ 3 files changed, 19 insertions(+), 7 deletions(-) diff --git a/compiler/cbmc/src/goto_program/expr.rs b/compiler/cbmc/src/goto_program/expr.rs index 2713452f349a..4f812960f391 100644 --- a/compiler/cbmc/src/goto_program/expr.rs +++ b/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, @@ -815,7 +815,7 @@ impl Expr { && (lhs.typ.is_pointer() || lhs.typ.is_numeric() || lhs.typ.is_vector()) || (lhs.typ.is_pointer() && rhs.typ.is_integer()) } - Plus | OverflowMinus | OverflowMult | OverflowPlus => { + Plus => { (lhs.typ == rhs.typ && (lhs.typ.is_numeric() || lhs.typ.is_vector())) || (lhs.typ.is_pointer() && rhs.typ.is_integer()) } @@ -848,6 +848,15 @@ impl Expr { } // Floating Point Equalities IeeeFloatEqual | IeeeFloatNotequal => lhs.typ == rhs.typ && lhs.typ.is_floating_point(), + // Overflow flags + 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()) + } } } diff --git a/compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs b/compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs index de5027feb18d..ef185b9a305c 100644 --- a/compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs +++ b/compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs @@ -146,10 +146,9 @@ impl<'tcx> GotocCtx<'tcx> { }}; } - // Intrinsics which encode a SIMD arithmetic operation with overflow check - // RMC overflow operations accept SIMD vectors but the results are unsound. - // TODO: Create a CBMC issue. - // For now, we expand the overflow check. + // 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); @@ -182,7 +181,7 @@ impl<'tcx> GotocCtx<'tcx> { // Intrinsics which encode a simple wrapping arithmetic operation macro_rules! codegen_wrapping_op { - ($f:ident) => {{ self.binop(p, fargs, |a, b| a.$f(b)) }}; + ($f:ident) => {{ codegen_intrinsic_binop!($f) }}; } // Intrinsics which encode a simple binary operation diff --git a/compiler/rustc_codegen_rmc/src/compiler_interface.rs b/compiler/rustc_codegen_rmc/src/compiler_interface.rs index 4fa3cff51d34..144aa2116a6c 100644 --- a/compiler/rustc_codegen_rmc/src/compiler_interface.rs +++ b/compiler/rustc_codegen_rmc/src/compiler_interface.rs @@ -58,6 +58,10 @@ impl CodegenBackend for GotocCodegenBackend { ) -> Box { 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; From f9dd8d42d830480b5c2fa37054ef714500625dce Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 18 Nov 2021 13:36:07 -0800 Subject: [PATCH 4/5] Adding new test cases for unsafe operation. --- src/test/rmc/ArithOperators/unsafe.rs | 21 +++++++++++++++++++ .../rmc/ArithOperators/unsafe_add_fail.rs | 12 +++++++++++ .../rmc/ArithOperators/unsafe_mul_fail.rs | 12 +++++++++++ .../rmc/ArithOperators/unsafe_sub_fail.rs | 12 +++++++++++ src/test/rmc/ArithOperators/wrapping.rs | 1 + 5 files changed, 58 insertions(+) create mode 100644 src/test/rmc/ArithOperators/unsafe.rs create mode 100644 src/test/rmc/ArithOperators/unsafe_add_fail.rs create mode 100644 src/test/rmc/ArithOperators/unsafe_mul_fail.rs create mode 100644 src/test/rmc/ArithOperators/unsafe_sub_fail.rs diff --git a/src/test/rmc/ArithOperators/unsafe.rs b/src/test/rmc/ArithOperators/unsafe.rs new file mode 100644 index 000000000000..0e7615de2fbc --- /dev/null +++ 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); + }}; +} + +pub fn main() { + verify_no_overflow!(checked_add, +); + verify_no_overflow!(checked_sub, -); + verify_no_overflow!(checked_mul, *); +} diff --git a/src/test/rmc/ArithOperators/unsafe_add_fail.rs b/src/test/rmc/ArithOperators/unsafe_add_fail.rs new file mode 100644 index 000000000000..d1459c69fb90 --- /dev/null +++ b/src/test/rmc/ArithOperators/unsafe_add_fail.rs @@ -0,0 +1,12 @@ +// 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 + +pub fn check_add(a: u8, b: u8) { + unsafe { + a + b; + } +} diff --git a/src/test/rmc/ArithOperators/unsafe_mul_fail.rs b/src/test/rmc/ArithOperators/unsafe_mul_fail.rs new file mode 100644 index 000000000000..1ae384e3785a --- /dev/null +++ b/src/test/rmc/ArithOperators/unsafe_mul_fail.rs @@ -0,0 +1,12 @@ +// 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 + +pub fn check_add(a: u8, b: u8) { + unsafe { + a * b; + } +} diff --git a/src/test/rmc/ArithOperators/unsafe_sub_fail.rs b/src/test/rmc/ArithOperators/unsafe_sub_fail.rs new file mode 100644 index 000000000000..e97c75927625 --- /dev/null +++ b/src/test/rmc/ArithOperators/unsafe_sub_fail.rs @@ -0,0 +1,12 @@ +// 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 + +pub fn check_sub(a: u8, b: u8) { + unsafe { + a - b; + } +} diff --git a/src/test/rmc/ArithOperators/wrapping.rs b/src/test/rmc/ArithOperators/wrapping.rs index bf1598f1f8d1..ca7c4ec0368f 100644 --- a/src/test/rmc/ArithOperators/wrapping.rs +++ b/src/test/rmc/ArithOperators/wrapping.rs @@ -11,5 +11,6 @@ pub fn main() { 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()); } From fb22b618f837e615aa2c0a5b6884a65f92cec9d1 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 22 Nov 2021 22:48:48 -0800 Subject: [PATCH 5/5] Fix tests after sync with main branch --- src/test/rmc/ArithOperators/unchecked.rs | 2 +- src/test/rmc/ArithOperators/unchecked_sub_fail.rs | 2 +- src/test/rmc/ArithOperators/unsafe.rs | 2 +- src/test/rmc/ArithOperators/unsafe_add_fail.rs | 1 + src/test/rmc/ArithOperators/unsafe_mul_fail.rs | 1 + src/test/rmc/ArithOperators/unsafe_sub_fail.rs | 1 + src/test/rmc/ArithOperators/wrapping.rs | 2 +- 7 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/test/rmc/ArithOperators/unchecked.rs b/src/test/rmc/ArithOperators/unchecked.rs index e8bec8b24df8..c43966300785 100644 --- a/src/test/rmc/ArithOperators/unchecked.rs +++ b/src/test/rmc/ArithOperators/unchecked.rs @@ -15,7 +15,7 @@ macro_rules! verify_no_overflow { }}; } -pub fn main() { +fn main() { verify_no_overflow!(checked_add, unchecked_add); verify_no_overflow!(checked_sub, unchecked_sub); verify_no_overflow!(checked_mul, unchecked_mul); diff --git a/src/test/rmc/ArithOperators/unchecked_sub_fail.rs b/src/test/rmc/ArithOperators/unchecked_sub_fail.rs index 4372dfe3d754..2c5b2cfb5baa 100644 --- a/src/test/rmc/ArithOperators/unchecked_sub_fail.rs +++ b/src/test/rmc/ArithOperators/unchecked_sub_fail.rs @@ -6,7 +6,7 @@ #![feature(unchecked_math)] -pub fn main() { +fn main() { let a: u8 = rmc::nondet(); let b: u8 = rmc::nondet(); unsafe { a.unchecked_sub(b) }; diff --git a/src/test/rmc/ArithOperators/unsafe.rs b/src/test/rmc/ArithOperators/unsafe.rs index 0e7615de2fbc..626b8e9f0e8a 100644 --- a/src/test/rmc/ArithOperators/unsafe.rs +++ b/src/test/rmc/ArithOperators/unsafe.rs @@ -14,7 +14,7 @@ macro_rules! verify_no_overflow { }}; } -pub fn main() { +fn main() { verify_no_overflow!(checked_add, +); verify_no_overflow!(checked_sub, -); verify_no_overflow!(checked_mul, *); diff --git a/src/test/rmc/ArithOperators/unsafe_add_fail.rs b/src/test/rmc/ArithOperators/unsafe_add_fail.rs index d1459c69fb90..8e1f38902c67 100644 --- a/src/test/rmc/ArithOperators/unsafe_add_fail.rs +++ b/src/test/rmc/ArithOperators/unsafe_add_fail.rs @@ -4,6 +4,7 @@ // 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 { diff --git a/src/test/rmc/ArithOperators/unsafe_mul_fail.rs b/src/test/rmc/ArithOperators/unsafe_mul_fail.rs index 1ae384e3785a..231ef7cc34ae 100644 --- a/src/test/rmc/ArithOperators/unsafe_mul_fail.rs +++ b/src/test/rmc/ArithOperators/unsafe_mul_fail.rs @@ -4,6 +4,7 @@ // 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 { diff --git a/src/test/rmc/ArithOperators/unsafe_sub_fail.rs b/src/test/rmc/ArithOperators/unsafe_sub_fail.rs index e97c75927625..e9caeca6fac7 100644 --- a/src/test/rmc/ArithOperators/unsafe_sub_fail.rs +++ b/src/test/rmc/ArithOperators/unsafe_sub_fail.rs @@ -4,6 +4,7 @@ // 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 { diff --git a/src/test/rmc/ArithOperators/wrapping.rs b/src/test/rmc/ArithOperators/wrapping.rs index ca7c4ec0368f..0c683c925fab 100644 --- a/src/test/rmc/ArithOperators/wrapping.rs +++ b/src/test/rmc/ArithOperators/wrapping.rs @@ -4,7 +4,7 @@ // Check that none of these operations trigger spurious overflow checks. #![feature(core_intrinsics)] -pub fn main() { +fn main() { let a: u8 = rmc::nondet(); let b: u8 = rmc::nondet(); let sum0 = core::intrinsics::wrapping_add(a, b);