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() }