Performance improvements

charon/Cargo.toml

@@ -84,6 +84,7 @@ flate2 = { version = "1.0.34", optional = true }
 fraction = "0.15.3"
 hashbrown = { version = "0.15.0", default-features = false }
 indexmap = { version = "2.7.1", features = ["serde"] }
+rustc-hash = "2"
 index_vec = { version = "0.1.3", features = ["serde"] }
 indoc = "2"
 itertools.workspace = true

charon/src/ast/hash_cons.rs

@@ -39,7 +39,8 @@ pub struct HashConsId(u64);
 // direct dependency and as a dylib, then the static will be duplicated, causing hashing and
 // equality on `HashCons` to be broken.
 mod intern_table {
-    use indexmap::IndexMap as SeqHashMap;
+    use indexmap::IndexMap;
+    use rustc_hash::FxBuildHasher;
     use std::borrow::Borrow;
     use std::sync::atomic::{AtomicU64, Ordering};
     use std::sync::{Arc, LazyLock, RwLock};
@@ -48,6 +49,10 @@ mod intern_table {
     use crate::common::hash_by_addr::HashByAddr;
     use crate::common::type_map::{Mappable, Mapper, TypeMap};
 
+    // The interner is hot in translation; use FxHash (deterministic and ~5x faster than the
+    // default SipHash for the small-keyed maps charon stresses).
+    type SeqHashMap<K, V> = IndexMap<K, V, FxBuildHasher>;
+
     // Only way we create a `HashConsId`.
     fn fresh_id() -> HashConsId {
         static ID: AtomicU64 = AtomicU64::new(0);

charon/src/bin/charon-driver/driver.rs

@@ -40,6 +40,20 @@ fn set_mir_options(config: &mut Config) {
     }
 }
 
+/// Enable rustc's parallel front-end. The heaviest part of charon's runtime on real crates is
+/// rustc's `check_crate` (typeck + const-eval, ~60% of wall time on const-heavy crates), and
+/// that work is parallelised across body owners. We use at most half the available cores to
+/// leave headroom for the rest of the toolchain (cargo, other charon invocations in a build),
+/// and cap at 8 because returns plateau there in our measurements.
+fn set_parallel_frontend(config: &mut Config) {
+    if config.opts.unstable_opts.threads <= 1 {
+        let available = std::thread::available_parallelism()
+            .map(|n| n.get())
+            .unwrap_or(1);
+        config.opts.unstable_opts.threads = (available / 2).clamp(1, 8);
+    }
+}
+
 /// Don't even try to codegen. This avoids errors due to checking if the output filename is
 /// available (despite the fact that we won't emit it because we stop compilation early).
 fn set_no_codegen(config: &mut Config) {
@@ -82,6 +96,7 @@ fn setup_compiler(config: &mut Config, options: &CliOpts, do_translate: bool) {
         });
 
         set_no_codegen(config);
+        set_parallel_frontend(config);
     }
     set_mir_options(config);
 }

charon/src/bin/charon-driver/hax/types/new/full_def.rs

@@ -928,14 +928,17 @@ where
                 param_env: get_param_env(s, args),
                 ty: self_ty.sinto(s),
                 kind,
