Incrementally update charon submodule with LLBC backend adaptations

Cargo.lock

@@ -257,7 +257,7 @@ checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801"
 
 [[package]]
 name = "charon"
-version = "0.1.62"
+version = "0.1.65"
 dependencies = [
  "annotate-snippets",
  "anstream",
@@ -268,15 +268,17 @@ dependencies = [
  "convert_case",
  "derive_generic_visitor",
  "env_logger",
- "hashlink",
  "index_vec",
+ "indexmap",
  "indoc",
  "itertools 0.13.0",
  "lazy_static",
  "log",
  "macros",
  "nom",
  "nom-supreme",
+ "num-bigint",
+ "num-rational",
  "petgraph 0.6.5",
  "rustc_version",
  "serde",
@@ -803,15 +805,6 @@ dependencies = [
  "petgraph 0.8.3",
 ]
 
-[[package]]
-name = "hashbrown"
-version = "0.14.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1"
-dependencies = [
- "ahash",
-]
-
 [[package]]
 name = "hashbrown"
 version = "0.15.5"
@@ -827,16 +820,6 @@ version = "0.16.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "5419bdc4f6a9207fbeba6d11b604d481addf78ecd10c11ad51e76c2f6482748d"
 
-[[package]]
-name = "hashlink"
-version = "0.9.1"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6ba4ff7128dee98c7dc9794b6a411377e1404dba1c97deb8d1a55297bd25d8af"
-dependencies = [
- "hashbrown 0.14.5",
- "serde",
-]
-
 [[package]]
 name = "heck"
 version = "0.5.0"
@@ -1012,6 +995,8 @@ checksum = "6717a8d2a5a929a1a2eb43a12812498ed141a0bcfb7e8f7844fbdbe4303bba9f"
 dependencies = [
  "equivalent",
  "hashbrown 0.16.0",
+ "serde",
+ "serde_core",
 ]
 
 [[package]]

kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs

@@ -14,7 +14,6 @@ use crate::kani_middle::transform::{BodyTransformation, GlobalPasses};
 use crate::kani_queries::QueryDb;
 use charon_lib::ast::{AnyTransId, TranslatedCrate, meta::ItemOpacity::*, meta::Span};
 use charon_lib::errors::ErrorCtx;
-use charon_lib::errors::error_or_panic;
 use charon_lib::name_matcher::NamePattern;
 use charon_lib::transform::TransformCtx;
 use charon_lib::transform::ctx::{TransformOptions, TransformPass};
@@ -41,6 +40,7 @@ use rustc_session::Session;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
 use rustc_session::output::out_filename;
 use std::any::Any;
+use std::cell::RefCell;
 use std::fs::File;
 use std::path::Path;
 use std::sync::{Arc, Mutex};
@@ -115,12 +115,13 @@ impl LlbcCodegenBackend {
             debug!("Translating: {item:?}");
             match item {
                 MonoItem::Fn(instance) => {
+                    let mut errors_borrow = ccx.errors.borrow_mut();
                     let mut fcx = Context::new(
                         tcx,
                         *instance,
                         &mut ccx.translated,
                         &mut id_map,
-                        &mut ccx.errors,
+                        &mut *errors_borrow,
                     );
                     let _ = fcx.translate();
                 }
@@ -167,7 +168,7 @@ impl LlbcCodegenBackend {
         }
 
         // TODO: display an error report about the external dependencies, if necessary
-        if ccx.errors.error_count > 0 {
+        if ccx.errors.borrow().error_count > 0 {
             todo!()
         }
 
@@ -400,7 +401,7 @@ fn get_transform_options(tcx: &TranslatedCrate, error_ctx: &mut ErrorCtx) -> Tra
         Ok(p) => Ok(p),
         Err(e) => {
             let msg = format!("failed to parse pattern `{s}` ({e})");
-            error_or_panic!(error_ctx, &TranslatedCrate::default(), Span::dummy(), msg)
+            Err(error_ctx.span_err(&TranslatedCrate::default(), Span::dummy(), &msg))
         }
     };
     let options = tcx.options.clone();
@@ -443,6 +444,7 @@ fn get_transform_options(tcx: &TranslatedCrate, error_ctx: &mut ErrorCtx) -> Tra
         no_merge_goto_chains: false,
         item_opacities,
         print_built_llbc: true,
+        remove_associated_types: Vec::new(),
     }
 }
 
@@ -451,5 +453,5 @@ fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx {
     let translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() };
     let mut errors = ErrorCtx::new(true, false);
     let options = get_transform_options(&translated, &mut errors);
-    TransformCtx { options, translated, errors }
+    TransformCtx { options, translated, errors: std::cell::RefCell::new(errors) }
 }

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

@@ -52,7 +52,7 @@ use charon_lib::ullbc_ast::{
     RawTerminator as CharonRawTerminator, Statement as CharonStatement,
     SwitchTargets as CharonSwitchTargets, Terminator as CharonTerminator,
 };
-use charon_lib::{error_assert, error_or_panic};
+use charon_lib::{error_assert, raise_error, register_error};
 use core::panic;
 use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::ty::{TyCtxt, TypingEnv};
@@ -114,8 +114,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         self.tcx
     }
 
