Skip to content

Commit a7c239e

Browse files
authored
Migrate rvalue and coercion module to use StableMIR (rust-lang#2938)
This migration was fairly straight forward, most constructs have a 1:1 map from internal APIs to StableMIR APIs. I've also removed the `is_coroutine()` and the `is_box()` methods from `ty_stable`, since they were added to the StableMIR APIs together with other type methods here: rust-lang#118846.
1 parent e5ad17f commit a7c239e

File tree

10 files changed

+471
-379
lines changed

10 files changed

+471
-379
lines changed

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -426,7 +426,11 @@ impl<'tcx> GotocCtx<'tcx> {
426426
"cttz_nonzero" => codegen_count_intrinsic!(cttz, false),
427427
"discriminant_value" => {
428428
let ty = instance.args.type_at(0);
429-
let e = self.codegen_get_discriminant(fargs.remove(0).dereference(), ty, ret_ty);
429+
let e = self.codegen_get_discriminant(
430+
fargs.remove(0).dereference(),
431+
rustc_internal::stable(ty),
432+
rustc_internal::stable(ret_ty),
433+
);
430434
self.codegen_expr_to_place(p, e)
431435
}
432436
"exact_div" => self.codegen_exact_div(fargs, p, loc),

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@ use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Stmt, Sym
88
use rustc_middle::mir::Operand as OperandInternal;
99
use rustc_middle::ty::{Const as ConstInternal, Instance as InstanceInternal};
1010
use rustc_smir::rustc_internal;
11-
use rustc_span::def_id::DefId;
1211
use rustc_span::Span as SpanInternal;
1312
use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
1413
use stable_mir::mir::mono::{Instance, StaticDef};
@@ -17,7 +16,7 @@ use stable_mir::ty::{
1716
Allocation, Const, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, RigidTy, Size, Span, Ty,
1817
TyKind, UintTy,
1918
};
20-
use stable_mir::CrateDef;
19+
use stable_mir::{CrateDef, CrateItem};
2120
use tracing::{debug, trace};
2221

2322
#[derive(Clone, Debug)]
@@ -80,7 +79,7 @@ impl<'tcx> GotocCtx<'tcx> {
8079
/// generate code for it as simple literals or constants if possible. Otherwise, we create
8180
/// a memory allocation for them and access them indirectly.
8281
/// - ZeroSized: These are ZST constants and they just need to match the right type.
83-
fn codegen_const(&mut self, constant: &Const, span: Option<Span>) -> Expr {
82+
pub fn codegen_const(&mut self, constant: &Const, span: Option<Span>) -> Expr {
8483
trace!(?constant, "codegen_constant");
8584
match constant.kind() {
8685
ConstantKind::Allocated(alloc) => self.codegen_allocation(alloc, constant.ty(), span),
@@ -379,8 +378,8 @@ impl<'tcx> GotocCtx<'tcx> {
379378
/// Generate a goto expression for a pointer to a thread-local variable.
380379
///
381380
/// These are not initialized here, see `codegen_static`.
382-
pub fn codegen_thread_local_pointer(&mut self, def_id: DefId) -> Expr {
383-
let instance = rustc_internal::stable(InstanceInternal::mono(self.tcx, def_id));
381+
pub fn codegen_thread_local_pointer(&mut self, def: CrateItem) -> Expr {
382+
let instance = Instance::try_from(def).unwrap();
384383
self.codegen_instance_pointer(instance, true)
385384
}
386385

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

Lines changed: 19 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -7,18 +7,13 @@
77
88
use super::typ::TypeExt;
99
use crate::codegen_cprover_gotoc::codegen::ty_stable::{pointee_type, StableConverter};
10-
use crate::codegen_cprover_gotoc::codegen::typ::{
11-
pointee_type as pointee_type_internal, std_pointee_type,
12-
};
10+
use crate::codegen_cprover_gotoc::codegen::typ::std_pointee_type;
1311
use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
1412
use crate::codegen_cprover_gotoc::GotocCtx;
1513
use crate::unwrap_or_return_codegen_unimplemented;
1614
use cbmc::goto_program::{Expr, Location, Type};
15+
use rustc_middle::mir::{Local as LocalInternal, Place as PlaceInternal};
1716
use rustc_middle::ty::layout::LayoutOf;
18-
use rustc_middle::{
19-
mir::{Local as LocalInternal, Place as PlaceInternal},
20-
ty::Ty as TyInternal,
21-
};
2217
use rustc_smir::rustc_internal;
2318
use rustc_target::abi::{TagEncoding, Variants};
2419
use stable_mir::mir::{FieldIdx, Local, Mutability, Place, ProjectionElem};
@@ -152,13 +147,12 @@ impl ProjectedPlace {
152147
}
153148
}
154149

155-
pub fn try_new_internal<'tcx>(
150+
pub fn try_from_ty(
156151
goto_expr: Expr,
157-
ty: TyInternal<'tcx>,
158-
ctx: &mut GotocCtx<'tcx>,
152+
ty: Ty,
153+
ctx: &mut GotocCtx,
159154
) -> Result<Self, UnimplementedData> {
160-
let ty = ctx.monomorphize(ty);
161-
Self::try_new(goto_expr, TypeOrVariant::Type(rustc_internal::stable(ty)), None, None, ctx)
155+
Self::try_new(goto_expr, TypeOrVariant::Type(ty), None, None, ctx)
162156
}
163157

164158
pub fn try_new(
@@ -415,7 +409,7 @@ impl<'tcx> GotocCtx<'tcx> {
415409
match proj {
416410
ProjectionElem::Deref => {
417411
let base_type = before.mir_typ();
418-
let inner_goto_expr = if is_box(base_type) {
412+
let inner_goto_expr = if base_type.kind().is_box() {
419413
self.deref_box(before.goto_expr)
420414
} else {
421415
before.goto_expr
@@ -605,7 +599,7 @@ impl<'tcx> GotocCtx<'tcx> {
605599
Variants::Single { .. } => before.goto_expr,
606600
Variants::Multiple { tag_encoding, .. } => match tag_encoding {
607601
TagEncoding::Direct => {
608-
let cases = if is_coroutine(ty_kind) {
602+
let cases = if ty_kind.is_coroutine() {
609603
before.goto_expr
610604
} else {
611605
before.goto_expr.member("cases", &self.symbol_table)
@@ -644,21 +638,26 @@ impl<'tcx> GotocCtx<'tcx> {
644638
/// - For `*(Wrapper<T>)` where `T: Unsized`, the projection's `goto_expr` returns an object,
645639
/// and we need to take it's address and build the fat pointer.
646640
pub fn codegen_place_ref(&mut self, place: &PlaceInternal<'tcx>) -> Expr {
647-
let place_ty = self.place_ty(place);
648-
let projection = unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(place));
649-
if self.use_thin_pointer(place_ty) {
641+
self.codegen_place_ref_stable(&StableConverter::convert_place(self, *place))
642+
}
643+
644+
pub fn codegen_place_ref_stable(&mut self, place: &Place) -> Expr {
645+
let place_ty = self.place_ty_stable(place);
646+
let projection =
647+
unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(place));
648+
if self.use_thin_pointer_stable(place_ty) {
650649
// Just return the address of the place dereferenced.
651650
projection.goto_expr.address_of()
652-
} else if place_ty == pointee_type_internal(self.local_ty(place.local)).unwrap() {
651+
} else if place_ty == pointee_type(self.local_ty_stable(place.local)).unwrap() {
653652
// Just return the fat pointer if this is a simple &(*local).
654653
projection.fat_ptr_goto_expr.unwrap()
655654
} else {
656655
// Build a new fat pointer to the place dereferenced with the metadata from the
657656
// original fat pointer.
658657
let data = projection_data_ptr(&projection);
659658
let fat_ptr = projection.fat_ptr_goto_expr.unwrap();
660-
let place_type = self.codegen_ty_ref(place_ty);
661-
if self.use_vtable_fat_pointer(place_ty) {
659+
let place_type = self.codegen_ty_ref_stable(place_ty);
660+
if self.use_vtable_fat_pointer_stable(place_ty) {
662661
let vtable = fat_ptr.member("vtable", &self.symbol_table);
663662
dynamic_fat_ptr(place_type, data, vtable, &self.symbol_table)
664663
} else {
@@ -781,14 +780,6 @@ impl<'tcx> GotocCtx<'tcx> {
781780
}
782781
}
783782

784-
fn is_box(ty: Ty) -> bool {
785-
matches!(ty.kind(), TyKind::RigidTy(RigidTy::Adt(def, _)) if def.is_box())
786-
}
787-
788-
fn is_coroutine(ty_kind: TyKind) -> bool {
789-
matches!(ty_kind, TyKind::RigidTy(RigidTy::Coroutine(..)))
790-
}
791-
792783
/// Extract the data pointer from a projection.
793784
/// The return type of the projection is not consistent today, so we need to specialize the
794785
/// behavior in order to get a consistent expression that represents a pointer to the projected

0 commit comments

Comments
 (0)