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/function.rs

@@ -28,7 +28,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// - Indices [1, N] represent the function parameters where N is the number of parameters.
     /// - Indices that are greater than N represent local variables.
     fn codegen_declare_variables(&mut self) {
-        let mir = self.current_fn().mir();
+        let mir = self.current_fn().body_internal();
         let ldecls = mir.local_decls();
         let num_args = self.get_params_size();
         ldecls.indices().enumerate().for_each(|(idx, lc)| {
@@ -76,7 +76,7 @@ impl<'tcx> GotocCtx<'tcx> {
             debug!("Double codegen of {:?}", old_sym);
         } else {
             assert!(old_sym.is_function());
-            let mir = self.current_fn().mir();
+            let mir = self.current_fn().body_internal();
             self.print_instance(instance, mir);
             self.codegen_function_prelude();
             self.codegen_declare_variables();
@@ -94,7 +94,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Codegen changes required due to the function ABI.
     /// We currently untuple arguments for RustCall ABI where the `spread_arg` is set.
     fn codegen_function_prelude(&mut self) {
-        let mir = self.current_fn().mir();
+        let mir = self.current_fn().body_internal();
         if let Some(spread_arg) = mir.spread_arg {
             self.codegen_spread_arg(mir, spread_arg);
         }
@@ -228,7 +228,7 @@ impl<'tcx> GotocCtx<'tcx> {
         debug!(krate = self.current_fn().krate().as_str());
         debug!(is_std = self.current_fn().is_std());
         self.ensure(&self.current_fn().name(), |ctx, fname| {
-            let mir = ctx.current_fn().mir();
+            let mir = ctx.current_fn().body_internal();
             Symbol::function(
                 fname,
                 ctx.fn_typ(),

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,13 @@ 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 stable_mir::CrateDef;
 use tracing::{debug, trace};
 
 enum AllocData<'a> {
@@ -702,6 +706,20 @@ 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)
+            .expect(&format!("Failed to instantiate `{}` with `{args:?}`", def.name()));
+        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
@@ -735,6 +753,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.