-    fn span_err(&mut self, span: CharonSpan, msg: &str) {
-        self.errors.span_err(self.translated, span, msg);
+    fn span_err(&mut self, span: CharonSpan, msg: &str) -> CharonError {
+        self.errors.span_err(self.translated, span, msg)
     }
 
     fn continue_on_failure(&self) -> bool {
@@ -442,7 +442,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             trait_clauses: CharonVector::new(),
             regions_outlive: Vec::new(),
             types_outlive: Vec::new(),
-            trait_type_constraints: Vec::new(),
+            trait_type_constraints: CharonVector::new(),
         }
     }
 
@@ -523,7 +523,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             trait_clauses,
             regions_outlive: Vec::new(),
             types_outlive: Vec::new(),
-            trait_type_constraints: Vec::new(),
+            trait_type_constraints: CharonVector::new(),
         }
     }
 
@@ -595,7 +595,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             trait_clauses,
             regions_outlive: Vec::new(),
             types_outlive: Vec::new(),
-            trait_type_constraints: Vec::new(),
+            trait_type_constraints: CharonVector::new(),
         }
     }
 
@@ -857,7 +857,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                     // block.
                 }
                 _ => {
-                    error_or_panic!(self, span, format!("Unexpected DefPathData: {:?}", data));
+                    raise_error!(self, span, "Unexpected DefPathData: {:?}", data);
                 }
             }
         }
@@ -1000,7 +1000,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                     // block.
                 }
                 _ => {
-                    error_or_panic!(self, span, format!("Unexpected DefPathData: {:?}", data));
+                    raise_error!(self, span, "Unexpected DefPathData: {:?}", data);
                 }
             }
         }
@@ -1106,7 +1106,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                     // block.
                 }
                 _ => {
-                    error_or_panic!(self, span, format!("Unexpected DefPathData: {:?}", data));
+                    raise_error!(self, span, "Unexpected DefPathData: {:?}", data);
                 }
             }
         }
@@ -1253,7 +1253,11 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 },
             };
             let subs_traitref = CharonTraitRef {
-                kind: CharonTraitRefKind::BuiltinOrAuto(subs_traitdeclref.clone()),
+                kind: CharonTraitRefKind::BuiltinOrAuto {
+                    trait_decl_ref: subs_traitdeclref.clone(),
+                    parent_trait_refs: CharonVector::new(),
+                    types: Vec::new(),
+                },
                 trait_decl_ref: subs_traitdeclref,
             };
             trait_refs.push(subs_traitref);
@@ -1488,7 +1492,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
         };
         if let Some(content) = content {
             let span = self.translate_span(stmt.span);
-            return Some(CharonStatement { span, content });
+            return Some(CharonStatement { span, content, comments_before: Vec::new() });
         };
         None
     }
@@ -1559,8 +1563,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
             _ => todo!(),
         };
         (
-            statement.map(|statement| CharonStatement { span, content: statement }),
-            CharonTerminator { span, content: terminator },
+            statement.map(|statement| CharonStatement {
+                span,
+                content: statement,
+                comments_before: Vec::new(),
+            }),
+            CharonTerminator { span, content: terminator, comments_before: Vec::new() },
         )
     }
 

scripts/charon-patch.diff

@@ -4,7 +4,7 @@ index 20f8a9df..a1bf1ee6 100644
 +++ b/charon/Cargo.toml
 @@ -2,7 +2,7 @@
  name = "charon"
- version = "0.1.62"
+ version = "0.1.65"
  authors = ["Son Ho <[email protected]>"]
 -edition = "2021"
 +edition = "2024"
@@ -24,3 +24,16 @@ index 59f7eaab..21508e19 100644
          self.vector.indices()
      }
 
+diff --git a/charon/src/transform/expand_associated_types.rs b/charon/src/transform/expand_associated_types.rs
+index 19978d56..c98c8e0e 100644
+--- a/charon/src/transform/expand_associated_types.rs
++++ b/charon/src/transform/expand_associated_types.rs
+@@ -761,7 +761,7 @@ impl<'a> ComputeItemModifications<'a> {
+         &'b mut self,
+         clause: &TraitClause,
+         clause_to_path: F,
+-    ) -> impl Iterator<Item = AssocTypePath> + use<'b, F>
++    ) -> impl Iterator<Item = AssocTypePath> + use<'a, 'b, F>
+     where
+         F: Fn(TraitClauseId) -> TraitRefPath,
+     {