From b7ece82280fbfc5025fd6fe95f092728172c58a7 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 8 Dec 2023 23:30:27 -0800 Subject: [PATCH] Clean up some code before migrating rvalue (#2928) Clean up old unreachable check due to missing component which has been a long time by the MirLinker. Also remove an old TODO code to add the def name to virtual calls. This has regressed before, so the risk of regressing doesn't seem worth for debug purpose. --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 36 ++++--------------- .../codegen/statement.rs | 15 ++------ .../src/codegen_cprover_gotoc/codegen/typ.rs | 2 +- .../codegen_cprover_gotoc/context/goto_ctx.rs | 5 --- .../src/codegen_cprover_gotoc/utils/names.rs | 9 ++--- 5 files changed, 12 insertions(+), 55 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index c781f272fb2d..8ded0b7f421a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -11,7 +11,7 @@ use crate::kani_middle::coercion::{ }; use crate::unwrap_or_return_codegen_unimplemented; use cbmc::goto_program::{ - arithmetic_overflow_result_type, BinaryOperator, Expr, Location, Stmt, Symbol, Type, + arithmetic_overflow_result_type, BinaryOperator, Expr, Location, Stmt, Type, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, }; use cbmc::MachineModel; @@ -1169,7 +1169,7 @@ impl<'tcx> GotocCtx<'tcx> { idx: usize, ) -> Expr { debug!(?instance, typ=?t, %idx, "codegen_vtable_method_field"); - let vtable_field_name = self.vtable_field_name(instance.def_id(), idx); + let vtable_field_name = self.vtable_field_name(idx); let vtable_type = Type::struct_tag(self.vtable_name(t)); let field_type = vtable_type.lookup_field_type(vtable_field_name, &self.symbol_table).unwrap(); @@ -1232,34 +1232,10 @@ impl<'tcx> GotocCtx<'tcx> { .address_of() .cast_to(trait_fn_ty) } else { - // We skip an entire submodule of the standard library, so drop is missing - // for it. Build and insert a function that just calls an unimplemented block - // to maintain soundness. - let drop_sym_name = format!("drop_unimplemented_{}", self.symbol_name(drop_instance)); - let pretty_name = - format!("drop_unimplemented<{}>", self.readable_instance_name(drop_instance)); - let drop_sym = self.ensure(&drop_sym_name, |ctx, name| { - // Function body - let unimplemented = ctx.codegen_unimplemented_stmt( - format!("drop_in_place for {drop_instance}").as_str(), - Location::none(), - "https://github.com/model-checking/kani/issues/281", - ); - - // Declare symbol for the single, self parameter - let param_typ = ctx.codegen_ty(trait_ty).to_pointer(); - let param_sym = ctx.gen_function_parameter(0, &drop_sym_name, param_typ); - - // Build and insert the function itself - Symbol::function( - name, - Type::code(vec![param_sym.to_function_parameter()], Type::empty()), - Some(Stmt::block(vec![unimplemented], Location::none())), - pretty_name, - Location::none(), - ) - }); - drop_sym.to_expr().address_of().cast_to(trait_fn_ty) + unreachable!( + "Missing drop implementation for {}", + self.readable_instance_name(drop_instance) + ); } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index a4597885716a..d673c7d37c83 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -6,7 +6,6 @@ use super::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_hir::def_id::DefId; use rustc_middle::mir; use rustc_middle::mir::{ AssertKind, BasicBlock, NonDivergingIntrinsic, Operand, Place, Statement, StatementKind, @@ -541,16 +540,9 @@ impl<'tcx> GotocCtx<'tcx> { return Stmt::goto(self.current_fn().find_label(&target.unwrap()), loc); } // Handle a virtual function call via a vtable lookup - InstanceDef::Virtual(def_id, idx) => { + InstanceDef::Virtual(_, idx) => { let self_ty = self.operand_ty(&args[0]); - self.codegen_virtual_funcall( - self_ty, - def_id, - idx, - destination, - &mut fargs, - loc, - ) + self.codegen_virtual_funcall(self_ty, idx, destination, &mut fargs, loc) } // Normal, non-virtual function calls InstanceDef::Item(..) @@ -623,13 +615,12 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_virtual_funcall( &mut self, self_ty: Ty<'tcx>, - def_id: DefId, idx: usize, place: &Place<'tcx>, fargs: &mut [Expr], loc: Location, ) -> Vec { - let vtable_field_name = self.vtable_field_name(def_id, idx); + let vtable_field_name = self.vtable_field_name(idx); trace!(?self_ty, ?place, ?vtable_field_name, "codegen_virtual_funcall"); debug!(?fargs, "codegen_virtual_funcall"); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index ec5756c4d09b..3a9d54a384af 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -481,7 +481,7 @@ impl<'tcx> GotocCtx<'tcx> { let fn_ptr = fn_ty.to_pointer(); // vtable field name, i.e., 3_vol (idx_method) - let vtable_field_name = self.vtable_field_name(instance.def_id(), idx); + let vtable_field_name = self.vtable_field_name(idx); DatatypeComponent::field(vtable_field_name, fn_ptr) } 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 01fb198d16fa..6619a6949681 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -138,11 +138,6 @@ impl<'tcx> GotocCtx<'tcx> { self.gen_stack_variable(c, fname, "var", t, Location::none(), false) } - // Generate a Symbol Expression representing a function parameter from the MIR - pub fn gen_function_parameter(&mut self, c: u64, fname: &str, t: Type) -> Symbol { - self.gen_stack_variable(c, fname, "var", t, Location::none(), true) - } - /// Given a counter `c` a function name `fname, and a prefix `prefix`, generates a new function local variable /// It is an error to reuse an existing `c`, `fname` `prefix` tuple. fn gen_stack_variable( diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs index da684b601668..2782f2cee47c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs @@ -5,7 +5,6 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::InternedString; -use rustc_hir::def_id::DefId; use rustc_hir::def_id::LOCAL_CRATE; use rustc_middle::mir::mono::CodegenUnitNameBuilder; use rustc_middle::mir::Local; @@ -83,12 +82,8 @@ impl<'tcx> GotocCtx<'tcx> { /// The name for the struct field on a vtable for a given function. Because generic /// functions can share the same name, we need to use the index of the entry in the /// vtable. This is the same index that will be passed in virtual function calls as - /// InstanceDef::Virtual(def_id, idx). We could use solely the index as a key into - /// the vtable struct, but we add the method name for debugging readability. - /// Example: 3_vol - pub fn vtable_field_name(&self, _def_id: DefId, idx: usize) -> InternedString { - // format!("{}_{}", idx, with_no_trimmed_paths!(|| self.tcx.item_name(def_id))) - // TODO: use def_id https://github.com/model-checking/kani/issues/364 + /// InstanceDef::Virtual(def_id, idx). + pub fn vtable_field_name(&self, idx: usize) -> InternedString { idx.to_string().into() }