Merge branch 'main' into bounded-boxed-slice

Author: zhassan-aws

.github/workflows/kani.yml

@@ -108,6 +108,13 @@ jobs:
         with:
           os: ubuntu-24.04
 
+      # Patch Charon so that it compiles. This is temporary until we're able to
+      # upgrade the pinned commit which requires fixing
+      # https://github.com/AeneasVerif/charon/issues/806 and updating the
+      # mir-to-ullbc code
+      - name: Patch Charon
+        run: cd charon && git apply ../scripts/charon-patch.diff
+
       - name: Build Kani with Charon
         run: cargo build-dev -- --features cprover --features llbc
 

.github/workflows/release.yml

@@ -319,7 +319,7 @@ jobs:
 
       - name: Create release
         id: create_release
-        uses: ncipollo/release-action@v1.19.1
+        uses: ncipollo/release-action@v1.20.0
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
         with:

Cargo.lock

@@ -217,12 +217,6 @@ version = "3.19.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "46c5e41b57b8bba42a04676d81cb89e9ee8e859a1a66f80a5a72e1cb76b34d43"
 
-[[package]]
-name = "byteorder"
-version = "1.5.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b"
-
 [[package]]
 name = "bytes"
 version = "1.10.1"
@@ -466,12 +460,12 @@ checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b"
 name = "cprover_bindings"
 version = "0.65.0"
 dependencies = [
- "fxhash",
  "lazy_static",
  "linear-map",
  "memuse",
  "num",
  "num-traits",
+ "rustc-hash",
  "serde",
  "serde_test",
  "string-interner",
@@ -752,15 +746,6 @@ dependencies = [
  "percent-encoding",
 ]
 
-[[package]]
-name = "fxhash"
-version = "0.2.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c31b6d751ae2c7f11320402d34e41349dd1016f8d5d45e48c4312bc8625af50c"
-dependencies = [
- "byteorder",
-]
-
 [[package]]
 name = "getopts"
 version = "0.2.24"
@@ -1113,7 +1098,6 @@ dependencies = [
  "charon",
  "clap",
  "cprover_bindings",
- "fxhash",
  "itertools 0.14.0",
  "kani_metadata",
  "lazy_static",
@@ -1748,6 +1732,12 @@ version = "0.1.26"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "56f7d92ca342cea22a06f2121d944b4fd82af56988c270852495420f961d4ace"
 
+[[package]]
+name = "rustc-hash"
+version = "2.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "357703d41365b4b27c590e3ed91eabb1b663f07c4c084095e60cbed4362dff0d"
+
 [[package]]
 name = "rustc_version"
 version = "0.4.1"

cprover_bindings/Cargo.toml

@@ -20,7 +20,7 @@ serde = {version = "1", features = ["derive"]}
 string-interner = "0.19"
 tracing = "0.1"
 linear-map = {version = "1.2", features = ["serde_impl"]}
-fxhash = "0.2.1"
+rustc-hash = "2.1.1"
 
 [dev-dependencies]
 serde_test = "1"

cprover_bindings/src/irep/goto_binary_serde.rs

@@ -81,7 +81,7 @@
 use crate::irep::{Irep, IrepId, Symbol, SymbolTable};
 use crate::{InternString, InternedString};
 #[cfg(not(test))]
-use fxhash::FxHashMap;
+use rustc_hash::FxHashMap;
 #[cfg(test)]
 use std::collections::HashMap;
 use std::fs::File;

kani-compiler/Cargo.toml

@@ -12,7 +12,6 @@ publish = false
 cbmc = { path = "../cprover_bindings", package = "cprover_bindings", optional = true }
 charon = { path = "../charon/charon", optional = true, default-features = false } 
 clap = { version = "4.4.11", features = ["derive", "cargo"] }
-fxhash = "0.2.1"
 itertools = "0.14"
 kani_metadata = { path = "../kani_metadata" }
 lazy_static = "1.5.0"

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

@@ -69,6 +69,7 @@ use rustc_public::ty::{
     Ty, TyConst, TyConstKind, TyKind, UintTy,
 };
 use rustc_public::{CrateDef, CrateDefType, DefId};
+use rustc_public_bridge::IndexedVal;
 use std::collections::HashMap;
 use std::iter::zip;
 use std::path::PathBuf;
@@ -1009,7 +1010,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             name.push(CharonPathElem::Ident(crate_name, CharonDisambiguator::new(0)));
         }
 
-        if let Some(impl_defid_internal) = self.tcx.impl_of_method(def_id) {
+        if let Some(impl_defid_internal) = self.tcx.impl_of_assoc(def_id) {
             let traitref = self
                 .tcx
                 .impl_trait_ref(impl_defid_internal)

kani-compiler/src/kani_middle/attributes.rs

@@ -4,10 +4,10 @@
 
 use std::collections::{BTreeMap, HashSet};
 
-use fxhash::FxHashMap;
 use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub};
 use quote::ToTokens;
 use rustc_ast::{LitKind, MetaItem, MetaItemKind};
+use rustc_data_structures::fx::FxHashMap;
 use rustc_errors::ErrorGuaranteed;
 use rustc_hir::{
     AttrArgs, Attribute,

kani-compiler/src/kani_middle/codegen_units.rs

@@ -17,12 +17,12 @@ use crate::kani_middle::reachability::filter_crate_items;
 use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map};
 use crate::kani_middle::{can_derive_arbitrary, implements_arbitrary};
 use crate::kani_queries::QueryDb;
-use fxhash::{FxHashMap, FxHashSet};
 use kani_metadata::{
     ArtifactType, AssignsContract, AutoHarnessMetadata, AutoHarnessSkipReason, HarnessMetadata,
     KaniMetadata, find_proof_harnesses,
 };
 use regex::RegexSet;
+use rustc_data_structures::fx::{FxHashMap, FxHashSet};
 use rustc_hir::def_id::DefId;
 use rustc_middle::ty::TyCtxt;
 use rustc_public::mir::mono::Instance;

kani-compiler/src/kani_middle/mod.rs

@@ -6,7 +6,7 @@
 use std::collections::HashSet;
 
 use crate::kani_queries::QueryDb;
-use fxhash::FxHashMap;
+use rustc_data_structures::fx::FxHashMap;
 use rustc_hir::{def::DefKind, def_id::DefId as InternalDefId, def_id::LOCAL_CRATE};
 use rustc_middle::ty::TyCtxt;
 use rustc_public::mir::TerminatorKind;