-                value: const_value(s, def_id, args_or_default()),
+                // Evaluated lazily by the caller via `const_value()` because const-eval is
+                // expensive and the field is only consumed in the rare MIR-missing fallback path.
+                value: None,
             }
         }
         RDefKind::AssocConst { .. } => FullDefKind::AssocConst {
             param_env: get_param_env(s, args),
             associated_item: AssocItem::sfrom_instantiated(s, &tcx.associated_item(def_id), args),
             ty: type_of_self().sinto(s),
-            value: const_value(s, def_id, args_or_default()),
+            // Same as for `Const`: evaluated lazily.
+            value: None,
         },
         RDefKind::Static {
             safety,
@@ -1343,7 +1346,10 @@ fn get_implied_predicates<'tcx, S: UnderOwnerState<'tcx>>(
     implied_predicates.sinto(s)
 }
 
-fn const_value<'tcx, S: UnderOwnerState<'tcx>>(
+/// Evaluate the value of a `Const` or `AssocConst` item. Used lazily by translation code that
+/// needs the constant value as a fallback when no MIR is available; we avoid running this during
+/// `FullDef` construction because const-eval is one of the largest single costs in translation.
+pub(crate) fn const_value<'tcx, S: UnderOwnerState<'tcx>>(
     s: &S,
     def_id: RDefId,
     args: ty::GenericArgsRef<'tcx>,

charon/src/bin/charon-driver/translate/translate_bodies.rs

@@ -154,16 +154,20 @@ impl<'tcx> ItemTransCtx<'tcx, '_> {
         // Retrieve the body
         if let Some(body) = self.get_mir(def.this(), span)? {
             Ok(self.translate_body(span, body, &def.source_text))
-        } else {
-            if let hax::FullDefKind::Const { value, .. }
-            | hax::FullDefKind::AssocConst { value, .. } = def.kind()
-                && let Some(value) = value
+        } else if matches!(
+            def.kind(),
+            hax::FullDefKind::Const { .. } | hax::FullDefKind::AssocConst { .. }
+        ) {
+            // For globals without MIR we generate a body by evaluating the constant.
+            // Const-eval is expensive, so we run it here only when MIR is actually missing
+            // (instead of eagerly in `translate_full_def_kind`, where the result was rarely used).
+            let s = self.hax_state_with_id();
+            let item = def.this();
+            let rust_def_id = item.def_id.as_def_id_even_synthetic();
+            let args = item.rustc_args(s);
+            if let Some(value) = crate::hax::const_value(s, rust_def_id, args)
             {
-                // For globals we can generate a body by evaluating the global.
-                // TODO: we lost the MIR of some consts on a rustc update. A trait assoc const
-                // default value no longer has a cross-crate MIR so it's unclear how to retreive
-                // the value. See the `trait-default-const-cross-crate` test.
-                let c = self.translate_constant_expr(span, value)?;
+                let c = self.translate_constant_expr(span, &value)?;
                 let mut bb = BodyBuilder::new(span, 0);
                 let ret = bb.new_var(None, c.ty.clone());
                 bb.push_statement(StatementKind::Assign(
@@ -174,6 +178,8 @@ impl<'tcx> ItemTransCtx<'tcx, '_> {
             } else {
                 Ok(Body::Missing)
             }
+        } else {
+            Ok(Body::Missing)
         }
     }
 

charon/src/bin/charon-driver/translate/translate_ctx.rs

@@ -11,7 +11,8 @@ use charon_lib::options::TranslateOptions;
 use rustc_middle::ty::TyCtxt;
 use std::borrow::Cow;
 use std::cell::RefCell;
-use std::collections::{HashMap, HashSet, VecDeque};
+use rustc_hash::{FxHashMap as HashMap, FxHashSet as HashSet};
+use std::collections::VecDeque;
 use std::fmt::Debug;
 use std::ops::{Deref, DerefMut};
 use std::path::PathBuf;

charon/src/common.rs

@@ -97,9 +97,9 @@ impl<T> Default for CycleDetector<T> {
 }
 
 pub mod type_map {
+    use rustc_hash::FxHashMap;
     use std::{
         any::{Any, TypeId},
-        collections::HashMap,
         marker::PhantomData,
     };
 
@@ -111,8 +111,12 @@ pub mod type_map {
 
     /// A map that maps types to values in a generic manner: we store for each type `T` a value of
     /// type `M::Value<T>`.
+    ///
+    /// We use `FxHashMap` because this map is on the hot interning path and the default
+    /// `SipHash` shows up in profiles; the keys are `TypeId`s, which already encode 128 bits of
+    /// well-distributed entropy, so a faster hash is fine.
     pub struct TypeMap<M> {
-        data: HashMap<TypeId, Box<dyn Mappable>>,
+        data: FxHashMap<TypeId, Box<dyn Mappable>>,
         phantom: PhantomData<M>,
     }