Fix assert!() and panic!() code generation (rust-lang#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 rust-lang#67, fixes rust-lang#466, fixes rust-lang#543, and fixes rust-lang#636. This
change also mitigates rust-lang#545.

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