[Bennet] Explicitly label lazy values

lib/testGeneration/bennet/abstractDomains/interpreter.ml

@@ -55,6 +55,7 @@ module Make (GT : GenTerms.T) (I : Domain.T with type t = GT.AD.t) = struct
       match tm_ with
       | `Arbitrary -> (GT.arbitrary_ tag bt loc, [ d ])
       | `Symbolic -> (GT.symbolic_ tag bt loc, [ d ])
+      | `Lazy -> (GT.lazy_ tag bt loc, [ d ])
       | `ArbitrarySpecialized bounds ->
         (GT.arbitrary_specialized_ bounds tag bt loc, [ d ])
       | `ArbitraryDomain _ -> failwith ("unreachable @ " ^ __LOC__)

lib/testGeneration/bennet/genContext.ml

@@ -28,7 +28,7 @@ module Make (GT : GenTerms.T) = struct
       let rec aux (gt : GT.t) : Sym.Set.t =
         let (Annot (gt_, _, _, _)) = gt in
         match gt_ with
-        | `Arbitrary | `Symbolic | `ArbitrarySpecialized _ | `ArbitraryDomain _
+        | `Arbitrary | `Symbolic | `Lazy | `ArbitrarySpecialized _ | `ArbitraryDomain _
         | `Return _ ->
           Sym.Set.empty
         | `Pick gts -> gts |> List.map aux |> List.fold_left Sym.Set.union Sym.Set.empty

lib/testGeneration/bennet/genTerms.ml

