Merge branch 'main' into smir-hooks

.github/workflows/audit.yml

@@ -16,7 +16,7 @@ jobs:
  audit:
  runs-on: ubuntu-latest
  steps:
- - uses: actions/checkout@v3
+ - uses: actions/checkout@v4
  - uses: EmbarkStudios/cargo-deny-action@v1
  with:
  arguments: --all-features --workspace

.github/workflows/bench.yml

@@ -30,14 +30,14 @@ jobs:
  echo "NEW_REF=${{ github.event.pull_request.head.sha }}" | tee -a "$GITHUB_ENV"
 
  - name: Check out Kani (old variant)
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
  with:
  path: ./old
  ref: ${{ env.OLD_REF }}
  fetch-depth: 2
 
  - name: Check out Kani (new variant)
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
  with:
  path: ./new
  ref: ${{ env.NEW_REF }}

.github/workflows/cbmc-latest.yml

@@ -22,7 +22,7 @@ jobs:
  os: [macos-12, ubuntu-20.04, ubuntu-22.04]
  steps:
  - name: Checkout Kani under "kani"
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
  with:
  path: kani
 
@@ -37,7 +37,7 @@ jobs:
  run: cargo build-dev
 
  - name: Checkout CBMC under "cbmc"
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
  with:
  repository: diffblue/cbmc
  path: cbmc
@@ -58,7 +58,7 @@ jobs:
  runs-on: ubuntu-20.04
  steps:
  - name: Checkout Kani under "kani"
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
  with:
  path: kani
 
@@ -73,7 +73,7 @@ jobs:
  run: cargo build-dev -- --release
 
  - name: Checkout CBMC under "cbmc"
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
  with:
  repository: diffblue/cbmc
  path: cbmc

.github/workflows/cbmc-update.yml

@@ -19,7 +19,7 @@ jobs:
  runs-on: ubuntu-22.04
  steps:
  - name: Checkout Kani
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
 
  - name: Setup Kani Dependencies
  uses: ./.github/actions/setup

.github/workflows/extra_jobs.yml

@@ -33,7 +33,7 @@ jobs:
  runs-on: ubuntu-latest
  steps:
  - name: Checkout Kani
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
 
  - name: Label PR
  id: labeler

.github/workflows/format-check.yml

@@ -14,7 +14,7 @@ jobs:
  runs-on: ubuntu-latest
  steps:
  - name: Checkout Kani
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
 
  - name: Execute copyright check
  run: ./scripts/ci/run-copyright-check.sh
@@ -33,7 +33,7 @@ jobs:
  runs-on: ubuntu-20.04
  steps:
  - name: Checkout Kani
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
 
  - name: Setup Kani Dependencies
  uses: ./.github/actions/setup

.github/workflows/kani-m1.yml

@@ -16,7 +16,7 @@ jobs:
  runs-on: macos-13-xlarge
  steps:
  - name: Checkout Kani
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
 
  - name: Setup Kani Dependencies
  uses: ./.github/actions/setup

.github/workflows/kani.yml

@@ -20,7 +20,7 @@ jobs:
  os: [macos-12, ubuntu-20.04, ubuntu-22.04]
  steps:
  - name: Checkout Kani
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
 
  - name: Setup Kani Dependencies
  uses: ./.github/actions/setup
@@ -37,7 +37,7 @@ jobs:
  runs-on: ubuntu-20.04
  steps:
  - name: Checkout Kani
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
 
  - name: Setup Kani Dependencies
  uses: ./.github/actions/setup
@@ -58,7 +58,7 @@ jobs:
  runs-on: ubuntu-20.04
  steps:
  - name: Checkout Kani
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
 
  - name: Install benchcomp dependencies
  run: |
@@ -81,7 +81,7 @@ jobs:
  runs-on: ubuntu-20.04
  steps:
  - name: Checkout Kani
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
 
  - name: Setup Kani Dependencies
  uses: ./.github/actions/setup
@@ -102,7 +102,7 @@ jobs:
  contents: write
  steps:
  - name: Checkout Kani
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
 
  - name: Setup Kani Dependencies
  uses: ./.github/actions/setup

.github/workflows/release.yml

@@ -30,7 +30,7 @@ jobs:
  crate_version: ${{ steps.bundle.outputs.crate_version }}
  steps:
  - name: Checkout code
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
 
  - name: Setup Kani Dependencies
  uses: ./.github/actions/setup
