From 60e56a93da116f8745cd6ec5122ef0d270d056e3 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 23 Nov 2021 11:18:03 -0800 Subject: [PATCH] Fix spurious overflow counter examples. (#558) (#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 | 11 ++- .../src/codegen/intrinsic.rs | 77 ++++++++++++++++--- .../rustc_codegen_rmc/src/codegen/rvalue.rs | 1 + .../src/compiler_interface.rs | 4 + scripts/rmc-rustc | 1 + scripts/rmc.py | 9 ++- src/test/expected/dry-run/expected | 2 +- .../firecracker/virtio-block-parse/main.rs | 7 -- 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/unsafe.rs | 21 +++++ .../rmc/ArithOperators/unsafe_add_fail.rs | 13 ++++ .../rmc/ArithOperators/unsafe_mul_fail.rs | 13 ++++ .../rmc/ArithOperators/unsafe_sub_fail.rs | 13 ++++ src/test/rmc/ArithOperators/wrapping.rs | 16 ++++ src/test/rmc/Enum/discriminant.rs | 20 +++++ src/test/rmc/Enum/niche.rs | 22 ++++++ src/test/rmc/PointerOffset/Stable/main.rs | 8 -- src/test/rmc/PointerOffset/Unstable/main.rs | 8 -- src/test/rmc/SIMD/Operators/overflow.rs | 39 ++++++++++ src/test/rmc/Strings/main.rs | 11 --- src/test/rmc/SwitchInt/main.rs | 6 -- src/test/rmc/Whitespace/main.rs | 7 -- 25 files changed, 305 insertions(+), 65 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/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 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 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() {