Merge branch 'main' into dependabot/cargo/cargo-515e28c4c0

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