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.

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