Merge branch 'main' into dependabot/github_actions/actions/checkout-4

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