@@ -11,6 +11,7 @@ module Base (AD : Domain.T) = struct
   type ('tag, 'recur) ast =
     [ `Arbitrary (** Generate arbitrary values *)
     | `Symbolic (** Generate symbolic values *)
+    | `Lazy (** Lazily generate values *)
     | `ArbitrarySpecialized of (IT.t option * IT.t option) * (IT.t option * IT.t option)
       (** Generate arbitrary values: ((min_inc, min_ex), (max_inc, max_ex)) *)
     | `ArbitraryDomain of AD.Relative.t
@@ -62,6 +63,8 @@ module type T = sig
 
   val symbolic_ : tag_t -> BT.t -> Locations.t -> t
 
+  val lazy_ : tag_t -> BT.t -> Locations.t -> t
+
   val arbitrary_specialized_
     :  (IT.t option * IT.t option) * (IT.t option * IT.t option) ->
     tag_t ->
@@ -170,6 +173,7 @@ module Make (GT : T) = struct
     match tm_ with
     | `Arbitrary -> !^"arbitrary" ^^ angles (BT.pp bt) ^^ parens empty
     | `Symbolic -> !^"symbolic" ^^ angles (BT.pp bt) ^^ parens empty
+    | `Lazy -> !^"lazy" ^^ angles (BT.pp bt) ^^ parens empty
     | `ArbitrarySpecialized ((min_inc, min_ex), (max_inc, max_ex)) ->
       let pp_opt = function
         | None -> !^"None"
@@ -299,7 +303,7 @@ module Make (GT : T) = struct
 
   let rec free_vars_bts_ (gt_ : GT.t_) : BT.t Sym.Map.t =
     match gt_ with
-    | `Arbitrary | `ArbitraryDomain _ | `Symbolic -> Sym.Map.empty
+    | `Arbitrary | `ArbitraryDomain _ | `Symbolic | `Lazy -> Sym.Map.empty
     | `ArbitrarySpecialized ((min_inc, min_ex), (max_inc, max_ex)) ->
       IT.free_vars_bts_list (List.filter_map Fun.id [ min_inc; min_ex; max_inc; max_ex ])
     | `Call (_, iargs) | `CallSized (_, iargs, _) -> IT.free_vars_bts_list iargs
@@ -381,7 +385,8 @@ module Make (GT : T) = struct
   let rec contains_call (gt : GT.t) : bool =
     let (Annot (gt_, _, _, _)) = gt in
     match gt_ with
-    | `Arbitrary | `ArbitraryDomain _ | `ArbitrarySpecialized _ | `Symbolic | `Return _ ->
+    | `Arbitrary | `ArbitraryDomain _ | `ArbitrarySpecialized _ | `Symbolic | `Lazy
+    | `Return _ ->
       false
     | `Call _ | `CallSized _ -> true
     | `LetStar ((_, gt1), gt2) | `ITE (_, gt1, gt2) ->
@@ -406,7 +411,7 @@ module Make (GT : T) = struct
   let rec contains_constraint (gt : GT.t) : bool =
     let (Annot (gt_, _, _, _)) = gt in
     match gt_ with
-    | `Arbitrary | `Symbolic | `Return _ -> false
+    | `Arbitrary | `Symbolic | `Lazy | `Return _ -> false
     | `ArbitraryDomain _ | `ArbitrarySpecialized _ | `Asgn _ | `AsgnElab _ | `Assert _
     | `AssertDomain _ ->
       true
@@ -428,7 +433,7 @@ module Make (GT : T) = struct
     let rec aux (gt : GT.t) : Sym.Set.t =
       let (Annot (gt_, _, _, _)) = gt in
       match gt_ with
-      | `Arbitrary | `Symbolic | `ArbitraryDomain _ -> Sym.Set.empty
+      | `Arbitrary | `Symbolic | `Lazy | `ArbitraryDomain _ -> Sym.Set.empty
       | `ArbitrarySpecialized ((min_inc, min_ex), (max_inc, max_ex)) ->
         [ min_inc; min_ex; max_inc; max_ex ]
         |> List.filter_map Fun.id
@@ -467,6 +472,7 @@ module Make (GT : T) = struct
     match gt_ with
     | `Arbitrary -> arbitrary_ tag bt loc
     | `Symbolic -> symbolic_ tag bt loc
+    | `Lazy -> lazy_ tag bt loc
     | `ArbitrarySpecialized ((min_inc, min_ex), (max_inc, max_ex)) ->
       arbitrary_specialized_
         ( (Option.map (IT.subst su) min_inc, Option.map (IT.subst su) min_ex),
@@ -561,6 +567,7 @@ module Make (GT : T) = struct
     match gt_ with
     | `Arbitrary -> arbitrary_ tag bt loc
     | `Symbolic -> symbolic_ tag bt loc
+    | `Lazy -> lazy_ tag bt loc
     | `ArbitrarySpecialized bounds -> arbitrary_specialized_ bounds tag bt loc
     | `ArbitraryDomain ad -> arbitrary_domain_ ad tag bt loc
     | `Call (fsym, its) -> call_ (fsym, its) tag bt loc
@@ -613,6 +620,7 @@ module Make (GT : T) = struct
       match gt_ with
       | `Arbitrary -> arbitrary_ tag bt loc
       | `Symbolic -> symbolic_ tag bt loc
+      | `Lazy -> lazy_ tag bt loc
       | `ArbitrarySpecialized bounds -> arbitrary_specialized_ bounds tag bt loc
       | `ArbitraryDomain ad -> arbitrary_domain_ ad tag bt loc
       | `Call (fsym, its) -> call_ (fsym, its) tag bt loc
@@ -665,6 +673,7 @@ module Make (GT : T) = struct
     match tm with
     | `Arbitrary -> `Arbitrary
     | `Symbolic -> `Symbolic
+    | `Lazy -> `Lazy
     | `ArbitrarySpecialized bounds -> `ArbitrarySpecialized bounds
     | `ArbitraryDomain ad -> `ArbitraryDomain ad
     | `Call (fsym, iargs) -> `Call (fsym, iargs)
@@ -702,6 +711,7 @@ module Make (GT : T) = struct
     match tm_ with
     | `Arbitrary -> arbitrary_ tag bt loc
     | `Symbolic -> symbolic_ tag bt loc
+    | `Lazy -> lazy_ tag bt loc
     | `ArbitrarySpecialized bounds -> arbitrary_specialized_ bounds tag bt loc
     | `ArbitraryDomain ad -> arbitrary_domain_ ad tag bt loc
     | `Call (fsym, iargs) -> call_ (fsym, iargs) tag bt loc
@@ -818,6 +828,8 @@ module Defaults (StageName : sig
 struct
   let unsupported name = failwith (name ^ " not supported in " ^ StageName.name ^ " DSL")
 
+  let lazy_ _ _ _ = unsupported "lazy_"
+
   let arbitrary_specialized_ _ _ _ _ = unsupported "arbitrary_specialized_"
 
   let arbitrary_domain_ _ _ _ _ = unsupported "arbitrary_domain_"

lib/testGeneration/bennet/stage3/instantiate.ml

@@ -29,7 +29,7 @@ module Make (AD : Domain.T) = struct
     | `Pick _ -> Sym.Map.empty
     | `Instantiate _ -> failwith ("unreachable @ " ^ __LOC__)
     | `Return it -> IT.free_vars_bts it
-    | `Arbitrary | `Symbolic -> Sym.Map.empty
+    | `Arbitrary | `Symbolic | `Lazy -> Sym.Map.empty
     | `Call (_fsym, iargs) ->
       iargs
       |> List.filter (fun it -> Option.is_none (IT.is_sym it))
@@ -57,6 +57,7 @@ module Make (AD : Domain.T) = struct
         match gt_ with
         | `Arbitrary -> `Arbitrary
         | `Symbolic -> `Symbolic
+        | `Lazy -> `Lazy
         | `Call (fsym, its) -> `Call (fsym, its)
         | `Return it -> `Return it
         | `Asgn ((addr, sct), it, gt') -> `Asgn ((addr, sct), it, aux instantiated' gt')
@@ -66,8 +67,9 @@ module Make (AD : Domain.T) = struct
              an instantiate before its first use in the continuation. *)
           let next_instantiated =
             match gt1 with
