[CN-Test-Gen] Flag for disabling passes

rems-project · Nov 12, 2024 · 583da5e · 583da5e
1 parent 875771a
commit 583da5e
Show file tree

Hide file tree

Showing 4 changed files with 48 additions and 15 deletions.
diff --git a/backend/cn/bin/main.ml b/backend/cn/bin/main.ml
@@ -449,6 +449,7 @@ let run_tests
   max_stack_depth
   max_generator_size
   coverage
+  disable_passes
   =
   (* flags *)
   Cerb_debug.debug_level := debug_level;
@@ -514,7 +515,8 @@ let run_tests
               exit_fast;
               max_stack_depth;
               max_generator_size;
-              coverage
+              coverage;
+              disable_passes
             }
           in
           TestGeneration.run
@@ -989,6 +991,23 @@ module Testing_flags = struct
   let test_coverage =
     let doc = "Record coverage of tests" in
     Arg.(value & flag & info [ "coverage" ] ~doc)
+
+
+  let disable_passes =
+    let doc = "skip this optimization pass (or comma-separated names)" in
+    Arg.(
+      value
+      & opt
+          (list
+             (enum
+                [ ("reorder", "reorder");
+                  ("picks", "picks");
+                  ("flatten", "flatten");
+                  ("consistency", "consistency");
+                  ("lift_constraints", "lift_constraints")
+                ]))
+          []
+      & info [ "disable" ] ~doc)
 end
 
 let testing_cmd =
@@ -1024,6 +1043,7 @@ let testing_cmd =
     $ Testing_flags.test_max_stack_depth
     $ Testing_flags.test_max_generator_size
     $ Testing_flags.test_coverage
+    $ Testing_flags.disable_passes
   in
   let doc =
     "Generates RapidCheck tests for all functions in [FILE] with CN specifications.\n\

diff --git a/backend/cn/lib/testGeneration/genOptimize.ml b/backend/cn/lib/testGeneration/genOptimize.ml
@@ -6,6 +6,7 @@ module GT = GenTerms
 module GS = GenStatements
 module GD = GenDefinitions
 module GA = GenAnalysis
+module Config = TestGenConfig
 module SymSet = Set.Make (Sym)
 module SymMap = Map.Make (Sym)
 module StringSet = Set.Make (String)
@@ -3453,14 +3454,14 @@ module Specialization = struct
 end
 
 let all_passes (prog5 : unit Mucore.file) =
-  (PartialEvaluation.pass prog5
-   :: PushPull.pass
-   :: MemberIndirection.pass
-   :: Inline.passes)
+  [ PartialEvaluation.pass prog5 ]
+  @ (if Config.has_pass "flatten" then [ PushPull.pass ] else [])
+  @ [ MemberIndirection.pass ]
+  @ Inline.passes
   @ RemoveUnused.passes
   @ [ TermSimplification.pass prog5; TermSimplification'.pass; PointerOffsets.pass ]
   @ BranchPruning.passes
-  @ SplitConstraints.passes
+  @ if Config.has_pass "lift_constraints" then SplitConstraints.passes else []
 
 
 let optimize_gen (prog5 : unit Mucore.file) (passes : StringSet.t) (gt : GT.t) : GT.t =
@@ -3496,13 +3497,18 @@ let optimize_gen_def (prog5 : unit Mucore.file) (passes : StringSet.t) (gd : GD.
   |> aux
   |> Fusion.Each.transform
   |> aux
-  |> FlipIfs.transform
+  |> (if Config.has_pass "picks" then FlipIfs.transform else fun gd' -> gd')
   |> aux
-  |> Reordering.transform []
-  |> ConstraintPropagation.transform
-  |> Specialization.Equality.transform
-  |> Specialization.Integer.transform
-  |> Specialization.Pointer.transform
+  |> (if Config.has_pass "reorder" then Reordering.transform [] else fun gd' -> gd')
+  |> (if Config.has_pass "consistency" then
+        fun gd' ->
+      gd'
+      |> ConstraintPropagation.transform
+      |> Specialization.Equality.transform
+      |> Specialization.Integer.transform
+      |> Specialization.Pointer.transform
+      else
+        fun gd' -> gd')
   |> InferAllocationSize.transform
   |> aux
 

diff --git a/backend/cn/lib/testGeneration/testGenConfig.ml b/backend/cn/lib/testGeneration/testGenConfig.ml
@@ -13,7 +13,8 @@ type t =
     exit_fast : bool;
     max_stack_depth : int option;
     max_generator_size : int option;
-    coverage : bool
+    coverage : bool;
+    disable_passes : string list
   }
 
 let default =
@@ -29,7 +30,8 @@ let default =
     exit_fast = false;
     max_stack_depth = None;
     max_generator_size = None;
-    coverage = false
+    coverage = false;
+    disable_passes = []
   }
 
 
@@ -62,3 +64,5 @@ let has_max_stack_depth () = !instance.max_stack_depth
 let has_max_generator_size () = !instance.max_generator_size
 
 let is_coverage () = !instance.coverage
+
+let has_pass s = not (List.mem String.equal s !instance.disable_passes)
diff --git a/backend/cn/lib/testGeneration/testGenConfig.mli b/backend/cn/lib/testGeneration/testGenConfig.mli
@@ -13,7 +13,8 @@ type t =
     exit_fast : bool;
     max_stack_depth : int option;
     max_generator_size : int option;
-    coverage : bool
+    coverage : bool;
+    disable_passes : string list
   }
 
 val default : t
@@ -45,3 +46,5 @@ val has_max_stack_depth : unit -> int option
 val has_max_generator_size : unit -> int option
 
 val is_coverage : unit -> bool
+
+val has_pass : string -> bool