Update Charon submodule to 2024-11-04

Cargo.lock

@@ -145,18 +145,15 @@ dependencies = [
 
 [[package]]
 name = "bitflags"
-version = "2.6.0"
+version = "1.3.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
+checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
 
 [[package]]
-name = "bitmaps"
-version = "2.1.0"
+name = "bitflags"
+version = "2.6.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "031043d04099746d8db04daf1fa424b2bc8bd69d92b25962dcde24da39ab64a2"
-dependencies = [
- "typenum",
-]
+checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
 
 [[package]]
 name = "brownstone"
@@ -249,7 +246,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
 name = "charon"
-version = "0.1.36"
+version = "0.1.45"
 dependencies = [
  "anyhow",
  "assert_cmd",
@@ -260,7 +257,6 @@ dependencies = [
  "derive-visitor",
  "env_logger",
  "hashlink",
- "im",
  "index_vec",
  "indoc",
  "itertools 0.13.0",
@@ -272,6 +268,7 @@ dependencies = [
  "petgraph",
  "pretty",
  "regex",
+ "rustc_apfloat",
  "rustc_version",
  "serde",
  "serde-map-to-array",
@@ -282,7 +279,7 @@ dependencies = [
  "toml",
  "tracing",
  "tracing-subscriber",
- "tracing-tree 0.3.1",
+ "tracing-tree 0.4.0 (git+https://github.com/Nadrieril/tracing-tree)",
  "which",
 ]
 
@@ -454,7 +451,7 @@ version = "0.27.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f476fe445d41c9e991fd07515a6f463074b782242ccf4a5b7b1d1012e70824df"
 dependencies = [
- "bitflags",
+ "bitflags 2.6.0",
  "crossterm_winapi",
  "libc",
  "parking_lot",
@@ -703,20 +700,6 @@ version = "2.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4"
 
-[[package]]
-name = "im"
-version = "15.1.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "d0acd33ff0285af998aaf9b57342af478078f53492322fafc47450e09397e0e9"
-dependencies = [
- "bitmaps",
- "rand_core",
- "rand_xoshiro",
- "sized-chunks",
- "typenum",
- "version_check",
-]
-
 [[package]]
 name = "indent_write"
 version = "2.2.0"
@@ -814,7 +797,7 @@ dependencies = [
  "syn 2.0.87",
  "tracing",
  "tracing-subscriber",
- "tracing-tree 0.4.0",
+ "tracing-tree 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)",
 ]
 
 [[package]]
@@ -1121,6 +1104,15 @@ dependencies = [
  "autocfg",
 ]
 
+[[package]]
+name = "num_threads"
+version = "0.1.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5c7398b9c8b70908f6371f47ed36737907c87c52af34c268fed0bf0ceb92ead9"
+dependencies = [
+ "libc",
+]
+
 [[package]]
 name = "object"
 version = "0.36.5"
@@ -1329,15 +1321,6 @@ dependencies = [
  "getrandom",
 ]
 
-[[package]]
-name = "rand_xoshiro"
-version = "0.6.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6f97cdb2a36ed4183de61b2f824cc45c9f1037f28afe0a322e9fff4c108b5aaa"
-dependencies = [
- "rand_core",
-]
-
 [[package]]
 name = "rayon"
 version = "1.10.0"
@@ -1364,7 +1347,7 @@ version = "0.5.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9b6dfecf2c74bce2466cabf93f6664d6998a69eb21e39f4207930065b27b771f"
 dependencies = [
- "bitflags",
+ "bitflags 2.6.0",
 ]
 
 [[package]]
@@ -1417,6 +1400,16 @@ version = "0.1.24"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f"
 
+[[package]]
+name = "rustc_apfloat"
+version = "0.2.1+llvm-462a31f5a5ab"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "886d94c63c812a8037c4faca2607453a0fa4cf82f734665266876b022244543f"
+dependencies = [
+ "bitflags 1.3.2",
+ "smallvec",
+]
+
 [[package]]
 name = "rustc_version"
 version = "0.4.1"
@@ -1432,7 +1425,7 @@ version = "0.38.38"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "aa260229e6538e52293eeb577aabd09945a09d6d9cc0fc550ed7529056c2e32a"
 dependencies = [
- "bitflags",
+ "bitflags 2.6.0",
  "errno",
  "libc",
  "linux-raw-sys",
@@ -1600,16 +1593,6 @@ dependencies = [
  "libc",
 ]
 
-[[package]]
-name = "sized-chunks"
-version = "0.6.5"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "16d69225bde7a69b235da73377861095455d298f2b970996eec25ddbb42b3d1e"
-dependencies = [
- "bitmaps",
- "typenum",
-]
-
 [[package]]
 name = "smallvec"
 version = "1.13.2"
@@ -1757,7 +1740,9 @@ checksum = "5dfd88e563464686c916c7e46e623e520ddc6d79fa6641390f2e3fa86e83e885"
 dependencies = [
  "deranged",
  "itoa",
+ "libc",
  "num-conv",
+ "num_threads",
  "powerfmt",
  "serde",
  "time-core",
@@ -1906,9 +1891,9 @@ dependencies = [
 
 [[package]]
 name = "tracing-tree"
-version = "0.3.1"
+version = "0.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b56c62d2c80033cb36fae448730a2f2ef99410fe3ecbffc916681a32f6807dbe"
+checksum = "f459ca79f1b0d5f71c54ddfde6debfc59c8b6eeb46808ae492077f739dc7b49c"
 dependencies = [
  "nu-ansi-term 0.50.1",
  "tracing-core",
@@ -1919,10 +1904,10 @@ dependencies = [
 [[package]]
 name = "tracing-tree"
 version = "0.4.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f459ca79f1b0d5f71c54ddfde6debfc59c8b6eeb46808ae492077f739dc7b49c"
+source = "git+https://github.com/Nadrieril/tracing-tree#841286bfffd3c2200810244506cd127013dbeff9"
 dependencies = [
  "nu-ansi-term 0.50.1",
+ "time",
  "tracing-core",
  "tracing-log",
  "tracing-subscriber",
@@ -1962,12 +1947,6 @@ version = "2.0.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "6af6ae20167a9ece4bcb41af5b80f8a1f1df981f6391189ce00fd257af04126a"
 
-[[package]]
-name = "typenum"
-version = "1.17.0"
-source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825"
-
 [[package]]
 name = "unicode-ident"
 version = "1.0.13"

deny.toml

@@ -23,6 +23,7 @@ confidence-threshold = 0.8
 # All these exceptions should probably appear in: tools/build-kani/license-notes.txt
 exceptions = [
     { name = "unicode-ident", allow=["Unicode-DFS-2016"] },
+    { name = "rustc_apfloat", allow=["Apache-2.0 WITH LLVM-exception"] },
 ]
 
 [licenses.private]
@@ -42,3 +43,4 @@ wildcards = "allow"
 unknown-registry = "deny"
 unknown-git = "deny"
 allow-registry = ["https://github.com/rust-lang/crates.io-index"]
+allow-git = ["https://github.com/Nadrieril/tracing-tree"]

kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs

@@ -12,7 +12,7 @@ use crate::kani_middle::provide;
 use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items};
 use crate::kani_middle::transform::{BodyTransformation, GlobalPasses};
 use crate::kani_queries::QueryDb;
-use charon_lib::ast::TranslatedCrate;
+use charon_lib::ast::{AnyTransId, TranslatedCrate};
 use charon_lib::errors::ErrorCtx;
 use charon_lib::transform::TransformCtx;
 use charon_lib::transform::ctx::TransformOptions;
@@ -24,7 +24,7 @@ use rustc_codegen_ssa::back::archive::{
 use rustc_codegen_ssa::back::link::link_binary;
 use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_codegen_ssa::{CodegenResults, CrateInfo};
-use rustc_data_structures::fx::FxIndexMap;
+use rustc_data_structures::fx::{FxHashMap, FxIndexMap};
 use rustc_errors::{DEFAULT_LOCALE_RESOURCE, ErrorGuaranteed};
 use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE};
 use rustc_metadata::EncodedMetadata;
@@ -106,13 +106,19 @@ impl LlbcCodegenBackend {
 
         // Create a Charon transformation context that will be populated with translation results
         let mut ccx = create_charon_transformation_context(tcx);
+        let mut id_map: FxHashMap<DefId, AnyTransId> = FxHashMap::default();
 
         // Translate all the items
         for item in &items {
             match item {
                 MonoItem::Fn(instance) => {
-                    let mut fcx =
-                        Context::new(tcx, *instance, &mut ccx.translated, &mut ccx.errors);
+                    let mut fcx = Context::new(
+                        tcx,
+                        *instance,
+                        &mut ccx.translated,
+                        &mut id_map,
+                        &mut ccx.errors,
+                    );
                     let _ = fcx.translate();
                 }
                 MonoItem::Static(_def) => todo!(),
@@ -140,7 +146,7 @@ impl LlbcCodegenBackend {
 
         // Run the micro-passes that clean up bodies.
         for pass in charon_lib::transform::ULLBC_PASSES.iter() {
-            pass.transform_ctx(&mut ccx)
+            pass.run(&mut ccx)
         }
 
         // # Go from ULLBC to LLBC (Low-Level Borrow Calculus) by reconstructing
@@ -151,7 +157,7 @@ impl LlbcCodegenBackend {
 
         // Run the micro-passes that clean up bodies.
         for pass in charon_lib::transform::LLBC_PASSES.iter() {
-            pass.transform_ctx(&mut ccx)
+            pass.run(&mut ccx)
         }
 
         // Print the LLBC if requested. This is useful for expected tests.
@@ -161,8 +167,10 @@ impl LlbcCodegenBackend {
             debug!("# Final LLBC before serialization:\n\n{}\n", ccx);
         }
 
-        // Display an error report about the external dependencies, if necessary
-        ccx.errors.report_external_deps_errors();
+        // TODO: display an error report about the external dependencies, if necessary
+        if ccx.errors.error_count > 0 {
+            todo!()
+        }
 
         let crate_data: charon_lib::export::CrateData = charon_lib::export::CrateData::new(&ccx);
 
@@ -393,18 +401,20 @@ fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx {
     let options = TransformOptions {
         no_code_duplication: false,
         hide_marker_traits: false,
+        no_merge_goto_chains: false,
         item_opacities: Vec::new(),
     };
     let crate_name = tcx.crate_name(LOCAL_CRATE).as_str().into();
     let translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() };
     let errors = ErrorCtx {
         continue_on_failure: true,
-        errors_as_warnings: false,
-        dcx: tcx.dcx(),
-        decls_with_errors: HashSet::new(),
+        error_on_warnings: false,
+        dcx: &(),
+        external_decls_with_errors: HashSet::new(),
         ignored_failed_decls: HashSet::new(),
-        dep_sources: HashMap::new(),
+        external_dep_sources: HashMap::new(),
         def_id: None,
+        def_id_is_local: true,
         error_count: 0,
     };
     TransformCtx { options, translated, errors }