Migrate static handling and most of the operand codegen code to Stabl…

…eMIR (#2931)

Migrate most of the operand code generation to use StableMIR APIs, and
static handling.

This change is so far the one that required some re-work, since
constants in StableMIR differ a bit from internal APIs. In the Rust
compiler internal APIs, constant values can be using either: Scalar,
Slice, Indirect (represented by an Allocation), and ZST. In the
StableAPIs, a constant value is always represented with an Allocation.

To avoid making changes to the final gotoc, we generate code for
allocations in two steps, we first try to generate just a regular
constant literal if the constant is small (similar logic to handling the
Scalar internal type).

For more complex cases, we create an allocation and read from it,
similar to how Indirect / Slice internal handling used to work.

---------

Co-authored-by: Zyad Hassan <[email protected]>

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,
                             );