From b59856d918a8f718f68a7bb5f4e2bdf568008d61 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 5 Sep 2025 11:25:00 -0700 Subject: [PATCH 1/3] Fix LLBC regressions --- .github/workflows/kani.yml | 7 +++++ .../codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 3 ++- scripts/charon.patch | 26 +++++++++++++++++++ 3 files changed, 35 insertions(+), 1 deletion(-) create mode 100644 scripts/charon.patch diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index bc2750e8d56b..7238bd05290e 100644 --- a/.github/workflows/kani.yml +++ b/.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 + - name: Build Kani with Charon run: cargo build-dev -- --features cprover --features llbc diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs index c9a980b25f22..60f2e0f6a101 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs +++ b/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) diff --git a/scripts/charon.patch b/scripts/charon.patch new file mode 100644 index 000000000000..543be483244d --- /dev/null +++ b/scripts/charon.patch @@ -0,0 +1,26 @@ +diff --git a/charon/Cargo.toml b/charon/Cargo.toml +index 20f8a9df..a1bf1ee6 100644 +--- a/charon/Cargo.toml ++++ b/charon/Cargo.toml +@@ -2,7 +2,7 @@ + name = "charon" + version = "0.1.62" + authors = ["Son Ho "] +-edition = "2021" ++edition = "2024" + license = "Apache-2.0" + + [lib] +diff --git a/charon/src/ids/vector.rs b/charon/src/ids/vector.rs +index 59f7eaab..21508e19 100644 +--- a/charon/src/ids/vector.rs ++++ b/charon/src/ids/vector.rs +@@ -217,7 +217,7 @@ where + self.iter_indexed().map(|(id, _)| id) + } + +- pub fn all_indices(&self) -> impl Iterator { ++ pub fn all_indices(&self) -> impl Iterator + use { + self.vector.indices() + } + From 8c646f0e1289b16794d77e03bef04e305fe5e712 Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 5 Sep 2025 11:46:33 -0700 Subject: [PATCH 2/3] Rename patch file to skip copyright check --- scripts/{charon.patch => charon-patch.diff} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename scripts/{charon.patch => charon-patch.diff} (100%) diff --git a/scripts/charon.patch b/scripts/charon-patch.diff similarity index 100% rename from scripts/charon.patch rename to scripts/charon-patch.diff From 70985798da002c89e9aad01d10fae7486cdfb30d Mon Sep 17 00:00:00 2001 From: Zyad Hassan Date: Fri, 5 Sep 2025 12:06:22 -0700 Subject: [PATCH 3/3] Update filename --- .github/workflows/kani.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 7238bd05290e..911a09eac496 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -113,7 +113,7 @@ jobs: # 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 + run: cd charon && git apply ../scripts/charon-patch.diff - name: Build Kani with Charon run: cargo build-dev -- --features cprover --features llbc