[Bennet] Re-impl old specialization (#465)

Author: ZippeyKeys12

lib/testGeneration/bennet/abstractDomains/interpreter.ml

@@ -16,6 +16,8 @@ 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 ])
+      | `ArbitrarySpecialized bounds ->
+        (GT.arbitrary_specialized_ bounds tag bt loc, [ d ])
       | `ArbitraryDomain _ -> failwith ("unreachable @ " ^ __LOC__)
       | `Return _ ->
         let tm' = if should_assert then GT.assert_domain_ (d, tm) tag loc else tm in

lib/testGeneration/bennet/abstractDomains/interval_.ml

@@ -112,9 +112,9 @@ module IntervalBasis = struct
     else if is_top b then
       !^"⊤"
     else if Z.equal start stop then
-      !^(Z.to_string start)
+      z start
     else
-      brackets (!^(Z.to_string start) ^^ !^".." ^^ !^(Z.to_string stop))
+      brackets (z start ^^ !^".." ^^ z stop)
 
 
   let forward_abs_binop (op : IT.binop) (b1 : t) (b2 : t) : t option =

lib/testGeneration/bennet/abstractDomains/wrappedInterval.ml

@@ -720,9 +720,9 @@ module WrappedIntervalBasis = struct
     else if is_top b then
       !^"⊤"
     else if Z.equal start stop then
-      !^(Z.to_string start)
+      z start
     else
-      brackets (!^(Z.to_string start) ^^ !^".." ^^ !^(Z.to_string stop))
+      brackets (z start ^^ !^".." ^^ z stop)
 
 
   (* Bitwise operation helpers *)

lib/testGeneration/bennet/bennet.ml

@@ -32,36 +32,38 @@ let debug_stage (stage : string) (str : string) : unit =
 
 
 let parse_domain (s : string list) : (module Domain.T) =
-  let domain_names =
-    s |> List.map String.trim |> List.filter (fun x -> String.length x > 0)
-  in
-  (* Parse individual domain names *)
-  let parse_single_domain (name : string) : (module Domain.T) option =
-    match name with
-    | _ when String.equal name AbstractDomains.Ownership.name ->
-      Pp.(warn_noloc !^"Ownership abstract domain is always included");
-      None
-    | _ when String.equal name AbstractDomains.Interval.name ->
-      Some (module AbstractDomains.Interval)
-    | _ when String.equal name AbstractDomains.WrappedInterval.name ->
-      Some (module AbstractDomains.WrappedInterval)
-    | _ ->
-      Pp.warn_noloc Pp.(!^"Unknown abstract domain," ^^^ squotes !^name);
-      None
-  in
-  match domain_names with
-  | [] ->
-    (* No domains specified - return ownership domain *)
-    (module AbstractDomains.Ownership)
-  | additional_domains ->
-    (* Parse additional domains and filter out ownership if already specified *)
-    let parsed_additional = List.filter_map parse_single_domain additional_domains in
-    let ownership_module = (module AbstractDomains.Ownership : Domain.T) in
-    (* Check if ownership is already in the list *)
-    let all_domains = ownership_module :: parsed_additional in
-    (match all_domains with
-     | [ single ] -> single (* If only ownership, return it directly *)
-     | multiple -> AbstractDomains.product_domains multiple)
+  if List.is_empty s then (* Default *)
+    AbstractDomains.product_domains
+      [ (module AbstractDomains.Ownership); (module AbstractDomains.Interval) ]
+  else (
+    let domain_names =
+      s |> List.map String.trim |> List.filter (fun x -> String.length x > 0)
+    in
+    (* Parse individual domain names *)
+    let parse_single_domain (name : string) : (module Domain.T) option =
+      match name with
+      | _ when String.equal name AbstractDomains.Ownership.name -> None
+      | _ when String.equal name AbstractDomains.Interval.name ->
+        Some (module AbstractDomains.Interval)
+      | _ when String.equal name AbstractDomains.WrappedInterval.name ->
+        Some (module AbstractDomains.WrappedInterval)
+      | _ ->
+        Pp.warn_noloc Pp.(!^"Unknown abstract domain," ^^^ squotes !^name);
+        None
+    in
+    match domain_names with
+    | [] ->
+      (* No domains specified - return ownership domain *)
+      (module AbstractDomains.Ownership)
+    | additional_domains ->
+      (* Parse additional domains and filter out ownership if already specified *)
+      let parsed_additional = List.filter_map parse_single_domain additional_domains in
+      let ownership_module = (module AbstractDomains.Ownership : Domain.T) in
+      (* Check if ownership is already in the list *)
+      let all_domains = ownership_module :: parsed_additional in
+      (match all_domains with
+       | [ single ] -> single (* If only ownership, return it directly *)
+       | multiple -> AbstractDomains.product_domains multiple))
 
 
 let test_setup () : Pp.document =

lib/testGeneration/bennet/genContext.ml

@@ -30,7 +30,9 @@ 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 | `ArbitraryDomain _ | `Return _ -> Sym.Set.empty
+        | `Arbitrary | `Symbolic | `ArbitrarySpecialized _ | `ArbitraryDomain _
+        | `Return _ ->
+          Sym.Set.empty
         | `Pick gts -> gts |> List.map aux |> List.fold_left Sym.Set.union Sym.Set.empty
         | `PickSized wgts | `PickSizedElab (_, wgts) ->
           wgts

lib/testGeneration/bennet/genTerms.ml

@@ -11,6 +11,8 @@ module Base (AD : Domain.T) = struct
   type ('tag, 'recur) ast =
     [ `Arbitrary (** Generate arbitrary values *)
     | `Symbolic (** Generate symbolic 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
     | `Call of Sym.t * IT.t list
       (** Call a defined generator according to a [Sym.t] with arguments [IT.t list] *)