-            | GenTerms.Annot (`Arbitrary, _, _, _) | GenTerms.Annot (`Symbolic, _, _, _)
-              ->
+            | GenTerms.Annot (`Arbitrary, _, _, _)
+            | GenTerms.Annot (`Symbolic, _, _, _)
+            | GenTerms.Annot (`Lazy, _, _, _) ->
               instantiated'
             | Annot ((`Call _ | `Return _ | `Map _), _, _, _) ->
               Sym.Set.add x instantiated'

lib/testGeneration/bennet/stage3/lazify.ml

@@ -0,0 +1,33 @@
+module Make (AD : Domain.T) = struct
+  module Ctx = Ctx.Make (AD)
+  module Def = Def.Make (AD)
+  module Term = Term.Make (AD)
+
+  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)
+      ->
+      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
+    | `Assert (lc, gt_rest) -> Term.assert_ (lc, transform_gt gt_rest) () loc
+    | `ITE (it_if, gt_then, gt_else) ->
+      Term.ite_ (it_if, transform_gt gt_then, transform_gt gt_else) () loc
+    | `Map ((i, i_bt, it_perm), gt_inner) ->
+      Term.map_ ((i, i_bt, it_perm), transform_gt gt_inner) () loc
+    | `Pick gts -> Term.pick_ (List.map transform_gt gts) () bt loc
+    | `Instantiate ((x, gt_inner), gt_rest) ->
+      Term.instantiate_ ((x, transform_gt gt_inner), transform_gt gt_rest) () loc
+
+
+  let transform_gd (gd : Def.t) : Def.t = { gd with body = transform_gt gd.body }
+
+  let transform (ctx : Ctx.t) : Ctx.t =
+    Cerb_debug.print_debug 2 [] (fun () -> "lazify");
+    List.map_snd transform_gd ctx
+end

lib/testGeneration/bennet/stage3/simplifyNames.ml

@@ -17,7 +17,7 @@ module Make (AD : Domain.T) = struct
     let rec aux (vars : int StringMap.t) (gt : Term.t) : int StringMap.t * Term.t =
       let (Annot (gt_, (), bt, loc)) = gt in
       match gt_ with
-      | `Arbitrary | `Symbolic | `Call _ | `Return _ -> (vars, gt)
+      | `Arbitrary | `Symbolic | `Lazy | `Call _ | `Return _ -> (vars, gt)
       | `Pick gts ->
         let vars, gts =
           List.fold_right

lib/testGeneration/bennet/stage3/specializeEquality.ml

@@ -12,7 +12,9 @@ module Make (AD : Domain.T) = struct
       let open Option in
       let (Annot (gt_, (), _, loc)) = gt in
       match gt_ with
-      | `Arbitrary | `Symbolic | `Pick _ | `Call _ | `Return _ | `ITE _ | `Map _ -> None
+      | `Arbitrary | `Symbolic | `Lazy | `Pick _ | `Call _ | `Return _ | `ITE _ | `Map _
+        ->
+        None
       | `Asgn ((it_addr, sct), it_val, gt_rest) ->
         let@ gt_rest, it = aux gt_rest in
         return (Term.asgn_ ((it_addr, sct), it_val, gt_rest) () loc, it)
@@ -48,11 +50,12 @@ module Make (AD : Domain.T) = struct
     let rec aux (vars : Sym.Set.t) (gt : Term.t) : Term.t =
       let (Annot (gt_, (), bt, loc)) = gt in
       match gt_ with
-      | `Arbitrary | `Symbolic | `Call _ | `Return _ -> gt
+      | `Arbitrary | `Symbolic | `Lazy | `Call _ | `Return _ -> gt
       | `Pick gts -> Term.pick_ (List.map (aux vars) gts) () bt loc
       | `Asgn ((it_addr, sct), it_val, gt_rest) ->
         Term.asgn_ ((it_addr, sct), it_val, aux vars gt_rest) () loc
