Fix assert!() and panic!() code generation

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<Type> {
         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<BuiltinFn> {
         vec![
+            Abort,
             CProverAssert,
             CProverAssume,
             Calloc,

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<Span>) -> 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<Span>) -> Location {
         sp.map_or(Location::none(), |x| self.codegen_span(&x))
     }

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<Span>, fargs: Vec<Expr>) -> Stmt {
+    pub fn codegen_panic(&self, span: Option<Span>, fargs: Vec<Expr>) -> 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<Span>) -> 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<String> {
+    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,
+    }
+}

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<dyn Any> {
         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<T>(base_filename: &PathBuf, extension: &str, source: &T)
 where
     T: serde::Serialize,

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<BasicBlock>,
         span: Option<Span>,
     ) -> 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)
     }
 }
 

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
-}

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 \

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
+

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");
+}

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
+

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);
+}

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
+

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");
+    }
+}

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::<u8>() {
+        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),
+        _ => {}
+    }
 }

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