@@ -56,6 +58,13 @@ module type T = sig
 
   val symbolic_ : tag_t -> BT.t -> Locations.t -> t
 
+  val arbitrary_specialized_
+    :  (IT.t option * IT.t option) * (IT.t option * IT.t option) ->
+    tag_t ->
+    BT.t ->
+    Locations.t ->
+    t
+
   val arbitrary_domain_ : AD.Relative.t -> tag_t -> BT.t -> Locations.t -> t
 
   val call_ : Sym.t * IT.t list -> tag_t -> BT.t -> Locations.t -> t
@@ -149,6 +158,17 @@ module Make (GT : T) = struct
     match tm_ with
     | `Arbitrary -> !^"arbitrary" ^^ angles (BT.pp bt) ^^ parens empty
     | `Symbolic -> !^"symbolic" ^^ angles (BT.pp bt) ^^ parens empty
+    | `ArbitrarySpecialized ((min_inc, min_ex), (max_inc, max_ex)) ->
+      let pp_opt = function
+        | None -> !^"None"
+        | Some it -> !^"Some" ^^^ parens (IT.pp it)
+      in
+      !^"arbitrary_specialized"
+      ^^ angles (BT.pp bt)
+      ^^ parens
+           (parens (pp_opt min_inc ^^ comma ^^^ pp_opt min_ex)
+            ^^ comma
+            ^^^ parens (pp_opt max_inc ^^ comma ^^^ pp_opt max_ex))
     | `ArbitraryDomain d ->
       !^"arbitrary_domain" ^^ angles (BT.pp bt) ^^ parens (AD.Relative.pp d)
     | `Call (fsym, iargs) ->
@@ -255,6 +275,8 @@ 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
+    | `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
     | `Asgn ((it_addr, _), it_val, gt') | `AsgnElab (_, ((_, it_addr), _), it_val, gt') ->
       Sym.Map.union
@@ -323,7 +345,8 @@ module Make (GT : T) = struct
   let rec contains_call (gt : GT.t) : bool =
     let (Annot (gt_, _, _, _)) = gt in
     match gt_ with
-    | `Arbitrary | `ArbitraryDomain _ | `Symbolic | `Return _ -> false
+    | `Arbitrary | `ArbitraryDomain _ | `ArbitrarySpecialized _ | `Symbolic | `Return _ ->
+      false
     | `Call _ | `CallSized _ -> true
     | `LetStar ((_, gt1), gt2) | `ITE (_, gt1, gt2) ->
       contains_call gt1 || contains_call gt2
@@ -344,7 +367,8 @@ module Make (GT : T) = struct
   let rec contains_constraint (gt : GT.t) : bool =
     let (Annot (gt_, _, _, _)) = gt in
     match gt_ with
-    | `Arbitrary | `ArbitraryDomain _ | `Symbolic | `Return _ -> false
+    | `Arbitrary | `ArbitraryDomain _ | `ArbitrarySpecialized _ | `Symbolic | `Return _ ->
+      false
     | `Asgn _ | `AsgnElab _ | `Assert _ | `AssertDomain _ -> true
     | `Call _ | `CallSized _ -> true (* Could be less conservative... *)
     | `LetStar ((_, gt1), gt2) | `ITE (_, gt1, gt2) ->
@@ -362,6 +386,11 @@ module Make (GT : T) = struct
       let (Annot (gt_, _, _, _)) = gt in
       match gt_ with
       | `Arbitrary | `Symbolic | `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
+        |> List.map IT.preds_of
+        |> List.fold_left Sym.Set.union Sym.Set.empty
       | `Return it -> IT.preds_of it
       | `Call (_, its) | `CallSized (_, its, _) ->
         its |> List.map IT.preds_of |> List.fold_left Sym.Set.union Sym.Set.empty
@@ -392,6 +421,13 @@ module Make (GT : T) = struct
     match gt_ with
     | `Arbitrary -> arbitrary_ tag bt loc
     | `Symbolic -> symbolic_ 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),
