Converting more of rvalue stuff

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

@@ -429,7 +429,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 let e = self.codegen_get_discriminant(
                     fargs.remove(0).dereference(),
                     rustc_internal::stable(ty),
-                    ret_ty,
+                    rustc_internal::stable(ret_ty),
                 );
                 self.codegen_expr_to_place(p, e)
             }

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

@@ -8,7 +8,6 @@ use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Stmt, Sym
 use rustc_middle::mir::Operand as OperandInternal;
 use rustc_middle::ty::{Const as ConstInternal, Instance as InstanceInternal};
 use rustc_smir::rustc_internal;
-use rustc_span::def_id::DefId;
 use rustc_span::Span as SpanInternal;
 use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
 use stable_mir::mir::mono::{Instance, StaticDef};
@@ -17,7 +16,7 @@ use stable_mir::ty::{
     Allocation, Const, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, RigidTy, Size, Span, Ty,
     TyKind, UintTy,
 };
-use stable_mir::CrateDef;
+use stable_mir::{CrateDef, CrateItem};
 use tracing::{debug, trace};
 
 #[derive(Clone, Debug)]
@@ -80,7 +79,7 @@ impl<'tcx> GotocCtx<'tcx> {
     ///   generate code for it as simple literals or constants if possible. Otherwise, we create
     ///   a memory allocation for them and access them indirectly.
     /// - ZeroSized: These are ZST constants and they just need to match the right type.
-    fn codegen_const(&mut self, constant: &Const, span: Option<Span>) -> Expr {
+    pub fn codegen_const(&mut self, constant: &Const, span: Option<Span>) -> Expr {
         trace!(?constant, "codegen_constant");
         match constant.kind() {
             ConstantKind::Allocated(alloc) => self.codegen_allocation(alloc, constant.ty(), span),
@@ -379,8 +378,8 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Generate a goto expression for a pointer to a thread-local variable.
     ///
     /// These are not initialized here, see `codegen_static`.
-    pub fn codegen_thread_local_pointer(&mut self, def_id: DefId) -> Expr {
-        let instance = rustc_internal::stable(InstanceInternal::mono(self.tcx, def_id));
+    pub fn codegen_thread_local_pointer(&mut self, def: CrateItem) -> Expr {
+        let instance = Instance::try_from(def).unwrap();
         self.codegen_instance_pointer(instance, true)
     }
 

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

@@ -6,10 +6,10 @@
 //! in [GotocCtx::codegen_place] below.
 
 use super::typ::TypeExt;
-use crate::codegen_cprover_gotoc::codegen::ty_stable::{pointee_type, StableConverter};
-use crate::codegen_cprover_gotoc::codegen::typ::{
-    pointee_type as pointee_type_internal, std_pointee_type,
+use crate::codegen_cprover_gotoc::codegen::ty_stable::{
+    is_box, is_coroutine, pointee_type, StableConverter,
 };
+use crate::codegen_cprover_gotoc::codegen::typ::std_pointee_type;
 use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::unwrap_or_return_codegen_unimplemented;
@@ -411,7 +411,7 @@ impl<'tcx> GotocCtx<'tcx> {
         match proj {
             ProjectionElem::Deref => {
                 let base_type = before.mir_typ();
-                let inner_goto_expr = if is_box(base_type) {
+                let inner_goto_expr = if is_box(&base_type.kind()) {
                     self.deref_box(before.goto_expr)
                 } else {
                     before.goto_expr
@@ -601,7 +601,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     Variants::Single { .. } => before.goto_expr,
                     Variants::Multiple { tag_encoding, .. } => match tag_encoding {
                         TagEncoding::Direct => {
-                            let cases = if is_coroutine(ty_kind) {
+                            let cases = if is_coroutine(&ty_kind) {
                                 before.goto_expr
                             } else {
                                 before.goto_expr.member("cases", &self.symbol_table)
@@ -640,21 +640,26 @@ impl<'tcx> GotocCtx<'tcx> {
     /// - For `*(Wrapper<T>)` where `T: Unsized`, the projection's `goto_expr` returns an object,
     ///   and we need to take it's address and build the fat pointer.
     pub fn codegen_place_ref(&mut self, place: &PlaceInternal<'tcx>) -> Expr {
-        let place_ty = self.place_ty(place);
-        let projection = unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(place));
-        if self.use_thin_pointer(place_ty) {
+        self.codegen_place_ref_stable(&StableConverter::convert_place(self, *place))
+    }
+
+    pub fn codegen_place_ref_stable(&mut self, place: &Place) -> Expr {
+        let place_ty = self.place_ty_stable(place);
+        let projection =
+            unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(place));
+        if self.use_thin_pointer_stable(place_ty) {
             // Just return the address of the place dereferenced.
             projection.goto_expr.address_of()
-        } else if place_ty == pointee_type_internal(self.local_ty(place.local)).unwrap() {
+        } else if place_ty == pointee_type(self.local_ty_stable(place.local)).unwrap() {
             // Just return the fat pointer if this is a simple &(*local).
             projection.fat_ptr_goto_expr.unwrap()
         } else {
             // Build a new fat pointer to the place dereferenced with the metadata from the
             // original fat pointer.
             let data = projection_data_ptr(&projection);
             let fat_ptr = projection.fat_ptr_goto_expr.unwrap();
-            let place_type = self.codegen_ty_ref(place_ty);
-            if self.use_vtable_fat_pointer(place_ty) {
+            let place_type = self.codegen_ty_ref_stable(place_ty);
+            if self.use_vtable_fat_pointer_stable(place_ty) {
                 let vtable = fat_ptr.member("vtable", &self.symbol_table);
                 dynamic_fat_ptr(place_type, data, vtable, &self.symbol_table)
             } else {
@@ -777,14 +782,6 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 }
 
-fn is_box(ty: Ty) -> bool {
-    matches!(ty.kind(), TyKind::RigidTy(RigidTy::Adt(def, _)) if def.is_box())
-}
-
-fn is_coroutine(ty_kind: TyKind) -> bool {
-    matches!(ty_kind, TyKind::RigidTy(RigidTy::Coroutine(..)))
-}
-
 /// Extract the data pointer from a projection.
 /// The return type of the projection is not consistent today, so we need to specialize the
 /// behavior in order to get a consistent expression that represents a pointer to the projected