Separate RMC sanity check function (rust-lang#201)

Co-authored-by: Daniel Schwartz-Narbonne <[email protected]>

Author: 2 people

compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/stmt.rs

@@ -187,6 +187,25 @@ impl Stmt {
         Stmt::assert(Expr::bool_false(), msg, loc)
     }
 
+    /// A __CPROVER_assert to sanity check expected components of code
+    /// generation. If users see these assertions fail, something in the
+    /// translation to Gotoc has gone wrong, and we want them to file an issue.
+    pub fn assert_sanity_check(expect_true: Expr, message: &str, url: &str, loc: Location) -> Stmt {
+        let assert_msg =
+            format!("Code generation sanity check: {}. Please report failures:\n{}", message, url);
+
+        Stmt::block(
+            vec![
+                // Assert our expected true expression.
+                Stmt::assert(expect_true.clone(), &assert_msg, loc.clone()),
+                // If expect_true is false, assume false to block any further
+                // exploration of this path.
+                Stmt::assume(expect_true, loc.clone()),
+            ],
+            loc,
+        )
+    }
+
     /// `__CPROVER_assume(cond);`
     pub fn assume(cond: Expr, loc: Location) -> Self {
         assert!(cond.typ().is_bool(), "Assume expected bool, got {:?}", cond);

compiler/rustc_codegen_llvm/src/gotoc/cbmc/utils.rs

@@ -2,6 +2,10 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! Useful utilities for CBMC
 
+/// RMC bug report URL, for asserts/errors
+pub const BUG_REPORT_URL: &str =
+    "https://github.com/model-checking/rmc/issues/new?template=bug_report.md";
+
 /// The aggregate name used in CBMC for aggregates of type `n`.
 pub fn aggr_name(n: &str) -> String {
     format!("tag-{}", n)

compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs

@@ -1,7 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use super::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type};
-use super::cbmc::utils::aggr_name;
+use super::cbmc::utils::{aggr_name, BUG_REPORT_URL};
 use super::cbmc::MachineModel;
 use super::metadata::*;
 use super::typ::{is_pointer, pointee_type};
@@ -788,10 +788,9 @@ impl<'tcx> GotocCtx<'tcx> {
         let temp_var = self.gen_temp_variable(ty, Location::none()).to_expr();
         let decl = Stmt::decl(temp_var.clone(), None, Location::none());
         let check = Expr::eq(Expr::object_size(temp_var.address_of()), vt_size.clone());
-
-        // TODO: Add an rmc_sanity_check function https://github.com/model-checking/rmc/issues/200
         let assert_msg = format!("Correct CBMC vtable size for {:?}", operand_type.kind());
-        let size_assert = Stmt::assert(check, &assert_msg, Location::none());
+        let size_assert =
+            Stmt::assert_sanity_check(check, &assert_msg, BUG_REPORT_URL, Location::none());
         Stmt::block(vec![decl, size_assert], Location::none())
     }