Merge branch 'main' into dependabot/github_actions/ncipollo/release-a…

…ction-1.13.0

.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: |
@@ -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 }}
@@ -284,7 +284,7 @@ jobs:
  OWNER: '${{ github.repository_owner }}'
 
  - name: Build and push
- uses: docker/build-push-action@v3
+ uses: docker/build-push-action@v5
  with:
  context: .
  file: scripts/ci/Dockerfile.bundle-release-20-04

.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/intrinsic.rs

@@ -1729,7 +1729,7 @@ impl<'tcx> GotocCtx<'tcx> {
  // [u32; n]: translated wrapped in a struct
  let indexes = fargs.remove(0);
 
- let (_, vec_subtype) = rust_arg_types[0].simd_size_and_type(self.tcx);
+ let (in_type_len, vec_subtype) = rust_arg_types[0].simd_size_and_type(self.tcx);
  let (ret_type_len, ret_type_subtype) = rust_ret_type.simd_size_and_type(self.tcx);
  if ret_type_len != n {
  let err_msg = format!(
@@ -1749,7 +1749,7 @@ impl<'tcx> GotocCtx<'tcx> {
  // An unsigned type here causes an invariant violation in CBMC.
  // Issue: https://github.com/diffblue/cbmc/issues/6298
  let st_rep = Type::ssize_t();
- let n_rep = Expr::int_constant(n, st_rep.clone());
+ let n_rep = Expr::int_constant(in_type_len, st_rep.clone());
 
  // P = indexes.expanded_map(v -> if v < N then vec1[v] else vec2[v-N])
  let elems = (0..n)

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

@@ -421,7 +421,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!(),
@@ -646,7 +647,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;
@@ -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/span.rs

@@ -5,9 +5,10 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Location;
-use rustc_middle::mir::{Local, VarDebugInfo, VarDebugInfoContents};
+use rustc_middle::mir::{Local, VarDebugInfoContents};
 use rustc_smir::rustc_internal;
 use rustc_span::Span;
+use stable_mir::mir::VarDebugInfo;
 
 impl<'tcx> GotocCtx<'tcx> {
  pub fn codegen_span(&self, sp: &Span) -> Location {
@@ -43,10 +44,12 @@ impl<'tcx> GotocCtx<'tcx> {
  sp.map_or(Location::none(), |x| self.codegen_span(&x))
  }
 
- pub fn find_debug_info(&self, l: &Local) -> Option<&VarDebugInfo<'tcx>> {
- self.current_fn().mir().var_debug_info.iter().find(|info| match info.value {
- VarDebugInfoContents::Place(p) => p.local == *l && p.projection.len() == 0,
- VarDebugInfoContents::Const(_) => false,
- })
+ pub fn find_debug_info(&self, l: &Local) -> Option<VarDebugInfo> {
+ rustc_internal::stable(self.current_fn().mir().var_debug_info.iter().find(|info| {
+ match info.value {
+ VarDebugInfoContents::Place(p) => p.local == *l && p.projection.len() == 0,
+ VarDebugInfoContents::Const(_) => false,
+ }
+ }))
  }
 }

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