diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 5a9f418ab..edaebcdeb 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -287,6 +287,7 @@ dependencies = [ "postcard", "regex", "reqwest", + "rustc-hash", "rustc_trait_elaboration", "rustc_version", "serde", @@ -1979,6 +1980,12 @@ version = "0.1.26" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "56f7d92ca342cea22a06f2121d944b4fd82af56988c270852495420f961d4ace" +[[package]] +name = "rustc-hash" +version = "2.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "94300abf3f1ae2e2b8ffb7b58043de3d399c73fa6f4b73826402a5c457614dbe" + [[package]] name = "rustc_trait_elaboration" version = "0.1.0" diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 9a333eaa7..23bb4e81a 100644 --- a/charon/Cargo.toml +++ b/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 diff --git a/charon/src/ast/hash_cons.rs b/charon/src/ast/hash_cons.rs index f00a9f4cc..52262305a 100644 --- a/charon/src/ast/hash_cons.rs +++ b/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 = IndexMap; + // Only way we create a `HashConsId`. fn fresh_id() -> HashConsId { static ID: AtomicU64 = AtomicU64::new(0); diff --git a/charon/src/bin/charon-driver/driver.rs b/charon/src/bin/charon-driver/driver.rs index da8e95d37..59d855fdc 100644 --- a/charon/src/bin/charon-driver/driver.rs +++ b/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); } diff --git a/charon/src/bin/charon-driver/hax/types/new/full_def.rs b/charon/src/bin/charon-driver/hax/types/new/full_def.rs index ac8f2f85e..f39f2a7f6 100644 --- a/charon/src/bin/charon-driver/hax/types/new/full_def.rs +++ b/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>, diff --git a/charon/src/bin/charon-driver/translate/translate_bodies.rs b/charon/src/bin/charon-driver/translate/translate_bodies.rs index 466510413..61dccf16a 100644 --- a/charon/src/bin/charon-driver/translate/translate_bodies.rs +++ b/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) } } diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 5fbaf221d..abff472fa 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/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; diff --git a/charon/src/common.rs b/charon/src/common.rs index 8ae3e1c52..8c7665783 100644 --- a/charon/src/common.rs +++ b/charon/src/common.rs @@ -97,9 +97,9 @@ impl Default for CycleDetector { } 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`. + /// + /// 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 { - data: HashMap>, + data: FxHashMap>, phantom: PhantomData, }