From 541fbf8a2e85f8f2a71979d1ff174d08d5157ed6 Mon Sep 17 00:00:00 2001 From: AlexanderPortland Date: Thu, 31 Jul 2025 15:02:06 -0700 Subject: [PATCH 1/3] make `Box` cloneable --- .../src/kani_middle/transform/automatic.rs | 4 +- .../transform/check_uninit/ptr_uninit/mod.rs | 2 +- .../src/kani_middle/transform/check_values.rs | 2 +- .../src/kani_middle/transform/contracts.rs | 4 +- .../kani_middle/transform/kani_intrinsics.rs | 2 +- .../kani_middle/transform/loop_contracts.rs | 2 +- .../src/kani_middle/transform/mod.rs | 46 +++++++++++++++++-- .../kani_middle/transform/rustc_intrinsics.rs | 2 +- .../src/kani_middle/transform/stubs.rs | 4 +- 9 files changed, 53 insertions(+), 15 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs index 922958f3d1d4..882d6f6e1858 100644 --- a/kani-compiler/src/kani_middle/transform/automatic.rs +++ b/kani-compiler/src/kani_middle/transform/automatic.rs @@ -30,7 +30,7 @@ use tracing::debug; /// Generate `T::any()` implementations for `T`s that do not implement Arbitrary in source code. /// Currently limited to structs and enums. -#[derive(Debug)] +#[derive(Debug, Clone)] pub struct AutomaticArbitraryPass { /// The FnDef of KaniModel::Any kani_any: FnDef, @@ -262,7 +262,7 @@ impl AutomaticArbitraryPass { } } /// Transform the dummy body of an automatic_harness Kani intrinsic to be a proof harness for a given function. -#[derive(Debug)] +#[derive(Debug, Clone)] pub struct AutomaticHarnessPass { kani_any: FnDef, init_contracts_hook: Instance, diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs index 9dbe109658cc..f2fa19909cbc 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/mod.rs @@ -28,7 +28,7 @@ mod uninit_visitor; /// Top-level pass that instruments the code with checks for uninitialized memory access through raw /// pointers. -#[derive(Debug)] +#[derive(Debug, Clone)] pub struct UninitPass { pub safety_check_type: CheckType, pub unsupported_check_type: CheckType, diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 0ec394d2cddc..d992f2749df4 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -38,7 +38,7 @@ use strum_macros::AsRefStr; use tracing::{debug, trace}; /// Instrument the code with checks for invalid values. -#[derive(Debug)] +#[derive(Debug, Clone)] pub struct ValidValuePass { pub safety_check_type: CheckType, pub unsupported_check_type: CheckType, diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index b0b4953ae4b9..efb73446216c 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -31,7 +31,7 @@ use tracing::{debug, trace}; /// depending on what the type of the input it /// /// any_modifies is replaced with any -#[derive(Debug)] +#[derive(Debug, Clone)] pub struct AnyModifiesPass { kani_any: Option, kani_any_modifies: Option, @@ -265,7 +265,7 @@ impl AnyModifiesPass { /// - Replace the non-used generated closures body with unreachable. /// 3. Replace the body of `kani_register_contract` by `kani::internal::run_contract_fn` to /// invoke the closure. -#[derive(Debug, Default)] +#[derive(Debug, Default, Clone)] pub struct FunctionWithContractPass { /// Function that is being checked, if any. check_fn: Option, diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 99bd271f525e..29c12f6cf96c 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -37,7 +37,7 @@ use std::str::FromStr; use tracing::{debug, trace}; /// Generate the body for a few Kani intrinsics. -#[derive(Debug)] +#[derive(Debug, Clone)] pub struct IntrinsicGeneratorPass { unsupported_check_type: CheckType, /// Used to cache FnDef lookups for models and Kani intrinsics. diff --git a/kani-compiler/src/kani_middle/transform/loop_contracts.rs b/kani-compiler/src/kani_middle/transform/loop_contracts.rs index 60dfb761d24e..8830dfa1678d 100644 --- a/kani-compiler/src/kani_middle/transform/loop_contracts.rs +++ b/kani-compiler/src/kani_middle/transform/loop_contracts.rs @@ -23,7 +23,7 @@ use rustc_span::Symbol; use std::collections::{HashMap, HashSet, VecDeque}; use std::fmt::Debug; -#[derive(Debug, Default)] +#[derive(Debug, Default, Clone)] pub struct LoopContractPass { /// Cache KaniRunContract function used to implement contracts. run_contract_fn: Option, diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 680fa2c03624..b36230f9356d 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -21,6 +21,7 @@ use crate::kani_middle::reachability::CallGraph; use crate::kani_middle::transform::body::CheckType; use crate::kani_middle::transform::check_uninit::{DelayedUbPass, UninitPass}; use crate::kani_middle::transform::check_values::ValidValuePass; +use crate::kani_middle::transform::clone::ClonableTransformPass; use crate::kani_middle::transform::contracts::{AnyModifiesPass, FunctionWithContractPass}; use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass; use crate::kani_middle::transform::loop_contracts::LoopContractPass; @@ -58,9 +59,9 @@ mod stubs; pub struct BodyTransformation { /// The passes that may change the function body according to harness configuration. /// The stubbing passes should be applied before so user stubs take precedence. - stub_passes: Vec>, + stub_passes: Vec>, /// The passes that may add safety checks to the function body. - inst_passes: Vec>, + inst_passes: Vec>, /// Cache transformation results. cache: HashMap, } @@ -86,7 +87,7 @@ impl BodyTransformation { transformer.add_pass( queries, ValidValuePass { - safety_check_type: safety_check_type.clone(), + safety_check_type, unsupported_check_type: unsupported_check_type.clone(), }, ); @@ -139,7 +140,7 @@ impl BodyTransformation { } } - fn add_pass(&mut self, query_db: &QueryDb, pass: P) { + fn add_pass(&mut self, query_db: &QueryDb, pass: P) { if pass.is_enabled(query_db) { match P::transformation_type() { TransformationType::Instrumentation => self.inst_passes.push(Box::new(pass)), @@ -249,3 +250,40 @@ impl GlobalPasses { modified } } + +mod clone { + //! This is all just machinery to implement `Clone` for a `Box`. + //! + //! To avoid circular reasoning, we use two traits that can each clone into a dyn of the other, and since + //! we set both up to have blanket implementations for all `T: TransformPass + Clone`, the compiler pieces them together properly + //! and we can implement `Clone` directly using the pair! + + use crate::kani_middle::transform::TransformPass; + + /// A wrapper trait essentially equivalent to `TransformPass + Clone` + pub(crate) trait ClonableTransformPass: TransformPass { + fn clone_there(&self) -> Box; + } + + impl Clone for Box { + fn clone(&self) -> Self { + self.clone_there().clone_back() + } + } + + impl ClonableTransformPass for T { + fn clone_there(&self) -> Box { + Box::new(self.clone()) + } + } + + pub(crate) trait CloneBackIntoPass { + fn clone_back(&self) -> Box; + } + + impl CloneBackIntoPass for T { + fn clone_back(&self) -> Box { + Box::new(self.clone()) + } + } +} diff --git a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs index 0d5747735e37..bb83ae1b5dc5 100644 --- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs @@ -27,7 +27,7 @@ use std::collections::HashMap; use tracing::debug; /// Generate the body for a few Kani intrinsics. -#[derive(Debug)] +#[derive(Debug, Clone)] pub struct RustcIntrinsicsPass { /// Used to cache FnDef lookups for intrinsics models. models: HashMap, diff --git a/kani-compiler/src/kani_middle/transform/stubs.rs b/kani-compiler/src/kani_middle/transform/stubs.rs index 01135109df97..fa7b6cdb4fb4 100644 --- a/kani-compiler/src/kani_middle/transform/stubs.rs +++ b/kani-compiler/src/kani_middle/transform/stubs.rs @@ -22,7 +22,7 @@ use tracing::{debug, trace}; /// /// This pass will replace the entire body, and it should only be applied to stubs /// that have a body. -#[derive(Debug)] +#[derive(Debug, Clone)] pub struct FnStubPass { stubs: Stubs, } @@ -74,7 +74,7 @@ impl FnStubPass { /// /// This pass will replace the function call, since one of the functions do not have a body to /// replace. -#[derive(Debug)] +#[derive(Debug, Clone)] pub struct ExternFnStubPass { pub stubs: Stubs, } From 42e056e685862c8f926b6b4a1a7516e06a967098 Mon Sep 17 00:00:00 2001 From: AlexanderPortland Date: Thu, 31 Jul 2025 15:05:24 -0700 Subject: [PATCH 2/3] clone template body transformer to avoid re-init --- .../src/codegen_cprover_gotoc/compiler_interface.rs | 6 +++++- kani-compiler/src/kani_middle/transform/mod.rs | 11 +++++++++++ 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index f5b4dd4e85ed..5f767078ffdd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -338,8 +338,12 @@ impl CodegenBackend for GotocCodegenBackend { for unit in units.iter() { // We reset the body cache for now because each codegen unit has different // configurations that affect how we transform the instance body. + + // Generate an empty 'template' transformer once per codegen unit and then clone for each harness within. + // (They all share the same options.) + let template_transformer = BodyTransformation::new(&queries, tcx, unit); for harness in &unit.harnesses { - let transformer = BodyTransformation::new(&queries, tcx, unit); + let transformer = template_transformer.clone_empty(); let model_path = units.harness_model_path(*harness).unwrap(); let is_automatic_harness = units.is_automatic_harness(harness); let contract_metadata = diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index b36230f9356d..f5663d05191f 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -140,6 +140,17 @@ impl BodyTransformation { } } + /// Clone an empty [BodyTransformation] for use within the same [CodegenUnit] and [TyCtxt] that were + /// used to create it. Will panic if the transformer has already been queried with `.body()`. + pub fn clone_empty(&self) -> Self { + debug_assert!(self.cache.is_empty()); + BodyTransformation { + stub_passes: self.stub_passes.to_vec(), + inst_passes: self.inst_passes.to_vec(), + cache: HashMap::new(), + } + } + fn add_pass(&mut self, query_db: &QueryDb, pass: P) { if pass.is_enabled(query_db) { match P::transformation_type() { From 7dfac5a446ccf05f079f9c8d84d941ed03fd0de9 Mon Sep 17 00:00:00 2001 From: AlexanderPortland Date: Mon, 4 Aug 2025 14:10:12 -0700 Subject: [PATCH 3/3] also clone GlobalPasses template --- .../compiler_interface.rs | 10 ++- .../transform/check_uninit/delayed_ub/mod.rs | 2 +- .../kani_middle/transform/dump_mir_pass.rs | 2 +- .../src/kani_middle/transform/mod.rs | 68 ++++++++++++------- 4 files changed, 52 insertions(+), 30 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 5f767078ffdd..b135adabd002 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -72,6 +72,7 @@ impl GotocCodegenBackend { /// Generate code that is reachable from the given starting points. /// /// Invariant: iff `check_contract.is_some()` then `return.2.is_some()` + #[allow(clippy::too_many_arguments)] fn codegen_items<'tcx>( &self, tcx: TyCtxt<'tcx>, @@ -79,6 +80,7 @@ impl GotocCodegenBackend { symtab_goto: &Path, machine_model: &MachineModel, check_contract: Option, + mut global_passes: GlobalPasses, mut transformer: BodyTransformation, ) -> (GotocCtx<'tcx>, Vec, Option) { // This runs reachability analysis before global passes are applied. @@ -107,7 +109,6 @@ impl GotocCodegenBackend { .collect(); // Apply all transformation passes, including global passes. - let mut global_passes = GlobalPasses::new(&self.queries.lock().unwrap(), tcx); let any_pass_modified = global_passes.run_global_passes( &mut transformer, tcx, @@ -334,6 +335,8 @@ impl CodegenBackend for GotocCodegenBackend { let mut units = CodegenUnits::new(&queries, tcx); let mut modifies_instances = vec![]; let mut loop_contracts_instances = vec![]; + + let template_passes = GlobalPasses::new(&queries, tcx); // Cross-crate collecting of all items that are reachable from the crate harnesses. for unit in units.iter() { // We reset the body cache for now because each codegen unit has different @@ -343,7 +346,6 @@ impl CodegenBackend for GotocCodegenBackend { // (They all share the same options.) let template_transformer = BodyTransformation::new(&queries, tcx, unit); for harness in &unit.harnesses { - let transformer = template_transformer.clone_empty(); let model_path = units.harness_model_path(*harness).unwrap(); let is_automatic_harness = units.is_automatic_harness(harness); let contract_metadata = @@ -355,7 +357,8 @@ impl CodegenBackend for GotocCodegenBackend { &results.machine_model, contract_metadata .map(|def| rustc_internal::internal(tcx, def.def_id())), - transformer, + template_passes.clone(), + template_transformer.clone_empty(), ); if gcx.has_loop_contracts { loop_contracts_instances.push(*harness); @@ -390,6 +393,7 @@ impl CodegenBackend for GotocCodegenBackend { &model_path, &results.machine_model, Default::default(), + GlobalPasses::new(&queries, tcx), transformer, ); assert!(contract_info.is_none()); diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs index 7019628de930..3c6c2c5259d8 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/mod.rs @@ -31,7 +31,7 @@ use rustc_session::config::OutputType; mod initial_target_visitor; mod instrumentation_visitor; -#[derive(Debug)] +#[derive(Debug, Clone)] pub struct DelayedUbPass { pub safety_check_type: CheckType, pub unsupported_check_type: CheckType, diff --git a/kani-compiler/src/kani_middle/transform/dump_mir_pass.rs b/kani-compiler/src/kani_middle/transform/dump_mir_pass.rs index b7af809d318c..c8b5edbf004d 100644 --- a/kani-compiler/src/kani_middle/transform/dump_mir_pass.rs +++ b/kani-compiler/src/kani_middle/transform/dump_mir_pass.rs @@ -17,7 +17,7 @@ use std::io::Write; use super::BodyTransformation; /// Dump all MIR bodies. -#[derive(Debug)] +#[derive(Debug, Clone)] pub struct DumpMirPass { enabled: bool, } diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index f5663d05191f..d3e8fd1e6ebe 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -21,7 +21,7 @@ use crate::kani_middle::reachability::CallGraph; use crate::kani_middle::transform::body::CheckType; use crate::kani_middle::transform::check_uninit::{DelayedUbPass, UninitPass}; use crate::kani_middle::transform::check_values::ValidValuePass; -use crate::kani_middle::transform::clone::ClonableTransformPass; +use crate::kani_middle::transform::clone::{ClonableGlobalPass, ClonableTransformPass}; use crate::kani_middle::transform::contracts::{AnyModifiesPass, FunctionWithContractPass}; use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass; use crate::kani_middle::transform::loop_contracts::LoopContractPass; @@ -211,10 +211,11 @@ enum TransformationResult { NotModified, } +#[derive(Clone)] pub struct GlobalPasses { /// The passes that operate on the whole codegen unit, they run after all previous passes are /// done. - global_passes: Vec>, + global_passes: Vec>, } impl GlobalPasses { @@ -232,7 +233,7 @@ impl GlobalPasses { global_passes } - fn add_global_pass(&mut self, query_db: &QueryDb, pass: P) { + fn add_global_pass(&mut self, query_db: &QueryDb, pass: P) { if pass.is_enabled(query_db) { self.global_passes.push(Box::new(pass)) } @@ -269,32 +270,49 @@ mod clone { //! we set both up to have blanket implementations for all `T: TransformPass + Clone`, the compiler pieces them together properly //! and we can implement `Clone` directly using the pair! - use crate::kani_middle::transform::TransformPass; + /// Builds a new dyn compatible wrapper trait that's essentially equivalent to extending + /// `$extends` with `Clone`. Requires an ident for an intermediate trait for avoiding cycles + /// in the implementation. + macro_rules! implement_clone { + ($new_trait_name: ident, $intermediate_trait_name: ident, $extends: path) => { + #[allow(private_interfaces)] + pub(crate) trait $new_trait_name: $extends { + fn clone_there(&self) -> Box; + } - /// A wrapper trait essentially equivalent to `TransformPass + Clone` - pub(crate) trait ClonableTransformPass: TransformPass { - fn clone_there(&self) -> Box; - } + impl Clone for Box { + fn clone(&self) -> Self { + self.clone_there().clone_back() + } + } - impl Clone for Box { - fn clone(&self) -> Self { - self.clone_there().clone_back() - } - } + #[allow(private_interfaces)] + impl $new_trait_name for T { + fn clone_there(&self) -> Box { + Box::new(self.clone()) + } + } - impl ClonableTransformPass for T { - fn clone_there(&self) -> Box { - Box::new(self.clone()) - } - } + trait $intermediate_trait_name { + fn clone_back(&self) -> Box; + } - pub(crate) trait CloneBackIntoPass { - fn clone_back(&self) -> Box; + impl $intermediate_trait_name for T { + fn clone_back(&self) -> Box { + Box::new(self.clone()) + } + } + }; } - impl CloneBackIntoPass for T { - fn clone_back(&self) -> Box { - Box::new(self.clone()) - } - } + implement_clone!( + ClonableTransformPass, + ClonableTransformPassMid, + crate::kani_middle::transform::TransformPass + ); + implement_clone!( + ClonableGlobalPass, + ClonableGlobalPassMid, + crate::kani_middle::transform::GlobalPass + ); }