diff --git a/compiler/cbmc/src/goto_program/builtin.rs b/compiler/cbmc/src/goto_program/builtin.rs index 53cc7fa078843..e73bf57223eac 100644 --- a/compiler/cbmc/src/goto_program/builtin.rs +++ b/compiler/cbmc/src/goto_program/builtin.rs @@ -6,6 +6,7 @@ use super::{Expr, Location, Symbol, Type}; #[derive(Debug, Clone, Copy)] pub enum BuiltinFn { + Abort, CProverAssert, CProverAssume, Calloc, @@ -63,6 +64,7 @@ pub enum BuiltinFn { impl ToString for BuiltinFn { fn to_string(&self) -> String { match self { + Abort => "abort", CProverAssert => "__CPROVER_assert", CProverAssume => "__CPROVER_assume", Calloc => "calloc", @@ -124,6 +126,7 @@ impl ToString for BuiltinFn { impl BuiltinFn { pub fn param_types(&self) -> Vec { match self { + Abort => vec![], CProverAssert => vec![Type::bool(), Type::c_char().to_pointer()], CProverAssume => vec![Type::bool()], Calloc => vec![Type::size_t(), Type::size_t()], @@ -178,6 +181,7 @@ impl BuiltinFn { pub fn return_type(&self) -> Type { match self { + Abort => Type::empty(), CProverAssert => Type::empty(), CProverAssume => Type::empty(), Calloc => Type::void_pointer(), @@ -235,6 +239,7 @@ impl BuiltinFn { pub fn list_all() -> Vec { vec![ + Abort, CProverAssert, CProverAssume, Calloc, diff --git a/compiler/rustc_codegen_rmc/src/codegen/span.rs b/compiler/rustc_codegen_rmc/src/codegen/span.rs index 6ab9dcdbfc3c1..417b410e44c2b 100644 --- a/compiler/rustc_codegen_rmc/src/codegen/span.rs +++ b/compiler/rustc_codegen_rmc/src/codegen/span.rs @@ -27,6 +27,19 @@ impl<'tcx> GotocCtx<'tcx> { ) } + /// Get the location of the caller. This will attempt to reach the macro caller. + /// This function uses rustc_span methods designed to returns span for the macro which + /// originally caused the expansion to happen. + /// Note: The API stops backtracing at include! boundary. + pub fn codegen_caller_span(&self, sp: &Option) -> Location { + if let Some(span) = sp { + let topmost = span.ctxt().outer_expn().expansion_cause().unwrap_or(*span); + self.codegen_span(&topmost) + } else { + Location::none() + } + } + pub fn codegen_span_option(&self, sp: Option) -> Location { sp.map_or(Location::none(), |x| self.codegen_span(&x)) } diff --git a/compiler/rustc_codegen_rmc/src/codegen/statement.rs b/compiler/rustc_codegen_rmc/src/codegen/statement.rs index 65b217620664e..4f163bb4b7d9a 100644 --- a/compiler/rustc_codegen_rmc/src/codegen/statement.rs +++ b/compiler/rustc_codegen_rmc/src/codegen/statement.rs @@ -3,7 +3,7 @@ use super::typ::TypeExt; use super::typ::FN_RETURN_VOID_VAR_NAME; use crate::{GotocCtx, VtableCtx}; -use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type}; +use cbmc::goto_program::{BuiltinFn, Expr, ExprValue, Location, Stmt, Type}; use rustc_hir::def_id::DefId; use rustc_middle::mir; use rustc_middle::mir::{ @@ -482,54 +482,28 @@ impl<'tcx> GotocCtx<'tcx> { } } - pub fn codegen_panic(&mut self, span: Option, fargs: Vec) -> Stmt { + pub fn codegen_panic(&self, span: Option, fargs: Vec) -> Stmt { // CBMC requires that the argument to the assertion must be a string constant. // If there is one in the MIR, use it; otherwise, explain that we can't. - // TODO: give a better message here. - let arg = match fargs[0].struct_expr_values() { - Some(values) => values[0].clone(), - _ => Expr::string_constant( - "This is a placeholder assertion message; the rust message requires dynamic string formatting, which is not supported by CBMC", - ), - }; + assert!(!fargs.is_empty(), "Panic requires a string message"); + let msg = extract_const_message(&fargs[0]).unwrap_or(String::from( + "This is a placeholder message; RMC doesn't support message formatted at runtime", + )); - let loc = self.codegen_span_option(span); - let cbb = self.current_fn().current_bb(); - - // TODO: is it proper? - // - // [assert!(expr)] generates code like - // if !expr { panic() } - // thus when we compile [panic], we would like to continue with - // the code following [assert!(expr)] as well as display the panic - // location using the assert's location. - let preds = &self.current_fn().mir().predecessors()[cbb]; - if preds.len() == 1 { - let pred: &BasicBlock = preds.first().unwrap(); - let pred_bbd = &self.current_fn().mir()[*pred]; - let pterm = pred_bbd.terminator(); - match pterm.successors().find(|bb| **bb != cbb) { - None => self.codegen_assert_false(arg, loc), - Some(alt) => { - let loc = self.codegen_span(&pterm.source_info.span); - Stmt::block( - vec![ - self.codegen_assert_false(arg, loc.clone()), - Stmt::goto(self.current_fn().find_label(alt), Location::none()), - ], - loc, - ) - } - } - } else { - self.codegen_assert_false(arg, loc) - } + self.codegen_fatal_error(&msg, span) } - // By the time we get this, the string constant has been codegenned. - // TODO: make this case also use the Stmt::assert_false() constructor - pub fn codegen_assert_false(&mut self, err: Expr, loc: Location) -> Stmt { - BuiltinFn::CProverAssert.call(vec![Expr::bool_false(), err], loc.clone()).as_stmt(loc) + // Generate code for fatal error which should trigger an assertion failure and abort the + // execution. + pub fn codegen_fatal_error(&self, msg: &str, span: Option) -> Stmt { + let loc = self.codegen_caller_span(&span); + Stmt::block( + vec![ + Stmt::assert_false(msg, loc.clone()), + BuiltinFn::Abort.call(vec![], loc.clone()).as_stmt(loc.clone()), + ], + loc, + ) } pub fn codegen_statement(&mut self, stmt: &Statement<'tcx>) -> Stmt { @@ -661,3 +635,22 @@ impl<'tcx> GotocCtx<'tcx> { .with_location(self.codegen_span(&stmt.source_info.span)) } } + +/// Tries to extract a string message from an `Expr`. +/// If the expression represents a pointer to a string constant, this will return the string +/// constant. Otherwise, return `None`. +fn extract_const_message(arg: &Expr) -> Option { + match arg.value() { + ExprValue::Struct { values } => match &values[0].value() { + ExprValue::AddressOf(address) => match address.value() { + ExprValue::Index { array, .. } => match array.value() { + ExprValue::StringConstant { s } => Some(s.to_string()), + _ => None, + }, + _ => None, + }, + _ => None, + }, + _ => None, + } +} diff --git a/compiler/rustc_codegen_rmc/src/compiler_interface.rs b/compiler/rustc_codegen_rmc/src/compiler_interface.rs index 008001a4422c9..9baeb8160afad 100644 --- a/compiler/rustc_codegen_rmc/src/compiler_interface.rs +++ b/compiler/rustc_codegen_rmc/src/compiler_interface.rs @@ -21,6 +21,7 @@ use rustc_middle::ty::{self, TyCtxt}; use rustc_session::config::{OutputFilenames, OutputType}; use rustc_session::cstore::MetadataLoaderDyn; use rustc_session::Session; +use rustc_target::spec::PanicStrategy; use std::collections::BTreeMap; use std::io::BufWriter; use std::iter::FromIterator; @@ -62,12 +63,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(); + check_options(&tcx.sess); + let codegen_units: &'tcx [CodegenUnit<'_>] = tcx.collect_and_partition_mono_items(()).1; let mut c = GotocCtx::new(tcx); @@ -191,6 +190,21 @@ impl CodegenBackend for GotocCodegenBackend { } } +fn check_options(session: &Session) { + if !session.overflow_checks() { + session.err("RMC requires overflow checks in order to provide a sound analysis."); + } + + if session.panic_strategy() != PanicStrategy::Abort { + session.err( + "RMC can only handle abort panic strategy (-C panic=abort). See for more details \ + https://github.com/model-checking/rmc/issues/692", + ); + } + + session.abort_if_errors(); +} + fn write_file(base_filename: &PathBuf, extension: &str, source: &T) where T: serde::Serialize, diff --git a/compiler/rustc_codegen_rmc/src/overrides/hooks.rs b/compiler/rustc_codegen_rmc/src/overrides/hooks.rs index 9dddea3cf2039..2b08c842ffeba 100644 --- a/compiler/rustc_codegen_rmc/src/overrides/hooks.rs +++ b/compiler/rustc_codegen_rmc/src/overrides/hooks.rs @@ -8,7 +8,7 @@ //! It would be too nasty if we spread around these sort of undocumented hooks in place, so //! this module addresses this issue. -use crate::utils::{instance_name_is, instance_name_starts_with}; +use crate::utils::instance_name_starts_with; use crate::GotocCtx; use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type}; use cbmc::NO_PRETTY_NAME; @@ -197,9 +197,11 @@ struct Panic; impl<'tcx> GotocHook<'tcx> for Panic { fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { - output_of_instance_is_never(tcx, instance) - && (instance_name_is(tcx, instance, "begin_panic") - || instance_name_is(tcx, instance, "panic")) + let def_id = instance.def.def_id(); + Some(def_id) == tcx.lang_items().panic_fn() + || Some(def_id) == tcx.lang_items().panic_display() + || Some(def_id) == tcx.lang_items().panic_fmt() + || Some(def_id) == tcx.lang_items().begin_panic_fn() } fn handle( @@ -231,15 +233,11 @@ impl<'tcx> GotocHook<'tcx> for Nevers { _target: Option, span: Option, ) -> Stmt { - let loc = tcx.codegen_span_option(span); - // _target must be None due to how rust compiler considers it - Stmt::assert_false( - &format!( - "a panicking function {} is invoked", - with_no_trimmed_paths(|| tcx.tcx.def_path_str(instance.def_id())) - ), - loc, - ) + let msg = format!( + "a panicking function {} is invoked", + with_no_trimmed_paths(|| tcx.tcx.def_path_str(instance.def_id())) + ); + tcx.codegen_fatal_error(&msg, span) } } diff --git a/compiler/rustc_codegen_rmc/src/utils/names.rs b/compiler/rustc_codegen_rmc/src/utils/names.rs index 771c425ced268..f4a235b9d78b4 100644 --- a/compiler/rustc_codegen_rmc/src/utils/names.rs +++ b/compiler/rustc_codegen_rmc/src/utils/names.rs @@ -144,16 +144,3 @@ pub fn instance_name_starts_with( } false } - -/// Helper function to determine if the function is exactly `expected` -// TODO: rationalize how we match the hooks https://github.com/model-checking/rmc/issues/130 -pub fn instance_name_is(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>, expected: &str) -> bool { - let def_path = tcx.def_path(instance.def.def_id()); - if let Some(data) = def_path.data.last() { - match data.data.name() { - DefPathDataName::Named(name) => return name.to_string() == expected, - DefPathDataName::Anon { .. } => (), - } - } - false -} diff --git a/scripts/rmc-rustc b/scripts/rmc-rustc index fd2a6168828cb..bd6cd21af2418 100755 --- a/scripts/rmc-rustc +++ b/scripts/rmc-rustc @@ -65,6 +65,8 @@ else set_rmc_lib_path RMC_FLAGS="-Z codegen-backend=gotoc \ -C overflow-checks=on \ + -C panic=abort \ + -Z panic_abort_tests=yes \ -Z trim-diagnostic-paths=no \ -Z human_readable_cgu_names \ --cfg=rmc \ diff --git a/src/test/expected/abort/expected b/src/test/expected/abort/expected new file mode 100644 index 0000000000000..9775b83c1bf2c --- /dev/null +++ b/src/test/expected/abort/expected @@ -0,0 +1,3 @@ +line 12 a panicking function std::process::abort is invoked: FAILURE +line 16 a panicking function std::process::abort is invoked: SUCCESS + diff --git a/src/test/expected/abort/main.rs b/src/test/expected/abort/main.rs new file mode 100644 index 0000000000000..400e2d03be88d --- /dev/null +++ b/src/test/expected/abort/main.rs @@ -0,0 +1,20 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Test that the abort() function is respected and nothing beyond it will execute. + +use std::process; + +pub fn main() { + for i in 0..4 { + if i == 1 { + // This comes first and it should be reachable. + process::abort(); + } + if i == 2 { + // This should never happen. + process::abort(); + } + } + assert!(false, "This is unreachable"); +} diff --git a/src/test/expected/assert-location/assert-false/expected b/src/test/expected/assert-location/assert-false/expected new file mode 100644 index 0000000000000..0c3c39fb38d4c --- /dev/null +++ b/src/test/expected/assert-location/assert-false/expected @@ -0,0 +1,4 @@ +line 12 assertion failed: false: FAILURE +line 17 This is a placeholder message; RMC doesn't support message formatted at runtime: FAILURE +line 21 Fail with custom static message: FAILURE + diff --git a/src/test/expected/assert-location/assert-false/main.rs b/src/test/expected/assert-location/assert-false/main.rs new file mode 100644 index 0000000000000..1a90a3e96bfab --- /dev/null +++ b/src/test/expected/assert-location/assert-false/main.rs @@ -0,0 +1,29 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Check the location of the assert statement when using assert!(false); + +fn any_bool() -> bool { + rmc::nondet() +} + +pub fn main() { + if any_bool() { + assert!(false); + } + + if any_bool() { + let s = "Fail with custom runtime message"; + assert!(false, "{}", s); + } + + if any_bool() { + assert!(false, "Fail with custom static message"); + } +} + +#[inline(always)] +#[track_caller] +fn check_caller(b: bool) { + assert!(b); +} diff --git a/src/test/expected/assert-location/debug-assert/expected b/src/test/expected/assert-location/debug-assert/expected new file mode 100644 index 0000000000000..478384e65da2b --- /dev/null +++ b/src/test/expected/assert-location/debug-assert/expected @@ -0,0 +1,3 @@ +line 6 This should fail and stop the execution: FAILURE +line 7 This should be unreachable: SUCCESS + diff --git a/src/test/expected/assert-location/debug-assert/main.rs b/src/test/expected/assert-location/debug-assert/main.rs new file mode 100644 index 0000000000000..e36b67785343b --- /dev/null +++ b/src/test/expected/assert-location/debug-assert/main.rs @@ -0,0 +1,9 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +pub fn main() { + for i in 0..4 { + debug_assert!(i > 0, "This should fail and stop the execution"); + assert!(i == 0, "This should be unreachable"); + } +} diff --git a/src/test/expected/binop/main.rs b/src/test/expected/binop/main.rs index 5ab5e26aca59d..1c458eccf122f 100644 --- a/src/test/expected/binop/main.rs +++ b/src/test/expected/binop/main.rs @@ -56,19 +56,22 @@ fn ibxor_test(a: i32, b: i32, correct: i32, wrong: i32) { } fn main() { - iadd_test(1, 2, 3, 4); - isub_test(3, 4, -1, 0); - imul_test(5, 6, 30, 60); - idiv_test(8, 2, 4, 5); - idiv_test(9, 2, 4, 5); - imod_test(9, 3, 0, 1); - imod_test(10, 3, 1, 2); - ishl_test(2, 3, 16, 8); - ishr_test(8, 3, 1, 2); - ishr_test(-1, 2, -1, 1073741823); - ushr_test(4294967292, 2, 1073741823, 2); - iband_test(0, 2389034, 0, 2389034); - iband_test(3, 10, 2, 3); - ibor_test(0, 2389034, 2389034, 0); - ibxor_test(0, 2389034, 2389034, 0); + match rmc::nondet::() { + 0 => iadd_test(1, 2, 3, 4), + 1 => isub_test(3, 4, -1, 0), + 2 => imul_test(5, 6, 30, 60), + 3 => idiv_test(8, 2, 4, 5), + 4 => idiv_test(9, 2, 4, 5), + 5 => imod_test(9, 3, 0, 1), + 6 => imod_test(10, 3, 1, 2), + 7 => ishl_test(2, 3, 16, 8), + 8 => ishr_test(8, 3, 1, 2), + 9 => ishr_test(-1, 2, -1, 1073741823), + 10 => ushr_test(4294967292, 2, 1073741823, 2), + 11 => iband_test(0, 2389034, 0, 2389034), + 12 => iband_test(3, 10, 2, 3), + 13 => ibor_test(0, 2389034, 2389034, 0), + 14 => ibxor_test(0, 2389034, 2389034, 0), + _ => {} + } } diff --git a/src/test/expected/closure/expected b/src/test/expected/closure/expected index cda57e035c3dc..5d607f74e41ee 100644 --- a/src/test/expected/closure/expected +++ b/src/test/expected/closure/expected @@ -1,4 +1,3 @@ -resume instruction: SUCCESS line 18 attempt to compute `move _8 + move _9`, which would overflow: SUCCESS line 18 attempt to compute `move _5 + move _6`, which would overflow: SUCCESS line 18 attempt to compute `(*((*_1).0: &mut i32)) + move _4`, which would overflow: SUCCESS diff --git a/src/test/expected/enum/expected b/src/test/expected/enum/expected index 22b2f6a678418..fdc82ceb4003a 100644 --- a/src/test/expected/enum/expected +++ b/src/test/expected/enum/expected @@ -1,7 +1,7 @@ line 18 unreachable code: SUCCESS -line 18 assertion failed: false: SUCCESS line 19 assertion failed: x == 10: SUCCESS +line 20 assertion failed: false: SUCCESS line 22 unreachable code: SUCCESS -line 22 assertion failed: false: SUCCESS +line 23 assertion failed: false: SUCCESS line 25 assertion failed: x == 30 && y == 60.0: SUCCESS line 26 assertion failed: x == 31: FAILURE diff --git a/src/test/expected/float-nan/expected b/src/test/expected/float-nan/expected index f1db04b782d15..96a451353eee6 100644 --- a/src/test/expected/float-nan/expected +++ b/src/test/expected/float-nan/expected @@ -1,5 +1,5 @@ -line 11 assertion failed: 1.0 / f != 0.0 / f: SUCCESS -line 13 assertion failed: !(1.0 / f == 0.0 / f): SUCCESS -line 15 assertion failed: 1.0 / f == 0.0 / f: FAILURE -line 17 assertion failed: 0.0 / f == 0.0 / f: FAILURE -line 19 assertion failed: 0.0 / f != 0.0 / f: SUCCESS +line 12 assertion failed: 1.0 / f != 0.0 / f: SUCCESS +line 14 assertion failed: !(1.0 / f == 0.0 / f): SUCCESS +line 16 assertion failed: 1.0 / f == 0.0 / f: FAILURE +line 18 assertion failed: 0.0 / f == 0.0 / f: FAILURE +line 20 assertion failed: 0.0 / f != 0.0 / f: SUCCESS diff --git a/src/test/expected/float-nan/main.rs b/src/test/expected/float-nan/main.rs index 4b6e27ce3e5ee..c7e0a8556681d 100644 --- a/src/test/expected/float-nan/main.rs +++ b/src/test/expected/float-nan/main.rs @@ -6,15 +6,17 @@ fn main() { f -= 1.0; } - // at this point, f == 0.0 - // should succeed - assert!(1.0 / f != 0.0 / f); - // should succeed - assert!(!(1.0 / f == 0.0 / f)); - // should fail - assert!(1.0 / f == 0.0 / f); - // should fail - assert!(0.0 / f == 0.0 / f); - // should suceed - assert!(0.0 / f != 0.0 / f); + match rmc::nondet::() { + // at this point, f == 0.0 + // should succeed + 0 => assert!(1.0 / f != 0.0 / f), + // should succeed + 1 => assert!(!(1.0 / f == 0.0 / f)), + // should fail + 2 => assert!(1.0 / f == 0.0 / f), + // should fail + 3 => assert!(0.0 / f == 0.0 / f), + // should suceed + _ => assert!(0.0 / f != 0.0 / f), + } } diff --git a/src/test/expected/niche/expected b/src/test/expected/niche/expected index ce8e04bf66c4e..1a34839f56afc 100644 --- a/src/test/expected/niche/expected +++ b/src/test/expected/niche/expected @@ -1,5 +1,5 @@ -line 20 assertion failed: false: SUCCESS +line 22 assertion failed: false: SUCCESS line 20 unreachable code: SUCCESS line 25 unreachable code: SUCCESS -line 25 assertion failed: false: SUCCESS +line 26 assertion failed: false: SUCCESS line 27 assertion failed: a == *b: SUCCESS diff --git a/src/test/expected/niche2/expected b/src/test/expected/niche2/expected index 1d3eafe2aaf52..240359acbfcf6 100644 --- a/src/test/expected/niche2/expected +++ b/src/test/expected/niche2/expected @@ -1,5 +1,4 @@ -line 21 assertion failed: false: SUCCESS -line 21 unreachable code: SUCCESS +line 23 assertion failed: false: SUCCESS line 27 assertion failed: x == 10: SUCCESS line 28 assertion failed: false: SUCCESS line 33 assertion failed: false: SUCCESS diff --git a/src/test/expected/static-mutable-struct/expected b/src/test/expected/static-mutable-struct/expected index 2ce4276890b6c..9050f63e7059b 100644 --- a/src/test/expected/static-mutable-struct/expected +++ b/src/test/expected/static-mutable-struct/expected @@ -1,12 +1,12 @@ line 23 assertion failed: foo().x == 12: SUCCESS -line 24 assertion failed: foo().y == 12: FAILURE -line 25 assertion failed: foo().x == 14: FAILURE -line 26 assertion failed: foo().y == 14: SUCCESS -line 29 assertion failed: foo().x == 1: SUCCESS -line 30 assertion failed: foo().y == 1: FAILURE -line 31 assertion failed: foo().x == 2: FAILURE -line 32 assertion failed: foo().y == 2: SUCCESS -line 35 assertion failed: foo().x == 1 << 62: SUCCESS -line 36 assertion failed: foo().x == 1 << 31: FAILURE -line 37 assertion failed: foo().y == 1 << 31: SUCCESS +line 25 assertion failed: foo().y == 12: FAILURE +line 28 assertion failed: foo().x == 14: FAILURE +line 30 assertion failed: foo().y == 14: SUCCESS +line 33 assertion failed: foo().x == 1: SUCCESS +line 35 assertion failed: foo().y == 1: FAILURE +line 38 assertion failed: foo().x == 2: FAILURE +line 40 assertion failed: foo().y == 2: SUCCESS +line 43 assertion failed: foo().x == 1 << 62: SUCCESS +line 45 assertion failed: foo().x == 1 << 31: FAILURE +line 47 assertion failed: foo().y == 1 << 31: SUCCESS diff --git a/src/test/expected/static-mutable-struct/main.rs b/src/test/expected/static-mutable-struct/main.rs index 9630631363060..fa834ddb44ac2 100644 --- a/src/test/expected/static-mutable-struct/main.rs +++ b/src/test/expected/static-mutable-struct/main.rs @@ -21,18 +21,28 @@ fn mutate_the_thing(nx: i64, ny: i32) { fn main() { assert!(foo().x == 12); - assert!(foo().y == 12); - assert!(foo().x == 14); + if rmc::nondet() { + assert!(foo().y == 12); + } + if rmc::nondet() { + assert!(foo().x == 14); + } assert!(foo().y == 14); mutate_the_thing(1, 2); assert!(foo().x == 1); - assert!(foo().y == 1); - assert!(foo().x == 2); + if rmc::nondet() { + assert!(foo().y == 1); + } + if rmc::nondet() { + assert!(foo().x == 2); + } assert!(foo().y == 2); mutate_the_thing(1 << 62, 1 << 31); assert!(foo().x == 1 << 62); - assert!(foo().x == 1 << 31); + if rmc::nondet() { + assert!(foo().x == 1 << 31); + } assert!(foo().y == 1 << 31); } diff --git a/src/test/expected/static-mutable/expected b/src/test/expected/static-mutable/expected index 1e47840833bb1..46ac1dc09c419 100644 --- a/src/test/expected/static-mutable/expected +++ b/src/test/expected/static-mutable/expected @@ -1,4 +1,4 @@ -line 16 assertion failed: 10 == foo(): FAILURE -line 17 assertion failed: 12 == foo(): SUCCESS -line 19 assertion failed: 10 == foo(): SUCCESS -line 20 assertion failed: 12 == foo(): FAILURE +line 17 assertion failed: 10 == foo(): FAILURE +line 19 assertion failed: 12 == foo(): SUCCESS +line 21 assertion failed: 10 == foo(): SUCCESS +line 22 assertion failed: 12 == foo(): FAILURE diff --git a/src/test/expected/static-mutable/main.rs b/src/test/expected/static-mutable/main.rs index 6fbe66149fb81..71b414a26fee7 100644 --- a/src/test/expected/static-mutable/main.rs +++ b/src/test/expected/static-mutable/main.rs @@ -13,7 +13,9 @@ fn mutate_the_thing(new: i32) { } fn main() { - assert!(10 == foo()); + if rmc::nondet() { + assert!(10 == foo()); + } assert!(12 == foo()); mutate_the_thing(10); assert!(10 == foo()); diff --git a/src/test/expected/test3/expected b/src/test/expected/test3/expected index 1c9045ad231be..9a2c7106f3f66 100644 --- a/src/test/expected/test3/expected +++ b/src/test/expected/test3/expected @@ -1,8 +1,8 @@ line 9 attempt to compute `_2 - const 1_i32`, which would overflow: SUCCESS -line 14 assertion failed: a == 10.0 && i == 1: FAILURE -line 16 assertion failed: a == 9.0 && i == 0: FAILURE -line 18 assertion failed: a == 9.0 && i == 1: FAILURE -line 20 assertion failed: a == 10.0 && i == 0: SUCCESS +line 15 assertion failed: a == 10.0 && i == 1: FAILURE +line 17 assertion failed: a == 9.0 && i == 0: FAILURE +line 19 assertion failed: a == 9.0 && i == 1: FAILURE +line 21 assertion failed: a == 10.0 && i == 0: SUCCESS line 23 assertion failed: a == 9.0 || i == 0: SUCCESS line 25 assertion failed: a == 10.0 || i == 1: SUCCESS line 27 assertion failed: a == 9.0 || i == 1: FAILURE diff --git a/src/test/expected/test3/main.rs b/src/test/expected/test3/main.rs index 04c18b308dee3..3d1b943b10c5e 100644 --- a/src/test/expected/test3/main.rs +++ b/src/test/expected/test3/main.rs @@ -10,21 +10,22 @@ fn main() { } // at this point, a == 10.0 and i == 0 - // should fail - assert!(a == 10.0 && i == 1); - // should fail - assert!(a == 9.0 && i == 0); - // should fail - assert!(a == 9.0 && i == 1); - // should succeed - assert!(a == 10.0 && i == 0); - - // should succeed - assert!(a == 9.0 || i == 0); - // should succeed - assert!(a == 10.0 || i == 1); - // should fail - assert!(a == 9.0 || i == 1); - // should succeed - assert!(a == 10.0 || i == 0); + match rmc::nondet::() { + // should fail + 0 => assert!(a == 10.0 && i == 1), + // should fail + 1 => assert!(a == 9.0 && i == 0), + // should fail + 2 => assert!(a == 9.0 && i == 1), + // should succeed + 3 => assert!(a == 10.0 && i == 0), + // should succeed + 4 => assert!(a == 9.0 || i == 0), + // should succeed + 5 => assert!(a == 10.0 || i == 1), + // should fail + 6 => assert!(a == 9.0 || i == 1), + // should succeed + _ => assert!(a == 10.0 || i == 0), + } } diff --git a/src/test/rmc/Assert/MultipleAsserts/main.rs b/src/test/rmc/Assert/MultipleAsserts/main.rs new file mode 100644 index 0000000000000..1dbb88469a43a --- /dev/null +++ b/src/test/rmc/Assert/MultipleAsserts/main.rs @@ -0,0 +1,13 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// rmc-verify-fail +// Check that this doesn't trigger a fake loop. See issue #636. +#[no_mangle] +fn main() { + let x: bool = rmc::nondet(); + if x { + assert!(1 + 1 == 1); + } + assert!(1 + 1 == 3, "This one should fail too"); +} diff --git a/src/test/rmc/Cleanup/assert.rs b/src/test/rmc/Cleanup/assert.rs new file mode 100644 index 0000000000000..f4053410aa688 --- /dev/null +++ b/src/test/rmc/Cleanup/assert.rs @@ -0,0 +1,29 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// This test ensures that rmc follows the correct CFG for assertion failures. +// - Statements that succeeds an assertion failure should be unreachable. +// - Cleanup statements should still be executed though. +// - Note that failures while unwinding actually crashes the process. So drop may only be called +// once. +// File: cleanup.rs +// rmc-verify-fail + +#[derive(PartialEq, Eq)] +struct S { + a: u8, + b: u16, +} + +impl Drop for S { + fn drop(&mut self) { + assert!(false, "A1: This should still fail during cleanup"); + } +} + +pub fn main() { + let lhs = S { a: 42, b: 42 }; + let rhs = S { a: 0, b: 0 }; + assert!(lhs == rhs, "A2: A very false statement. Always fail."); + assert!(false, "A3: Unreachable assert. Code always panic before this line."); +} diff --git a/src/test/rmc/Cleanup/unwind_fixme.rs b/src/test/rmc/Cleanup/unwind_fixme.rs new file mode 100644 index 0000000000000..b919cd6219e02 --- /dev/null +++ b/src/test/rmc/Cleanup/unwind_fixme.rs @@ -0,0 +1,35 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// We currently do not support stack unwinding panic strategy. Once we do, this testcase should +// fail during the verification with both the panic and the assertion failing. +// https://github.com/model-checking/rmc/issues/692 +// +// To run manually, execute: +// ``` +// RUSTFLAGS="--C panic=unwind --crate-type lib" rmc unwind_fixme.rs --function create +// ``` +// +// compile-flags: --C panic=unwind --crate-type lib +// rmc-flags: --function create +// rmc-verify-fail + +pub struct DummyResource { + pub data: Option, +} + +impl Drop for DummyResource { + fn drop(&mut self) { + assert!(self.data.is_some(), "This should fail"); + } +} + +#[no_mangle] +pub fn create(empty: bool) -> DummyResource { + let mut dummy = DummyResource { data: None }; + if empty { + unimplemented!("This is not supported yet"); + } + dummy.data = Some(String::from("data")); + dummy +} diff --git a/src/test/rmc/DynTrait/dyn_fn_param_fail.rs b/src/test/rmc/DynTrait/dyn_fn_param_fail.rs index 88fb28c8e513d..c143fd8f06788 100644 --- a/src/test/rmc/DynTrait/dyn_fn_param_fail.rs +++ b/src/test/rmc/DynTrait/dyn_fn_param_fail.rs @@ -10,14 +10,18 @@ include!("../Helpers/vtable_utils_ignore.rs"); fn takes_dyn_fun(fun: &dyn Fn() -> u32) { let x = fun(); - rmc::expect_fail(x != 5, "Wrong return"); + if rmc::nondet() { + rmc::expect_fail(x != 5, "Wrong return"); + } /* The function dynamic object has no associated data */ rmc::expect_fail(size_from_vtable(vtable!(fun)) != 0, "Wrong size"); } pub fn unit_to_u32() -> u32 { - assert!(false); + if rmc::nondet() { + assert!(false); + } 5 as u32 }