diff --git a/compiler/cbmc/src/goto_program/expr.rs b/compiler/cbmc/src/goto_program/expr.rs index 6dafa01e3afdc..4f812960f3918 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, @@ -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()) } } } diff --git a/compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs b/compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs index 713aa55c3dc77..ef185b9a305c6 100644 --- a/compiler/rustc_codegen_rmc/src/codegen/intrinsic.rs +++ b/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()); diff --git a/compiler/rustc_codegen_rmc/src/codegen/rvalue.rs b/compiler/rustc_codegen_rmc/src/codegen/rvalue.rs index 268ac52f93c0e..966f132236847 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/compiler/rustc_codegen_rmc/src/compiler_interface.rs b/compiler/rustc_codegen_rmc/src/compiler_interface.rs index 4fa3cff51d349..144aa2116a6cb 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; diff --git a/scripts/rmc-rustc b/scripts/rmc-rustc index 0069fa033f5f9..8d981fed5dd2c 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 4317dbad6b592..964caf7ca7a3a 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 ece530e0232a0..cfc13d01ccb72 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/firecracker/virtio-block-parse/main.rs b/src/test/firecracker/virtio-block-parse/main.rs index c6384023786fa..669866b599429 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/ArithOperators/unchecked.rs b/src/test/rmc/ArithOperators/unchecked.rs new file mode 100644 index 0000000000000..c43966300785d --- /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); + }}; +} + +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 0000000000000..bfaf65e8def78 --- /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 0000000000000..c289667fe1a85 --- /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 0000000000000..2c5b2cfb5baad --- /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)] + +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 new file mode 100644 index 0000000000000..626b8e9f0e8a0 --- /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); + }}; +} + +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 0000000000000..8e1f38902c678 --- /dev/null +++ b/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; + } +} 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 0000000000000..231ef7cc34aee --- /dev/null +++ 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; + } +} 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 0000000000000..e9caeca6fac79 --- /dev/null +++ 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; + } +} diff --git a/src/test/rmc/ArithOperators/wrapping.rs b/src/test/rmc/ArithOperators/wrapping.rs new file mode 100644 index 0000000000000..0c683c925fab5 --- /dev/null +++ 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()); +} diff --git a/src/test/rmc/Enum/discriminant.rs b/src/test/rmc/Enum/discriminant.rs new file mode 100644 index 0000000000000..3dcda4624610a --- /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 0000000000000..804eb14bdfb44 --- /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/PointerOffset/Stable/main.rs b/src/test/rmc/PointerOffset/Stable/main.rs index 9d6ecad8d5a48..4d19fe8c1e473 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 0ada271203261..87ae21b955ff5 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/SIMD/Operators/overflow.rs b/src/test/rmc/SIMD/Operators/overflow.rs new file mode 100644 index 0000000000000..8570d6d1142b6 --- /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); + } +} diff --git a/src/test/rmc/Strings/main.rs b/src/test/rmc/Strings/main.rs index c7cc4fc3193ea..081b7357dd5bb 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 9c341457e2049..7c99721c9f401 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 3e321e7a83b27..0faa4516797f7 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() {