Migrate hooks and place modules to use mostly StableMIR APIs

kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs

@@ -22,6 +22,7 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use cbmc::InternedString;
 use rustc_span::Span;
+use stable_mir::ty::Span as SpanStable;
 use std::convert::AsRef;
 use strum_macros::{AsRefStr, EnumString};
 use tracing::debug;
@@ -138,8 +139,8 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// Generate code to cover the given condition at the current location
-    pub fn codegen_cover(&self, cond: Expr, msg: &str, span: Option<Span>) -> Stmt {
-        let loc = self.codegen_caller_span(&span);
+    pub fn codegen_cover(&self, cond: Expr, msg: &str, span: SpanStable) -> Stmt {
+        let loc = self.codegen_caller_span_stable(span);
         // Should use Stmt::cover, but currently this doesn't work with CBMC
         // unless it is run with '--cover cover' (see
         // https://github.com/diffblue/cbmc/issues/6613). So for now use
@@ -172,12 +173,8 @@ impl<'tcx> GotocCtx<'tcx> {
     /// reachability check.
     /// If reachability checks are disabled, the function returns the message
     /// unmodified and an empty (skip) statement.
-    pub fn codegen_reachability_check(
-        &mut self,
-        msg: String,
-        span: Option<Span>,
-    ) -> (String, Stmt) {
-        let loc = self.codegen_caller_span(&span);
+    pub fn codegen_reachability_check(&mut self, msg: String, span: SpanStable) -> (String, Stmt) {
+        let loc = self.codegen_caller_span_stable(span);
         if self.queries.args().check_assertion_reachability {
             // Generate a unique ID for the assert
             let assert_id = self.next_check_id();
@@ -224,15 +221,16 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// Kani hooks function calls to `panic` and calls this intead.
-    pub fn codegen_panic(&self, span: Option<Span>, fargs: Vec<Expr>) -> Stmt {
+    pub fn codegen_panic(&self, span: SpanStable, 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.
         assert!(!fargs.is_empty(), "Panic requires a string message");
         let msg = self.extract_const_message(&fargs[0]).unwrap_or(String::from(
             "This is a placeholder message; Kani doesn't support message formatted at runtime",
         ));
 
-        self.codegen_fatal_error(PropertyClass::Assertion, &msg, span)
+        let loc = self.codegen_caller_span_stable(span);
+        self.codegen_assert_assume_false(PropertyClass::Assertion, &msg, loc)
     }
 
     /// Kani does not currently support all MIR constructs.

kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs

@@ -3,8 +3,13 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use rustc_middle::mir::{BasicBlock, BasicBlockData};
+use stable_mir::mir::BasicBlockIdx;
 use tracing::debug;
 
+pub fn bb_label(bb: BasicBlockIdx) -> String {
+    format!("bb{bb}")
+}
+
 impl<'tcx> GotocCtx<'tcx> {
     /// Generates Goto-C for a basic block.
     ///
@@ -14,7 +19,6 @@ impl<'tcx> GotocCtx<'tcx> {
     /// `self.current_fn_mut().push_onto_block(...)`
     pub fn codegen_block(&mut self, bb: BasicBlock, bbd: &BasicBlockData<'tcx>) {
         debug!(?bb, "Codegen basicblock");
-        self.current_fn_mut().set_current_bb(bb);
         let label: String = self.current_fn().find_label(&bb);
         let check_coverage = self.queries.args().check_coverage;
         // the first statement should be labelled. if there is no statements, then the
@@ -67,6 +71,5 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.current_fn_mut().push_onto_block(tcode);
             }
         }
-        self.current_fn_mut().reset_current_bb();
     }
 }

kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs

@@ -17,7 +17,9 @@ mod statement;
 mod static_var;
 
 // Visible for all codegen module.
+mod ty_stable;
 pub(super) mod typ;
 
 pub use assert::PropertyClass;
+pub use block::bb_label;
 pub use typ::TypeExt;

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

@@ -10,9 +10,12 @@ use rustc_middle::mir::interpret::{read_target_uint, AllocId, Allocation, Global
 use rustc_middle::mir::{Const as mirConst, ConstOperand, ConstValue, Operand, UnevaluatedConst};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{self, Const, ConstKind, FloatTy, Instance, IntTy, Ty, Uint, UintTy};
+use rustc_smir::rustc_internal;
 use rustc_span::def_id::DefId;
 use rustc_span::Span;
 use rustc_target::abi::{Size, TagEncoding, Variants};
+use stable_mir::mir::mono::Instance as InstanceStable;
+use stable_mir::ty::{FnDef, GenericArgs, Span as SpanStable};
 use tracing::{debug, trace};
 
 enum AllocData<'a> {
@@ -700,6 +703,19 @@ impl<'tcx> GotocCtx<'tcx> {
         self.codegen_fn_item(instance, span)
     }
 
+    pub fn codegen_fndef_stable(
+        &mut self,
+        def: FnDef,
+        args: &GenericArgs,
+        span: Option<SpanStable>,
+    ) -> Expr {
+        let instance = InstanceStable::resolve(def, args).unwrap();
+        self.codegen_fn_item(
+            rustc_internal::internal(instance),
+            rustc_internal::internal(span).as_ref(),
+        )
+    }
+
     /// Ensure that the given instance is in the symbol table, returning the symbol.
     ///
     /// FIXME: The function should not have to return the type of the function symbol as well
@@ -733,6 +749,12 @@ impl<'tcx> GotocCtx<'tcx> {
             .with_location(self.codegen_span_option(span.cloned()))
     }
 
+    pub fn codegen_func_expr_stable(&mut self, instance: InstanceStable, span: SpanStable) -> Expr {
+        let (func_symbol, func_typ) = self.codegen_func_symbol(rustc_internal::internal(instance));
+        Expr::symbol_expression(func_symbol.name, func_typ)
+            .with_location(self.codegen_span_stable(span))
+    }
+
     /// Generate a goto expression referencing the singleton value for a MIR "function item".
     ///
     /// For a given function instance, generate a ZST struct and return a singleton reference to that.