Skip to content

Commit dd541be

Browse files
Clone a template BodyTransformer to avoid re-initialization (#4259)
Currently, we have to create a new `BodyTransformer` for each harness individually. However, this takes a lot of time (as we have to constantly re-validate all our Kani functions and reinitialize everything based on the `QueryDb`) and the transformer's options are all shared between harnesses of the same codegen unit anyway. This PR makes the `BodyTransformer` struct `Clone`-able, allowing us to initialize a single 'template' transformer for each codegen unit and then cheaply clone the template for each harness within the unit. Based on testing, the clone takes just ~3µs when using the default # of transformation passes, which is much faster than initialization. ### Results This change made a noticeable **4.8% reduction in the end to end compile time of the standard library** (at std commit [177d0fd](model-checking/verify-rust-std@177d0fd) & assuming #4257 is merged into Kani). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
1 parent 42951d1 commit dd541be

File tree

12 files changed

+96
-22
lines changed

12 files changed

+96
-22
lines changed

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -90,6 +90,7 @@ impl GotocCodegenBackend {
9090
symtab_goto: &Path,
9191
machine_model: &MachineModel,
9292
check_contract: Option<InternalDefId>,
93+
mut global_passes: GlobalPasses,
9394
mut transformer: BodyTransformation,
9495
thread_pool: &ThreadPool,
9596
) -> (MinimalGotocCtx, Vec<MonoItem>, Option<AssignsContract>) {
@@ -119,7 +120,6 @@ impl GotocCodegenBackend {
119120
.collect();
120121

121122
// Apply all transformation passes, including global passes.
122-
let mut global_passes = GlobalPasses::new(&self.queries.lock().unwrap(), tcx);
123123
let any_pass_modified = global_passes.run_global_passes(
124124
&mut transformer,
125125
tcx,
@@ -393,12 +393,17 @@ impl CodegenBackend for GotocCodegenBackend {
393393
let num_harnesses: usize = units.iter().map(|unit| unit.harnesses.len()).sum();
394394
export_thread_pool.add_workers(Self::thread_pool_size(Some(num_harnesses)));
395395

396+
let template_passes = GlobalPasses::new(&queries, tcx);
397+
396398
// Cross-crate collecting of all items that are reachable from the crate harnesses.
397399
for unit in units.iter() {
398400
// We reset the body cache for now because each codegen unit has different
399401
// configurations that affect how we transform the instance body.
402+
403+
// Generate an empty 'template' transformer once per codegen unit and then clone for each harness within.
404+
// (They all share the same options.)
405+
let template_transformer = BodyTransformation::new(&queries, tcx, unit);
400406
for harness in &unit.harnesses {
401-
let transformer = BodyTransformation::new(&queries, tcx, unit);
402407
let model_path = units.harness_model_path(*harness).unwrap();
403408
let is_automatic_harness = units.is_automatic_harness(harness);
404409
let contract_metadata =
@@ -410,7 +415,8 @@ impl CodegenBackend for GotocCodegenBackend {
410415
&results.machine_model,
411416
contract_metadata
412417
.map(|def| rustc_internal::internal(tcx, def.def_id())),
413-
transformer,
418+
template_passes.clone(),
419+
template_transformer.clone_empty(),
414420
&export_thread_pool,
415421
);
416422
if min_gcx.has_loop_contracts {
@@ -450,6 +456,7 @@ impl CodegenBackend for GotocCodegenBackend {
450456
&model_path,
451457
&results.machine_model,
452458
Default::default(),
459+
GlobalPasses::new(&queries, tcx),
453460
transformer,
454461
&export_thread_pool,
455462
);

kani-compiler/src/kani_middle/transform/automatic.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ use tracing::debug;
3030

3131
/// Generate `T::any()` implementations for `T`s that do not implement Arbitrary in source code.
3232
/// Currently limited to structs and enums.
33-
#[derive(Debug)]
33+
#[derive(Debug, Clone)]
3434
pub struct AutomaticArbitraryPass {
3535
/// The FnDef of KaniModel::Any
3636
kani_any: FnDef,
@@ -282,7 +282,7 @@ impl AutomaticArbitraryPass {
282282
}
283283
}
284284
/// Transform the dummy body of an automatic_harness Kani intrinsic to be a proof harness for a given function.
285-
#[derive(Debug)]
285+
#[derive(Debug, Clone)]
286286
pub struct AutomaticHarnessPass {
287287
kani_any: FnDef,
288288
init_contracts_hook: Instance,

kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ use rustc_session::config::OutputType;
3131
mod initial_target_visitor;
3232
mod instrumentation_visitor;
3333

34-
#[derive(Debug)]
34+
#[derive(Debug, Clone)]
3535
pub struct DelayedUbPass {
3636
pub safety_check_type: CheckType,
3737
pub unsupported_check_type: CheckType,

kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ mod uninit_visitor;
2828

2929
/// Top-level pass that instruments the code with checks for uninitialized memory access through raw
3030
/// pointers.
31-
#[derive(Debug)]
31+
#[derive(Debug, Clone)]
3232
pub struct UninitPass {
3333
pub safety_check_type: CheckType,
3434
pub unsupported_check_type: CheckType,

kani-compiler/src/kani_middle/transform/check_values.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ use strum_macros::AsRefStr;
3838
use tracing::{debug, trace};
3939

4040
/// Instrument the code with checks for invalid values.
41-
#[derive(Debug)]
41+
#[derive(Debug, Clone)]
4242
pub struct ValidValuePass {
4343
pub safety_check_type: CheckType,
4444
pub unsupported_check_type: CheckType,

kani-compiler/src/kani_middle/transform/contracts.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ use tracing::{debug, trace};
3131
/// depending on what the type of the input it
3232
///
3333
/// any_modifies is replaced with any
34-
#[derive(Debug)]
34+
#[derive(Debug, Clone)]
3535
pub struct AnyModifiesPass {
3636
kani_any: Option<FnDef>,
3737
kani_any_modifies: Option<FnDef>,
@@ -265,7 +265,7 @@ impl AnyModifiesPass {
265265
/// - Replace the non-used generated closures body with unreachable.
266266
/// 3. Replace the body of `kani_register_contract` by `kani::internal::run_contract_fn` to
267267
/// invoke the closure.
268-
#[derive(Debug, Default)]
268+
#[derive(Debug, Default, Clone)]
269269
pub struct FunctionWithContractPass {
270270
/// Function that is being checked, if any.
271271
check_fn: Option<FnDef>,

kani-compiler/src/kani_middle/transform/dump_mir_pass.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ use std::io::Write;
1717
use super::BodyTransformation;
1818

1919
/// Dump all MIR bodies.
20-
#[derive(Debug)]
20+
#[derive(Debug, Clone)]
2121
pub struct DumpMirPass {
2222
enabled: bool,
2323
}

kani-compiler/src/kani_middle/transform/kani_intrinsics.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ use std::str::FromStr;
3737
use tracing::{debug, trace};
3838

3939
/// Generate the body for a few Kani intrinsics.
40-
#[derive(Debug)]
40+
#[derive(Debug, Clone)]
4141
pub struct IntrinsicGeneratorPass {
4242
unsupported_check_type: CheckType,
4343
/// Used to cache FnDef lookups for models and Kani intrinsics.

kani-compiler/src/kani_middle/transform/loop_contracts.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ use rustc_span::Symbol;
2323
use std::collections::{HashMap, HashSet, VecDeque};
2424
use std::fmt::Debug;
2525

26-
#[derive(Debug, Default)]
26+
#[derive(Debug, Default, Clone)]
2727
pub struct LoopContractPass {
2828
/// Cache KaniRunContract function used to implement contracts.
2929
run_contract_fn: Option<FnDef>,

kani-compiler/src/kani_middle/transform/mod.rs

Lines changed: 73 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ use crate::kani_middle::reachability::CallGraph;
2121
use crate::kani_middle::transform::body::CheckType;
2222
use crate::kani_middle::transform::check_uninit::{DelayedUbPass, UninitPass};
2323
use crate::kani_middle::transform::check_values::ValidValuePass;
24+
use crate::kani_middle::transform::clone::{ClonableGlobalPass, ClonableTransformPass};
2425
use crate::kani_middle::transform::contracts::{AnyModifiesPass, FunctionWithContractPass};
2526
use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass;
2627
use crate::kani_middle::transform::loop_contracts::LoopContractPass;
@@ -58,9 +59,9 @@ mod stubs;
5859
pub struct BodyTransformation {
5960
/// The passes that may change the function body according to harness configuration.
6061
/// The stubbing passes should be applied before so user stubs take precedence.
61-
stub_passes: Vec<Box<dyn TransformPass>>,
62+
stub_passes: Vec<Box<dyn ClonableTransformPass>>,
6263
/// The passes that may add safety checks to the function body.
63-
inst_passes: Vec<Box<dyn TransformPass>>,
64+
inst_passes: Vec<Box<dyn ClonableTransformPass>>,
6465
/// Cache transformation results.
6566
cache: HashMap<Instance, TransformationResult>,
6667
}
@@ -86,7 +87,7 @@ impl BodyTransformation {
8687
transformer.add_pass(
8788
queries,
8889
ValidValuePass {
89-
safety_check_type: safety_check_type.clone(),
90+
safety_check_type,
9091
unsupported_check_type: unsupported_check_type.clone(),
9192
},
9293
);
@@ -139,7 +140,18 @@ impl BodyTransformation {
139140
}
140141
}
141142

142-
fn add_pass<P: TransformPass + 'static>(&mut self, query_db: &QueryDb, pass: P) {
143+
/// Clone an empty [BodyTransformation] for use within the same [CodegenUnit] and [TyCtxt] that were
144+
/// used to create it. Will panic if the transformer has already been queried with `.body()`.
145+
pub fn clone_empty(&self) -> Self {
146+
debug_assert!(self.cache.is_empty());
147+
BodyTransformation {
148+
stub_passes: self.stub_passes.to_vec(),
149+
inst_passes: self.inst_passes.to_vec(),
150+
cache: HashMap::new(),
151+
}
152+
}
153+
154+
fn add_pass<P: ClonableTransformPass + 'static>(&mut self, query_db: &QueryDb, pass: P) {
143155
if pass.is_enabled(query_db) {
144156
match P::transformation_type() {
145157
TransformationType::Instrumentation => self.inst_passes.push(Box::new(pass)),
@@ -199,10 +211,11 @@ enum TransformationResult {
199211
NotModified,
200212
}
201213

214+
#[derive(Clone)]
202215
pub struct GlobalPasses {
203216
/// The passes that operate on the whole codegen unit, they run after all previous passes are
204217
/// done.
205-
global_passes: Vec<Box<dyn GlobalPass>>,
218+
global_passes: Vec<Box<dyn ClonableGlobalPass>>,
206219
}
207220

208221
impl GlobalPasses {
@@ -220,7 +233,7 @@ impl GlobalPasses {
220233
global_passes
221234
}
222235

223-
fn add_global_pass<P: GlobalPass + 'static>(&mut self, query_db: &QueryDb, pass: P) {
236+
fn add_global_pass<P: ClonableGlobalPass + 'static>(&mut self, query_db: &QueryDb, pass: P) {
224237
if pass.is_enabled(query_db) {
225238
self.global_passes.push(Box::new(pass))
226239
}
@@ -249,3 +262,57 @@ impl GlobalPasses {
249262
modified
250263
}
251264
}
265+
266+
mod clone {
267+
//! This is all just machinery to implement `Clone` for a `Box<dyn TransformPass + Clone>`.
268+
//!
269+
//! To avoid circular reasoning, we use two traits that can each clone into a dyn of the other, and since
270+
//! we set both up to have blanket implementations for all `T: TransformPass + Clone`, the compiler pieces them together properly
271+
//! and we can implement `Clone` directly using the pair!
272+
273+
/// Builds a new dyn compatible wrapper trait that's essentially equivalent to extending
274+
/// `$extends` with `Clone`. Requires an ident for an intermediate trait for avoiding cycles
275+
/// in the implementation.
276+
macro_rules! implement_clone {
277+
($new_trait_name: ident, $intermediate_trait_name: ident, $extends: path) => {
278+
#[allow(private_interfaces)]
279+
pub(crate) trait $new_trait_name: $extends {
280+
fn clone_there(&self) -> Box<dyn $intermediate_trait_name>;
281+
}
282+
283+
impl Clone for Box<dyn $new_trait_name> {
284+
fn clone(&self) -> Self {
285+
self.clone_there().clone_back()
286+
}
287+
}
288+
289+
#[allow(private_interfaces)]
290+
impl<T: $extends + Clone + 'static> $new_trait_name for T {
291+
fn clone_there(&self) -> Box<dyn $intermediate_trait_name> {
292+
Box::new(self.clone())
293+
}
294+
}
295+
296+
trait $intermediate_trait_name {
297+
fn clone_back(&self) -> Box<dyn $new_trait_name>;
298+
}
299+
300+
impl<T: $extends + Clone + 'static> $intermediate_trait_name for T {
301+
fn clone_back(&self) -> Box<dyn $new_trait_name> {
302+
Box::new(self.clone())
303+
}
304+
}
305+
};
306+
}
307+
308+
implement_clone!(
309+
ClonableTransformPass,
310+
ClonableTransformPassMid,
311+
crate::kani_middle::transform::TransformPass
312+
);
313+
implement_clone!(
314+
ClonableGlobalPass,
315+
ClonableGlobalPassMid,
316+
crate::kani_middle::transform::GlobalPass
317+
);
318+
}

0 commit comments

Comments
 (0)