also clone GlobalPasses template

Author: AlexanderPortland

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -72,13 +72,15 @@ 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>,
         starting_items: &[MonoItem],
         symtab_goto: &Path,
         machine_model: &MachineModel,
         check_contract: Option<InternalDefId>,
+        mut global_passes: GlobalPasses,
         mut transformer: BodyTransformation,
     ) -> (GotocCtx<'tcx>, Vec<MonoItem>, Option<AssignsContract>) {
         // 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());

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,

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,
 }

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<Box<dyn GlobalPass>>,
+    global_passes: Vec<Box<dyn ClonableGlobalPass>>,
 }
 
 impl GlobalPasses {
@@ -232,7 +233,7 @@ impl GlobalPasses {
         global_passes
     }
 
-    fn add_global_pass<P: GlobalPass + 'static>(&mut self, query_db: &QueryDb, pass: P) {
+    fn add_global_pass<P: ClonableGlobalPass + 'static>(&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<dyn $intermediate_trait_name>;
+            }
 
-    /// A wrapper trait essentially equivalent to `TransformPass + Clone`
-    pub(crate) trait ClonableTransformPass: TransformPass {
-        fn clone_there(&self) -> Box<dyn CloneBackIntoPass>;
-    }
+            impl Clone for Box<dyn $new_trait_name> {
+                fn clone(&self) -> Self {
+                    self.clone_there().clone_back()
+                }
+            }
 
-    impl Clone for Box<dyn ClonableTransformPass> {
-        fn clone(&self) -> Self {
-            self.clone_there().clone_back()
-        }
-    }
+            #[allow(private_interfaces)]
+            impl<T: $extends + Clone + 'static> $new_trait_name for T {
+                fn clone_there(&self) -> Box<dyn $intermediate_trait_name> {
+                    Box::new(self.clone())
+                }
+            }
 
-    impl<T: TransformPass + Clone + 'static> ClonableTransformPass for T {
-        fn clone_there(&self) -> Box<dyn CloneBackIntoPass> {
-            Box::new(self.clone())
-        }
-    }
+            trait $intermediate_trait_name {
+                fn clone_back(&self) -> Box<dyn $new_trait_name>;
+            }
 
-    pub(crate) trait CloneBackIntoPass {
-        fn clone_back(&self) -> Box<dyn ClonableTransformPass>;
+            impl<T: $extends + Clone + 'static> $intermediate_trait_name for T {
+                fn clone_back(&self) -> Box<dyn $new_trait_name> {
+                    Box::new(self.clone())
+                }
+            }
+        };
     }
 
-    impl<T: TransformPass + Clone + 'static> CloneBackIntoPass for T {
-        fn clone_back(&self) -> Box<dyn ClonableTransformPass> {
-            Box::new(self.clone())
-        }
-    }
+    implement_clone!(
+        ClonableTransformPass,
+        ClonableTransformPassMid,
+        crate::kani_middle::transform::TransformPass
+    );
+    implement_clone!(
+        ClonableGlobalPass,
+        ClonableGlobalPassMid,
+        crate::kani_middle::transform::GlobalPass
+    );
 }