From 625990c8a5cc5782906381607a01ca54b2a31b0b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 14 Dec 2021 13:04:52 -0800 Subject: [PATCH] Fix assert!() and panic!() code generation (#687) I refactored how we codegen panic statements so it now it terminate the program per its spec. I have also removed the hack we had to try to get the assert location. Since we currently do not support stack unwinding, the panic codegen will always terminate immediately and it will not try to unwind the stack. I added an option to RMC to force the compiler to use abort as the panic strategy and a check to rmc codegen that will fail if the user tries to override that. Another note is that we currently do not support `#[track_caller]` and I have not changed that. This change fixes #67, fixes #466, fixes #543, and fixes #636. This change also mitigates #545. --- compiler/cbmc/src/goto_program/builtin.rs | 5 ++ .../rustc_codegen_rmc/src/codegen/span.rs | 13 +++ .../src/codegen/statement.rs | 81 +++++++++---------- .../src/compiler_interface.rs | 22 ++++- .../rustc_codegen_rmc/src/overrides/hooks.rs | 24 +++--- compiler/rustc_codegen_rmc/src/utils/names.rs | 13 --- scripts/rmc-rustc | 2 + src/test/expected/abort/expected | 3 + src/test/expected/abort/main.rs | 20 +++++ .../assert-location/assert-false/expected | 4 + .../assert-location/assert-false/main.rs | 29 +++++++ .../assert-location/debug-assert/expected | 3 + .../assert-location/debug-assert/main.rs | 9 +++ src/test/expected/binop/main.rs | 33 ++++---- src/test/expected/closure/expected | 1 - src/test/expected/enum/expected | 4 +- src/test/expected/float-nan/expected | 10 +-- src/test/expected/float-nan/main.rs | 24 +++--- src/test/expected/niche/expected | 4 +- src/test/expected/niche2/expected | 3 +- .../expected/static-mutable-struct/expected | 20 ++--- .../expected/static-mutable-struct/main.rs | 20 +++-- src/test/expected/static-mutable/expected | 8 +- src/test/expected/static-mutable/main.rs | 4 +- src/test/expected/test3/expected | 8 +- src/test/expected/test3/main.rs | 35 ++++---- src/test/rmc/Assert/MultipleAsserts/main.rs | 13 +++ src/test/rmc/Cleanup/assert.rs | 29 +++++++ src/test/rmc/Cleanup/unwind_fixme.rs | 35 ++++++++ src/test/rmc/DynTrait/dyn_fn_param_fail.rs | 8 +- 30 files changed, 332 insertions(+), 155 deletions(-) create mode 100644 src/test/expected/abort/expected create mode 100644 src/test/expected/abort/main.rs create mode 100644 src/test/expected/assert-location/assert-false/expected create mode 100644 src/test/expected/assert-location/assert-false/main.rs create mode 100644 src/test/expected/assert-location/debug-assert/expected create mode 100644 src/test/expected/assert-location/debug-assert/main.rs create mode 100644 src/test/rmc/Assert/MultipleAsserts/main.rs create mode 100644 src/test/rmc/Cleanup/assert.rs create mode 100644 src/test/rmc/Cleanup/unwind_fixme.rs diff --git a/compiler/cbmc/src/goto_program/builtin.rs b/compiler/cbmc/src/goto_program/builtin.rs index 53cc7fa07884..e73bf57223ea 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 6ab9dcdbfc3c..417b410e44c2 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 65b217620664..4f163bb4b7d9 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 008001a4422c..9baeb8160afa 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 9dddea3cf203..2b08c842ffeb 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 771c425ced26..f4a235b9d78b 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 fd2a6168828c..bd6cd21af241 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 000000000000..9775b83c1bf2 --- /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 000000000000..400e2d03be88 --- /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 000000000000..0c3c39fb38d4 --- /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 000000000000..1a90a3e96bfa --- /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 000000000000..478384e65da2 --- /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 000000000000..e36b67785343 --- /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 5ab5e26aca59..1c458eccf122 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 cda57e035c3d..5d607f74e41e 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 22b2f6a67841..fdc82ceb4003 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 f1db04b782d1..96a451353eee 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 4b6e27ce3e5e..c7e0a8556681 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 ce8e04bf66c4..1a34839f56af 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 1d3eafe2aaf5..240359acbfcf 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 2ce4276890b6..9050f63e7059 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 963063136306..fa834ddb44ac 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 1e47840833bb..46ac1dc09c41 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 6fbe66149fb8..71b414a26fee 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 1c9045ad231b..9a2c7106f3f6 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 04c18b308dee..3d1b943b10c5 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 000000000000..1dbb88469a43 --- /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 000000000000..f4053410aa68 --- /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 000000000000..b919cd6219e0 --- /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 88fb28c8e513..c143fd8f0678 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 }