Clean up some code before migrating rvalue

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)
+            );
         }
     }
 

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<Stmt> {
-        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");
 

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

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(

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