@@ -135,7 +135,7 @@ jobs:
  cargo kani setup --use-local-bundle ./${{ matrix.prev_job.bundle }}
 
  - name: Checkout tests
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
 
  - name: Run tests
  # TODO: Customize compiletest to run custom kani. For now, just run a few cargo kani tests.
@@ -160,7 +160,7 @@ jobs:
  KANI_SRC: ./kani_src
  steps:
  - name: Checkout Kani
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
  with:
  path: ${{ env.KANI_SRC }}
 
@@ -204,7 +204,7 @@ jobs:
  upload_url: ${{ steps.create_release.outputs.upload_url }}
  steps:
  - name: Checkout code
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
 
  - name: Get version
  run: |
@@ -235,7 +235,7 @@ jobs:
 
  - name: Create release
  id: create_release
- uses: ncipollo/release-action@v1.12.0
+ uses: ncipollo/release-action@v1.13.0
  env:
  GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
  with:
@@ -258,7 +258,7 @@ jobs:
  target: x86_64-unknown-linux-gnu
  steps:
  - name: Checkout code
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
 
  - name: Setup Kani Dependencies
  uses: ./.github/actions/setup
@@ -271,7 +271,7 @@ jobs:
  cargo package -p kani-verifier
 
  - name: 'Login to GitHub Container Registry'
- uses: docker/login-action@v2
+ uses: docker/login-action@v3
  with:
  registry: ghcr.io
  username: ${{ github.repository_owner }}

.github/workflows/slow-tests.yml

@@ -21,7 +21,7 @@ jobs:
  os: [macos-12, ubuntu-20.04, ubuntu-22.04]
  steps:
  - name: Checkout Kani
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
 
  - name: Setup Kani Dependencies
  uses: ./.github/actions/setup

.github/workflows/toolchain-upgrade.yml

@@ -19,7 +19,7 @@ jobs:
  runs-on: ubuntu-22.04
  steps:
  - name: Checkout Kani
- uses: actions/checkout@v3
+ uses: actions/checkout@v4
 
  - name: Setup Kani Dependencies
  uses: ./.github/actions/setup

kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

@@ -425,7 +425,8 @@ impl<'tcx> GotocCtx<'tcx> {
  }
  (Scalar::Ptr(ptr, _size), _) => {
  let res_t = self.codegen_ty(ty);
- let (alloc_id, offset) = ptr.into_parts();
+ let (prov, offset) = ptr.into_parts();
+ let alloc_id = prov.alloc_id();
  self.codegen_alloc_pointer(res_t, alloc_id, offset, span)
  }
  _ => unimplemented!(),
@@ -650,7 +651,8 @@ impl<'tcx> GotocCtx<'tcx> {
  Size::from_bytes(self.symbol_table.machine_model().pointer_width_in_bytes());
 
  let mut next_offset = Size::ZERO;
- for &(offset, alloc_id) in alloc.provenance().ptrs().iter() {
+ for &(offset, prov) in alloc.provenance().ptrs().iter() {
+ let alloc_id = prov.alloc_id();
  if offset > next_offset {
  let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter(
  next_offset.bytes_usize()..offset.bytes_usize(),

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;
@@ -1165,7 +1165,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();
@@ -1228,34 +1228,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,
@@ -552,16 +551,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(..)
@@ -634,13 +626,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

@@ -332,11 +332,11 @@ impl<'tcx> GotocCtx<'tcx> {
  ty: Ty<'tcx>,
  args: ty::GenericArgsRef<'tcx>,
  ) -> ty::PolyFnSig<'tcx> {
- let sig = args.as_coroutine().poly_sig();
+ let sig = args.as_coroutine().sig();
 
- let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(
- sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))),
- );
+ let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(iter::once(
+ ty::BoundVariableKind::Region(ty::BrEnv),
+ ));
  let br = ty::BoundRegion {
  var: ty::BoundVar::from_usize(bound_vars.len() - 1),
  kind: ty::BoundRegionKind::BrEnv,
@@ -349,7 +349,6 @@ impl<'tcx> GotocCtx<'tcx> {
  let pin_args = self.tcx.mk_args(&[env_ty.into()]);
  let env_ty = Ty::new_adt(self.tcx, pin_adt_ref, pin_args);
 
- let sig = sig.skip_binder();
  // The `FnSig` and the `ret_ty` here is for a coroutines main
  // `coroutine::resume(...) -> CoroutineState` function in case we
  // have an ordinary coroutine, or the `Future::poll(...) -> Poll`
@@ -482,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

@@ -139,11 +139,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(