diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index b87f6f808aa8..9ca725b5a268 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/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) -> 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, - ) -> (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,7 +221,7 @@ impl<'tcx> GotocCtx<'tcx> { } /// Kani hooks function calls to `panic` and calls this intead. - pub fn codegen_panic(&self, span: Option, fargs: Vec) -> Stmt { + pub fn codegen_panic(&self, span: SpanStable, fargs: Vec) -> 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"); @@ -232,7 +229,8 @@ impl<'tcx> GotocCtx<'tcx> { "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. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs index b6743174aabb..11cdf47f4ed2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs +++ b/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(); } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 77d68af745ae..f3d79c7f06c5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/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(), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs index 4dbd0385f62c..938a784765e0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/mod.rs +++ b/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; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 59a18348d582..3339a1419f4a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/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, + ) -> 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. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 551de7034e15..5056d9d006ad 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -6,26 +6,31 @@ //! in [GotocCtx::codegen_place] below. use super::typ::TypeExt; -use crate::codegen_cprover_gotoc::codegen::typ::{pointee_type, std_pointee_type}; +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::utils::{dynamic_fat_ptr, slice_fat_ptr}; use crate::codegen_cprover_gotoc::GotocCtx; use crate::unwrap_or_return_codegen_unimplemented; use cbmc::goto_program::{Expr, Location, Type}; -use rustc_hir::Mutability; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::{ - mir::{Local, Place, ProjectionElem}, - ty::{self, Ty, TypeAndMut, VariantDef}, + mir::{Local as LocalInternal, Place as PlaceInternal}, + ty::Ty as TyInternal, }; -use rustc_target::abi::{FieldIdx, TagEncoding, VariantIdx, Variants}; +use rustc_smir::rustc_internal; +use rustc_target::abi::{TagEncoding, Variants}; +use stable_mir::mir::{FieldIdx, Local, Mutability, Place, ProjectionElem}; +use stable_mir::ty::{RigidTy, Ty, TyKind, VariantDef, VariantIdx}; use tracing::{debug, trace, warn}; /// A projection in Kani can either be to a type (the normal case), /// or a variant in the case of a downcast. #[derive(Copy, Clone, Debug)] -pub enum TypeOrVariant<'tcx> { - Type(Ty<'tcx>), - Variant(&'tcx VariantDef), +pub enum TypeOrVariant { + Type(Ty), + Variant(VariantDef), CoroutineVariant(VariantIdx), } @@ -55,33 +60,31 @@ impl UnimplementedData { /// Relevent information about a projected place (i.e. an lvalue). #[derive(Debug)] -pub struct ProjectedPlace<'tcx> { +pub struct ProjectedPlace { /// The goto expression that represents the lvalue pub goto_expr: Expr, /// The MIR type of that expression. Normally a type, but can be a variant following a downcast. - /// Invariant: guaranteed to be monomorphized by the type constructor - pub mir_typ_or_variant: TypeOrVariant<'tcx>, + pub mir_typ_or_variant: TypeOrVariant, /// If a fat pointer was traversed during the projection, it is stored here. /// This is useful if we need to use any of its fields, for e.g. to generate a rvalue ref /// or to implement the `length` operation. pub fat_ptr_goto_expr: Option, /// The MIR type of the visited fat pointer, if one was traversed during the projection. - /// Invariant: guaranteed to be monomorphized by the type constructor - pub fat_ptr_mir_typ: Option>, + pub fat_ptr_mir_typ: Option, } /// Getters #[allow(dead_code)] -impl<'tcx> ProjectedPlace<'tcx> { +impl ProjectedPlace { pub fn goto_expr(&self) -> &Expr { &self.goto_expr } - pub fn mir_typ_or_variant(&self) -> &TypeOrVariant<'tcx> { + pub fn mir_typ_or_variant(&self) -> &TypeOrVariant { &self.mir_typ_or_variant } - pub fn mir_typ(&self) -> Ty<'tcx> { + pub fn mir_typ(&self) -> Ty { self.mir_typ_or_variant.expect_type() } @@ -89,29 +92,29 @@ impl<'tcx> ProjectedPlace<'tcx> { &self.fat_ptr_goto_expr } - pub fn fat_ptr_mir_typ(&self) -> &Option> { + pub fn fat_ptr_mir_typ(&self) -> &Option { &self.fat_ptr_mir_typ } } /// Constructor -impl<'tcx> ProjectedPlace<'tcx> { +impl ProjectedPlace { fn check_expr_typ_mismatch( expr: &Expr, - typ: &TypeOrVariant<'tcx>, - ctx: &mut GotocCtx<'tcx>, + typ: &TypeOrVariant, + ctx: &mut GotocCtx, ) -> Option<(Type, Type)> { match typ { TypeOrVariant::Type(t) => { let expr_ty = expr.typ().clone(); - let type_from_mir = ctx.codegen_ty(*t); + let type_from_mir = ctx.codegen_ty_stable(*t); if expr_ty != type_from_mir { match t.kind() { // Slice references (`&[T]`) store raw pointers to the element type `T` // due to pointer decay. They are fat pointers with the following repr: // SliceRef { data: *T, len: usize }. // In those cases, the projection will yield a pointer type. - ty::Slice(..) | ty::Str + TyKind::RigidTy(RigidTy::Slice(..)) | TyKind::RigidTy(RigidTy::Str) if expr_ty.is_pointer() && expr_ty.base_type() == type_from_mir.base_type() => { @@ -119,7 +122,7 @@ impl<'tcx> ProjectedPlace<'tcx> { } // TODO: Do we really need this? // https://github.com/model-checking/kani/issues/1092 - ty::Dynamic(..) + TyKind::RigidTy(RigidTy::Dynamic(..)) if expr_ty.is_pointer() && *expr_ty.base_type().unwrap() == type_from_mir => { @@ -138,26 +141,33 @@ impl<'tcx> ProjectedPlace<'tcx> { fn check_fat_ptr_typ( fat_ptr: &Option, - fat_ptr_typ: &Option>, - ctx: &mut GotocCtx<'tcx>, + fat_ptr_typ: &Option, + ctx: &mut GotocCtx, ) -> bool { if let Some(fat_ptr) = fat_ptr { fat_ptr.typ().is_rust_fat_ptr(&ctx.symbol_table) - && fat_ptr.typ() == &ctx.codegen_ty(fat_ptr_typ.unwrap()) + && fat_ptr.typ() == &ctx.codegen_ty_stable(fat_ptr_typ.unwrap()) } else { true } } + pub fn try_new_internal<'tcx>( + goto_expr: Expr, + ty: TyInternal<'tcx>, + ctx: &mut GotocCtx<'tcx>, + ) -> Result { + let ty = ctx.monomorphize(ty); + Self::try_new(goto_expr, TypeOrVariant::Type(rustc_internal::stable(ty)), None, None, ctx) + } + pub fn try_new( goto_expr: Expr, - mir_typ_or_variant: TypeOrVariant<'tcx>, + mir_typ_or_variant: TypeOrVariant, fat_ptr_goto_expr: Option, - fat_ptr_mir_typ: Option>, - ctx: &mut GotocCtx<'tcx>, + fat_ptr_mir_typ: Option, + ctx: &mut GotocCtx, ) -> Result { - let mir_typ_or_variant = mir_typ_or_variant.monomorphize(ctx); - let fat_ptr_mir_typ = fat_ptr_mir_typ.map(|t| ctx.monomorphize(t)); if let Some(fat_ptr) = &fat_ptr_goto_expr { assert!( fat_ptr.typ().is_rust_fat_ptr(&ctx.symbol_table), @@ -166,9 +176,6 @@ impl<'tcx> ProjectedPlace<'tcx> { ctx.current_fn().readable_name() ); } - // TODO: these assertions fail on a few regressions. Figure out why. - // I think it may have to do with boxed fat pointers. - // https://github.com/model-checking/kani/issues/277 if let Some((expr_ty, ty_from_mir)) = Self::check_expr_typ_mismatch(&goto_expr, &mir_typ_or_variant, ctx) { @@ -201,17 +208,8 @@ impl<'tcx> ProjectedPlace<'tcx> { } } -impl<'tcx> TypeOrVariant<'tcx> { - pub fn monomorphize(self, ctx: &GotocCtx<'tcx>) -> Self { - match self { - TypeOrVariant::Type(t) => TypeOrVariant::Type(ctx.monomorphize(t)), - TypeOrVariant::Variant(_) | TypeOrVariant::CoroutineVariant(_) => self, - } - } -} - -impl<'tcx> TypeOrVariant<'tcx> { - pub fn expect_type(&self) -> Ty<'tcx> { +impl TypeOrVariant { + pub fn expect_type(&self) -> Ty { match self { TypeOrVariant::Type(t) => *t, TypeOrVariant::Variant(v) => panic!("expect a type but variant is found: {v:?}"), @@ -222,7 +220,7 @@ impl<'tcx> TypeOrVariant<'tcx> { } #[allow(dead_code)] - pub fn expect_variant(&self) -> &'tcx VariantDef { + pub fn expect_variant(&self) -> &VariantDef { match self { TypeOrVariant::Type(t) => panic!("expect a variant but type is found: {t:?}"), TypeOrVariant::Variant(v) => v, @@ -242,54 +240,61 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_field( &mut self, parent_expr: Expr, - parent_ty_or_var: TypeOrVariant<'tcx>, - field: &FieldIdx, - field_ty_or_var: TypeOrVariant<'tcx>, + parent_ty_or_var: TypeOrVariant, + field_idx: FieldIdx, + field_ty_or_var: TypeOrVariant, ) -> Result { match parent_ty_or_var { TypeOrVariant::Type(parent_ty) => { match parent_ty.kind() { - ty::Alias(..) - | ty::Bool - | ty::Char - | ty::Int(_) - | ty::Uint(_) - | ty::Float(_) - | ty::FnPtr(_) - | ty::Never - | ty::FnDef(..) - | ty::CoroutineWitness(..) - | ty::Foreign(..) - | ty::Dynamic(..) - | ty::Bound(..) - | ty::Placeholder(..) - | ty::Param(_) - | ty::Infer(_) - | ty::Error(_) => unreachable!("type {parent_ty:?} does not have a field"), - ty::Tuple(_) => { - Ok(parent_expr - .member(Self::tuple_fld_name(field.index()), &self.symbol_table)) + TyKind::Alias(..) + | TyKind::RigidTy(RigidTy::Bool) + | TyKind::RigidTy(RigidTy::Char) + | TyKind::RigidTy(RigidTy::Int(_)) + | TyKind::RigidTy(RigidTy::Uint(_)) + | TyKind::RigidTy(RigidTy::Float(_)) + | TyKind::RigidTy(RigidTy::FnPtr(_)) + | TyKind::RigidTy(RigidTy::Never) + | TyKind::RigidTy(RigidTy::FnDef(..)) + | TyKind::RigidTy(RigidTy::CoroutineWitness(..)) + | TyKind::RigidTy(RigidTy::Foreign(..)) + | TyKind::RigidTy(RigidTy::Dynamic(..)) + | TyKind::Bound(..) + | TyKind::Param(..) => { + unreachable!("type {parent_ty:?} does not have a field") + } + TyKind::RigidTy(RigidTy::Tuple(_)) => { + Ok(parent_expr.member(Self::tuple_fld_name(field_idx), &self.symbol_table)) + } + TyKind::RigidTy(RigidTy::Adt(def, _)) + if rustc_internal::internal(def).repr().simd() => + { + Ok(self.codegen_simd_field( + parent_expr, + field_idx, + field_ty_or_var.expect_type(), + )) } - ty::Adt(def, _) if def.repr().simd() => Ok(self.codegen_simd_field( - parent_expr, - *field, - field_ty_or_var.expect_type(), - )), // if we fall here, then we are handling either a struct or a union - ty::Adt(def, _) => { - let field = &def.variants().raw[0].fields[*field]; + TyKind::RigidTy(RigidTy::Adt(def, _)) => { + let fields = def.variants_iter().next().unwrap().fields(); + let field = &fields[field_idx]; Ok(parent_expr.member(field.name.to_string(), &self.symbol_table)) } - ty::Closure(..) => { - Ok(parent_expr.member(field.index().to_string(), &self.symbol_table)) + TyKind::RigidTy(RigidTy::Closure(..)) => { + Ok(parent_expr.member(field_idx.to_string(), &self.symbol_table)) } - ty::Coroutine(..) => { - let field_name = self.coroutine_field_name(field.as_usize()); + TyKind::RigidTy(RigidTy::Coroutine(..)) => { + let field_name = self.coroutine_field_name(field_idx); Ok(parent_expr .member("direct_fields", &self.symbol_table) .member(field_name, &self.symbol_table)) } - ty::Str | ty::Array(_, _) | ty::Slice(_) | ty::RawPtr(_) | ty::Ref(_, _, _) => { + TyKind::RigidTy(RigidTy::Str) + | TyKind::RigidTy(RigidTy::Array(_, _)) + | TyKind::RigidTy(RigidTy::Slice(_)) + | TyKind::RigidTy(RigidTy::RawPtr(..)) + | TyKind::RigidTy(RigidTy::Ref(_, _, _)) => { unreachable!( "element of {parent_ty:?} is not accessed via field projection" ) @@ -298,11 +303,12 @@ impl<'tcx> GotocCtx<'tcx> { } // if we fall here, then we are handling an enum TypeOrVariant::Variant(parent_var) => { - let field = &parent_var.fields[*field]; + let fields = parent_var.fields(); + let field = &fields[field_idx]; Ok(parent_expr.member(field.name.to_string(), &self.symbol_table)) } TypeOrVariant::CoroutineVariant(_var_idx) => { - let field_name = self.coroutine_field_name(field.index()); + let field_name = self.coroutine_field_name(field_idx); Ok(parent_expr.member(field_name, &self.symbol_table)) } } @@ -334,21 +340,15 @@ impl<'tcx> GotocCtx<'tcx> { /// /// Since the goto representation for both is the same, we use the expected type to decide /// what to return. - fn codegen_simd_field( - &mut self, - parent_expr: Expr, - field: FieldIdx, - field_ty: Ty<'tcx>, - ) -> Expr { - let field_ty = self.monomorphize(field_ty); - if matches!(field_ty.kind(), ty::Array { .. }) { + fn codegen_simd_field(&mut self, parent_expr: Expr, field_idx: FieldIdx, field_ty: Ty) -> Expr { + if matches!(field_ty.kind(), TyKind::RigidTy(RigidTy::Array { .. })) { // Array based - assert_eq!(field.index(), 0); - let field_typ = self.codegen_ty(field_ty); + assert_eq!(field_idx, 0); + let field_typ = self.codegen_ty_stable(field_ty); parent_expr.reinterpret_cast(field_typ) } else { // Return the given field. - let index_expr = Expr::int_constant(field.index(), Type::size_t()); + let index_expr = Expr::int_constant(field_idx, Type::size_t()); parent_expr.index_array(index_expr) } } @@ -365,18 +365,22 @@ impl<'tcx> GotocCtx<'tcx> { /// a named variable. /// /// Recursively finds the actual FnDef from a pointer or box. - fn codegen_local_fndef(&mut self, ty: ty::Ty<'tcx>) -> Option { + fn codegen_local_fndef(&mut self, ty: Ty) -> Option { match ty.kind() { // A local that is itself a FnDef, like Fn::call_once - ty::FnDef(defid, args) => Some(self.codegen_fndef(*defid, args, None)), + TyKind::RigidTy(RigidTy::FnDef(def, args)) => { + Some(self.codegen_fndef_stable(def, &args, None)) + } // A local can be pointer to a FnDef, like Fn::call and Fn::call_mut - ty::RawPtr(inner) => self - .codegen_local_fndef(inner.ty) + TyKind::RigidTy(RigidTy::RawPtr(inner, _)) => self + .codegen_local_fndef(inner) .map(|f| if f.can_take_address_of() { f.address_of() } else { f }), // A local can be a boxed function pointer - ty::Adt(def, _) if def.is_box() => { - let boxed_ty = self.codegen_ty(ty); - self.codegen_local_fndef(ty.boxed_ty()) + TyKind::RigidTy(RigidTy::Adt(def, args)) if def.is_box() => { + let boxed_ty = self.codegen_ty_stable(ty); + // The type of `T` for `Box` can be derived from the first definition args. + let inner_ty = args.0[0].ty().unwrap(); + self.codegen_local_fndef(*inner_ty) .map(|f| self.box_value(f.address_of(), boxed_ty)) } _ => None, @@ -385,14 +389,15 @@ impl<'tcx> GotocCtx<'tcx> { /// Codegen for a local fn codegen_local(&mut self, l: Local) -> Expr { + let local_ty = self.local_ty_stable(l); // Check if the local is a function definition (see comment above) - if let Some(fn_def) = self.codegen_local_fndef(self.local_ty(l)) { + if let Some(fn_def) = self.codegen_local_fndef(local_ty) { return fn_def; } // Otherwise, simply look up the local by the var name. - let vname = self.codegen_var_name(&l); - Expr::symbol_expression(vname, self.codegen_ty(self.local_ty(l))) + let vname = self.codegen_var_name(&LocalInternal::from(l)); + Expr::symbol_expression(vname, self.codegen_ty_stable(local_ty)) } /// A projection is an operation that translates an lvalue to another lvalue. @@ -402,22 +407,26 @@ impl<'tcx> GotocCtx<'tcx> { /// the return value is the expression after. fn codegen_projection( &mut self, - before: Result, UnimplementedData>, - proj: ProjectionElem>, - ) -> Result, UnimplementedData> { + before: Result, + proj: &ProjectionElem, + ) -> Result { let before = before?; trace!(?before, ?proj, "codegen_projection"); match proj { ProjectionElem::Deref => { let base_type = before.mir_typ(); - let inner_goto_expr = if base_type.is_box() { + let inner_goto_expr = if is_box(base_type) { self.deref_box(before.goto_expr) } else { before.goto_expr }; - let inner_mir_typ = std_pointee_type(base_type).unwrap(); - let (fat_ptr_mir_typ, fat_ptr_goto_expr) = if self.use_thin_pointer(inner_mir_typ) { + let inner_mir_typ_internal = + std_pointee_type(rustc_internal::internal(base_type)).unwrap(); + let inner_mir_typ = rustc_internal::stable(inner_mir_typ_internal); + let (fat_ptr_mir_typ, fat_ptr_goto_expr) = if self + .use_thin_pointer(inner_mir_typ_internal) + { (before.fat_ptr_mir_typ, before.fat_ptr_goto_expr) } else { (Some(before.mir_typ_or_variant.expect_type()), Some(inner_goto_expr.clone())) @@ -433,7 +442,9 @@ impl<'tcx> GotocCtx<'tcx> { pointee_type(fat_ptr_mir_typ.unwrap()).unwrap().kind(), ); assert!( - self.use_fat_pointer(pointee_type(fat_ptr_mir_typ.unwrap()).unwrap()), + self.use_fat_pointer(rustc_internal::internal( + pointee_type(fat_ptr_mir_typ.unwrap()).unwrap() + )), "Unexpected type: {:?} -- {:?}", fat_ptr.typ(), fat_ptr_mir_typ, @@ -441,10 +452,14 @@ impl<'tcx> GotocCtx<'tcx> { }; let expr = match inner_mir_typ.kind() { - ty::Slice(_) | ty::Str | ty::Dynamic(..) => { + TyKind::RigidTy(RigidTy::Slice(_)) + | TyKind::RigidTy(RigidTy::Str) + | TyKind::RigidTy(RigidTy::Dynamic(..)) => { inner_goto_expr.member("data", &self.symbol_table) } - ty::Adt(..) if self.is_unsized(inner_mir_typ) => { + TyKind::RigidTy(RigidTy::Adt(..)) + if self.is_unsized(inner_mir_typ_internal) => + { // in tests/kani/Strings/os_str_reduced.rs, we see // ``` // p.projection = [ @@ -463,7 +478,7 @@ impl<'tcx> GotocCtx<'tcx> { .member("data", &self.symbol_table) // In the case of a vtable fat pointer, this data member is a void pointer, // so ensure the pointer has the correct type before dereferencing it. - .cast_to(self.codegen_ty(inner_mir_typ).to_pointer()) + .cast_to(self.codegen_ty_stable(inner_mir_typ).to_pointer()) .dereference() } _ => inner_goto_expr.dereference(), @@ -471,10 +486,10 @@ impl<'tcx> GotocCtx<'tcx> { let typ = TypeOrVariant::Type(inner_mir_typ); ProjectedPlace::try_new(expr, typ, fat_ptr_goto_expr, fat_ptr_mir_typ, self) } - ProjectionElem::Field(f, t) => { - let typ = TypeOrVariant::Type(t); + ProjectionElem::Field(idx, ty) => { + let typ = TypeOrVariant::Type(*ty); let expr = - self.codegen_field(before.goto_expr, before.mir_typ_or_variant, &f, typ)?; + self.codegen_field(before.goto_expr, before.mir_typ_or_variant, *idx, typ)?; ProjectedPlace::try_new( expr, typ, @@ -485,14 +500,17 @@ impl<'tcx> GotocCtx<'tcx> { } ProjectionElem::Index(i) => { let base_type = before.mir_typ(); - let idxe = self.codegen_local(i); + let idxe = self.codegen_local(*i); let typ = match base_type.kind() { - ty::Array(elemt, _) | ty::Slice(elemt) => TypeOrVariant::Type(*elemt), + TyKind::RigidTy(RigidTy::Array(elemt, _)) + | TyKind::RigidTy(RigidTy::Slice(elemt)) => TypeOrVariant::Type(elemt), _ => unreachable!("must index an array"), }; let expr = match base_type.kind() { - ty::Array(..) => self.codegen_idx_array(before.goto_expr, idxe), - ty::Slice(..) => before.goto_expr.index(idxe), + TyKind::RigidTy(RigidTy::Array(..)) => { + self.codegen_idx_array(before.goto_expr, idxe) + } + TyKind::RigidTy(RigidTy::Slice(..)) => before.goto_expr.index(idxe), _ => unreachable!("must index an array"), }; ProjectedPlace::try_new( @@ -504,7 +522,7 @@ impl<'tcx> GotocCtx<'tcx> { ) } ProjectionElem::ConstantIndex { offset, min_length, from_end } => { - self.codegen_constant_index(before, offset, min_length, from_end) + self.codegen_constant_index(before, *offset, *min_length, *from_end) } // Best effort to codegen subslice projection. // Full support to be added in @@ -512,16 +530,16 @@ impl<'tcx> GotocCtx<'tcx> { ProjectionElem::Subslice { from, to, from_end } => { // https://rust-lang.github.io/rfcs/2359-subslice-pattern-syntax.html match before.mir_typ().kind() { - ty::Array(ty, len) => { - let len = len.try_to_target_usize(self.tcx).unwrap(); - let subarray_len = if from_end { + TyKind::RigidTy(RigidTy::Array(ty, len)) => { + let len = len.eval_target_usize().unwrap(); + let subarray_len = if *from_end { // `to` counts from the end of the array len - to - from } else { to - from }; - let typ = Ty::new_array(self.tcx, *ty, subarray_len); - let goto_typ = self.codegen_ty(typ); + let typ = Ty::try_new_array(ty, subarray_len).unwrap(); + let goto_typ = self.codegen_ty_stable(typ); // unimplemented Err(UnimplementedData::new( "Sub-array binding", @@ -530,8 +548,8 @@ impl<'tcx> GotocCtx<'tcx> { *before.goto_expr.location(), )) } - ty::Slice(elemt) => { - let len = if from_end { + TyKind::RigidTy(RigidTy::Slice(_)) => { + let len = if *from_end { let olen = before .fat_ptr_goto_expr .clone() @@ -542,12 +560,11 @@ impl<'tcx> GotocCtx<'tcx> { } else { Expr::int_constant(to - from, Type::size_t()) }; - let typ = Ty::new_slice(self.tcx, *elemt); - let typ_and_mut = TypeAndMut { ty: typ, mutbl: Mutability::Mut }; - let ptr_typ = Ty::new_ptr(self.tcx, typ_and_mut); - let goto_type = self.codegen_ty(ptr_typ); + let typ = before.mir_typ(); + let ptr_typ = Ty::new_ptr(typ, Mutability::Not); + let goto_type = self.codegen_ty_stable(ptr_typ); - let index = Expr::int_constant(from, Type::ssize_t()); + let index = Expr::int_constant(*from, Type::ssize_t()); let from_elem = before.goto_expr.index(index); let data = from_elem.address_of(); let fat_ptr = slice_fat_ptr(goto_type, data, len, &self.symbol_table); @@ -562,28 +579,33 @@ impl<'tcx> GotocCtx<'tcx> { _ => unreachable!("must be array or slice"), } } - ProjectionElem::Downcast(_, idx) => { + ProjectionElem::Downcast(idx) => { // downcast converts a variable of an enum type to one of its discriminated cases - let t = before.mir_typ(); - let (case_name, type_or_variant) = match t.kind() { - ty::Adt(def, _) => { - let variant = def.variant(idx); - (variant.name.as_str().into(), TypeOrVariant::Variant(variant)) + let ty = before.mir_typ(); + let ty_kind = ty.kind(); + let (case_name, type_or_variant) = match &ty_kind { + TyKind::RigidTy(RigidTy::Adt(def, _)) => { + let variant = def.variant(*idx).unwrap(); + (variant.name().into(), TypeOrVariant::Variant(variant)) } - ty::Coroutine(..) => { - (self.coroutine_variant_name(idx), TypeOrVariant::CoroutineVariant(idx)) + TyKind::RigidTy(RigidTy::Coroutine(..)) => { + let idx_internal = rustc_internal::internal(idx); + ( + self.coroutine_variant_name(idx_internal), + TypeOrVariant::CoroutineVariant(*idx), + ) } _ => unreachable!( "cannot downcast {:?} to a variant (only enums and coroutines can)", - &t.kind() + &ty.kind() ), }; - let layout = self.layout_of(t); + let layout = self.layout_of(rustc_internal::internal(ty)); let expr = match &layout.variants { Variants::Single { .. } => before.goto_expr, Variants::Multiple { tag_encoding, .. } => match tag_encoding { TagEncoding::Direct => { - let cases = if t.is_coroutine() { + let cases = if is_coroutine(ty_kind) { before.goto_expr } else { before.goto_expr.member("cases", &self.symbol_table) @@ -605,8 +627,8 @@ impl<'tcx> GotocCtx<'tcx> { } ProjectionElem::OpaqueCast(ty) | ProjectionElem::Subtype(ty) => { ProjectedPlace::try_new( - before.goto_expr.cast_to(self.codegen_ty(self.monomorphize(ty))), - TypeOrVariant::Type(ty), + before.goto_expr.cast_to(self.codegen_ty_stable(*ty)), + TypeOrVariant::Type(*ty), before.fat_ptr_goto_expr, before.fat_ptr_mir_typ, self, @@ -621,13 +643,13 @@ impl<'tcx> GotocCtx<'tcx> { /// build the fat pointer from there. /// - For `*(Wrapper)` 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: &Place<'tcx>) -> Expr { + 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) { // Just return the address of the place dereferenced. projection.goto_expr.address_of() - } else if place_ty == pointee_type(self.local_ty(place.local)).unwrap() { + } else if place_ty == pointee_type_internal(self.local_ty(place.local)).unwrap() { // Just return the fat pointer if this is a simple &(*local). projection.fat_ptr_goto_expr.unwrap() } else { @@ -652,17 +674,17 @@ impl<'tcx> GotocCtx<'tcx> { /// This function follows the MIR projection to get the final useable lvalue. /// If it passes through a fat pointer along the way, it stores info about it, /// which can be useful in reconstructing fat pointer operations. - pub fn codegen_place( + pub fn codegen_place_stable( &mut self, - p: &Place<'tcx>, - ) -> Result, UnimplementedData> { - debug!(place=?p, "codegen_place"); - let initial_expr = self.codegen_local(p.local); - let initial_typ = TypeOrVariant::Type(self.local_ty(p.local)); + place: &Place, + ) -> Result { + debug!(?place, "codegen_place"); + let initial_expr = self.codegen_local(place.local); + let initial_typ = TypeOrVariant::Type(self.local_ty_stable(place.local)); debug!(?initial_typ, ?initial_expr, "codegen_place"); let initial_projection = ProjectedPlace::try_new(initial_expr, initial_typ, None, None, self); - let result = p + let result = place .projection .iter() .fold(initial_projection, |accum, proj| self.codegen_projection(accum, proj)); @@ -670,22 +692,29 @@ impl<'tcx> GotocCtx<'tcx> { Err(data) => Err(UnimplementedData::new( &data.operation, &data.bug_url, - self.codegen_ty(self.place_ty(p)), + self.codegen_ty_stable(self.place_ty_stable(place)), data.loc, )), _ => result, } } + pub fn codegen_place( + &mut self, + place: &PlaceInternal<'tcx>, + ) -> Result { + self.codegen_place_stable(&StableConverter::convert_place(self, *place)) + } + /// Given a projection, generate an lvalue that represents the given variant index. pub fn codegen_variant_lvalue( &mut self, - initial_projection: ProjectedPlace<'tcx>, + initial_projection: ProjectedPlace, variant_idx: VariantIdx, - ) -> ProjectedPlace<'tcx> { + ) -> ProjectedPlace { debug!(?initial_projection, ?variant_idx, "codegen_variant_lvalue"); - let downcast = ProjectionElem::Downcast(None, variant_idx); - self.codegen_projection(Ok(initial_projection), downcast).unwrap() + let downcast = ProjectionElem::Downcast(variant_idx); + self.codegen_projection(Ok(initial_projection), &downcast).unwrap() } // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.ProjectionElem.html @@ -698,20 +727,20 @@ impl<'tcx> GotocCtx<'tcx> { // [_, _, .._, _, X] => { offset: 1, min_length: 4, from_end: true }, fn codegen_constant_index( &mut self, - before: ProjectedPlace<'tcx>, + before: ProjectedPlace, offset: u64, min_length: u64, from_end: bool, - ) -> Result, UnimplementedData> { + ) -> Result { match before.mir_typ().kind() { //TODO, ask on zulip if we can ever have from_end here? - ty::Array(elemt, length) => { - let length = length.try_to_target_usize(self.tcx).unwrap(); + TyKind::RigidTy(RigidTy::Array(elemt, length)) => { + let length = length.eval_target_usize().unwrap(); assert!(length >= min_length); let idx = if from_end { length - offset } else { offset }; let idxe = Expr::int_constant(idx, Type::ssize_t()); let expr = self.codegen_idx_array(before.goto_expr, idxe); - let typ = TypeOrVariant::Type(*elemt); + let typ = TypeOrVariant::Type(elemt); ProjectedPlace::try_new( expr, typ, @@ -720,7 +749,7 @@ impl<'tcx> GotocCtx<'tcx> { self, ) } - ty::Slice(elemt) => { + TyKind::RigidTy(RigidTy::Slice(elemt)) => { let offset_e = Expr::int_constant(offset, Type::size_t()); //TODO, should we assert min_length? Or is that already handled by the typechecker? let idxe = if from_end { @@ -731,7 +760,7 @@ impl<'tcx> GotocCtx<'tcx> { offset_e }; let expr = before.goto_expr.plus(idxe).dereference(); - let typ = TypeOrVariant::Type(*elemt); + let typ = TypeOrVariant::Type(elemt); ProjectedPlace::try_new( expr, typ, @@ -752,6 +781,14 @@ 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 diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 8ded0b7f421a..e4b550c93591 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use super::typ::pointee_type; -use crate::codegen_cprover_gotoc::codegen::place::{ProjectedPlace, TypeOrVariant}; +use crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace; use crate::codegen_cprover_gotoc::codegen::PropertyClass; use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr}; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; @@ -22,6 +22,7 @@ use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, use rustc_middle::ty::adjustment::PointerCoercion; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry}; +use rustc_smir::rustc_internal; use rustc_target::abi::{FieldIdx, FieldsShape, Size, TagEncoding, VariantIdx, Variants}; use std::collections::BTreeMap; use tracing::{debug, trace, warn}; @@ -552,15 +553,10 @@ impl<'tcx> GotocCtx<'tcx> { stmts.push(decl); if !operands.is_empty() { // 2- Initialize the members of the temporary variant. - let initial_projection = ProjectedPlace::try_new( - temp_var.clone(), - TypeOrVariant::Type(res_ty), - None, - None, - self, - ) - .unwrap(); - let variant_proj = self.codegen_variant_lvalue(initial_projection, variant_index); + let initial_projection = + ProjectedPlace::try_new_internal(temp_var.clone(), res_ty, self).unwrap(); + let variant_proj = self + .codegen_variant_lvalue(initial_projection, rustc_internal::stable(variant_index)); let variant_expr = variant_proj.goto_expr.clone(); let layout = self.layout_of(res_ty); let fields = match &layout.variants { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index 3fbfd3629775..70b00357d264 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs @@ -9,13 +9,14 @@ use rustc_middle::mir::{Local, VarDebugInfoContents}; use rustc_smir::rustc_internal; use rustc_span::Span; use stable_mir::mir::VarDebugInfo; +use stable_mir::ty::Span as SpanStable; impl<'tcx> GotocCtx<'tcx> { pub fn codegen_span(&self, sp: &Span) -> Location { - self.stable_codegen_span(&rustc_internal::stable(sp)) + self.codegen_span_stable(rustc_internal::stable(sp)) } - pub fn stable_codegen_span(&self, sp: &stable_mir::ty::Span) -> Location { + pub fn codegen_span_stable(&self, sp: SpanStable) -> Location { let loc = sp.get_lines(); Location::new( sp.get_filename().to_string(), @@ -26,6 +27,9 @@ impl<'tcx> GotocCtx<'tcx> { Some(loc.end_col), ) } + pub fn codegen_caller_span_stable(&self, sp: SpanStable) -> Location { + self.codegen_caller_span(&Some(rustc_internal::internal(sp))) + } /// Get the location of the caller. This will attempt to reach the macro caller. /// This function uses rustc_span methods designed to returns span for the macro which @@ -45,11 +49,11 @@ impl<'tcx> GotocCtx<'tcx> { } pub fn find_debug_info(&self, l: &Local) -> Option { - rustc_internal::stable(self.current_fn().mir().var_debug_info.iter().find(|info| { - match info.value { + rustc_internal::stable(self.current_fn().body_internal().var_debug_info.iter().find( + |info| match info.value { VarDebugInfoContents::Place(p) => p.local == *l && p.projection.len() == 0, VarDebugInfoContents::Const(_) => false, - } - })) + }, + )) } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index d673c7d37c83..9ab0cbcc8d98 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -14,6 +14,7 @@ use rustc_middle::mir::{ use rustc_middle::ty; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{Instance, InstanceDef, Ty}; +use rustc_smir::rustc_internal; use rustc_span::Span; use rustc_target::abi::VariantIdx; use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants}; @@ -174,8 +175,10 @@ impl<'tcx> GotocCtx<'tcx> { msg.description() }; - let (msg_str, reach_stmt) = - self.codegen_reachability_check(msg.to_owned(), Some(term.source_info.span)); + let (msg_str, reach_stmt) = self.codegen_reachability_check( + msg.to_owned(), + rustc_internal::stable(term.source_info.span), + ); Stmt::block( vec![ @@ -530,8 +533,16 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_untupled_args(instance, &mut fargs, args.last()); } - if let Some(hk) = self.hooks.hook_applies(self.tcx, instance) { - return hk.handle(self, instance, fargs, *destination, *target, Some(span)); + let stable_instance = rustc_internal::stable(instance); + if let Some(hk) = self.hooks.hook_applies(self.tcx, stable_instance) { + return hk.handle( + self, + stable_instance, + fargs, + rustc_internal::stable(destination), + target.map(BasicBlock::as_usize), + rustc_internal::stable(span), + ); } let mut stmts: Vec = match instance.def { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs new file mode 100644 index 000000000000..64222f15e091 --- /dev/null +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs @@ -0,0 +1,72 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Stable functions involving type manipulation. +//! +//! This may for now invoke functions that use internal Rust compiler APIs. +//! While we migrate to stable APIs, this module will contain stable versions of functions from +//! `typ.rs`. + +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_smir::rustc_internal; +use stable_mir::mir::{Local, Place}; +use stable_mir::ty::{RigidTy, Ty, TyKind}; + +impl<'tcx> GotocCtx<'tcx> { + pub fn place_ty_stable(&self, place: &Place) -> Ty { + place.ty(self.current_fn().body().locals()).unwrap() + } + + pub fn codegen_ty_stable(&mut self, ty: Ty) -> Type { + self.codegen_ty(rustc_internal::internal(ty)) + } + + pub fn local_ty_stable(&mut self, local: Local) -> Ty { + self.current_fn().body().local_decl(local).unwrap().ty + } +} +/// If given type is a Ref / Raw ref, return the pointee type. +pub fn pointee_type(mir_type: Ty) -> Option { + match mir_type.kind() { + TyKind::RigidTy(RigidTy::Ref(_, pointee_type, _)) => Some(pointee_type), + TyKind::RigidTy(RigidTy::RawPtr(ty, ..)) => Some(ty), + _ => None, + } +} + +/// Convert internal rustc's structs into StableMIR ones. +/// +/// The body of a StableMIR instance already comes monomorphized, which is different from rustc's +/// internal representation. To allow us to migrate parts of the code generation stage with +/// smaller PRs, we have to instantiate rustc's components when converting them to stable. +/// +/// Once we finish migrating the entire function code generation, we can remove this code. +pub struct StableConverter<'a, 'tcx> { + gcx: &'a GotocCtx<'tcx>, +} + +impl<'a, 'tcx> StableConverter<'a, 'tcx> { + pub fn convert_place(gcx: &'a GotocCtx<'tcx>, mut place: PlaceInternal<'tcx>) -> Place { + let mut converter = StableConverter { gcx }; + converter.visit_place( + &mut place, + PlaceContext::NonUse(NonUseContext::VarDebugInfo), + mir::Location::START, + ); + rustc_internal::stable(place) + } +} + +impl<'a, 'tcx> MutVisitor<'tcx> for StableConverter<'a, 'tcx> { + fn tcx(&self) -> TyCtxt<'tcx> { + self.gcx.tcx + } + + fn visit_ty(&mut self, ty: &mut TyInternal<'tcx>, _: mir::visit::TyContext) { + *ty = self.gcx.monomorphize(*ty); + } +} diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 3a9d54a384af..9b875985b1ab 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -436,19 +436,19 @@ impl<'tcx> GotocCtx<'tcx> { } pub fn local_ty(&self, l: Local) -> Ty<'tcx> { - self.monomorphize(self.current_fn().mir().local_decls()[l].ty) + self.monomorphize(self.current_fn().body_internal().local_decls()[l].ty) } pub fn rvalue_ty(&self, rv: &Rvalue<'tcx>) -> Ty<'tcx> { - self.monomorphize(rv.ty(self.current_fn().mir().local_decls(), self.tcx)) + self.monomorphize(rv.ty(self.current_fn().body_internal().local_decls(), self.tcx)) } pub fn operand_ty(&self, o: &Operand<'tcx>) -> Ty<'tcx> { - self.monomorphize(o.ty(self.current_fn().mir().local_decls(), self.tcx)) + self.monomorphize(o.ty(self.current_fn().body_internal().local_decls(), self.tcx)) } pub fn place_ty(&self, p: &Place<'tcx>) -> Ty<'tcx> { - self.monomorphize(p.ty(self.current_fn().mir().local_decls(), self.tcx).ty) + self.monomorphize(p.ty(self.current_fn().body_internal().local_decls(), self.tcx).ty) } /// Is the MIR type a zero-sized type. @@ -1710,7 +1710,7 @@ impl<'tcx> GotocCtx<'tcx> { // components as parameters with a special naming convention // so that we can "retuple" them in the function prelude. // See: compiler/rustc_codegen_llvm/src/gotoc/mod.rs:codegen_function_prelude - if let Some(spread) = self.current_fn().mir().spread_arg { + if let Some(spread) = self.current_fn().body_internal().spread_arg { if lc.index() >= spread.index() { let (name, _) = self.codegen_spread_arg_name(&lc); ident = name; diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs index 1c503cadd3b3..e39d44743c5f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs @@ -3,26 +3,26 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Stmt; -use rustc_middle::mir::BasicBlock; -use rustc_middle::mir::Body; -use rustc_middle::ty::Instance; -use rustc_middle::ty::PolyFnSig; +use rustc_middle::mir::{BasicBlock, Body as InternalBody}; +use rustc_middle::ty::{Instance as InternalInstance, PolyFnSig}; +use rustc_smir::rustc_internal; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::Body; +use stable_mir::CrateDef; /// This structure represents useful data about the function we are currently compiling. #[derive(Debug)] pub struct CurrentFnCtx<'tcx> { /// The GOTO block we are compiling into block: Vec, - /// The current MIR basic block - current_bb: Option, /// The codegen instance for the current function - instance: Instance<'tcx>, + instance: Instance, /// The crate this function is from krate: String, - /// The goto labels for all blocks - labels: Vec, - /// The mir for the current instance - mir: &'tcx Body<'tcx>, + /// The MIR for the current instance. This is using the internal representation. + mir: &'tcx InternalBody<'tcx>, + /// The MIR for the current instance. + body: Body, /// The symbol name of the current function name: String, /// A human readable pretty name for the current function @@ -35,17 +35,21 @@ pub struct CurrentFnCtx<'tcx> { /// Constructor impl<'tcx> CurrentFnCtx<'tcx> { - pub fn new(instance: Instance<'tcx>, gcx: &GotocCtx<'tcx>, labels: Vec) -> Self { + pub fn new(instance: Instance, gcx: &GotocCtx<'tcx>) -> Self { + let internal_instance = rustc_internal::internal(instance); + let body = instance.body().unwrap(); + let readable_name = instance.name(); + let name = + if &readable_name == "main" { readable_name.clone() } else { instance.mangled_name() }; Self { block: vec![], - current_bb: None, instance, - krate: gcx.get_crate(instance), - labels, - mir: gcx.tcx.instance_mir(instance.def), - name: gcx.symbol_name(instance), - readable_name: gcx.readable_instance_name(instance), - sig: gcx.fn_sig_of_instance(instance), + mir: gcx.tcx.instance_mir(internal_instance.def), + krate: instance.def.krate().name, + body, + name, + readable_name, + sig: gcx.fn_sig_of_instance(internal_instance), temp_var_counter: 0, } } @@ -67,21 +71,13 @@ impl<'tcx> CurrentFnCtx<'tcx> { pub fn push_onto_block(&mut self, s: Stmt) { self.block.push(s) } - - pub fn reset_current_bb(&mut self) { - self.current_bb = None; - } - - pub fn set_current_bb(&mut self, bb: BasicBlock) { - self.current_bb = Some(bb); - } } /// Getters impl<'tcx> CurrentFnCtx<'tcx> { /// The function we are currently compiling - pub fn instance(&self) -> Instance<'tcx> { - self.instance + pub fn instance(&self) -> InternalInstance<'tcx> { + rustc_internal::internal(self.instance) } /// The crate that function came from @@ -89,8 +85,8 @@ impl<'tcx> CurrentFnCtx<'tcx> { self.krate.to_string() } - /// The MIR for the function we are currently compiling - pub fn mir(&self) -> &'tcx Body<'tcx> { + /// The internal MIR for the function we are currently compiling using internal APIs. + pub fn body_internal(&self) -> &'tcx InternalBody<'tcx> { self.mir } @@ -108,6 +104,11 @@ impl<'tcx> CurrentFnCtx<'tcx> { pub fn sig(&self) -> PolyFnSig<'tcx> { self.sig } + + /// The body of the function. + pub fn body(&self) -> &Body { + &self.body + } } /// Utility functions @@ -118,6 +119,6 @@ impl CurrentFnCtx<'_> { } pub fn find_label(&self, bb: &BasicBlock) -> String { - self.labels[bb.index()].clone() + format!("{bb:?}") } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 6619a6949681..d8901ae53803 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -31,6 +31,7 @@ use rustc_middle::ty::layout::{ TyAndLayout, }; use rustc_middle::ty::{self, Instance, Ty, TyCtxt}; +use rustc_smir::rustc_internal; use rustc_span::source_map::respan; use rustc_span::Span; use rustc_target::abi::call::FnAbi; @@ -44,7 +45,7 @@ pub struct GotocCtx<'tcx> { pub queries: QueryDb, /// the generated symbol table for gotoc pub symbol_table: SymbolTable, - pub hooks: GotocHooks<'tcx>, + pub hooks: GotocHooks, /// the full crate name, including versioning info pub full_crate_name: String, /// a global counter for generating unique names for global variables @@ -298,16 +299,7 @@ impl<'tcx> GotocCtx<'tcx> { /// Mutators impl<'tcx> GotocCtx<'tcx> { pub fn set_current_fn(&mut self, instance: Instance<'tcx>) { - self.current_fn = Some(CurrentFnCtx::new( - instance, - self, - self.tcx - .instance_mir(instance.def) - .basic_blocks - .indices() - .map(|bb| format!("{bb:?}")) - .collect(), - )); + self.current_fn = Some(CurrentFnCtx::new(rustc_internal::stable(instance), self)); } pub fn reset_current_fn(&mut self) { diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index e648d9ffc006..e20ca5d41c60 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -8,36 +8,37 @@ //! It would be too nasty if we spread around these sort of undocumented hooks in place, so //! this module addresses this issue. -use crate::codegen_cprover_gotoc::codegen::PropertyClass; +use crate::codegen_cprover_gotoc::codegen::{bb_label, PropertyClass}; use crate::codegen_cprover_gotoc::GotocCtx; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type}; -use rustc_middle::mir::{BasicBlock, Place}; -use rustc_middle::ty::print::with_no_trimmed_paths; -use rustc_middle::ty::{Instance, TyCtxt}; -use rustc_span::Span; +use rustc_middle::ty::TyCtxt; +use rustc_smir::rustc_internal; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::{BasicBlockIdx, Place}; +use stable_mir::{ty::Span, CrateDef}; use std::rc::Rc; use tracing::debug; -pub trait GotocHook<'tcx> { +pub trait GotocHook { /// if the hook applies, it means the codegen would do something special to it - fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool; + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool; /// the handler for codegen fn handle( &self, - tcx: &mut GotocCtx<'tcx>, - instance: Instance<'tcx>, + gcx: &mut GotocCtx, + instance: Instance, fargs: Vec, - assign_to: Place<'tcx>, - target: Option, - span: Option, + assign_to: Place, + target: Option, + span: Span, ) -> Stmt; } fn matches_function(tcx: TyCtxt, instance: Instance, attr_name: &str) -> bool { let attr_sym = rustc_span::symbol::Symbol::intern(attr_name); if let Some(attr_id) = tcx.all_diagnostic_items(()).name_to_id.get(&attr_sym) { - if instance.def.def_id() == *attr_id { + if rustc_internal::internal(instance.def.def_id()) == *attr_id { debug!("matched: {:?} {:?}", attr_id, attr_sym); return true; } @@ -54,34 +55,34 @@ fn matches_function(tcx: TyCtxt, instance: Instance, attr_name: &str) -> bool { /// /// for more details. struct Cover; -impl<'tcx> GotocHook<'tcx> for Cover { - fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { +impl GotocHook for Cover { + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { matches_function(tcx, instance, "KaniCover") } fn handle( &self, - tcx: &mut GotocCtx<'tcx>, - _instance: Instance<'tcx>, + gcx: &mut GotocCtx, + _instance: Instance, mut fargs: Vec, - _assign_to: Place<'tcx>, - target: Option, - span: Option, + _assign_to: Place, + target: Option, + span: Span, ) -> Stmt { assert_eq!(fargs.len(), 2); let cond = fargs.remove(0).cast_to(Type::bool()); let msg = fargs.remove(0); - let msg = tcx.extract_const_message(&msg).unwrap(); + let msg = gcx.extract_const_message(&msg).unwrap(); let target = target.unwrap(); - let caller_loc = tcx.codegen_caller_span(&span); + let caller_loc = gcx.codegen_caller_span_stable(span); - let (msg, reach_stmt) = tcx.codegen_reachability_check(msg, span); + let (msg, reach_stmt) = gcx.codegen_reachability_check(msg, span); Stmt::block( vec![ reach_stmt, - tcx.codegen_cover(cond, &msg, span), - Stmt::goto(tcx.current_fn().find_label(&target), caller_loc), + gcx.codegen_cover(cond, &msg, span), + Stmt::goto(bb_label(target), caller_loc), ], caller_loc, ) @@ -89,69 +90,63 @@ impl<'tcx> GotocHook<'tcx> for Cover { } struct Assume; -impl<'tcx> GotocHook<'tcx> for Assume { - fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { +impl GotocHook for Assume { + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { matches_function(tcx, instance, "KaniAssume") } fn handle( &self, - tcx: &mut GotocCtx<'tcx>, - _instance: Instance<'tcx>, + gcx: &mut GotocCtx, + _instance: Instance, mut fargs: Vec, - _assign_to: Place<'tcx>, - target: Option, - span: Option, + _assign_to: Place, + target: Option, + span: Span, ) -> Stmt { assert_eq!(fargs.len(), 1); let cond = fargs.remove(0).cast_to(Type::bool()); let target = target.unwrap(); - let loc = tcx.codegen_span_option(span); + let loc = gcx.codegen_span_stable(span); - Stmt::block( - vec![ - tcx.codegen_assume(cond, loc), - Stmt::goto(tcx.current_fn().find_label(&target), loc), - ], - loc, - ) + Stmt::block(vec![gcx.codegen_assume(cond, loc), Stmt::goto(bb_label(target), loc)], loc) } } struct Assert; -impl<'tcx> GotocHook<'tcx> for Assert { - fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { +impl GotocHook for Assert { + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { matches_function(tcx, instance, "KaniAssert") } fn handle( &self, - tcx: &mut GotocCtx<'tcx>, - _instance: Instance<'tcx>, + gcx: &mut GotocCtx, + _instance: Instance, mut fargs: Vec, - _assign_to: Place<'tcx>, - target: Option, - span: Option, + _assign_to: Place, + target: Option, + span: Span, ) -> Stmt { assert_eq!(fargs.len(), 2); let cond = fargs.remove(0).cast_to(Type::bool()); let msg = fargs.remove(0); - let msg = tcx.extract_const_message(&msg).unwrap(); + let msg = gcx.extract_const_message(&msg).unwrap(); let target = target.unwrap(); - let caller_loc = tcx.codegen_caller_span(&span); + let caller_loc = gcx.codegen_caller_span_stable(span); - let (msg, reach_stmt) = tcx.codegen_reachability_check(msg, span); + let (msg, reach_stmt) = gcx.codegen_reachability_check(msg, span); // Since `cond` might have side effects, assign it to a temporary // variable so that it's evaluated once, then assert and assume it // TODO: I don't think `cond` can have side effects, this is MIR, it's going to be temps - let (tmp, decl) = tcx.decl_temp_variable(cond.typ().clone(), Some(cond), caller_loc); + let (tmp, decl) = gcx.decl_temp_variable(cond.typ().clone(), Some(cond), caller_loc); Stmt::block( vec![ reach_stmt, decl, - tcx.codegen_assert_assume(tmp, PropertyClass::Assertion, &msg, caller_loc), - Stmt::goto(tcx.current_fn().find_label(&target), caller_loc), + gcx.codegen_assert_assume(tmp, PropertyClass::Assertion, &msg, caller_loc), + Stmt::goto(bb_label(target), caller_loc), ], caller_loc, ) @@ -160,34 +155,36 @@ impl<'tcx> GotocHook<'tcx> for Assert { struct Nondet; -impl<'tcx> GotocHook<'tcx> for Nondet { - fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { +impl GotocHook for Nondet { + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { matches_function(tcx, instance, "KaniAnyRaw") } fn handle( &self, - tcx: &mut GotocCtx<'tcx>, - _instance: Instance<'tcx>, + gcx: &mut GotocCtx, + _instance: Instance, fargs: Vec, - assign_to: Place<'tcx>, - target: Option, - span: Option, + assign_to: Place, + target: Option, + span: Span, ) -> Stmt { assert!(fargs.is_empty()); - let loc = tcx.codegen_span_option(span); + let loc = gcx.codegen_span_stable(span); let target = target.unwrap(); - let pt = tcx.place_ty(&assign_to); - if pt.is_unit() { - Stmt::goto(tcx.current_fn().find_label(&target), loc) + let pt = gcx.place_ty_stable(&assign_to); + if pt.kind().is_unit() { + Stmt::goto(bb_label(target), loc) } else { - let pe = - unwrap_or_return_codegen_unimplemented_stmt!(tcx, tcx.codegen_place(&assign_to)) - .goto_expr; + let pe = unwrap_or_return_codegen_unimplemented_stmt!( + gcx, + gcx.codegen_place_stable(&assign_to) + ) + .goto_expr; Stmt::block( vec![ - pe.assign(tcx.codegen_ty(pt).nondet(), loc), - Stmt::goto(tcx.current_fn().find_label(&target), loc), + pe.assign(gcx.codegen_ty_stable(pt).nondet(), loc), + Stmt::goto(bb_label(target), loc), ], loc, ) @@ -197,9 +194,9 @@ impl<'tcx> GotocHook<'tcx> for Nondet { struct Panic; -impl<'tcx> GotocHook<'tcx> for Panic { - fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { - let def_id = instance.def.def_id(); +impl GotocHook for Panic { + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { + let def_id = rustc_internal::internal(instance.def.def_id()); Some(def_id) == tcx.lang_items().panic_fn() || tcx.has_attr(def_id, rustc_span::sym::rustc_const_panic_str) || Some(def_id) == tcx.lang_items().panic_fmt() @@ -209,50 +206,53 @@ impl<'tcx> GotocHook<'tcx> for Panic { fn handle( &self, - tcx: &mut GotocCtx<'tcx>, - _instance: Instance<'tcx>, + gcx: &mut GotocCtx, + _instance: Instance, fargs: Vec, - _assign_to: Place<'tcx>, - _target: Option, - span: Option, + _assign_to: Place, + _target: Option, + span: Span, ) -> Stmt { - tcx.codegen_panic(span, fargs) + gcx.codegen_panic(span, fargs) } } struct RustAlloc; // Removing this hook causes regression failures. // https://github.com/model-checking/kani/issues/1170 -impl<'tcx> GotocHook<'tcx> for RustAlloc { - fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { - let full_name = with_no_trimmed_paths!(tcx.def_path_str(instance.def_id())); +impl GotocHook for RustAlloc { + fn hook_applies(&self, _tcx: TyCtxt, instance: Instance) -> bool { + let full_name = instance.name(); full_name == "alloc::alloc::exchange_malloc" } fn handle( &self, - tcx: &mut GotocCtx<'tcx>, - instance: Instance<'tcx>, + gcx: &mut GotocCtx, + instance: Instance, mut fargs: Vec, - assign_to: Place<'tcx>, - target: Option, - span: Option, + assign_to: Place, + target: Option, + span: Span, ) -> Stmt { debug!(?instance, "Replace allocation"); - let loc = tcx.codegen_span_option(span); + let loc = gcx.codegen_span_stable(span); let target = target.unwrap(); let size = fargs.remove(0); Stmt::block( vec![ - unwrap_or_return_codegen_unimplemented_stmt!(tcx, tcx.codegen_place(&assign_to)) - .goto_expr - .assign( - BuiltinFn::Malloc - .call(vec![size], loc) - .cast_to(Type::unsigned_int(8).to_pointer()), - loc, - ), - Stmt::goto(tcx.current_fn().find_label(&target), Location::none()), + unwrap_or_return_codegen_unimplemented_stmt!( + gcx, + gcx.codegen_place_stable(&assign_to) + ) + .goto_expr + .assign( + BuiltinFn::Malloc + .call(vec![size], loc) + .cast_to(Type::unsigned_int(8).to_pointer()), + loc, + ), + Stmt::goto(bb_label(target), Location::none()), ], Location::none(), ) @@ -271,30 +271,30 @@ impl<'tcx> GotocHook<'tcx> for RustAlloc { /// ``` pub struct MemCmp; -impl<'tcx> GotocHook<'tcx> for MemCmp { - fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { - let name = with_no_trimmed_paths!(tcx.def_path_str(instance.def_id())); +impl GotocHook for MemCmp { + fn hook_applies(&self, _tcx: TyCtxt, instance: Instance) -> bool { + let name = instance.name(); name == "core::slice::cmp::memcmp" || name == "std::slice::cmp::memcmp" } fn handle( &self, - tcx: &mut GotocCtx<'tcx>, - instance: Instance<'tcx>, + gcx: &mut GotocCtx, + instance: Instance, mut fargs: Vec, - assign_to: Place<'tcx>, - target: Option, - span: Option, + assign_to: Place, + target: Option, + span: Span, ) -> Stmt { - let loc = tcx.codegen_span_option(span); + let loc = gcx.codegen_span_stable(span); let target = target.unwrap(); let first = fargs.remove(0); let second = fargs.remove(0); let count = fargs.remove(0); - let (count_var, count_decl) = tcx.decl_temp_variable(count.typ().clone(), Some(count), loc); - let (first_var, first_decl) = tcx.decl_temp_variable(first.typ().clone(), Some(first), loc); + let (count_var, count_decl) = gcx.decl_temp_variable(count.typ().clone(), Some(count), loc); + let (first_var, first_decl) = gcx.decl_temp_variable(first.typ().clone(), Some(first), loc); let (second_var, second_decl) = - tcx.decl_temp_variable(second.typ().clone(), Some(second), loc); + gcx.decl_temp_variable(second.typ().clone(), Some(second), loc); let is_count_zero = count_var.clone().is_zero(); // We have to ensure that the pointers are valid even if we're comparing zero bytes. // According to Rust's current definition (see https://github.com/model-checking/kani/issues/1489), @@ -304,22 +304,16 @@ impl<'tcx> GotocHook<'tcx> for MemCmp { let is_second_ok = second_var.clone().is_nonnull(); let should_skip_pointer_checks = is_count_zero.and(is_first_ok).and(is_second_ok); let place_expr = - unwrap_or_return_codegen_unimplemented_stmt!(tcx, tcx.codegen_place(&assign_to)) + unwrap_or_return_codegen_unimplemented_stmt!(gcx, gcx.codegen_place_stable(&assign_to)) .goto_expr; let rhs = should_skip_pointer_checks.ternary( Expr::int_constant(0, place_expr.typ().clone()), // zero bytes are always equal (as long as pointers are nonnull and aligned) - tcx.codegen_func_expr(instance, span.as_ref()) + gcx.codegen_func_expr_stable(instance, span) .call(vec![first_var, second_var, count_var]), ); let code = place_expr.assign(rhs, loc).with_location(loc); Stmt::block( - vec![ - count_decl, - first_decl, - second_decl, - code, - Stmt::goto(tcx.current_fn().find_label(&target), loc), - ], + vec![count_decl, first_decl, second_decl, code, Stmt::goto(bb_label(target), loc)], loc, ) } @@ -334,19 +328,19 @@ impl<'tcx> GotocHook<'tcx> for MemCmp { /// contracts where we can structurally guarantee the use is safe. struct UntrackedDeref; -impl<'tcx> GotocHook<'tcx> for UntrackedDeref { - fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { +impl GotocHook for UntrackedDeref { + fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool { matches_function(tcx, instance, "KaniUntrackedDeref") } fn handle( &self, - tcx: &mut GotocCtx<'tcx>, - _instance: Instance<'tcx>, + gcx: &mut GotocCtx, + _instance: Instance, mut fargs: Vec, - assign_to: Place<'tcx>, - _target: Option, - span: Option, + assign_to: Place, + _target: Option, + span: Span, ) -> Stmt { assert_eq!( fargs.len(), @@ -355,11 +349,14 @@ impl<'tcx> GotocHook<'tcx> for UntrackedDeref { This function should only be called from code generated by kani macros, \ as such this is likely a code-generation error." ); - let loc = tcx.codegen_span_option(span); + let loc = gcx.codegen_span_stable(span); Stmt::block( vec![Stmt::assign( - unwrap_or_return_codegen_unimplemented_stmt!(tcx, tcx.codegen_place(&assign_to)) - .goto_expr, + unwrap_or_return_codegen_unimplemented_stmt!( + gcx, + gcx.codegen_place_stable(&assign_to) + ) + .goto_expr, fargs.pop().unwrap().dereference(), loc, )], @@ -368,7 +365,7 @@ impl<'tcx> GotocHook<'tcx> for UntrackedDeref { } } -pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> { +pub fn fn_hooks() -> GotocHooks { GotocHooks { hooks: vec![ Rc::new(Panic), @@ -383,16 +380,12 @@ pub fn fn_hooks<'tcx>() -> GotocHooks<'tcx> { } } -pub struct GotocHooks<'tcx> { - hooks: Vec + 'tcx>>, +pub struct GotocHooks { + hooks: Vec>, } -impl<'tcx> GotocHooks<'tcx> { - pub fn hook_applies( - &self, - tcx: TyCtxt<'tcx>, - instance: Instance<'tcx>, - ) -> Option + 'tcx>> { +impl GotocHooks { + pub fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> Option> { for h in &self.hooks { if h.hook_applies(tcx, instance) { return Some(h.clone()); diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs index f565c6b869f9..413d1cb12ca6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs @@ -6,7 +6,7 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{Expr, ExprValue, Location, SymbolTable, Type}; use cbmc::{btree_string_map, InternedString}; use rustc_middle::ty::layout::LayoutOf; -use rustc_middle::ty::{Instance, Ty}; +use rustc_middle::ty::Ty; use tracing::debug; // Should move into rvalue @@ -86,13 +86,6 @@ impl<'tcx> GotocCtx<'tcx> { /// Members traverse path to get to the raw pointer of a box (b.0.pointer.pointer). const RAW_PTR_FROM_BOX: [&str; 3] = ["0", "pointer", "pointer"]; -impl<'tcx> GotocCtx<'tcx> { - /// Given an "instance" find the crate it came from - pub fn get_crate(&self, instance: Instance<'tcx>) -> String { - self.tcx.crate_name(instance.def_id().krate).to_string() - } -} - impl<'tcx> GotocCtx<'tcx> { /// Dereference a boxed type `std::boxed::Box` to get a `*T`. ///