Merge branch 'main' into slice-init-shadow

.github/workflows/kani.yml

@@ -17,7 +17,7 @@ jobs:
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:
-        os: [macos-13, ubuntu-20.04, ubuntu-22.04]
+        os: [macos-13, ubuntu-20.04, ubuntu-22.04, macos-14]
     steps:
       - name: Checkout Kani
         uses: actions/checkout@v4

.github/workflows/release.yml

@@ -44,6 +44,32 @@ jobs:
           os: macos-13
           arch: x86_64-apple-darwin
 
+  build_bundle_macos_aarch64:
+    name: BuildBundle-MacOs-ARM
+    runs-on: macos-14
+    permissions:
+      contents: write
+    outputs:
+      version: ${{ steps.bundle.outputs.version }}
+      bundle: ${{ steps.bundle.outputs.bundle }}
+      package: ${{ steps.bundle.outputs.package }}
+      crate_version: ${{ steps.bundle.outputs.crate_version }}
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v4
+
+      - name: Setup Kani Dependencies
+        uses: ./.github/actions/setup
+        with:
+          os: macos-14
+
+      - name: Build bundle
+        id: bundle
+        uses: ./.github/actions/build-bundle
+        with:
+          os: macos-14
+          arch: aarch64-apple-darwin
+
   build_bundle_linux:
     name: BuildBundle-Linux
     runs-on: ubuntu-20.04
@@ -82,7 +108,7 @@ jobs:
             build-essential bash-completion curl lsb-release sudo g++ gcc flex \
             bison make patch git python3.7 python3.7-dev python3.7-distutils
           update-alternatives --install /usr/bin/python3 python3 /usr/bin/python3.7 1
-          curl -s https://bootstrap.pypa.io/get-pip.py -o get-pip.py
+          curl -s https://bootstrap.pypa.io/pip/3.7/get-pip.py -o get-pip.py
           python3 get-pip.py --force-reinstall
           rm get-pip.py
 
@@ -180,7 +206,7 @@ jobs:
 
       - name: Run cargo-kani tests after moving
         run: |
-          for dir in function multiple-harnesses verbose; do
+          for dir in supported-lib-types/rlib multiple-harnesses verbose; do
             >&2 echo "Running test $dir"
             pushd ${{ github.workspace }}/../post-setup-tests/cargo-ui/$dir
             cargo kani
@@ -384,7 +410,7 @@ jobs:
           OWNER: '${{ github.repository_owner }}'
 
       - name: Build and push
-        uses: docker/build-push-action@v5
+        uses: docker/build-push-action@v6
         with:
           context: .
           file: scripts/ci/Dockerfile.bundle-release-20-04

Cargo.lock

@@ -140,19 +140,19 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
 name = "clap"
-version = "4.5.6"
+version = "4.5.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a9689a29b593160de5bc4aacab7b5d54fb52231de70122626c178e6a368994c7"
+checksum = "5db83dced34638ad474f39f250d7fea9598bdd239eaced1bdf45d597da0f433f"
 dependencies = [
  "clap_builder",
  "clap_derive",
 ]
 
 [[package]]
 name = "clap_builder"
