Migrate static handling and most of the operand codegen code to StableMIR

cprover_bindings/src/goto_program/expr.rs

@@ -627,6 +627,34 @@ impl Expr {
         expr!(IntConstant(i), typ)
     }
 
+    pub fn ssize_constant(i: i128, symbol_table: &SymbolTable) -> Self {
+        match symbol_table.machine_model().pointer_width {
+            32 => {
+                let val = BigInt::from(i as i32);
+                expr!(IntConstant(val), Type::ssize_t())
+            }
+            64 => {
+                let val = BigInt::from(i as i64);
+                expr!(IntConstant(val), Type::ssize_t())
+            }
+            i => unreachable!("Expected 32 or 64 bits pointer width, but got `{i}`"),
+        }
+    }
+
+    pub fn size_constant(i: u128, symbol_table: &SymbolTable) -> Self {
+        match symbol_table.machine_model().pointer_width {
+            32 => {
+                let val = BigInt::from(i as u32);
+                expr!(IntConstant(val), Type::size_t())
+            }
+            64 => {
+                let val = BigInt::from(i as u64);
+                expr!(IntConstant(val), Type::size_t())
+            }
+            i => unreachable!("Expected 32 or 64 bits pointer width, but got `{i}`"),
+        }
+    }
+
     pub fn typecheck_call(function: &Expr, arguments: &[Expr]) -> bool {
         // For variadic functions, all named arguments must match the type of their formal param.
         // Extra arguments (e.g the ... args) can have any type.

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

@@ -16,7 +16,9 @@ use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
 use cbmc::{InternString, InternedString};
 use lazy_static::lazy_static;
 use rustc_middle::ty::Instance;
+use rustc_smir::rustc_internal;
 use rustc_target::abi::call::Conv;
+use stable_mir::mir::mono::Instance as InstanceStable;
 use tracing::{debug, trace};
 
 lazy_static! {
@@ -44,8 +46,9 @@ impl<'tcx> GotocCtx<'tcx> {
     ///
     /// For other foreign items, we declare a shim and add to the list of foreign shims to be
     /// handled later.
-    pub fn codegen_foreign_fn(&mut self, instance: Instance<'tcx>) -> &Symbol {
+    pub fn codegen_foreign_fn(&mut self, instance: InstanceStable) -> &Symbol {
         debug!(?instance, "codegen_foreign_function");
+        let instance = rustc_internal::internal(instance);
         let fn_name = self.symbol_name(instance).intern();
         if self.symbol_table.contains(fn_name) {
             // Symbol has been added (either a built-in CBMC function or a Rust allocation function).

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

@@ -12,6 +12,7 @@ use rustc_middle::mir::{BasicBlock, Operand, Place};
 use rustc_middle::ty::layout::{LayoutOf, ValidityRequirement};
 use rustc_middle::ty::{self, Ty};
 use rustc_middle::ty::{Instance, InstanceDef};
+use rustc_smir::rustc_internal;
 use rustc_span::Span;
 use tracing::debug;
 
@@ -233,14 +234,14 @@ impl<'tcx> GotocCtx<'tcx> {
         // Intrinsics which encode a value known during compilation
         macro_rules! codegen_intrinsic_const {
             () => {{
-                let value = self
-                    .tcx
-                    .const_eval_instance(ty::ParamEnv::reveal_all(), instance, span)
-                    .unwrap();
+                let place = rustc_internal::stable(p);
+                let place_ty = self.place_ty_stable(&place);
+                let stable_instance = rustc_internal::stable(instance);
+                let alloc = stable_instance.try_const_eval(place_ty).unwrap();
                 // We assume that the intrinsic has type checked at this point, so
                 // we can use the place type as the expression type.
-                let e = self.codegen_const_value(value, self.place_ty(p), span.as_ref());
-                self.codegen_expr_to_place(p, e)
+                let e = self.codegen_allocation(&alloc, place_ty, rustc_internal::stable(span));
+                self.codegen_expr_to_place_stable(&place, e)
             }};
         }
 

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

@@ -369,7 +369,7 @@ impl<'tcx> GotocCtx<'tcx> {
         match ty.kind() {
             // A local that is itself a FnDef, like Fn::call_once
             TyKind::RigidTy(RigidTy::FnDef(def, args)) => {
-                Some(self.codegen_fndef_stable(def, &args, None))
+                Some(self.codegen_fndef(def, &args, None))
             }
             // A local can be pointer to a FnDef, like Fn::call and Fn::call_mut
             TyKind::RigidTy(RigidTy::RawPtr(inner, _)) => self

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

@@ -162,7 +162,7 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_rvalue_len(&mut self, p: &Place<'tcx>) -> Expr {
         let pt = self.place_ty(p);
         match pt.kind() {
-            ty::Array(_, sz) => self.codegen_const(*sz, None),
+            ty::Array(_, sz) => self.codegen_const_internal(*sz, None),
             ty::Slice(_) => unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(p))
                 .fat_ptr_goto_expr
                 .unwrap()
@@ -761,7 +761,7 @@ impl<'tcx> GotocCtx<'tcx> {
             Rvalue::ThreadLocalRef(def_id) => {
                 // Since Kani is single-threaded, we treat a thread local like a static variable:
                 self.store_concurrent_construct("thread local (replaced by static variable)", loc);
-                self.codegen_static_pointer(*def_id, true)
+                self.codegen_thread_local_pointer(*def_id)
             }
             // A CopyForDeref is equivalent to a read from a place at the codegen level.
             // https://github.com/rust-lang/rust/blob/1673f1450eeaf4a5452e086db0fe2ae274a0144f/compiler/rustc_middle/src/mir/syntax.rs#L1055
@@ -1006,7 +1006,7 @@ impl<'tcx> GotocCtx<'tcx> {
                             .unwrap();
                     // We need to handle this case in a special way because `codegen_operand` compiles FnDefs to dummy structs.
                     // (cf. the function documentation)
-                    self.codegen_func_expr(instance, None).address_of()
+                    self.codegen_func_expr_internal(instance, None).address_of()
                 }
                 _ => unreachable!(),
             },
@@ -1017,7 +1017,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         Instance::resolve_closure(self.tcx, *def_id, args, ty::ClosureKind::FnOnce)
                             .expect("failed to normalize and resolve closure during codegen")
                             .polymorphize(self.tcx);
-                    self.codegen_func_expr(instance, None).address_of()
+                    self.codegen_func_expr_internal(instance, None).address_of()
                 } else {
                     unreachable!("{:?} cannot be cast to a fn ptr", operand)
                 }
@@ -1384,7 +1384,7 @@ impl<'tcx> GotocCtx<'tcx> {
             (ty::Array(src_elt_type, src_elt_count), ty::Slice(dst_elt_type)) => {
                 // Cast to a slice fat pointer.
                 assert_eq!(src_elt_type, dst_elt_type);
-                let dst_goto_len = self.codegen_const(*src_elt_count, None);
+                let dst_goto_len = self.codegen_const_internal(*src_elt_count, None);
                 let src_pointee_ty = pointee_type(coerce_info.src_ty).unwrap();
                 let dst_data_expr = if src_pointee_ty.is_array() {
                     src_goto_expr.cast_to(self.codegen_ty(*src_elt_type).to_pointer())

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

@@ -27,6 +27,11 @@ impl<'tcx> GotocCtx<'tcx> {
             Some(loc.end_col),
         )
     }
+
+    pub fn codegen_span_option_stable(&self, sp: Option<SpanStable>) -> Location {
+        sp.map_or(Location::none(), |span| self.codegen_span_stable(span))
+    }
+
     pub fn codegen_caller_span_stable(&self, sp: SpanStable) -> Location {
         self.codegen_caller_span(&Some(rustc_internal::internal(sp)))
     }

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

@@ -18,6 +18,7 @@ use rustc_smir::rustc_internal;
 use rustc_span::Span;
 use rustc_target::abi::VariantIdx;
 use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants};
+use stable_mir::mir::Place as PlaceStable;
 use tracing::{debug, debug_span, trace};
 
 impl<'tcx> GotocCtx<'tcx> {
@@ -346,7 +347,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         // Non-virtual, direct drop_in_place call
                         assert!(!matches!(drop_instance.def, InstanceDef::Virtual(_, _)));
 
-                        let func = self.codegen_func_expr(drop_instance, None);
+                        let func = self.codegen_func_expr_internal(drop_instance, None);
                         // The only argument should be a self reference
                         let args = vec![place_ref];
 
@@ -567,7 +568,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     | InstanceDef::CloneShim(..) => {
                         // We need to handle FnDef items in a special way because `codegen_operand` compiles them to dummy structs.
                         // (cf. the function documentation)
-                        let func_exp = self.codegen_func_expr(instance, None);
+                        let func_exp = self.codegen_func_expr_internal(instance, None);
                         vec![
                             self.codegen_expr_to_place(destination, func_exp.call(fargs))
                                 .with_location(loc),
@@ -697,6 +698,16 @@ impl<'tcx> GotocCtx<'tcx> {
     /// A MIR [Place] is an L-value (i.e. the LHS of an assignment).
     ///
     /// In Kani, we slightly optimize the special case for Unit and don't assign anything.
+    pub(crate) fn codegen_expr_to_place_stable(&mut self, p: &PlaceStable, e: Expr) -> Stmt {
+        if e.typ().is_unit() {
+            e.as_stmt(Location::none())
+        } else {
+            unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place_stable(p))
+                .goto_expr
+                .assign(e, Location::none())
+        }
+    }
+
     pub(crate) fn codegen_expr_to_place(&mut self, p: &Place<'tcx>, e: Expr) -> Stmt {
         if self.place_ty(p).is_unit() {
             e.as_stmt(Location::none())

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

@@ -5,9 +5,8 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Symbol;
-use rustc_hir::def_id::DefId;
-use rustc_middle::mir::mono::MonoItem;
-use rustc_middle::ty::{GenericArgs, Instance};
+use stable_mir::mir::mono::{Instance, StaticDef};
+use stable_mir::CrateDef;
 use tracing::debug;
 
 impl<'tcx> GotocCtx<'tcx> {
@@ -16,24 +15,24 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Note that each static variable have their own location in memory. Per Rust documentation:
     /// "statics declare global variables. These represent a memory address."
     /// Source: <https://rust-lang.github.io/rfcs/0246-const-vs-static.html>
-    pub fn codegen_static(&mut self, def_id: DefId, item: MonoItem<'tcx>) {
+    pub fn codegen_static(&mut self, def: StaticDef) {
         debug!("codegen_static");
-        let alloc = self.tcx.eval_static_initializer(def_id).unwrap();
-        let symbol_name = item.symbol_name(self.tcx).to_string();
-        self.codegen_alloc_in_memory(alloc.inner(), symbol_name);
+        let alloc = def.eval_initializer().unwrap();
+        let symbol_name = Instance::from(def).mangled_name();
+        self.codegen_alloc_in_memory(alloc, symbol_name);
     }
 
     /// Mutates the Goto-C symbol table to add a forward-declaration of the static variable.
-    pub fn declare_static(&mut self, def_id: DefId, item: MonoItem<'tcx>) {
+    pub fn declare_static(&mut self, def: StaticDef) {
+        let instance = Instance::from(def);
         // Unique mangled monomorphized name.
-        let symbol_name = item.symbol_name(self.tcx).to_string();
+        let symbol_name = instance.mangled_name();
         // Pretty name which may include function name.
-        let pretty_name = Instance::new(def_id, GenericArgs::empty()).to_string();
-        debug!(?symbol_name, ?pretty_name, "declare_static {}", item);
+        let pretty_name = instance.name();
+        debug!(?def, ?symbol_name, ?pretty_name, "declare_static");
 
-        let typ = self.codegen_ty(self.tcx.type_of(def_id).instantiate_identity());
-        let span = self.tcx.def_span(def_id);
-        let location = self.codegen_span(&span);
+        let typ = self.codegen_ty_stable(instance.ty());
+        let location = self.codegen_span_stable(def.span());
         let symbol = Symbol::static_variable(symbol_name.clone(), symbol_name, typ, location)
             .with_is_hidden(false) // Static items are always user defined.
             .with_pretty_name(pretty_name);

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

@@ -10,11 +10,12 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Type;
 use rustc_middle::mir;
 use rustc_middle::mir::visit::{MutVisitor, NonUseContext, PlaceContext};
-use rustc_middle::mir::Place as PlaceInternal;
-use rustc_middle::ty::{Ty as TyInternal, TyCtxt};
+use rustc_middle::mir::{Operand as OperandInternal, Place as PlaceInternal};
+use rustc_middle::ty::{self, Const as ConstInternal, Ty as TyInternal, TyCtxt};
 use rustc_smir::rustc_internal;
-use stable_mir::mir::{Local, Place};
-use stable_mir::ty::{RigidTy, Ty, TyKind};
+use stable_mir::mir::mono::Instance;
+use stable_mir::mir::{Local, Operand, Place};
+use stable_mir::ty::{Const, RigidTy, Ty, TyKind};
 
 impl<'tcx> GotocCtx<'tcx> {
     pub fn place_ty_stable(&self, place: &Place) -> Ty {
@@ -28,6 +29,31 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn local_ty_stable(&mut self, local: Local) -> Ty {
         self.current_fn().body().local_decl(local).unwrap().ty
     }
+
+    pub fn operand_ty_stable(&mut self, operand: &Operand) -> Ty {
+        operand.ty(self.current_fn().body().locals()).unwrap()
+    }
+
+    pub fn is_zst_stable(&self, ty: Ty) -> bool {
+        self.is_zst(rustc_internal::internal(ty))
+    }
+
+    pub fn codegen_fndef_type_stable(&mut self, instance: Instance) -> Type {
+        let func = self.symbol_name_stable(instance);
+        self.ensure_struct(
+            format!("{func}::FnDefStruct"),
+            format!("{}::FnDefStruct", instance.name()),
+            |_, _| vec![],
+        )
+    }
+
+    pub fn fn_sig_of_instance_stable(&self, instance: Instance) -> ty::PolyFnSig<'tcx> {
+        self.fn_sig_of_instance(rustc_internal::internal(instance))
+    }
+
+    pub fn use_fat_pointer_stable(&self, pointer_ty: Ty) -> bool {
+        self.use_fat_pointer(rustc_internal::internal(pointer_ty))
+    }
 }
 /// If given type is a Ref / Raw ref, return the pointee type.
 pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
@@ -59,6 +85,18 @@ impl<'a, 'tcx> StableConverter<'a, 'tcx> {
         );
         rustc_internal::stable(place)
     }
+
+    pub fn convert_operand(gcx: &'a GotocCtx<'tcx>, mut operand: OperandInternal<'tcx>) -> Operand {
+        let mut converter = StableConverter { gcx };
+        converter.visit_operand(&mut operand, mir::Location::START);
+        rustc_internal::stable(operand)
+    }
+
+    pub fn convert_constant(gcx: &'a GotocCtx<'tcx>, mut constant: ConstInternal<'tcx>) -> Const {
+        let mut converter = StableConverter { gcx };
+        converter.visit_ty_const(&mut constant, mir::Location::START);
+        rustc_internal::stable(constant)
+    }
 }
 
 impl<'a, 'tcx> MutVisitor<'tcx> for StableConverter<'a, 'tcx> {
@@ -69,4 +107,22 @@ impl<'a, 'tcx> MutVisitor<'tcx> for StableConverter<'a, 'tcx> {
     fn visit_ty(&mut self, ty: &mut TyInternal<'tcx>, _: mir::visit::TyContext) {
         *ty = self.gcx.monomorphize(*ty);
     }
+
+    fn visit_ty_const(&mut self, ct: &mut ty::Const<'tcx>, _location: mir::Location) {
+        *ct = self.gcx.monomorphize(*ct);
+    }
+
+    fn visit_constant(&mut self, constant: &mut mir::ConstOperand<'tcx>, location: mir::Location) {
+        let const_ = self.gcx.monomorphize(constant.const_);
+        let val = match const_.eval(self.gcx.tcx, ty::ParamEnv::reveal_all(), None) {
+            Ok(v) => v,
+            Err(mir::interpret::ErrorHandled::Reported(..)) => return,
+            Err(mir::interpret::ErrorHandled::TooGeneric(..)) => {
+                unreachable!("Failed to evaluate instance constant: {:?}", const_)
+            }
+        };
+        let ty = constant.ty();
+        constant.const_ = mir::Const::Val(val, ty);
+        self.super_constant(constant, location);
+    }
 }

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

@@ -18,6 +18,7 @@ use rustc_middle::ty::{
     UintTy, VariantDef, VtblEntry,
 };
 use rustc_middle::ty::{List, TypeFoldable};
+use rustc_smir::rustc_internal;
 use rustc_span::def_id::DefId;
 use rustc_target::abi::{
     Abi::Vector, FieldIdx, FieldsShape, Integer, LayoutS, Primitive, Size, TagEncoding,
@@ -680,7 +681,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     fn codegen_ty_raw_array(&mut self, elem_ty: Ty<'tcx>, len: Const<'tcx>) -> Type {
-        let size = self.codegen_const(len, None).int_constant_value().unwrap();
+        let size = self.codegen_const_internal(len, None).int_constant_value().unwrap();
         let elemt = self.codegen_ty(elem_ty);
         elemt.array_of(size)
     }
@@ -1323,12 +1324,7 @@ impl<'tcx> GotocCtx<'tcx> {
     ///
     /// For details, see <https://github.com/model-checking/kani/pull/1338>
     pub fn codegen_fndef_type(&mut self, instance: Instance<'tcx>) -> Type {
-        let func = self.symbol_name(instance);
-        self.ensure_struct(
-            format!("{func}::FnDefStruct"),
-            format!("{}::FnDefStruct", self.readable_instance_name(instance)),
-            |_, _| vec![],
-        )
+        self.codegen_fndef_type_stable(rustc_internal::stable(instance))
     }
 
     /// codegen for struct

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -46,6 +46,7 @@ use rustc_session::Session;
 use rustc_smir::rustc_internal;
 use rustc_target::abi::Endian;
 use rustc_target::spec::PanicStrategy;
+use stable_mir::mir::mono::MonoItem as MonoItemStable;
 use std::any::Any;
 use std::collections::BTreeMap;
 use std::collections::HashSet;
@@ -111,8 +112,11 @@ impl GotocCodegenBackend {
                             );
                         }
                         MonoItem::Static(def_id) => {
+                            let MonoItemStable::Static(def) = rustc_internal::stable(item) else {
+                                unreachable!()
+                            };
                             gcx.call_with_panic_debug_info(
-                                |ctx| ctx.declare_static(def_id, *item),
+                                |ctx| ctx.declare_static(def),
                                 format!("declare_static: {def_id:?}"),
                                 def_id,
                             );
@@ -136,8 +140,11 @@ impl GotocCodegenBackend {
                             );
                         }
                         MonoItem::Static(def_id) => {
+                            let MonoItemStable::Static(def) = rustc_internal::stable(item) else {
+                                unreachable!()
+                            };
                             gcx.call_with_panic_debug_info(
-                                |ctx| ctx.codegen_static(def_id, *item),
+                                |ctx| ctx.codegen_static(def),
                                 format!("codegen_static: {def_id:?}"),
                                 def_id,
                             );