-      | `LetStar ((x, (Annot (`Arbitrary, (), _, loc) as gt_inner)), gt_rest) ->
+      | `LetStar ((x, (Annot (`Arbitrary, (), _, loc) as gt_inner)), gt_rest)
+      | `LetStar ((x, (Annot (`Lazy, (), _, loc) as gt_inner)), gt_rest) ->
         let gt_rest, gt_res =
           match find_constraint vars x gt_rest with
           | Some (gt_rest, it) -> (gt_rest, Term.return_ it () loc)
@@ -66,7 +69,8 @@ module Make (AD : Domain.T) = struct
         Term.ite_ (it_if, aux vars gt_then, aux vars gt_else) () loc
       | `Map ((i, i_bt, it_perm), gt_inner) ->
         Term.map_ ((i, i_bt, it_perm), aux (Sym.Set.add i vars) gt_inner) () loc
-      | `Instantiate ((x, (Annot (`Arbitrary, (), _, loc) as gt_inner)), gt_rest) ->
+      | `Instantiate ((x, (Annot (`Arbitrary, (), _, loc) as gt_inner)), gt_rest)
+      | `Instantiate ((x, (Annot (`Lazy, (), _, loc) as gt_inner)), gt_rest) ->
         let gt_rest, gt_res =
           match find_constraint vars x gt_rest with
           | Some (gt_rest, it) -> (gt_rest, Term.return_ it () loc)

lib/testGeneration/bennet/stage3/stage3.ml

@@ -7,6 +7,7 @@
 module Make (AD : Domain.T) = struct
   open struct
     module Convert = Convert.Make (AD)
+    module Lazify = Lazify.Make (AD)
     module Instantiate = Instantiate.Make (AD)
     module SpecializeEquality = SpecializeEquality.Make (AD)
     module SimplifyNames = SimplifyNames.Make (AD)
@@ -22,7 +23,8 @@ module Make (AD : Domain.T) = struct
     |> Convert.transform
     |> SpecializeEquality.transform
     |> (if TestGenConfig.is_lazy_gen () then
-          fun ctx -> ctx |> Instantiate.transform |> SpecializeEquality.transform
+          fun ctx ->
+        ctx |> Lazify.transform |> Instantiate.transform |> SpecializeEquality.transform
         else
           Fun.id)
     |> SimplifyNames.transform

lib/testGeneration/bennet/stage3/term.ml

@@ -15,6 +15,7 @@ module Make (AD : Domain.T) = struct
       type 'recur ast =
         [ `Arbitrary (** Generate arbitrary values *)
         | `Symbolic (** Generate symbolic values *)
+        | `Lazy (** Lazily generate values *)
         | `Call of Sym.t * IT.t list
           (** `Call a defined generator according to a [Sym.t] with arguments [IT.t list] *)
         | `Asgn of (IT.t * Sctypes.t) * IT.t * 'recur annot
@@ -50,6 +51,10 @@ module Make (AD : Domain.T) = struct
           let name = "Stage 3"
         end)
 
+      let lazy_ (tag : tag_t) (bt : BT.t) (loc : Locations.t) : t =
+        Annot (`Lazy, tag, bt, loc)
+
+
       let call_ ((fsym, its) : Sym.t * IT.t list) (tag : tag_t) (bt : BT.t) loc : t =
         Annot (`Call (fsym, its), tag, bt, loc)
 

lib/testGeneration/bennet/stage4/convert.ml

@@ -12,6 +12,7 @@ module Make (AD : Domain.T) = struct
       match gt_ with
       | `Arbitrary -> `Arbitrary
       | `Symbolic -> `Symbolic
+      | `Lazy -> `Lazy
       | `Call (fsym, args) -> `Call (fsym, args)
       | `Asgn ((it_addr, sct), it_val, gt_rest) ->
         `Asgn ((it_addr, sct), it_val, transform_gt gt_rest)

lib/testGeneration/bennet/stage4/smtPruning.ml

@@ -13,8 +13,8 @@ module Make (AD : Domain.T) = struct
       let here = Locations.other __LOC__ in
       let (Annot (tm_, (), bt, loc)) = tm in
       match tm_ with
-      | `Arbitrary | `ArbitraryDomain _ | `ArbitrarySpecialized _ | `Symbolic | `Return _
-      | `Call _ ->
+      | `Arbitrary | `ArbitraryDomain _ | `ArbitrarySpecialized _ | `Symbolic | `Lazy
+      | `Return _ | `Call _ ->
         let@ check = provable loc in
         return
           (match check (LC.T (IT.bool_ false here)) with
@@ -75,7 +75,8 @@ module Make (AD : Domain.T) = struct
           (let open Option in
            let@ gt_rest in
            return (Term.let_star_ ((x, Term.return_ it () loc_ret), gt_rest) () loc))
-      | `LetStar ((x, (Annot ((`Arbitrary | `Symbolic), _, bt', _) as gt_inner)), gt_rest)
+      | `LetStar
+          ((x, (Annot ((`Arbitrary | `Symbolic | `Lazy), _, bt', _) as gt_inner)), gt_rest)
         ->
         let@ () = add_l x bt' (loc, lazy (Sym.pp x)) in
         let@ gt_rest = aux new_constraint gt_rest in

lib/testGeneration/bennet/stage4/specialize.ml

@@ -132,8 +132,8 @@ module Make (AD : Domain.T) = struct
       in
       let (Annot (gt_, _, _, _)) = gt in
       match gt_ with
-      | `Arbitrary | `Symbolic | `ArbitrarySpecialized _ | `ArbitraryDomain _ | `Call _
-      | `Return _ ->
+      | `Arbitrary | `Symbolic | `Lazy | `ArbitrarySpecialized _ | `ArbitraryDomain _
+      | `Call _ | `Return _ ->
         empty_rep
       | `Pick gts ->
         (* Collect constraints from all branches *)
@@ -194,8 +194,8 @@ module Make (AD : Domain.T) = struct
     let rec specialize (vars : Sym.Set.t) (gt : Term.t) : Term.t =
       let (Annot (gt_, _, bt, loc)) = gt in
       match gt_ with
-      | `Arbitrary | `Symbolic | `ArbitrarySpecialized _ | `ArbitraryDomain _ | `Call _
-      | `Return _ ->
+      | `Arbitrary | `Symbolic | `Lazy | `ArbitrarySpecialized _ | `ArbitraryDomain _
+      | `Call _ | `Return _ ->
         gt
       | `Pick gts -> Term.pick_ (List.map (specialize vars) gts) () bt loc
       | `Asgn ((it_addr, sct), it_val, gt_rest) ->

lib/testGeneration/bennet/stage4/specializeDomain.ml

@@ -10,6 +10,9 @@ module Make (AD : Domain.T) = struct
       let (Annot (gt_, tag, bt, loc)) = gt in
       match gt_ with
       (* Important parts *)
+      | `LetStar ((x, (Annot (`Lazy, _, _, _) as gt_inner)), gt_rest) ->
+        let gt_rest, d = aux (Sym.Set.add x vars) gt_rest in
+        (Term.let_star_ ((x, gt_inner), gt_rest) tag loc, d)
       | `LetStar
           ((x, Annot ((`Arbitrary | `Symbolic), tag_inner, bt_inner, loc_inner)), gt_rest)
         ->
@@ -32,6 +35,9 @@ module Make (AD : Domain.T) = struct
           (Term.assert_domain_ (d_remove_x, gt') tag loc, d_remove_x)
         else
           (gt', d)
+      | `Instantiate ((x, (Annot (`Lazy, _, _, _) as gt_inner)), gt_rest) ->
+        let gt_rest, d = aux vars gt_rest in
+        (Term.instantiate_ ((x, gt_inner), gt_rest) tag loc, d)
       | `Instantiate
           ((x, Annot ((`Arbitrary | `Symbolic), tag_inner, bt_inner, loc_inner)), gt_rest)
         ->
@@ -47,8 +53,8 @@ module Make (AD : Domain.T) = struct
         let gt' = Term.instantiate_ ((x, gt_inner), gt_rest) tag loc in
         (gt', d)
         (* The rest *)
-      | `Arbitrary | `Symbolic | `ArbitrarySpecialized _ | `ArbitraryDomain _ | `Call _
-      | `Return _ ->
+      | `Arbitrary | `Symbolic | `Lazy | `ArbitrarySpecialized _ | `ArbitraryDomain _
+      | `Call _ | `Return _ ->
         (gt, AD.top)
       | `Pick gts ->
         let gts, ds = List.split (List.map (aux vars) gts) in

lib/testGeneration/bennet/stage4/term.ml

@@ -15,6 +15,7 @@ module Make (AD : Domain.T) = struct
       type 'recur ast =
         [ `Arbitrary (** Generate arbitrary values *)
         | `Symbolic (** Generate symbolic values *)
+        | `Lazy (** Lazily generate values *)
         | `ArbitrarySpecialized of
             (IT.t option * IT.t option) * (IT.t option * IT.t option)
           (** Generate arbitrary values: ((min_inc, min_ex), (max_inc, max_ex)) *)
@@ -55,6 +56,10 @@ module Make (AD : Domain.T) = struct
           let name = "Stage 4"
         end)
 
+      let lazy_ (tag : tag_t) (bt : BT.t) (loc : Locations.t) : t =
+        Annot (`Lazy, tag, bt, loc)
+
+
       let arbitrary_domain_
             (d : AD.Relative.t)
             (tag : tag_t)

lib/testGeneration/bennet/stage5/convert.ml

@@ -15,8 +15,8 @@ module Make (AD : Domain.T) = struct
     let rec aux (gr : Stage4.Term.t) : int =
       let (Annot (gr_, (), _, _)) = gr in
       match gr_ with
-      | `Arbitrary | `Symbolic | `ArbitrarySpecialized _ | `ArbitraryDomain _ | `Return _
-        ->
+      | `Arbitrary | `Symbolic | `Lazy | `ArbitrarySpecialized _ | `ArbitraryDomain _
+      | `Return _ ->
         0
       | `Pick choices -> choices |> List.map aux |> List.fold_left max 0
       | `Call (fsym, _) -> if Sym.Set.mem fsym syms then 1 else 0
@@ -39,6 +39,7 @@ module Make (AD : Domain.T) = struct
       match gr_ with
       | `Arbitrary -> (GenTerms.Annot (`Arbitrary, (), bt, loc), Sym.Set.empty)
       | `Symbolic -> (GenTerms.Annot (`Symbolic, (), bt, loc), Sym.Set.empty)
+      | `Lazy -> (GenTerms.Annot (`Lazy, (), bt, loc), Sym.Set.empty)
       | `ArbitrarySpecialized bounds ->
         (GenTerms.Annot (`ArbitrarySpecialized bounds, (), bt, loc), Sym.Set.empty)
       | `ArbitraryDomain d ->