-version = "4.5.6"
+version = "4.5.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "2e5387378c84f6faa26890ebf9f0a92989f8873d4d380467bcd0d8d8620424df"
+checksum = "f7e204572485eb3fbf28f871612191521df159bc3e15a9f5064c66dba3a8c05f"
 dependencies = [
  "anstream",
  "anstyle",
@@ -390,9 +390,9 @@ checksum = "f8478577c03552c21db0e2724ffb8986a5ce7af88107e6be5d2ee6e158c12800"
 
 [[package]]
 name = "itertools"
-version = "0.12.1"
+version = "0.13.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "ba291022dbbd398a455acf126c1e341954079855bc60dfdda641363bd6922569"
+checksum = "413ee7dfc52ee1a4949ceeb7dbc8a33f2d6c088194d9f922fb8318faf1f01186"
 dependencies = [
  "either",
 ]
@@ -470,7 +470,7 @@ dependencies = [
 
 [[package]]
 name = "kani_core"
-version = "0.51.0"
+version = "0.52.0"
 dependencies = [
  "kani_macros",
 ]
@@ -551,9 +551,9 @@ dependencies = [
 
 [[package]]
 name = "memchr"
-version = "2.7.2"
+version = "2.7.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6c8640c5d730cb13ebd907d8d04b52f55ac9a2eec55b440c8892f40d56c76c1d"
+checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3"
 
 [[package]]
 name = "memuse"
@@ -801,9 +801,9 @@ dependencies = [
 
 [[package]]
 name = "redox_syscall"
-version = "0.5.1"
+version = "0.5.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "469052894dcb553421e483e4209ee581a45100d31b4018de03e5a7ad86374a7e"
+checksum = "c82cf8cff14456045f55ec4241383baeff27af886adb72ffb2162f99911de0fd"
 dependencies = [
  "bitflags",
 ]
@@ -999,9 +999,9 @@ dependencies = [
 
 [[package]]
 name = "string-interner"
-version = "0.15.0"
+version = "0.17.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "07f9fdfdd31a0ff38b59deb401be81b73913d76c9cc5b1aed4e1330a223420b9"
+checksum = "1c6a0d765f5807e98a091107bae0a56ea3799f66a5de47b2c84c94a39c09974e"
 dependencies = [
  "cfg-if",
  "hashbrown",

cprover_bindings/Cargo.toml

@@ -17,7 +17,7 @@ lazy_static = "1.4.0"
 num = "0.4.0"
 num-traits = "0.2"
 serde = {version = "1", features = ["derive"]}
-string-interner = "0.15.0"
+string-interner = "0.17.0"
 tracing = "0.1"
 linear-map = {version = "1.2", features = ["serde_impl"]}
 

cprover_bindings/src/goto_program/expr.rs

@@ -140,6 +140,7 @@ pub enum ExprValue {
     /// `({ op1; op2; ...})`
     StatementExpression {
         statements: Vec<Stmt>,
+        location: Location,
     },
     /// A raw string constant. Note that you normally actually want a pointer to the first element.
     /// `"s"`
@@ -739,10 +740,10 @@ impl Expr {
     /// <https://gcc.gnu.org/onlinedocs/gcc/Statement-Exprs.html>
     /// e.g. `({ int y = foo (); int z; if (y > 0) z = y; else z = - y; z; })`
     /// `({ op1; op2; ...})`
-    pub fn statement_expression(ops: Vec<Stmt>, typ: Type) -> Self {
+    pub fn statement_expression(ops: Vec<Stmt>, typ: Type, loc: Location) -> Self {
         assert!(!ops.is_empty());
         assert_eq!(ops.last().unwrap().get_expression().unwrap().typ, typ);
-        expr!(StatementExpression { statements: ops }, typ)
+        expr!(StatementExpression { statements: ops, location: loc }, typ).with_location(loc)
     }
 
     /// Internal helper function for Struct initalizer

cprover_bindings/src/irep/to_irep.rs

@@ -299,9 +299,9 @@ impl ToIrep for ExprValue {
                 named_sub: linear_map![],
             },
             ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]),
-            ExprValue::StatementExpression { statements: ops } => side_effect_irep(
+            ExprValue::StatementExpression { statements: ops, location: loc } => side_effect_irep(
                 IrepId::StatementExpression,
-                vec![Stmt::block(ops.to_vec(), Location::none()).to_irep(mm)],
+                vec![Stmt::block(ops.to_vec(), *loc).to_irep(mm)],
             ),
             ExprValue::StringConstant { s } => Irep {
                 id: IrepId::StringConstant,

docs/src/usage.md

@@ -80,10 +80,11 @@ For more information please consult this [blog post](https://blog.rust-lang.org/
 
 ## The build process
 
-When Kani builds your code, it does two important things:
+When Kani builds your code, it does three important things:
 
-1. It sets `cfg(kani)`.
+1. It sets `cfg(kani)` for target crate compilation (including dependencies).
 2. It injects the `kani` crate.
+3. It sets `cfg(kani_host)` for host build targets such as any build script and procedural macro crates.
 
 A proof harness (which you can [learn more about in the tutorial](./kani-tutorial.md)), is a function annotated with `#[kani::proof]` much like a test is annotated with `#[test]`.
 But you may experience a similar problem using Kani as you would with `dev-dependencies`: if you try writing `#[kani::proof]` directly in your code, `cargo build` will fail because it doesn't know what the `kani` crate is.

kani-compiler/Cargo.toml

@@ -12,7 +12,7 @@ publish = false
 cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true }
 clap = { version = "4.4.11", features = ["derive", "cargo"] }
 home = "0.5"
-itertools = "0.12"
+itertools = "0.13"
 kani_metadata = {path = "../kani_metadata"}
 lazy_static = "1.4.0"
 num = { version = "0.4.0", optional = true }

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

@@ -252,7 +252,7 @@ impl<'tcx> GotocCtx<'tcx> {
             t.nondet().as_stmt(loc),
         ];
 
-        Expr::statement_expression(body, t).with_location(loc)
+        Expr::statement_expression(body, t, loc)
     }
 
     /// Kani does not currently support all MIR constructs.
@@ -356,7 +356,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     // Encode __CPROVER_r_ok(ptr, size).
                     // First, generate a CBMC expression representing the pointer.
                     let ptr = {
-                        let ptr_projection = self.codegen_place_stable(&ptr_place).unwrap();
+                        let ptr_projection = self.codegen_place_stable(&ptr_place, *loc).unwrap();
                         let place_ty = self.place_ty_stable(place);
                         if self.use_thin_pointer_stable(place_ty) {
                             ptr_projection.goto_expr().clone()

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

@@ -3,7 +3,7 @@
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::kani_middle::attributes::KaniAttributes;
 use cbmc::goto_program::FunctionContract;
-use cbmc::goto_program::Lambda;
+use cbmc::goto_program::{Lambda, Location};
 use kani_metadata::AssignsContract;
 use rustc_hir::def_id::DefId as InternalDefId;
 use rustc_smir::rustc_internal;
@@ -47,6 +47,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             _ => None,
         });
+
         let recursion_tracker_def = recursion_tracker
             .next()
             .expect("There should be at least one recursion tracker (REENTRY) in scope");
@@ -94,7 +95,7 @@ impl<'tcx> GotocCtx<'tcx> {
             vec![]
         });
         self.attach_modifies_contract(instance_of_check, assigns_contract);
-        let wrapper_name = self.symbol_name_stable(instance_of_check);
+        let wrapper_name = instance_of_check.mangled_name();
 
         AssignsContract {
             recursion_tracker: full_recursion_tracker_name,
@@ -104,7 +105,11 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Convert the Kani level contract into a CBMC level contract by creating a
     /// CBMC lambda.
-    fn codegen_modifies_contract(&mut self, modified_places: Vec<Local>) -> FunctionContract {
+    fn codegen_modifies_contract(
+        &mut self,
+        modified_places: Vec<Local>,
+        loc: Location,
+    ) -> FunctionContract {
         let goto_annotated_fn_name = self.current_fn().name();
         let goto_annotated_fn_typ = self
             .symbol_table
@@ -119,7 +124,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 Lambda::as_contract_for(
                     &goto_annotated_fn_typ,
                     None,
-                    self.codegen_place_stable(&local.into()).unwrap().goto_expr.dereference(),
+                    self.codegen_place_stable(&local.into(), loc).unwrap().goto_expr.dereference(),
                 )
             })
             .collect();
@@ -137,7 +142,8 @@ impl<'tcx> GotocCtx<'tcx> {
         assert!(self.current_fn.is_none());
         let body = instance.body().unwrap();
         self.set_current_fn(instance, &body);
-        let goto_contract = self.codegen_modifies_contract(modified_places);
+        let goto_contract =
+            self.codegen_modifies_contract(modified_places, self.codegen_span_stable(body.span));
         let name = self.current_fn().name();
 
         self.symbol_table.attach_contract(name, goto_contract);

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

@@ -49,7 +49,8 @@ impl<'tcx> GotocCtx<'tcx> {
     /// handled later.
     pub fn codegen_foreign_fn(&mut self, instance: Instance) -> &Symbol {
         debug!(?instance, "codegen_foreign_function");
-        let fn_name = self.symbol_name_stable(instance).intern();
+        let fn_name = instance.mangled_name().intern();
+        let loc = self.codegen_span_stable(instance.def.span());
         if self.symbol_table.contains(fn_name) {
             // Symbol has been added (either a built-in CBMC function or a Rust allocation function).
             self.symbol_table.lookup(fn_name).unwrap()
@@ -63,8 +64,7 @@ impl<'tcx> GotocCtx<'tcx> {
             // https://github.com/model-checking/kani/issues/2426
             self.ensure(fn_name, |gcx, _| {
                 let typ = gcx.codegen_ffi_type(instance);
-                Symbol::function(fn_name, typ, None, instance.name(), Location::none())
-                    .with_is_extern(true)
+                Symbol::function(fn_name, typ, None, instance.name(), loc).with_is_extern(true)
             })
         } else {
             let shim_name = format!("{fn_name}_ffi_shim");
@@ -77,7 +77,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     typ,
                     Some(gcx.codegen_ffi_shim(shim_name.as_str().into(), instance)),
                     instance.name(),
-                    Location::none(),
+                    loc,
                 )
             })
         }
@@ -109,7 +109,7 @@ impl<'tcx> GotocCtx<'tcx> {
         } else {
             let ret_expr = unwrap_or_return_codegen_unimplemented_stmt!(
                 self,
-                self.codegen_place_stable(ret_place)
+                self.codegen_place_stable(ret_place, loc)
             )
             .goto_expr;
             let ret_type = ret_expr.typ().clone();
@@ -134,7 +134,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Generate type for the given foreign instance.
     fn codegen_ffi_type(&mut self, instance: Instance) -> Type {
-        let fn_name = self.symbol_name_stable(instance);
+        let fn_name = instance.mangled_name();
         let fn_abi = instance.fn_abi().unwrap();
         let loc = self.codegen_span_stable(instance.def.span());
         let params = fn_abi
@@ -166,7 +166,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// This will behave like `codegen_unimplemented_stmt` but print a message that includes
     /// the name of the function not supported and the calling convention.
     fn codegen_ffi_unsupported(&mut self, instance: Instance, loc: Location) -> Stmt {
-        let fn_name = &self.symbol_name_stable(instance);
+        let fn_name = &instance.mangled_name();
         debug!(?fn_name, ?loc, "codegen_ffi_unsupported");
 
         // Save this occurrence so we can emit a warning in the compilation report.

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

@@ -52,7 +52,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn codegen_function(&mut self, instance: Instance) {
-        let name = self.symbol_name_stable(instance);
+        let name = instance.mangled_name();
         let old_sym = self.symbol_table.lookup(&name).unwrap();
 
         let _trace_span = debug_span!("CodegenFunction", name = instance.name()).entered();
@@ -204,7 +204,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let body = self.transformer.body(self.tcx, instance);
         self.set_current_fn(instance, &body);
         debug!(krate=?instance.def.krate(), is_std=self.current_fn().is_std(), "declare_function");
-        self.ensure(self.symbol_name_stable(instance), |ctx, fname| {
+        self.ensure(instance.mangled_name(), |ctx, fname| {
             Symbol::function(
                 fname,
                 ctx.fn_typ(instance, &body),