From 47c2155243d399df2923437b68b541c3cd096557 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 18 Dec 2023 22:31:56 +0000 Subject: [PATCH] Migrate function, block and statement modules to StableMIR (#2947) Migrate these modules to use StableMIR except for calls that depend on the function signature and ABI. Note that we shouldn't really be using function signature as captured here: https://github.com/model-checking/kani/issues/1365. So I suggest that we move to using the FnAbi as soon as we add that to StableMIR. --------- Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- .../codegen_cprover_gotoc/codegen/assert.rs | 5 +- .../codegen_cprover_gotoc/codegen/block.rs | 21 +- .../codegen/foreign_function.rs | 2 +- .../codegen_cprover_gotoc/codegen/function.rs | 163 ++++---- .../codegen/intrinsic.rs | 5 +- .../codegen_cprover_gotoc/codegen/operand.rs | 22 +- .../codegen_cprover_gotoc/codegen/place.rs | 16 +- .../codegen_cprover_gotoc/codegen/rvalue.rs | 19 +- .../src/codegen_cprover_gotoc/codegen/span.rs | 15 - .../codegen/statement.rs | 379 ++++++++---------- .../codegen/ty_stable.rs | 120 ++---- .../src/codegen_cprover_gotoc/codegen/typ.rs | 61 +-- .../compiler_interface.rs | 28 +- .../context/current_fn.rs | 56 +-- .../codegen_cprover_gotoc/context/goto_ctx.rs | 9 +- .../codegen_cprover_gotoc/overrides/hooks.rs | 28 +- .../src/codegen_cprover_gotoc/utils/debug.rs | 30 +- .../src/codegen_cprover_gotoc/utils/names.rs | 16 +- kani-compiler/src/kani_middle/mod.rs | 2 + rust-toolchain.toml | 2 +- 20 files changed, 408 insertions(+), 591 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 2658b75812a7..68573cd2a1cd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -21,7 +21,6 @@ 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}; @@ -149,8 +148,8 @@ impl<'tcx> GotocCtx<'tcx> { } /// Generate a cover statement for code coverage reports. - pub fn codegen_coverage(&self, span: Span) -> Stmt { - let loc = self.codegen_caller_span(&span); + pub fn codegen_coverage(&self, 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 diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs index 11cdf47f4ed2..692fdb9c385b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs @@ -2,8 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::codegen_cprover_gotoc::GotocCtx; -use rustc_middle::mir::{BasicBlock, BasicBlockData}; -use stable_mir::mir::BasicBlockIdx; +use stable_mir::mir::{BasicBlock, BasicBlockIdx}; use tracing::debug; pub fn bb_label(bb: BasicBlockIdx) -> String { @@ -17,20 +16,20 @@ impl<'tcx> GotocCtx<'tcx> { /// /// This function does not return a value, but mutates state with /// `self.current_fn_mut().push_onto_block(...)` - pub fn codegen_block(&mut self, bb: BasicBlock, bbd: &BasicBlockData<'tcx>) { - debug!(?bb, "Codegen basicblock"); - let label: String = self.current_fn().find_label(&bb); + pub fn codegen_block(&mut self, bb: BasicBlockIdx, bbd: &BasicBlock) { + debug!(?bb, "codegen_block"); + let label = bb_label(bb); let check_coverage = self.queries.args().check_coverage; // the first statement should be labelled. if there is no statements, then the // terminator should be labelled. match bbd.statements.len() { 0 => { - let term = bbd.terminator(); + let term = &bbd.terminator; let tcode = self.codegen_terminator(term); // When checking coverage, the `coverage` check should be // labelled instead. if check_coverage { - let span = term.source_info.span; + let span = term.span; let cover = self.codegen_coverage(span); self.current_fn_mut().push_onto_block(cover.with_label(label)); self.current_fn_mut().push_onto_block(tcode); @@ -44,7 +43,7 @@ impl<'tcx> GotocCtx<'tcx> { // When checking coverage, the `coverage` check should be // labelled instead. if check_coverage { - let span = stmt.source_info.span; + let span = stmt.span; let cover = self.codegen_coverage(span); self.current_fn_mut().push_onto_block(cover.with_label(label)); self.current_fn_mut().push_onto_block(scode); @@ -54,16 +53,16 @@ impl<'tcx> GotocCtx<'tcx> { for s in &bbd.statements[1..] { if check_coverage { - let span = s.source_info.span; + let span = s.span; let cover = self.codegen_coverage(span); self.current_fn_mut().push_onto_block(cover); } let stmt = self.codegen_statement(s); self.current_fn_mut().push_onto_block(stmt); } - let term = bbd.terminator(); + let term = &bbd.terminator; if check_coverage { - let span = term.source_info.span; + let span = term.span; let cover = self.codegen_coverage(span); self.current_fn_mut().push_onto_block(cover); } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs index 617eeb8af506..22546be18909 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -137,7 +137,7 @@ impl<'tcx> GotocCtx<'tcx> { /// /// This will behave like `codegen_unimplemented_stmt` but print a message that includes /// the name of the function not supported and the calling convention. - pub fn codegen_ffi_unsupported(&mut self, instance: Instance<'tcx>, loc: Location) -> Stmt { + fn codegen_ffi_unsupported(&mut self, instance: Instance<'tcx>, loc: Location) -> Stmt { let fn_name = &self.symbol_name(instance); debug!(?fn_name, ?loc, "codegen_ffi_unsupported"); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index f3d79c7f06c5..52bf778ab235 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -7,96 +7,85 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{Expr, Stmt, Symbol}; use cbmc::InternString; use rustc_middle::mir::traversal::reverse_postorder; -use rustc_middle::mir::{Body, HasLocalDecls, Local}; -use rustc_middle::ty::{self, Instance}; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::{Body, Local}; +use stable_mir::ty::{RigidTy, TyKind}; +use stable_mir::CrateDef; use std::collections::BTreeMap; use std::iter::FromIterator; use tracing::{debug, debug_span}; /// Codegen MIR functions into gotoc impl<'tcx> GotocCtx<'tcx> { - /// Get the number of parameters that the current function expects. - fn get_params_size(&self) -> usize { - let sig = self.current_fn().sig(); - let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig); - // we don't call [codegen_function_sig] because we want to get a bit more metainformation. - sig.inputs().len() - } - /// Declare variables according to their index. /// - Index 0 represents the return value. /// - 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().body_internal(); - let ldecls = mir.local_decls(); - let num_args = self.get_params_size(); - ldecls.indices().enumerate().for_each(|(idx, lc)| { - if Some(lc) == mir.spread_arg { + fn codegen_declare_variables(&mut self, body: &Body) { + let ldecls = body.local_decls(); + let num_args = body.arg_locals().len(); + for (lc, ldata) in ldecls { + if Some(lc) == body.spread_arg() { // We have already added this local in the function prelude, so // skip adding it again here. - return; + continue; } let base_name = self.codegen_var_base_name(&lc); let name = self.codegen_var_name(&lc); - let ldata = &ldecls[lc]; - let var_ty = self.monomorphize(ldata.ty); - let var_type = self.codegen_ty(var_ty); - let loc = self.codegen_span(&ldata.source_info.span); + let var_type = self.codegen_ty_stable(ldata.ty); + let loc = self.codegen_span_stable(ldata.span); // Indices [1, N] represent the function parameters where N is the number of parameters. // Except that ZST fields are not included as parameters. - let sym = Symbol::variable( - name, - base_name, - var_type, - self.codegen_span(&ldata.source_info.span), - ) - .with_is_hidden(!self.is_user_variable(&lc)) - .with_is_parameter((idx > 0 && idx <= num_args) && !self.is_zst(var_ty)); + let sym = + Symbol::variable(name, base_name, var_type, self.codegen_span_stable(ldata.span)) + .with_is_hidden(!self.is_user_variable(&lc)) + .with_is_parameter((lc > 0 && lc <= num_args) && !self.is_zst_stable(ldata.ty)); let sym_e = sym.to_expr(); self.symbol_table.insert(sym); // Index 0 represents the return value, which does not need to be // declared in the first block - if lc.index() < 1 || lc.index() > mir.arg_count { + if lc < 1 || lc > body.arg_locals().len() { let init = self.codegen_default_initializer(&sym_e); self.current_fn_mut().push_onto_block(Stmt::decl(sym_e, init, loc)); } - }); + } } - pub fn codegen_function(&mut self, instance: Instance<'tcx>) { - self.set_current_fn(instance); - let name = self.current_fn().name(); + pub fn codegen_function(&mut self, instance: Instance) { + let name = self.symbol_name_stable(instance); let old_sym = self.symbol_table.lookup(&name).unwrap(); - let _trace_span = - debug_span!("CodegenFunction", name = self.current_fn().readable_name()).entered(); + let _trace_span = debug_span!("CodegenFunction", name = instance.name()).entered(); if old_sym.is_function_definition() { debug!("Double codegen of {:?}", old_sym); } else { assert!(old_sym.is_function()); - let mir = self.current_fn().body_internal(); - self.print_instance(instance, mir); - self.codegen_function_prelude(); - self.codegen_declare_variables(); - - reverse_postorder(mir).for_each(|(bb, bbd)| self.codegen_block(bb, bbd)); - - let loc = self.codegen_span(&mir.span); + let body = instance.body().unwrap(); + self.set_current_fn(instance, &body); + self.print_instance(instance, &body); + self.codegen_function_prelude(&body); + self.codegen_declare_variables(&body); + + // Get the order from internal body for now. + let internal_body = self.current_fn().body_internal(); + reverse_postorder(internal_body) + .for_each(|(bb, _)| self.codegen_block(bb.index(), &body.blocks[bb.index()])); + + let loc = self.codegen_span_stable(instance.def.span()); let stmts = self.current_fn_mut().extract_block(); - let body = Stmt::block(stmts, loc); - self.symbol_table.update_fn_declaration_with_definition(&name, body); + let goto_body = Stmt::block(stmts, loc); + self.symbol_table.update_fn_declaration_with_definition(&name, goto_body); + self.reset_current_fn(); } - self.reset_current_fn(); } /// 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().body_internal(); - if let Some(spread_arg) = mir.spread_arg { - self.codegen_spread_arg(mir, spread_arg); + fn codegen_function_prelude(&mut self, body: &Body) { + debug!(spread_arg=?body.spread_arg(), "codegen_function_prelude"); + if let Some(spread_arg) = body.spread_arg() { + self.codegen_spread_arg(body, spread_arg); } } @@ -117,34 +106,27 @@ impl<'tcx> GotocCtx<'tcx> { /// /// See: /// - fn codegen_spread_arg(&mut self, mir: &Body<'tcx>, spread_arg: Local) { - tracing::debug!(current=?self.current_fn, "codegen_spread_arg"); - let spread_data = &mir.local_decls()[spread_arg]; - let tup_ty = self.monomorphize(spread_data.ty); - if self.is_zst(tup_ty) { + fn codegen_spread_arg(&mut self, body: &Body, spread_arg: Local) { + debug!(current=?self.current_fn().name(), "codegen_spread_arg"); + let spread_data = &body.locals()[spread_arg]; + let tup_ty = spread_data.ty; + if self.is_zst_stable(tup_ty) { // No need to spread a ZST since it will be ignored. return; } - let loc = self.codegen_span(&spread_data.source_info.span); + let loc = self.codegen_span_stable(spread_data.span); // Get the function signature from MIR, _before_ we untuple - let fntyp = self.current_fn().instance().ty(self.tcx, ty::ParamEnv::reveal_all()); - let sig = match fntyp.kind() { - ty::FnPtr(..) | ty::FnDef(..) => fntyp.fn_sig(self.tcx).skip_binder(), - // Closures themselves will have their arguments already untupled, - // see Zulip link above. - ty::Closure(..) => unreachable!( - "Unexpected `spread arg` set for closure, got: {:?}, {:?}", - fntyp, - self.current_fn().readable_name() - ), - _ => unreachable!( - "Expected function type for `spread arg` prelude, got: {:?}, {:?}", - fntyp, - self.current_fn().readable_name() - ), - }; + let instance = self.current_fn().instance_stable(); + // Closures themselves will have their arguments already untupled, + // see Zulip link above. + assert!( + !instance.ty().kind().is_closure(), + "Unexpected spread arg `{}` set for closure `{}`", + spread_arg, + instance.name() + ); // When we codegen the function signature elsewhere, we will codegen the untupled version. // We then marshall the arguments into a local variable holding the expected tuple. @@ -166,7 +148,7 @@ impl<'tcx> GotocCtx<'tcx> { // }; // ``` // Note how the compiler has reordered the fields to improve packing. - let tup_type = self.codegen_ty(tup_ty); + let tup_type = self.codegen_ty_stable(tup_ty); // We need to marshall the arguments into the tuple // The arguments themselves have been tacked onto the explicit function paramaters by @@ -185,21 +167,19 @@ impl<'tcx> GotocCtx<'tcx> { // } // ``` - let tupe = sig.inputs().last().unwrap(); - let args = match tupe.kind() { - ty::Tuple(args) => *args, - _ => unreachable!("a function's spread argument must be a tuple"), + let TyKind::RigidTy(RigidTy::Tuple(args)) = tup_ty.kind() else { + unreachable!("a function's spread argument must be a tuple") }; - let starting_idx = sig.inputs().len(); + let starting_idx = spread_arg; let marshalled_tuple_fields = BTreeMap::from_iter(args.iter().enumerate().map(|(arg_i, arg_t)| { // The components come at the end, so offset by the untupled length. // This follows the naming convention defined in `typ.rs`. - let lc = Local::from_usize(arg_i + starting_idx); + let lc = arg_i + starting_idx; let (name, base_name) = self.codegen_spread_arg_name(&lc); - let sym = Symbol::variable(name, base_name, self.codegen_ty(arg_t), loc) + let sym = Symbol::variable(name, base_name, self.codegen_ty_stable(*arg_t), loc) .with_is_hidden(false) - .with_is_parameter(!self.is_zst(arg_t)); + .with_is_parameter(!self.is_zst_stable(*arg_t)); // The spread arguments are additional function paramaters that are patched in // They are to the function signature added in the `fn_typ` function. // But they were never added to the symbol table, which we currently do here. @@ -222,19 +202,18 @@ impl<'tcx> GotocCtx<'tcx> { ); } - pub fn declare_function(&mut self, instance: Instance<'tcx>) { - debug!("declaring {}; {:?}", instance, instance); - self.set_current_fn(instance); - 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().body_internal(); + pub fn declare_function(&mut self, instance: Instance) { + debug!("declaring {}; {:?}", instance.name(), instance); + let body = instance.body().unwrap(); + self.set_current_fn(instance, &body); + debug!(krate=?instance.def.krate(), is_std=self.current_fn().is_std(), "declare_function"); + self.ensure(&self.symbol_name_stable(instance), |ctx, fname| { Symbol::function( fname, - ctx.fn_typ(), + ctx.fn_typ(&body), None, - ctx.current_fn().readable_name(), - ctx.codegen_span(&mir.span), + instance.name(), + ctx.codegen_span_stable(instance.def.span()), ) }); self.reset_current_fn(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 8869b01bc65a..fa23b85c18f1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -138,7 +138,7 @@ impl<'tcx> GotocCtx<'tcx> { debug!(?fargs, "codegen_intrinsic"); debug!(?place, "codegen_intrinsic"); debug!(?span, "codegen_intrinsic"); - let sig = instance.fn_sig(); + let sig = instance.ty().kind().fn_sig().unwrap().skip_binder(); let ret_ty = sig.output(); let farg_types = sig.inputs(); let cbmc_ret_ty = self.codegen_ty_stable(ret_ty); @@ -414,7 +414,8 @@ impl<'tcx> GotocCtx<'tcx> { "cttz" => codegen_count_intrinsic!(cttz, true), "cttz_nonzero" => codegen_count_intrinsic!(cttz, false), "discriminant_value" => { - let ty = pointee_type_stable(instance.fn_sig().inputs()[0]).unwrap(); + let sig = instance.ty().kind().fn_sig().unwrap().skip_binder(); + let ty = pointee_type_stable(sig.inputs()[0]).unwrap(); let e = self.codegen_get_discriminant(fargs.remove(0).dereference(), ty, ret_ty); self.codegen_expr_to_place_stable(place, e) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 148318f1c33e..aaec506edf6e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -1,12 +1,10 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -use crate::codegen_cprover_gotoc::codegen::ty_stable::StableConverter; use crate::codegen_cprover_gotoc::utils::slice_fat_ptr; use crate::codegen_cprover_gotoc::GotocCtx; use crate::unwrap_or_return_codegen_unimplemented; use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Stmt, Symbol, Type}; -use rustc_middle::mir::Operand as OperandInternal; -use rustc_middle::ty::{Const as ConstInternal, Instance as InstanceInternal}; +use rustc_middle::ty::Const as ConstInternal; use rustc_smir::rustc_internal; use rustc_span::Span as SpanInternal; use stable_mir::mir::alloc::{AllocId, GlobalAlloc}; @@ -34,10 +32,6 @@ impl<'tcx> GotocCtx<'tcx> { /// A MIR operand is either a constant (literal or `const` declaration) or a place /// (being moved or copied for this operation). /// An "operand" in MIR is the argument to an "Rvalue" (and is also used by some statements.) - pub fn codegen_operand(&mut self, operand: &OperandInternal<'tcx>) -> Expr { - self.codegen_operand_stable(&StableConverter::convert_operand(self, operand.clone())) - } - pub fn codegen_operand_stable(&mut self, operand: &Operand) -> Expr { trace!(?operand, "codegen_operand"); match operand { @@ -67,7 +61,7 @@ impl<'tcx> GotocCtx<'tcx> { constant: ConstInternal<'tcx>, span: Option, ) -> Expr { - let stable_const = StableConverter::convert_constant(self, constant); + let stable_const = rustc_internal::stable(constant); let stable_span = rustc_internal::stable(span); self.codegen_const(&stable_const, stable_span) } @@ -586,7 +580,7 @@ impl<'tcx> GotocCtx<'tcx> { /// sometimes subtly differs from the type that codegen_function_sig returns. /// This is tracked in . fn codegen_func_symbol(&mut self, instance: Instance) -> (&Symbol, Type) { - let funct = self.codegen_function_sig(self.fn_sig_of_instance_stable(instance)); + let funct = self.codegen_function_sig_stable(self.fn_sig_of_instance_stable(instance)); let sym = if instance.is_foreign_item() { // Get the symbol that represents a foreign instance. self.codegen_foreign_fn(instance) @@ -606,16 +600,6 @@ impl<'tcx> GotocCtx<'tcx> { /// Note: In general with this `Expr` you should immediately either `.address_of()` or `.call(...)`. /// /// This should not be used where Rust expects a "function item" (See `codegen_fn_item`) - pub fn codegen_func_expr_internal( - &mut self, - instance: InstanceInternal<'tcx>, - span: Option<&SpanInternal>, - ) -> Expr { - let (func_symbol, func_typ) = self.codegen_func_symbol(rustc_internal::stable(instance)); - Expr::symbol_expression(func_symbol.name, func_typ) - .with_location(self.codegen_span_option(span.cloned())) - } - pub fn codegen_func_expr(&mut self, instance: Instance, span: Option) -> Expr { let (func_symbol, func_typ) = self.codegen_func_symbol(instance); Expr::symbol_expression(func_symbol.name, func_typ) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 75f184660765..fd9ff33e164e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -6,13 +6,12 @@ //! 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::ty_stable::pointee_type; 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; use cbmc::goto_program::{Expr, Location, Type}; -use rustc_middle::mir::{Local as LocalInternal, Place as PlaceInternal}; use rustc_middle::ty::layout::LayoutOf; use rustc_smir::rustc_internal; use rustc_target::abi::{TagEncoding, Variants}; @@ -390,7 +389,7 @@ impl<'tcx> GotocCtx<'tcx> { } // Otherwise, simply look up the local by the var name. - let vname = self.codegen_var_name(&LocalInternal::from(l)); + let vname = self.codegen_var_name(&l); Expr::symbol_expression(vname, self.codegen_ty_stable(local_ty)) } @@ -637,10 +636,6 @@ 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: &PlaceInternal<'tcx>) -> Expr { - 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 = @@ -698,13 +693,6 @@ impl<'tcx> GotocCtx<'tcx> { } } - 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, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 71c8e97420b8..c4ea258fe79e 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 crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace; -use crate::codegen_cprover_gotoc::codegen::ty_stable::{pointee_type_stable, StableConverter}; +use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable; 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}; @@ -17,7 +17,6 @@ use cbmc::goto_program::{ use cbmc::MachineModel; use cbmc::{btree_string_map, InternString, InternedString}; use num::bigint::BigInt; -use rustc_middle::mir::Rvalue as RvalueInternal; use rustc_middle::ty::{TyCtxt, VtblEntry}; use rustc_smir::rustc_internal; use rustc_target::abi::{FieldsShape, TagEncoding, Variants}; @@ -583,12 +582,8 @@ impl<'tcx> GotocCtx<'tcx> { stmts.push(assign_case); } // 3- Set discriminant. - let set_discriminant = self.codegen_set_discriminant( - rustc_internal::internal(res_ty), - temp_var.clone(), - rustc_internal::internal(variant_index), - loc, - ); + let set_discriminant = + self.codegen_set_discriminant(res_ty, temp_var.clone(), variant_index, loc); stmts.push(set_discriminant); // 4- Return temporary variable. stmts.push(temp_var.as_stmt(loc)); @@ -668,10 +663,6 @@ impl<'tcx> GotocCtx<'tcx> { } } - pub fn codegen_rvalue(&mut self, rv: &RvalueInternal<'tcx>, loc: Location) -> Expr { - self.codegen_rvalue_stable(&StableConverter::convert_rvalue(self, rv.clone()), loc) - } - pub fn codegen_rvalue_stable(&mut self, rv: &Rvalue, loc: Location) -> Expr { let res_ty = self.rvalue_ty_stable(rv); debug!(?rv, ?res_ty, "codegen_rvalue"); @@ -831,8 +822,8 @@ impl<'tcx> GotocCtx<'tcx> { // // Note: niche_variants can only represent values that fit in a u32. let result_type = self.codegen_ty_stable(res_ty); - let discr_mir_ty = self.codegen_enum_discr_typ(rustc_internal::internal(ty)); - let discr_type = self.codegen_ty(discr_mir_ty); + let discr_mir_ty = self.codegen_enum_discr_typ_stable(ty); + let discr_type = self.codegen_ty_stable(discr_mir_ty); let niche_val = self.codegen_get_niche(e, offset.bytes() as usize, discr_type); let relative_discr = wrapping_sub(&niche_val, u64::try_from(*niche_start).unwrap()); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index 9e81ffa57898..c06d64d298c4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs @@ -5,10 +5,8 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Location; -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> { @@ -44,17 +42,4 @@ impl<'tcx> GotocCtx<'tcx> { let topmost = span.ctxt().outer_expn().expansion_cause().unwrap_or(*span); self.codegen_span(&topmost) } - - pub fn codegen_span_option(&self, sp: Option) -> Location { - sp.map_or(Location::none(), |x| self.codegen_span(&x)) - } - - pub fn find_debug_info(&self, l: &Local) -> Option { - 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 9034b6a37783..e7b7ee5a376a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -2,24 +2,19 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use super::typ::TypeExt; use super::typ::FN_RETURN_VOID_VAR_NAME; -use super::PropertyClass; -use crate::codegen_cprover_gotoc::codegen::ty_stable::StableConverter; +use super::{bb_label, PropertyClass}; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{Expr, Location, Stmt, Type}; -use rustc_middle::mir; -use rustc_middle::mir::{ - AssertKind, BasicBlock, NonDivergingIntrinsic, Operand, Place, Statement, StatementKind, - SwitchTargets, Terminator, TerminatorKind, -}; -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}; -use stable_mir::mir::{Operand as OperandStable, Place as PlaceStable}; +use stable_mir::mir::mono::{Instance, InstanceKind}; +use stable_mir::mir::{ + AssertMessage, BasicBlockIdx, CopyNonOverlapping, NonDivergingIntrinsic, Operand, Place, + Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, RETURN_LOCAL, +}; +use stable_mir::ty::{RigidTy, Span, Ty, TyKind, VariantIdx}; use tracing::{debug, debug_span, trace}; impl<'tcx> GotocCtx<'tcx> { @@ -28,57 +23,70 @@ impl<'tcx> GotocCtx<'tcx> { /// statements and [Terminator]s, which can exclusively appear at the end of a basic block. /// /// See [GotocCtx::codegen_terminator] for those. - pub fn codegen_statement(&mut self, stmt: &Statement<'tcx>) -> Stmt { + pub fn codegen_statement(&mut self, stmt: &Statement) -> Stmt { let _trace_span = debug_span!("CodegenStatement", statement = ?stmt).entered(); debug!(?stmt, kind=?stmt.kind, "handling_statement"); - let location = self.codegen_span(&stmt.source_info.span); + let location = self.codegen_span_stable(stmt.span); match &stmt.kind { - StatementKind::Assign(box (l, r)) => { - let lty = self.place_ty(l); - let rty = self.rvalue_ty(r); + StatementKind::Assign(lhs, rhs) => { + let lty = self.place_ty_stable(lhs); + let rty = self.rvalue_ty_stable(rhs); // we ignore assignment for all zero size types - if self.is_zst(lty) { + if self.is_zst_stable(lty) { Stmt::skip(location) - } else if lty.is_fn_ptr() && rty.is_fn() && !rty.is_fn_ptr() { + } else if lty.kind().is_fn_ptr() && rty.kind().is_fn() && !rty.kind().is_fn_ptr() { // implicit address of a function pointer, e.g. // let fp: fn() -> i32 = foo; // where the reference is implicit. - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) - .goto_expr - .assign(self.codegen_rvalue(r, location).address_of(), location) - } else if rty.is_bool() { - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) - .goto_expr - .assign(self.codegen_rvalue(r, location).cast_to(Type::c_bool()), location) + unwrap_or_return_codegen_unimplemented_stmt!( + self, + self.codegen_place_stable(lhs) + ) + .goto_expr + .assign(self.codegen_rvalue_stable(rhs, location).address_of(), location) + } else if rty.kind().is_bool() { + unwrap_or_return_codegen_unimplemented_stmt!( + self, + self.codegen_place_stable(lhs) + ) + .goto_expr + .assign( + self.codegen_rvalue_stable(rhs, location).cast_to(Type::c_bool()), + location, + ) } else { - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) - .goto_expr - .assign(self.codegen_rvalue(r, location), location) + unwrap_or_return_codegen_unimplemented_stmt!( + self, + self.codegen_place_stable(lhs) + ) + .goto_expr + .assign(self.codegen_rvalue_stable(rhs, location), location) } } StatementKind::Deinit(place) => self.codegen_deinit(place, location), StatementKind::SetDiscriminant { place, variant_index } => { - let dest_ty = self.place_ty(place); - let dest_expr = - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place)) - .goto_expr; + let dest_ty = self.place_ty_stable(place); + let dest_expr = unwrap_or_return_codegen_unimplemented_stmt!( + self, + self.codegen_place_stable(place) + ) + .goto_expr; self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location) } StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me - StatementKind::Intrinsic(box NonDivergingIntrinsic::CopyNonOverlapping( - mir::CopyNonOverlapping { ref src, ref dst, ref count }, + StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping( + CopyNonOverlapping { src, dst, count }, )) => { - let operands = - [src, dst, count].map(|op| StableConverter::convert_operand(self, op.clone())); + let operands = [src, dst, count]; // Pack the operands and their types, then call `codegen_copy` let fargs = operands.iter().map(|op| self.codegen_operand_stable(op)).collect::>(); let farg_types = operands.map(|op| self.operand_ty_stable(&op)); self.codegen_copy("copy_nonoverlapping", true, fargs, &farg_types, None, location) } - StatementKind::Intrinsic(box NonDivergingIntrinsic::Assume(ref op)) => { - let cond = self.codegen_operand(op).cast_to(Type::bool()); + StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(ref op)) => { + let cond = self.codegen_operand_stable(op).cast_to(Type::bool()); self.codegen_assert_assume( cond, PropertyClass::Assume, @@ -87,9 +95,9 @@ impl<'tcx> GotocCtx<'tcx> { ) } StatementKind::PlaceMention(_) => todo!(), - StatementKind::FakeRead(_) + StatementKind::FakeRead(..) | StatementKind::Retag(_, _) - | StatementKind::AscribeUserType(_, _) + | StatementKind::AscribeUserType { .. } | StatementKind::Nop | StatementKind::Coverage { .. } | StatementKind::ConstEvalCounter => Stmt::skip(location), @@ -102,15 +110,13 @@ impl<'tcx> GotocCtx<'tcx> { /// because of the need for unwinding/drop. For instance, function calls. /// /// See also [`GotocCtx::codegen_statement`] for ordinary [Statement]s. - pub fn codegen_terminator(&mut self, term: &Terminator<'tcx>) -> Stmt { - let loc = self.codegen_span(&term.source_info.span); + pub fn codegen_terminator(&mut self, term: &Terminator) -> Stmt { + let loc = self.codegen_span_stable(term.span); let _trace_span = debug_span!("CodegenTerminator", statement = ?term.kind).entered(); debug!("handling terminator {:?}", term); //TODO: Instead of doing location::none(), and updating, just putit in when we make the stmt. match &term.kind { - TerminatorKind::Goto { target } => { - Stmt::goto(self.current_fn().find_label(target), loc) - } + TerminatorKind::Goto { target } => Stmt::goto(bb_label(*target), loc), TerminatorKind::SwitchInt { discr, targets } => { self.codegen_switch_int(discr, targets, loc) } @@ -118,29 +124,31 @@ impl<'tcx> GotocCtx<'tcx> { // because we don't want to raise the warning during compilation. // These operations will normally be codegen'd but normally be unreachable // since we make use of `-C unwind=abort`. - TerminatorKind::UnwindResume => self.codegen_mimic_unimplemented( + TerminatorKind::Resume => self.codegen_mimic_unimplemented( "TerminatorKind::Resume", loc, "https://github.com/model-checking/kani/issues/692", ), - TerminatorKind::UnwindTerminate(_) => self.codegen_mimic_unimplemented( - "TerminatorKind::UnwindTerminate", + TerminatorKind::Abort => self.codegen_mimic_unimplemented( + "TerminatorKind::Abort", loc, "https://github.com/model-checking/kani/issues/692", ), TerminatorKind::Return => { - let rty = self.current_fn().sig().skip_binder().output(); - if rty.is_unit() { + let rty = self.current_fn().sig().output(); + if rty.kind().is_unit() { self.codegen_ret_unit() } else { - let p = Place::from(mir::RETURN_PLACE); - let v = - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(&p)) - .goto_expr; - if self.place_ty(&p).is_bool() { - v.cast_to(Type::c_bool()).ret(loc) + let place = Place::from(RETURN_LOCAL); + let place_expr = unwrap_or_return_codegen_unimplemented_stmt!( + self, + self.codegen_place_stable(&place) + ) + .goto_expr; + if self.place_ty_stable(&place).kind().is_bool() { + place_expr.cast_to(Type::c_bool()).ret(loc) } else { - v.ret(loc) + place_expr.ret(loc) } } } @@ -149,36 +157,35 @@ impl<'tcx> GotocCtx<'tcx> { "unreachable code", loc, ), - TerminatorKind::Drop { place, target, unwind: _, replace: _ } => { + TerminatorKind::Drop { place, target, unwind: _ } => { self.codegen_drop(place, target, loc) } TerminatorKind::Call { func, args, destination, target, .. } => { - self.codegen_funcall(func, args, destination, target, term.source_info.span) + self.codegen_funcall(func, args, destination, target, term.span) } TerminatorKind::Assert { cond, expected, msg, target, .. } => { let cond = { - let r = self.codegen_operand(cond); + let r = self.codegen_operand_stable(cond); if *expected { r } else { Expr::not(r) } }; - let msg = if let AssertKind::BoundsCheck { .. } = &**msg { + let msg = if let AssertMessage::BoundsCheck { .. } = msg { // For bounds check the following panic message is generated at runtime: // "index out of bounds: the length is {len} but the index is {index}", // but CBMC only accepts static messages so we don't add values to the message. "index out of bounds: the length is less than or equal to the given index" - } else if let AssertKind::MisalignedPointerDereference { .. } = &**msg { + } else if let AssertMessage::MisalignedPointerDereference { .. } = msg { // Misaligned pointer dereference check messages is also a runtime messages. // Generate a generic one here. - "misaligned pointer dereference: address must be a multiple of its type's alignment" + "misaligned pointer dereference: address must be a multiple of its type's \ + alignment" } else { // For all other assert kind we can get the static message. - msg.description() + msg.description().unwrap() }; - let (msg_str, reach_stmt) = self.codegen_reachability_check( - msg.to_owned(), - rustc_internal::stable(term.source_info.span), - ); + let (msg_str, reach_stmt) = + self.codegen_reachability_check(msg.to_owned(), term.span); Stmt::block( vec![ @@ -189,17 +196,11 @@ impl<'tcx> GotocCtx<'tcx> { &msg_str, loc, ), - Stmt::goto(self.current_fn().find_label(target), loc), + Stmt::goto(bb_label(*target), loc), ], loc, ) } - TerminatorKind::FalseEdge { .. } | TerminatorKind::FalseUnwind { .. } => { - unreachable!("drop elaboration removes these TerminatorKind") - } - TerminatorKind::Yield { .. } | TerminatorKind::CoroutineDrop => { - unreachable!("we should not hit these cases") // why? - } TerminatorKind::InlineAsm { .. } => self.codegen_unimplemented_stmt( "TerminatorKind::InlineAsm", loc, @@ -212,19 +213,23 @@ impl<'tcx> GotocCtx<'tcx> { /// variant index. pub fn codegen_set_discriminant( &mut self, - dest_ty: Ty<'tcx>, + dest_ty: Ty, dest_expr: Expr, variant_index: VariantIdx, location: Location, ) -> Stmt { // this requires place points to an enum type. - let layout = self.layout_of(dest_ty); + let dest_ty_internal = rustc_internal::internal(dest_ty); + let variant_index_internal = rustc_internal::internal(variant_index); + let layout = self.layout_of(dest_ty_internal); match &layout.variants { Variants::Single { .. } => Stmt::skip(location), Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding { TagEncoding::Direct => { - let discr = dest_ty.discriminant_for_variant(self.tcx, variant_index).unwrap(); - let discr_t = self.codegen_enum_discr_typ(dest_ty); + let discr = dest_ty_internal + .discriminant_for_variant(self.tcx, variant_index_internal) + .unwrap(); + let discr_t = self.codegen_enum_discr_typ(dest_ty_internal); // The constant created below may not fit into the type. // https://github.com/model-checking/kani/issues/996 // @@ -241,18 +246,18 @@ impl<'tcx> GotocCtx<'tcx> { // The discr.ty doesn't always match the tag type. Explicitly cast if needed. let discr_expr = Expr::int_constant(discr.val, self.codegen_ty(discr.ty)) .cast_to(self.codegen_ty(discr_t)); - self.codegen_discriminant_field(dest_expr, rustc_internal::stable(dest_ty)) - .assign(discr_expr, location) + self.codegen_discriminant_field(dest_expr, dest_ty).assign(discr_expr, location) } TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => { - if *untagged_variant != variant_index { + if *untagged_variant != variant_index_internal { let offset = match &layout.fields { FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()], _ => unreachable!("niche encoding must have arbitrary fields"), }; - let discr_ty = self.codegen_enum_discr_typ(dest_ty); + let discr_ty = self.codegen_enum_discr_typ(dest_ty_internal); let discr_ty = self.codegen_ty(discr_ty); - let niche_value = variant_index.as_u32() - niche_variants.start().as_u32(); + let niche_value = + variant_index_internal.as_u32() - niche_variants.start().as_u32(); let niche_value = (niche_value as u128).wrapping_add(*niche_start); trace!(val=?niche_value, typ=?discr_ty, "codegen_set_discriminant niche"); let value = if niche_value == 0 @@ -276,15 +281,15 @@ impl<'tcx> GotocCtx<'tcx> { /// Our model of GotoC has a similar statement, which is later lowered /// to assigning a Nondet in CBMC, with a comment specifying that it /// corresponds to a Deinit. - fn codegen_deinit(&mut self, place: &Place<'tcx>, loc: Location) -> Stmt { - let dst_mir_ty = self.place_ty(place); - let dst_type = self.codegen_ty(dst_mir_ty); - let layout = self.layout_of(dst_mir_ty); + fn codegen_deinit(&mut self, place: &Place, loc: Location) -> Stmt { + let dst_mir_ty = self.place_ty_stable(place); + let dst_type = self.codegen_ty_stable(dst_mir_ty); + let layout = self.layout_of_stable(dst_mir_ty); if layout.is_zst() || dst_type.sizeof_in_bits(&self.symbol_table) == 0 { // We ignore assignment for all zero size types Stmt::skip(loc) } else { - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place)) + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place_stable(place)) .goto_expr .deinit(loc) } @@ -311,20 +316,20 @@ impl<'tcx> GotocCtx<'tcx> { /// /// TODO: this function doesn't handle unwinding which begins if the destructor panics /// - fn codegen_drop(&mut self, place: &Place<'tcx>, target: &BasicBlock, loc: Location) -> Stmt { - let place_ty = self.place_ty(place); - let drop_instance = Instance::resolve_drop_in_place(self.tcx, place_ty); + fn codegen_drop(&mut self, place: &Place, target: &BasicBlockIdx, loc: Location) -> Stmt { + let place_ty = self.place_ty_stable(place); + let drop_instance = Instance::resolve_drop_in_place(place_ty); debug!(?place_ty, ?drop_instance, "codegen_drop"); // Once upon a time we did a `hook_applies` check here, but we no longer seem to hook drops - let drop_implementation = match drop_instance.def { - InstanceDef::DropGlue(_, None) => { + let drop_implementation = match drop_instance.kind { + InstanceKind::Shim if drop_instance.is_empty_shim() => { // We can skip empty DropGlue functions Stmt::skip(loc) } - InstanceDef::DropGlue(_def_id, Some(_)) => { - let place_ref = self.codegen_place_ref(place); + InstanceKind::Shim => { + let place_ref = self.codegen_place_ref_stable(place); match place_ty.kind() { - ty::Dynamic(..) => { + TyKind::RigidTy(RigidTy::Dynamic(..)) => { // Virtual drop via a vtable lookup. // Pull the drop function off of the fat pointer's vtable pointer let vtable_ref = place_ref.to_owned().member("vtable", &self.symbol_table); @@ -346,9 +351,9 @@ impl<'tcx> GotocCtx<'tcx> { } _ => { // Non-virtual, direct drop_in_place call - assert!(!matches!(drop_instance.def, InstanceDef::Virtual(_, _))); + assert!(!matches!(drop_instance.kind, InstanceKind::Virtual { .. })); - let func = self.codegen_func_expr_internal(drop_instance, None); + let func = self.codegen_func_expr(drop_instance, None); // The only argument should be a self reference let args = vec![place_ref]; @@ -363,11 +368,11 @@ impl<'tcx> GotocCtx<'tcx> { } } } - _ => unreachable!( - "TerminatorKind::Drop but not InstanceDef::DropGlue should be impossible" + kind => unreachable!( + "Expected a `InstanceKind::Shim` for `TerminatorKind::Drop`, but found {kind:?}" ), }; - let goto_target = Stmt::goto(self.current_fn().find_label(target), loc); + let goto_target = Stmt::goto(bb_label(*target), loc); let block = vec![drop_implementation, goto_target]; Stmt::block(block, loc) } @@ -378,37 +383,38 @@ impl<'tcx> GotocCtx<'tcx> { /// The otherwise value is stores as the last value of targets. fn codegen_switch_int( &mut self, - discr: &Operand<'tcx>, + discr: &Operand, targets: &SwitchTargets, loc: Location, ) -> Stmt { - let v = self.codegen_operand(discr); + let v = self.codegen_operand_stable(discr); let switch_ty = v.typ().clone(); - if targets.all_targets().len() == 1 { + + // Switches with empty branches should've been eliminated already. + assert!(targets.len() > 1); + if targets.len() == 2 { // Translate to a guarded goto - let first_target = targets.iter().next().unwrap(); + let (case, first_target) = targets.branches().next().unwrap(); Stmt::block( vec![ - v.eq(Expr::int_constant(first_target.0, switch_ty)).if_then_else( - Stmt::goto(self.current_fn().find_label(&first_target.1), loc), + v.eq(Expr::int_constant(case, switch_ty)).if_then_else( + Stmt::goto(bb_label(first_target), loc), None, loc, ), - Stmt::goto(self.current_fn().find_label(&targets.otherwise()), loc), + Stmt::goto(bb_label(targets.otherwise()), loc), ], loc, ) } else { - // Switches with empty targets should've been eliminated already. - assert!(targets.all_targets().len() > 1); let cases = targets - .iter() + .branches() .map(|(c, bb)| { Expr::int_constant(c, switch_ty.clone()) - .switch_case(Stmt::goto(self.current_fn().find_label(&bb), loc)) + .switch_case(Stmt::goto(bb_label(bb), loc)) }) .collect(); - let default = Stmt::goto(self.current_fn().find_label(&targets.otherwise()), loc); + let default = Stmt::goto(bb_label(targets.otherwise()), loc); v.switch(cases, Some(default), loc) } } @@ -427,26 +433,22 @@ impl<'tcx> GotocCtx<'tcx> { /// See [GotocCtx::ty_needs_untupled_args] for more details. fn codegen_untupled_args( &mut self, - instance: Instance<'tcx>, + instance: Instance, fargs: &mut Vec, - last_mir_arg: Option<&Operand<'tcx>>, + last_mir_arg: Option<&Operand>, ) { - debug!( - "codegen_untuple_closure_args instance: {:?}, fargs {:?}", - self.readable_instance_name(instance), - fargs - ); + debug!("codegen_untuple_closure_args instance: {:?}, fargs {:?}", instance.name(), fargs); if !fargs.is_empty() { - let tuple_ty = self.operand_ty(last_mir_arg.unwrap()); - if self.is_zst(tuple_ty) { + let tuple_ty = self.operand_ty_stable(last_mir_arg.unwrap()); + if self.is_zst_stable(tuple_ty) { // Don't pass anything if all tuple elements are ZST. // ZST arguments are ignored. return; } let tupe = fargs.remove(fargs.len() - 1); - if let ty::Tuple(tupled_args) = tuple_ty.kind() { + if let TyKind::RigidTy(RigidTy::Tuple(tupled_args)) = tuple_ty.kind() { for (idx, arg_ty) in tupled_args.iter().enumerate() { - if !self.is_zst(arg_ty) { + if !self.is_zst_stable(*arg_ty) { // Access the tupled parameters through the `member` operation let idx_expr = tupe.clone().member(&idx.to_string(), &self.symbol_table); fargs.push(idx_expr); @@ -458,9 +460,9 @@ impl<'tcx> GotocCtx<'tcx> { /// Because function calls terminate basic blocks, to "end" a function call, we /// must jump to the next basic block. - fn codegen_end_call(&self, target: Option<&BasicBlock>, loc: Location) -> Stmt { + fn codegen_end_call(&self, target: Option, loc: Location) -> Stmt { if let Some(next_bb) = target { - Stmt::goto(self.current_fn().find_label(next_bb), loc) + Stmt::goto(bb_label(next_bb), loc) } else { self.codegen_sanity(Expr::bool_false(), "Unexpected return from Never function", loc) } @@ -471,11 +473,7 @@ impl<'tcx> GotocCtx<'tcx> { /// N.B. public only because instrinsics use this directly, too. /// When `skip_zst` is set to `true`, the return value will not include any argument that is ZST. /// This is used because we ignore ZST arguments, except for intrinsics. - pub(crate) fn codegen_funcall_args( - &mut self, - args: &[OperandStable], - skip_zst: bool, - ) -> Vec { + pub(crate) fn codegen_funcall_args(&mut self, args: &[Operand], skip_zst: bool) -> Vec { let fargs = args .iter() .filter_map(|op| { @@ -509,99 +507,72 @@ impl<'tcx> GotocCtx<'tcx> { /// 2. If a Kani hook applies, do that instead. fn codegen_funcall( &mut self, - func: &Operand<'tcx>, - args: &[Operand<'tcx>], - destination: &Place<'tcx>, - target: &Option, + func: &Operand, + args: &[Operand], + destination: &Place, + target: &Option, span: Span, ) -> Stmt { debug!(?func, ?args, ?destination, ?span, "codegen_funcall"); - let func_stable = StableConverter::convert_operand(self, func.clone()); - let args_stable = args - .iter() - .map(|arg| StableConverter::convert_operand(self, arg.clone())) - .collect::>(); - let destination_stable = StableConverter::convert_place(self, *destination); - - if self.is_intrinsic(&func_stable) { + if self.is_intrinsic(&func) { return self.codegen_funcall_of_intrinsic( - &func_stable, - &args_stable, - &destination_stable, - target.map(|bb| bb.index()), - rustc_internal::stable(span), + &func, + &args, + &destination, + target.map(|bb| bb), + span, ); } - let loc = self.codegen_span(&span); - let funct = self.operand_ty(func); - let mut fargs = self.codegen_funcall_args(&args_stable, true); - match &funct.kind() { - ty::FnDef(defid, subst) => { - let instance = - Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *defid, subst) - .unwrap() - .unwrap(); + let loc = self.codegen_span_stable(span); + let funct = self.operand_ty_stable(func); + let mut fargs = self.codegen_funcall_args(&args, true); + match funct.kind() { + TyKind::RigidTy(RigidTy::FnDef(def, subst)) => { + let instance = Instance::resolve(def, &subst).unwrap(); // TODO(celina): Move this check to be inside codegen_funcall_args. - if self.ty_needs_untupled_args(funct) { + if self.ty_needs_untupled_args(rustc_internal::internal(funct)) { self.codegen_untupled_args(instance, &mut fargs, args.last()); } - 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), - ); + if let Some(hk) = self.hooks.hook_applies(self.tcx, instance) { + return hk.handle(self, instance, fargs, destination, *target, span); } - let mut stmts: Vec = match instance.def { + let mut stmts: Vec = match instance.kind { // Here an empty drop glue is invoked; we just ignore it. - InstanceDef::DropGlue(_, None) => { - return Stmt::goto(self.current_fn().find_label(&target.unwrap()), loc); + InstanceKind::Shim if instance.is_empty_shim() => { + return Stmt::goto(bb_label(target.unwrap()), loc); } // Handle a virtual function call via a vtable lookup - InstanceDef::Virtual(_, idx) => { - let self_ty = self.operand_ty(&args[0]); + InstanceKind::Virtual { idx } => { + let self_ty = self.operand_ty_stable(&args[0]); self.codegen_virtual_funcall(self_ty, idx, destination, &mut fargs, loc) } // Normal, non-virtual function calls - InstanceDef::Item(..) - | InstanceDef::DropGlue(_, Some(_)) - | InstanceDef::FnPtrAddrShim(_, _) - | InstanceDef::Intrinsic(..) - | InstanceDef::FnPtrShim(..) - | InstanceDef::VTableShim(..) - | InstanceDef::ReifyShim(..) - | InstanceDef::ClosureOnceShim { .. } - | InstanceDef::CloneShim(..) => { + InstanceKind::Item | InstanceKind::Intrinsic | InstanceKind::Shim => { // 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_internal(instance, None); + let func_exp = self.codegen_func_expr(instance, None); vec![ - self.codegen_expr_to_place(destination, func_exp.call(fargs)) + self.codegen_expr_to_place_stable(destination, func_exp.call(fargs)) .with_location(loc), ] } - InstanceDef::ThreadLocalShim(_) => todo!(), }; - stmts.push(self.codegen_end_call(target.as_ref(), loc)); + stmts.push(self.codegen_end_call(*target, loc)); Stmt::block(stmts, loc) } // Function call through a pointer - ty::FnPtr(_) => { - let func_expr = self.codegen_operand(func).dereference(); + TyKind::RigidTy(RigidTy::FnPtr(_)) => { + let func_expr = self.codegen_operand_stable(func).dereference(); // Actually generate the function call and return. Stmt::block( vec![ - self.codegen_expr_to_place(destination, func_expr.call(fargs)) + self.codegen_expr_to_place_stable(destination, func_expr.call(fargs)) .with_location(loc), - Stmt::goto(self.current_fn().find_label(&target.unwrap()), loc), + Stmt::goto(bb_label(target.unwrap()), loc), ], loc, ) @@ -613,10 +584,10 @@ impl<'tcx> GotocCtx<'tcx> { /// Extract a reference to self for virtual method calls. /// /// See [GotocCtx::codegen_dynamic_function_sig] for more details. - fn extract_ptr(&self, arg_expr: Expr, arg_ty: Ty<'tcx>) -> Expr { + fn extract_ptr(&self, arg_expr: Expr, arg_ty: Ty) -> Expr { // Generate an expression that indexes the pointer. let expr = self - .receiver_data_path(arg_ty) + .receiver_data_path(rustc_internal::internal(arg_ty)) .fold(arg_expr, |curr_expr, (name, _)| curr_expr.member(name, &self.symbol_table)); trace!(?arg_ty, gotoc_ty=?expr.typ(), gotoc_expr=?expr.value(), "extract_ptr"); @@ -640,9 +611,9 @@ impl<'tcx> GotocCtx<'tcx> { /// 4. Generate the function call. fn codegen_virtual_funcall( &mut self, - self_ty: Ty<'tcx>, + self_ty: Ty, idx: usize, - place: &Place<'tcx>, + place: &Place, fargs: &mut [Expr], loc: Location, ) -> Vec { @@ -664,7 +635,7 @@ impl<'tcx> GotocCtx<'tcx> { let data_ptr = trait_fat_ptr.to_owned().member("data", &self.symbol_table); let mut ret_stmts = vec![]; - fargs[0] = if self_ty.is_adt() { + fargs[0] = if self_ty.kind().is_adt() { // Generate a temp variable and assign its inner pointer to the fat_ptr.data. match fn_ptr.typ() { Type::Pointer { typ: box Type::Code { parameters, .. } } => { @@ -697,7 +668,7 @@ impl<'tcx> GotocCtx<'tcx> { // Virtual function call and corresponding nonnull assertion. let call = fn_ptr.dereference().call(fargs.to_vec()); - let call_stmt = self.codegen_expr_to_place(place, call).with_location(loc); + let call_stmt = self.codegen_expr_to_place_stable(place, call).with_location(loc); let call_stmt = if self.vtable_ctx.emit_vtable_restrictions { self.virtual_call_with_restricted_fn_ptr(trait_fat_ptr.typ().clone(), idx, call_stmt) } else { @@ -712,7 +683,7 @@ 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, place: &PlaceStable, expr: Expr) -> Stmt { + pub(crate) fn codegen_expr_to_place_stable(&mut self, place: &Place, expr: Expr) -> Stmt { if self.place_ty_stable(place).kind().is_unit() { expr.as_stmt(Location::none()) } else { @@ -721,14 +692,4 @@ impl<'tcx> GotocCtx<'tcx> { .assign(expr, 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()) - } else { - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(p)) - .goto_expr - .assign(e, Location::none()) - } - } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs index a32de2040f75..2213676d5a63 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs @@ -8,21 +8,16 @@ 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::{ - Location, Operand as OperandInternal, Place as PlaceInternal, Rvalue as RvalueInternal, -}; use rustc_middle::ty::layout::{LayoutOf, TyAndLayout}; -use rustc_middle::ty::{self, Const as ConstInternal, GenericArgsRef, Ty as TyInternal, TyCtxt}; +use rustc_middle::ty::{self}; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; use stable_mir::mir::{Local, Operand, Place, Rvalue}; -use stable_mir::ty::{Const, RigidTy, Ty, TyKind}; +use stable_mir::ty::{FnSig, RigidTy, Ty, TyKind}; impl<'tcx> GotocCtx<'tcx> { pub fn place_ty_stable(&self, place: &Place) -> Ty { - place.ty(self.current_fn().body().locals()).unwrap() + place.ty(self.current_fn().locals()).unwrap() } pub fn codegen_ty_stable(&mut self, ty: Ty) -> Type { @@ -34,11 +29,11 @@ impl<'tcx> GotocCtx<'tcx> { } pub fn local_ty_stable(&self, local: Local) -> Ty { - self.current_fn().body().local_decl(local).unwrap().ty + self.current_fn().locals()[local].ty } pub fn operand_ty_stable(&self, operand: &Operand) -> Ty { - operand.ty(self.current_fn().body().locals()).unwrap() + operand.ty(self.current_fn().locals()).unwrap() } pub fn is_zst_stable(&self, ty: Ty) -> bool { @@ -58,8 +53,11 @@ impl<'tcx> GotocCtx<'tcx> { ) } - pub fn fn_sig_of_instance_stable(&self, instance: Instance) -> ty::PolyFnSig<'tcx> { - self.fn_sig_of_instance(rustc_internal::internal(instance)) + pub fn fn_sig_of_instance_stable(&self, instance: Instance) -> FnSig { + let fn_sig = self.fn_sig_of_instance(rustc_internal::internal(instance)); + let fn_sig = + self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), fn_sig); + rustc_internal::stable(fn_sig) } pub fn use_fat_pointer_stable(&self, pointer_ty: Ty) -> bool { @@ -87,13 +85,36 @@ impl<'tcx> GotocCtx<'tcx> { } pub fn rvalue_ty_stable(&self, rvalue: &Rvalue) -> Ty { - rvalue.ty(self.current_fn().body().locals()).unwrap() + rvalue.ty(self.current_fn().locals()).unwrap() } pub fn simd_size_and_type(&self, ty: Ty) -> (u64, Ty) { let (sz, ty) = rustc_internal::internal(ty).simd_size_and_type(self.tcx); (sz, rustc_internal::stable(ty)) } + + pub fn codegen_enum_discr_typ_stable(&self, ty: Ty) -> Ty { + rustc_internal::stable(self.codegen_enum_discr_typ(rustc_internal::internal(ty))) + } + + pub fn codegen_function_sig_stable(&mut self, sig: FnSig) -> Type { + let params = sig + .inputs() + .iter() + .filter_map(|ty| { + if self.is_zst_stable(*ty) { None } else { Some(self.codegen_ty_stable(*ty)) } + }) + .collect(); + + if sig.c_variadic { + Type::variadic_code_with_unnamed_parameters( + params, + self.codegen_ty_stable(sig.output()), + ) + } else { + Type::code_with_unnamed_parameters(params, self.codegen_ty_stable(sig.output())) + } + } } /// If given type is a Ref / Raw ref, return the pointee type. pub fn pointee_type(mir_type: Ty) -> Option { @@ -112,47 +133,6 @@ pub fn pretty_ty(ty: Ty) -> String { rustc_internal::internal(ty).to_string() } -/// 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) - } - - pub fn convert_rvalue(gcx: &'a GotocCtx<'tcx>, mut operand: RvalueInternal<'tcx>) -> Rvalue { - let mut converter = StableConverter { gcx }; - converter.visit_rvalue(&mut operand, mir::Location::START); - rustc_internal::stable(operand) - } - - 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) - } -} - pub fn pointee_type_stable(ty: Ty) -> Option { match ty.kind() { TyKind::RigidTy(RigidTy::Ref(_, pointee_ty, _)) @@ -160,35 +140,3 @@ pub fn pointee_type_stable(ty: Ty) -> Option { _ => None, } } - -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); - } - - fn visit_ty_const(&mut self, ct: &mut ty::Const<'tcx>, _location: mir::Location) { - *ct = self.gcx.monomorphize(*ct); - } - - fn visit_args(&mut self, args: &mut GenericArgsRef<'tcx>, _: Location) { - *args = self.gcx.monomorphize(*args); - } - - 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); - } -} diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 9f99801e95b9..661d6da38b6d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -8,7 +8,6 @@ use cbmc::{InternString, InternedString}; use rustc_ast::ast::Mutability; use rustc_hir::{LangItem, Unsafety}; use rustc_index::IndexVec; -use rustc_middle::mir::{HasLocalDecls, Local, Operand, Place, Rvalue}; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::print::with_no_trimmed_paths; use rustc_middle::ty::print::FmtPrinter; @@ -25,6 +24,7 @@ use rustc_target::abi::{ TyAndLayout, VariantIdx, Variants, }; use rustc_target::spec::abi::Abi; +use stable_mir::mir::Body; use std::iter; use tracing::{debug, trace, warn}; @@ -436,22 +436,6 @@ impl<'tcx> GotocCtx<'tcx> { } } - pub fn local_ty(&self, l: Local) -> Ty<'tcx> { - 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().body_internal().local_decls(), self.tcx)) - } - - pub fn operand_ty(&self, o: &Operand<'tcx>) -> Ty<'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().body_internal().local_decls(), self.tcx).ty) - } - /// Is the MIR type a zero-sized type. pub fn is_zst(&self, t: Ty<'tcx>) -> bool { self.layout_of(t).is_zst() @@ -735,6 +719,7 @@ impl<'tcx> GotocCtx<'tcx> { /// also c.f. /// c.f. pub fn codegen_ty(&mut self, ty: Ty<'tcx>) -> Type { + // TODO: Remove all monomorphize calls let normalized = self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), ty); let goto_typ = self.codegen_ty_inner(normalized); if let Some(tag) = goto_typ.tag() { @@ -1303,17 +1288,7 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_function_sig(&mut self, sig: PolyFnSig<'tcx>) -> Type { let sig = self.monomorphize(sig); let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig); - let params = sig - .inputs() - .iter() - .filter_map(|t| if self.is_zst(*t) { None } else { Some(self.codegen_ty(*t)) }) - .collect(); - - if sig.c_variadic { - Type::variadic_code_with_unnamed_parameters(params, self.codegen_ty(sig.output())) - } else { - Type::code_with_unnamed_parameters(params, self.codegen_ty(sig.output())) - } + self.codegen_function_sig_stable(rustc_internal::stable(sig)) } /// Creates a zero-sized struct for a FnDef. @@ -1681,39 +1656,39 @@ impl<'tcx> GotocCtx<'tcx> { } /// the function type of the current instance - pub fn fn_typ(&mut self) -> Type { - let sig = self.current_fn().sig(); - let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig); - // we don't call [codegen_function_sig] because we want to get a bit more metainformation. - let is_vtable_shim = - matches!(self.current_fn().instance().def, ty::InstanceDef::VTableShim(..)); + pub fn fn_typ(&mut self, body: &Body) -> Type { + let sig = self.current_fn().sig().clone(); + let internal_instance = self.current_fn().instance(); + let is_vtable_shim = matches!(internal_instance.def, ty::InstanceDef::VTableShim(..)); let mut params: Vec = sig .inputs() .iter() .enumerate() - .filter_map(|(i, t)| { + .filter_map(|(i, ty)| { + debug!(?i, ?ty, "fn_typ"); let is_vtable_shim_self = i == 0 && is_vtable_shim; - if self.is_zst(*t) && !is_vtable_shim_self { + if self.is_zst_stable(*ty) && !is_vtable_shim_self { // We ignore zero-sized parameters. // See https://github.com/model-checking/kani/issues/274 for more details. None } else { - let lc = Local::from_usize(i + 1); + // An arg is the local with index offset by one (return value is always local 0) + let lc = i + 1; let mut ident = self.codegen_var_name(&lc); // `spread_arg` indicates that the last argument is tupled - // at the LLVM/codegen level, so we need to declare the indivual + // at the LLVM/codegen level, so we need to declare the individual // 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().body_internal().spread_arg { - if lc.index() >= spread.index() { + if let Some(spread) = body.spread_arg() { + if lc >= spread { let (name, _) = self.codegen_spread_arg_name(&lc); ident = name; } } Some( - self.codegen_ty(*t) + self.codegen_ty_stable(*ty) .as_parameter(Some(ident.clone().into()), Some(ident.into())), ) } @@ -1734,9 +1709,9 @@ impl<'tcx> GotocCtx<'tcx> { debug!(?params, signature=?sig, "function_type"); if sig.c_variadic { - Type::variadic_code(params, self.codegen_ty(sig.output())) + Type::variadic_code(params, self.codegen_ty_stable(sig.output())) } else { - Type::code(params, self.codegen_ty(sig.output())) + Type::code(params, self.codegen_ty_stable(sig.output())) } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 5d27375de54f..21dea6160536 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -47,6 +47,7 @@ use rustc_smir::rustc_internal; use rustc_target::abi::Endian; use rustc_target::spec::PanicStrategy; use stable_mir::mir::mono::MonoItem as MonoItemStable; +use stable_mir::CrateDef; use std::any::Any; use std::collections::BTreeMap; use std::collections::HashSet; @@ -102,23 +103,21 @@ impl GotocCodegenBackend { for item in &items { match *item { MonoItem::Fn(instance) => { + let instance = rustc_internal::stable(instance); gcx.call_with_panic_debug_info( |ctx| ctx.declare_function(instance), - format!( - "declare_function: {}", - gcx.readable_instance_name(instance) - ), - instance.def_id(), + format!("declare_function: {}", instance.name()), + instance.def, ); } - MonoItem::Static(def_id) => { + MonoItem::Static(_) => { let MonoItemStable::Static(def) = rustc_internal::stable(item) else { unreachable!() }; gcx.call_with_panic_debug_info( |ctx| ctx.declare_static(def), - format!("declare_static: {def_id:?}"), - def_id, + format!("declare_static: {}", def.name()), + def, ); } MonoItem::GlobalAsm(_) => {} // Ignore this. We have already warned about it. @@ -129,24 +128,25 @@ impl GotocCodegenBackend { for item in &items { match *item { MonoItem::Fn(instance) => { + let instance = rustc_internal::stable(instance); gcx.call_with_panic_debug_info( |ctx| ctx.codegen_function(instance), format!( "codegen_function: {}\n{}", - gcx.readable_instance_name(instance), - gcx.symbol_name(instance) + instance.name(), + gcx.symbol_name_stable(instance) ), - instance.def_id(), + instance.def, ); } - MonoItem::Static(def_id) => { + MonoItem::Static(_) => { let MonoItemStable::Static(def) = rustc_internal::stable(item) else { unreachable!() }; gcx.call_with_panic_debug_info( |ctx| ctx.codegen_static(def), - format!("codegen_static: {def_id:?}"), - def_id, + format!("codegen_static: {}", def.name()), + def, ); } MonoItem::GlobalAsm(_) => {} // We have already warned above 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 e39d44743c5f..e73a4756a581 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs @@ -3,12 +3,15 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Stmt; -use rustc_middle::mir::{BasicBlock, Body as InternalBody}; -use rustc_middle::ty::{Instance as InternalInstance, PolyFnSig}; +use cbmc::InternedString; +use rustc_middle::mir::Body as InternalBody; +use rustc_middle::ty::Instance as InternalInstance; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; -use stable_mir::mir::Body; +use stable_mir::mir::{Body, Local, LocalDecl}; +use stable_mir::ty::FnSig; use stable_mir::CrateDef; +use std::collections::HashMap; /// This structure represents useful data about the function we are currently compiling. #[derive(Debug)] @@ -17,39 +20,48 @@ pub struct CurrentFnCtx<'tcx> { block: Vec, /// The codegen instance for the current function instance: Instance, + /// The current function signature. + fn_sig: FnSig, /// The crate this function is from krate: String, /// The MIR for the current instance. This is using the internal representation. mir: &'tcx InternalBody<'tcx>, - /// The MIR for the current instance. - body: Body, + /// A list of local declarations used to retrieve MIR component types. + locals: Vec, + /// A list of pretty names for locals that corrspond to user variables. + local_names: HashMap, /// The symbol name of the current function name: String, /// A human readable pretty name for the current function readable_name: String, - /// The signature of the current function - sig: PolyFnSig<'tcx>, /// A counter to enable creating temporary variables temp_var_counter: u64, } /// Constructor impl<'tcx> CurrentFnCtx<'tcx> { - pub fn new(instance: Instance, gcx: &GotocCtx<'tcx>) -> Self { + pub fn new(instance: Instance, gcx: &GotocCtx<'tcx>, body: &Body) -> 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() }; + let locals = body.locals().to_vec(); + let local_names = body + .var_debug_info + .iter() + .filter_map(|info| info.local().map(|local| (local, (&info.name).into()))) + .collect::>(); + let fn_sig = gcx.fn_sig_of_instance_stable(instance); Self { block: vec![], instance, + fn_sig, mir: gcx.tcx.instance_mir(internal_instance.def), krate: instance.def.krate().name, - body, + locals, + local_names, name, readable_name, - sig: gcx.fn_sig_of_instance(internal_instance), temp_var_counter: 0, } } @@ -80,9 +92,8 @@ impl<'tcx> CurrentFnCtx<'tcx> { rustc_internal::internal(self.instance) } - /// The crate that function came from - pub fn krate(&self) -> String { - self.krate.to_string() + pub fn instance_stable(&self) -> Instance { + self.instance } /// The internal MIR for the function we are currently compiling using internal APIs. @@ -101,13 +112,16 @@ impl<'tcx> CurrentFnCtx<'tcx> { } /// The signature of the function we are currently compiling - pub fn sig(&self) -> PolyFnSig<'tcx> { - self.sig + pub fn sig(&self) -> &FnSig { + &self.fn_sig } - /// The body of the function. - pub fn body(&self) -> &Body { - &self.body + pub fn locals(&self) -> &[LocalDecl] { + &self.locals + } + + pub fn local_name(&self, local: Local) -> Option { + self.local_names.get(&local).copied() } } @@ -117,8 +131,4 @@ impl CurrentFnCtx<'_> { pub fn is_std(&self) -> bool { self.krate == "std" || self.krate == "core" } - - pub fn find_label(&self, bb: &BasicBlock) -> String { - 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 61861827df96..4a30837ae812 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -29,12 +29,13 @@ use rustc_middle::ty::layout::{ FnAbiError, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError, LayoutOfHelpers, TyAndLayout, }; -use rustc_middle::ty::{self, Instance, Ty, TyCtxt}; -use rustc_smir::rustc_internal; +use rustc_middle::ty::{self, Ty, TyCtxt}; use rustc_span::source_map::respan; use rustc_span::Span; use rustc_target::abi::call::FnAbi; use rustc_target::abi::{HasDataLayout, TargetDataLayout}; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::Body; use stable_mir::ty::Allocation; pub struct GotocCtx<'tcx> { @@ -298,8 +299,8 @@ 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(rustc_internal::stable(instance), self)); + pub fn set_current_fn(&mut self, instance: Instance, body: &Body) { + self.current_fn = Some(CurrentFnCtx::new(instance, self, body)); } 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 b914c46c0f6c..97606688d1ed 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -29,7 +29,7 @@ pub trait GotocHook { gcx: &mut GotocCtx, instance: Instance, fargs: Vec, - assign_to: Place, + assign_to: &Place, target: Option, span: Span, ) -> Stmt; @@ -65,7 +65,7 @@ impl GotocHook for Cover { gcx: &mut GotocCtx, _instance: Instance, mut fargs: Vec, - _assign_to: Place, + _assign_to: &Place, target: Option, span: Span, ) -> Stmt { @@ -100,7 +100,7 @@ impl GotocHook for Assume { gcx: &mut GotocCtx, _instance: Instance, mut fargs: Vec, - _assign_to: Place, + _assign_to: &Place, target: Option, span: Span, ) -> Stmt { @@ -124,7 +124,7 @@ impl GotocHook for Assert { gcx: &mut GotocCtx, _instance: Instance, mut fargs: Vec, - _assign_to: Place, + _assign_to: &Place, target: Option, span: Span, ) -> Stmt { @@ -165,20 +165,20 @@ impl GotocHook for Nondet { gcx: &mut GotocCtx, _instance: Instance, fargs: Vec, - assign_to: Place, + assign_to: &Place, target: Option, span: Span, ) -> Stmt { assert!(fargs.is_empty()); let loc = gcx.codegen_span_stable(span); let target = target.unwrap(); - let pt = gcx.place_ty_stable(&assign_to); + 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!( gcx, - gcx.codegen_place_stable(&assign_to) + gcx.codegen_place_stable(assign_to) ) .goto_expr; Stmt::block( @@ -209,7 +209,7 @@ impl GotocHook for Panic { gcx: &mut GotocCtx, _instance: Instance, fargs: Vec, - _assign_to: Place, + _assign_to: &Place, _target: Option, span: Span, ) -> Stmt { @@ -231,7 +231,7 @@ impl GotocHook for RustAlloc { gcx: &mut GotocCtx, instance: Instance, mut fargs: Vec, - assign_to: Place, + assign_to: &Place, target: Option, span: Span, ) -> Stmt { @@ -243,7 +243,7 @@ impl GotocHook for RustAlloc { vec![ unwrap_or_return_codegen_unimplemented_stmt!( gcx, - gcx.codegen_place_stable(&assign_to) + gcx.codegen_place_stable(assign_to) ) .goto_expr .assign( @@ -282,7 +282,7 @@ impl GotocHook for MemCmp { gcx: &mut GotocCtx, instance: Instance, mut fargs: Vec, - assign_to: Place, + assign_to: &Place, target: Option, span: Span, ) -> Stmt { @@ -304,7 +304,7 @@ impl GotocHook 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!(gcx, gcx.codegen_place_stable(&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) @@ -338,7 +338,7 @@ impl GotocHook for UntrackedDeref { gcx: &mut GotocCtx, _instance: Instance, mut fargs: Vec, - assign_to: Place, + assign_to: &Place, _target: Option, span: Span, ) -> Stmt { @@ -354,7 +354,7 @@ impl GotocHook for UntrackedDeref { vec![Stmt::assign( unwrap_or_return_codegen_unimplemented_stmt!( gcx, - gcx.codegen_place_stable(&assign_to) + gcx.codegen_place_stable(assign_to) ) .goto_expr, fargs.pop().unwrap().dereference(), diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs index a6204ad2a57f..c30d1539bda2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs @@ -5,10 +5,9 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Location; -use rustc_middle::mir::Body; -use rustc_middle::ty::print::with_no_trimmed_paths; -use rustc_middle::ty::Instance; -use rustc_span::def_id::DefId; +use stable_mir::mir::mono::Instance; +use stable_mir::mir::Body; +use stable_mir::CrateDef; use std::cell::RefCell; use std::panic; use std::sync::LazyLock; @@ -56,37 +55,32 @@ static DEFAULT_HOOK: LazyLock) + Sync + Send + impl<'tcx> GotocCtx<'tcx> { // Calls the closure while updating the tracked global variable marking the // codegen item for panic debugging. - pub fn call_with_panic_debug_info)>( + pub fn call_with_panic_debug_info)>( &mut self, call: F, panic_debug: String, - def_id: DefId, + def: D, ) { CURRENT_CODEGEN_ITEM.with(|odb_cell| { - odb_cell - .replace((Some(panic_debug), Some(self.codegen_span(&self.tcx.def_span(def_id))))); + odb_cell.replace((Some(panic_debug), Some(self.codegen_span_stable(def.span())))); call(self); odb_cell.replace((None, None)); }); } - pub fn print_instance(&self, instance: Instance<'_>, mir: &'tcx Body<'tcx>) { + pub fn print_instance(&self, instance: Instance, body: &Body) { if cfg!(debug_assertions) { - debug!( - "handling {}, {}", - instance, - with_no_trimmed_paths!(self.tcx.def_path_str(instance.def_id())) - ); + debug!("handling {}", instance.name(),); debug!("variables: "); - for l in mir.args_iter().chain(mir.vars_and_temps_iter()) { - debug!("let {:?}: {:?}", l, self.local_ty(l)); + for (idx, decl) in body.locals().iter().enumerate() { + debug!("let _{idx}: {:?}", decl.ty); } - for (bb, bbd) in mir.basic_blocks.iter_enumerated() { + for (bb, bbd) in body.blocks.iter().enumerate() { debug!("block {:?}", bb); for stmt in &bbd.statements { debug!("{:?}", stmt); } - debug!("{:?}", bbd.terminator().kind); + debug!("{:?}", bbd.terminator.kind); } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index 587eef72a645..1b6d3da65cbd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -7,10 +7,10 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::InternedString; use rustc_hir::def_id::LOCAL_CRATE; use rustc_middle::mir::mono::CodegenUnitNameBuilder; -use rustc_middle::mir::Local; use rustc_middle::ty::print::with_no_trimmed_paths; use rustc_middle::ty::{Instance, TyCtxt}; use stable_mir::mir::mono::Instance as InstanceStable; +use stable_mir::mir::Local; use tracing::debug; impl<'tcx> GotocCtx<'tcx> { @@ -20,22 +20,22 @@ impl<'tcx> GotocCtx<'tcx> { } pub fn codegen_var_base_name(&self, l: &Local) -> String { - match self.find_debug_info(l) { - None => format!("var_{}", l.index()), - Some(info) => info.name, + match self.current_fn().local_name(*l) { + None => format!("var_{l}"), + Some(name) => name.to_string(), } } pub fn codegen_var_name(&self, l: &Local) -> String { let fname = self.current_fn().name(); - match self.find_debug_info(l) { - Some(info) => format!("{fname}::1::var{l:?}::{}", info.name), - None => format!("{fname}::1::var{l:?}"), + match self.current_fn().local_name(*l) { + Some(name) => format!("{fname}::1::var_{l}::{name}"), + None => format!("{fname}::1::var_{l}"), } } pub fn is_user_variable(&self, var: &Local) -> bool { - self.find_debug_info(var).is_some() + self.current_fn().local_name(*var).is_some() } // Special naming conventions for parameters that are spread from a tuple diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 0aec0c448219..c63b8303de17 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -231,6 +231,8 @@ impl SourceLocation { } /// Get the FnAbi of a given instance with no extra variadic arguments. +/// TODO: Get rid of this. Use instance.fn_sig() instead. +/// pub fn fn_abi<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> &'tcx FnAbi<'tcx, Ty<'tcx>> { let helper = CompilerHelpers { tcx }; helper.fn_abi_of_instance(instance, ty::List::empty()) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 5c17a2e4df62..b4d1d71ec9f8 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2023-12-15" +channel = "nightly-2023-12-16" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]