[Bennet] Conditional lazy generation (#497)

Author: ZippeyKeys12

lib/testGeneration/bennet/stage3/instantiate.ml

@@ -67,12 +67,11 @@ module Make (AD : Domain.T) = struct
              an instantiate before its first use in the continuation. *)
           let next_instantiated =
             match gt1 with
+            | GenTerms.Annot (`Lazy, _, _, _) -> instantiated'
             | GenTerms.Annot (`Arbitrary, _, _, _)
-            | GenTerms.Annot (`Symbolic, _, _, _)
-            | GenTerms.Annot (`Lazy, _, _, _) ->
-              instantiated'
             | Annot ((`Call _ | `Return _ | `Map _), _, _, _) ->
               Sym.Set.add x instantiated'
+            | GenTerms.Annot (`Symbolic, _, _, _) -> failwith ("unsupported @ " ^ __LOC__)
             | _ -> failwith ("unreachable @ " ^ __LOC__)
           in
           `LetStar ((x, gt1), aux next_instantiated gt2)

lib/testGeneration/bennet/stage3/lazify.ml

@@ -1,17 +1,46 @@
+module IT = IndexTerms
+module LC = LogicalConstraints
+
 module Make (AD : Domain.T) = struct
   module Ctx = Ctx.Make (AD)
   module Def = Def.Make (AD)
   module Term = Term.Make (AD)
 
+  let is_locally_constrained (x : Sym.t) (gt : Term.t) : bool =
+    let rec aux (gt : Term.t) : bool =
+      let (Annot (gt_, _, _, _)) = gt in
+      match gt_ with
+      | `Arbitrary | `Symbolic | `Lazy -> false
+      | `Return it_val -> Sym.Set.mem x (IT.free_vars it_val)
+      | `Asgn ((it_addr, _), _, gt_rest) ->
+        Sym.Set.mem x (IT.free_vars it_addr) || aux gt_rest
+      | `Assert (lc, gt_rest) -> Sym.Set.mem x (LC.free_vars lc) || aux gt_rest
+      | `Call _ -> false
+      | `LetStar
+          ((_, Annot ((`Arbitrary | `Symbolic | `Lazy | `Call _), _, _, _)), gt_rest) ->
+        aux gt_rest
+      | `LetStar ((_, Annot (`Map ((y, _y_bt, _it_perm), gt_inner), _, _, _)), gt_rest) ->
+        ((not (Sym.equal x y)) && aux gt_inner) || aux gt_rest
+      | `LetStar ((_, Annot (`Return it, _, _, _)), gt_rest) ->
+        Sym.Set.mem x (IT.free_vars it) || aux gt_rest
+      | `LetStar ((_, _), _) -> failwith ("unreachable @ " ^ __LOC__)
+      | `ITE (it_if, gt_then, gt_else) ->
+        Sym.Set.mem x (IT.free_vars it_if) || aux gt_then || aux gt_else
+      | `Map ((_, _, it_perm), gt') -> Sym.Set.mem x (IT.free_vars it_perm) || aux gt'
+      | `Instantiate _ -> failwith ("unreachable @ " ^ __LOC__)
+      | `Pick gts -> List.exists aux gts
+    in
+    aux gt
+
+
   let rec transform_gt (gt : Term.t) : Term.t =
     let (GenTerms.Annot (gt_, _tag, bt, loc)) = gt in
     match gt_ with
     | `Arbitrary | `Lazy | `Symbolic | `Call _ | `Return _ -> gt
     | `Asgn ((it_addr, sct), it_val, gt_rest) ->
       Term.asgn_ ((it_addr, sct), it_val, transform_gt gt_rest) () loc
-    | `LetStar
-        ((x, (GenTerms.Annot (`Arbitrary, _, inner_bt, inner_loc) as _gt_inner)), gt_rest)
-      ->
+    | `LetStar ((x, GenTerms.Annot (`Arbitrary, _, inner_bt, inner_loc)), gt_rest)
+      when not (is_locally_constrained x gt_rest) ->
       Term.let_star_ ((x, Term.lazy_ () inner_bt inner_loc), transform_gt gt_rest) () loc
     | `LetStar ((x, gt_inner), gt_rest) ->
       Term.let_star_ ((x, transform_gt gt_inner), transform_gt gt_rest) () loc

lib/testGeneration/bennet/stage6/convert.ml

@@ -68,15 +68,6 @@ module Make (AD : Domain.T) = struct
         let gt_inner = aux vars path_vars gt_inner in
         let gt_rest = aux vars path_vars gt_rest in
         GenTerms.Annot (`LetStar ((x, gt_inner), gt_rest), (path_vars, last_var), bt, loc)
-      | `LetStar
-          ( ( x,
-              (Annot ((`Arbitrary | `ArbitraryDomain _ | `ArbitrarySpecialized _), _, _, _)
-               as gt_inner) ),
-            gt_rest )
-        when TestGenConfig.is_lazy_gen () ->
-        let gt_inner = aux vars path_vars gt_inner in
-        let gt_rest = aux vars path_vars gt_rest in
-        GenTerms.Annot (`LetStar ((x, gt_inner), gt_rest), (path_vars, last_var), bt, loc)
       | `LetStar ((x, gt_inner), gt_rest) ->
         let gt_inner = aux vars path_vars gt_inner in
         let gt_rest = aux (x :: vars) path_vars gt_rest in

tests/run-cn-test-gen.py

@@ -43,11 +43,6 @@ def get_test_type(test_file, config):
             return 'PASS'
         else:
             return 'SKIP'
-    elif test_file.endswith('tutorial_queue.pass.c'):
-        if '--lazy-gen' in config:
-            return 'SKIP'
-        else:
-            return 'PASS'
     elif test_file.endswith('.pass.c'):
         return 'PASS'
     elif test_file.endswith('.fail.c'):