+          (Option.map (IT.subst su) max_inc, Option.map (IT.subst su) max_ex) )
+        tag
+        bt
+        loc
     | `ArbitraryDomain ad -> arbitrary_domain_ ad tag bt loc
     | `Call (fsym, iargs) -> call_ (fsym, List.map (IT.subst su) iargs) tag bt loc
     | `CallSized (fsym, iargs, sz) ->
@@ -460,6 +496,7 @@ module Make (GT : T) = struct
     match gt_ with
     | `Arbitrary -> arbitrary_ tag bt loc
     | `Symbolic -> symbolic_ 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
     | `CallSized (fsym, its, sz) -> call_sized_ (fsym, its, sz) tag bt loc
@@ -502,6 +539,7 @@ module Make (GT : T) = struct
       match gt_ with
       | `Arbitrary -> arbitrary_ tag bt loc
       | `Symbolic -> symbolic_ 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
       | `CallSized (fsym, its, sz) -> call_sized_ (fsym, its, sz) tag bt loc
@@ -544,6 +582,7 @@ module Make (GT : T) = struct
     match tm with
     | `Arbitrary -> `Arbitrary
     | `Symbolic -> `Symbolic
+    | `ArbitrarySpecialized bounds -> `ArbitrarySpecialized bounds
     | `ArbitraryDomain ad -> `ArbitraryDomain ad
     | `Call (fsym, iargs) -> `Call (fsym, iargs)
     | `CallSized (fsym, iargs, sz) -> `CallSized (fsym, iargs, sz)
@@ -576,6 +615,7 @@ module Make (GT : T) = struct
     match tm_ with
     | `Arbitrary -> arbitrary_ tag bt loc
     | `Symbolic -> symbolic_ 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
     | `CallSized (fsym, iargs, sz) -> call_sized_ (fsym, iargs, sz) tag bt loc
@@ -678,6 +718,8 @@ module Defaults (StageName : sig
 struct
   let unsupported name = failwith (name ^ " not supported in " ^ StageName.name ^ " DSL")
 
+  let arbitrary_specialized_ _ _ _ _ = unsupported "arbitrary_specialized_"
+
   let arbitrary_domain_ _ _ _ _ = unsupported "arbitrary_domain_"
 
   let pick_ _ _ _ _ = unsupported "pick_"

lib/testGeneration/bennet/stage3/smtPruning.ml

@@ -13,7 +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 _ | `Symbolic | `Return _ | `Call _ ->
+      | `Arbitrary | `ArbitraryDomain _ | `ArbitrarySpecialized _ | `Symbolic | `Return _
+      | `Call _ ->
         let@ check = provable loc in
         return
           (match check (LC.T (IT.bool_ false here)) with