[Bennet] Expand SMT pruning to include ADs

lib/testGeneration/bennet/abstractDomains/interpreter.ml

@@ -69,7 +69,7 @@ module Make (GT : GenTerms.T) (I : Domain.T with type t = GT.AD.t) = struct
             (match Ctx.find_opt fsym defs_ctx with
              | Some callee_gd ->
                (* Convert callee's domain to a constraint *)
-               let callee_constraint = AD.to_it callee_d in
+               let callee_constraint = AD.to_lc callee_d in
                (* Create substitution: formal_param -> actual_arg *)
                let subst =
                  IT.make_subst
@@ -79,9 +79,9 @@ module Make (GT : GenTerms.T) (I : Domain.T with type t = GT.AD.t) = struct
                       actual_args)
                in
                (* Substitute to get constraint in caller's terms *)
-               let caller_constraint = IT.subst subst callee_constraint in
+               let caller_constraint = LC.subst subst callee_constraint in
                (* Propagate constraint to refine caller's domain *)
-               I.abs_assert (LC.T caller_constraint) d
+               I.abs_assert caller_constraint d
              | None -> AD.meet d callee_d)
           | None ->
             (* function has no ownership info *)

lib/testGeneration/bennet/abstractDomains/interval_.ml

@@ -434,6 +434,10 @@ module IntervalBasis = struct
       let start_it = IT.num_lit_ t.start bt' loc in
       let stop_it = IT.num_lit_ t.stop bt' loc in
       IT.and_ [ IT.le_ (start_it, sym_it) loc; IT.le_ (sym_it, stop_it) loc ] loc)
+
+
+  let to_lc (t : t) (sym : Sym.t) : LogicalConstraints.t =
+    LogicalConstraints.T (to_it sym t)
 end
 
 module Inner : Domain.T = NonRelational.Make (IntervalBasis)

lib/testGeneration/bennet/abstractDomains/nonRelational.ml

@@ -657,6 +657,8 @@ module Make (B : BASIS) = struct
       IT.and_ constraints loc (* conjunction of all basis constraints *)
 
 
+  let to_lc (od : t) : LC.t = LC.T (to_it od)
+
   let is_meet_assoc = B.is_meet_assoc
 
   let is_join_assoc = B.is_join_assoc

lib/testGeneration/bennet/abstractDomains/ownership.ml

@@ -9,6 +9,7 @@
    - Some map tracks specific ownership bounds per symbol
 *)
 
+module BT = BaseTypes
 module IT = IndexTerms
 module LC = LogicalConstraints
 
@@ -24,33 +25,48 @@ module Inner = struct
   end
 
   module Relative = struct
-    type t = (int * int) option [@@deriving eq, ord]
+    type t = (BT.t * (int * int)) option [@@deriving eq, ord]
 
     let name = name
 
     let is_top oo =
-      match oo with Some (before, after) -> before == 0 && after == 0 | None -> false
+      match oo with
+      | Some (_, (before, after)) -> before == 0 && after == 0
+      | None -> false
 
 
     let is_bottom oo = Option.is_none oo
 
     let pp ob =
       let open Pp in
       match ob with
-      | Some (0, 0) -> !^"⊤"
-      | Some (front, back) ->
+      | Some (_, (0, 0)) -> !^"⊤"
+      | Some (_, (front, back)) ->
         !^"owns" ^^^ int front ^^^ !^"bytes in front and" ^^^ int back ^^^ !^"bytes after"
       | None -> !^"⊥"
 
 
     let pp_args oo =
       (* Should only be called on non-top/bottom *)
-      let before, after = Option.get oo in
+      let _, (before, after) = Option.get oo in
       string_of_int before ^ ", " ^ string_of_int after
+
+
+    let to_it (oo : t) (sym : Sym.t) : IT.t =
+      let loc = Locations.other __LOC__ in
+      match oo with
+      | Some (_, (0, 0)) | None -> IT.bool_ true loc
+      | Some (bt, (_, _)) ->
+        IT.not_
+          (IT.eq_ (IT.cast_ (BT.Loc ()) (IT.sym_ (sym, bt, loc)) loc, IT.null_ loc) loc)
+          loc
+
+
+    let to_lc (oo : t) (sym : Sym.t) : LC.t = LC.T (to_it oo sym)
   end
 
   (* Type represents ownership information as optional map from symbols to (front, back) byte counts *)
-  type t = (int * int) Sym.Map.t option [@@deriving eq, ord]
+  type t = (BT.t * (int * int)) Sym.Map.t option [@@deriving eq, ord]
 
   let bottom = None
 
@@ -68,9 +84,9 @@ module Inner = struct
       let d2 = Option.get d2 in
       (* d1 ≤ d2 if for each symbol in d1, its ownership bounds are >= those in d2 *)
       Sym.Map.for_all
-        (fun x (front, back) ->
+        (fun x (_, (front, back)) ->
            match Sym.Map.find_opt x d2 with
-           | Some (front', back') -> front >= front' && back >= back'
+           | Some (_, (front', back')) -> front >= front' && back >= back'
            | None -> true)
         d1)
 
@@ -84,16 +100,16 @@ module Inner = struct
         (Sym.Map.merge
            (fun _ o1 o2 ->
               match (o1, o2) with
-              | Some (front1, back1), Some (front2, back2) ->
+              | Some (bt, (front1, back1)), Some (_, (front2, back2)) ->
                 (* Take minimum bounds - more permissive ownership *)
-                Some (min front1 front2, min back1 back2)
+                Some (bt, (min front1 front2, min back1 back2))
               | None, _ | _, None -> None)
            d1
            d2)
     | None, d | d, None -> d
 
 
-  let join_many = List.fold_left join bottom
+  let join_many ds = List.fold_left join bottom ds
 
   (* Meet (greatest lower bound): combines ownership by taking maximum bounds
      This represents the least restrictive ownership that satisfies both inputs *)
@@ -104,16 +120,16 @@ module Inner = struct
         (Sym.Map.merge
            (fun _ o1 o2 ->
               match (o1, o2) with
-              | Some (front1, back1), Some (front2, back2) ->
+              | Some (bt, (front1, back1)), Some (_, (front2, back2)) ->
                 (* Take maximum bounds - more restrictive ownership *)
-                Some (max front1 front2, max back1 back2)
+                Some (bt, (max front1 front2, max back1 back2))
               | None, o | o, None -> o) (* include ownership from either side *)
            d1
            d2)
     | None, _ | _, None -> None (* meet with bottom gives bottom *)
 
 
-  let meet_many = List.fold_left meet top
+  let meet_many ds = List.fold_left meet top ds
 
   let rename ~(from : Sym.t) ~(to_ : Sym.t) (d : t) =
     let open Option in
@@ -135,10 +151,10 @@ module Inner = struct
     return (Sym.Map.filter (fun x _ -> Sym.Set.mem x xs) d)
 
 
-  let relative_to (x : Sym.t) (_ : BaseTypes.t) (d : t) : Relative.t =
+  let relative_to (x : Sym.t) (bt : BaseTypes.t) (d : t) : Relative.t =
     let open Option in
     let@ d = d in
-    return (Option.value ~default:(0, 0) (Sym.Map.find_opt x d))
+    return (Option.value ~default:(bt, (0, 0)) (Sym.Map.find_opt x d))
 
 
   let free_vars (od : t) =
@@ -148,9 +164,7 @@ module Inner = struct
 
 
   let free_vars_bts (od : t) : BaseTypes.t Sym.Map.t =
-    match od with
-    | Some d -> Sym.Map.map (fun _ -> BaseTypes.Loc ()) d
-    | None -> Sym.Map.empty
+    match od with Some d -> Sym.Map.map (fun (bt, _) -> bt) d | None -> Sym.Map.empty
 
 
   let pp d =
@@ -160,15 +174,15 @@ module Inner = struct
     | Some d ->
       separate_map
         (semi ^^ break 1)
-        (fun (x, (front, back)) ->
+        (fun (x, (_, (front, back))) ->
            Sym.pp x
            ^^^ !^"owns"
            ^^^ int front
            ^^^ !^"bytes in front and"
            ^^^ int back
            ^^^ !^"bytes after")
         (List.filter
-           (fun (_, (front, back)) -> not (front = 0 && back = 0))
+           (fun (_, (_, (front, back))) -> not (front = 0 && back = 0))
            (Sym.Map.bindings d))
     | None -> !^"⊥"
 
@@ -206,9 +220,9 @@ module Inner = struct
       let end_offset = start_offset + Memory.size_of_ctype sct in
       if start_offset < 0 then
         (* If [start_offset] is negative, [end_offset] might be negative *)
-        meet (Some (Sym.Map.singleton p (-start_offset, max 0 end_offset))) d
+        meet (Some (Sym.Map.singleton p (p_bt, (-start_offset, max 0 end_offset)))) d
       else (* If [start_offset] is positive, [end_offset] must be positive *)
-        meet (Some (Sym.Map.singleton p (0, end_offset))) d
+        meet (Some (Sym.Map.singleton p (p_bt, (0, end_offset)))) d
     | None -> d
 
 
@@ -223,6 +237,8 @@ module Inner = struct
     | Some _ -> IT.bool_ true loc (* ownership has no numeric constraints to express *)
 
 
+  let to_lc (d : t) : LC.t = LC.T (to_it d)
+
   let is_meet_assoc = true
 
   let is_join_assoc = true

lib/testGeneration/bennet/abstractDomains/product.ml

@@ -535,6 +535,17 @@ let product_domains (domains : (module Domain.T) list) =
           |> Array.map (fun (RPack ((module R), r)) -> R.pp_args r)
           |> Array.to_list
           |> String.concat ", "
+
+
+        let to_lc (s : t) (sym : Sym.t) : LC.t =
+          let loc = Locations.other __LOC__ in
+          let constraints =
+            s
+            |> Array.to_list
+            |> List.filter_map (fun (RPack ((module R), r)) ->
+              match R.to_lc r sym with LC.T it -> Some it | _ -> failwith "TODO")
+          in
+          LC.T (IT.and_ constraints loc)
       end
 
       let name = name
@@ -773,13 +784,16 @@ let product_domains (domains : (module Domain.T) list) =
         |> String.concat ", "
 
 
-      let to_it (product : t) : IT.t =
+      let to_lc (product : t) : LC.t =
         let loc = Locations.other __LOC__ in
         let constraints =
           Array.to_list product
-          |> List.map (fun comp -> match comp with DPack ((module D), s) -> D.to_it s)
+          |> List.map (fun comp ->
+            match comp with
+            | DPack ((module D), s) ->
+              (match D.to_lc s with LC.T it -> it | _ -> failwith "TODO"))
         in
-        IT.and_ constraints loc
+        LC.T (IT.and_ constraints loc)
 
 
       let is_meet_assoc =

lib/testGeneration/bennet/abstractDomains/wrappedInterval.ml

@@ -1284,6 +1284,10 @@ module WrappedIntervalBasis = struct
         IT.and_ [ IT.le_ (start_it, sym_it) loc; IT.le_ (sym_it, stop_it) loc ] loc
       else (* Wrapped interval [start..max] ∪ [min..stop]: start <= X || X <= stop *)
         IT.or_ [ IT.le_ (start_it, sym_it) loc; IT.le_ (sym_it, stop_it) loc ] loc)
+
+
+  let to_lc (t : t) (sym : Sym.t) : LogicalConstraints.t =
+    LogicalConstraints.T (to_it sym t)
 end
 
 module Inner : Domain.T = NonRelational.Make (WrappedIntervalBasis)

lib/testGeneration/bennet/domain.ml

@@ -22,6 +22,8 @@ module type RELATIVE_VIEW = sig
   val pp : t -> Pp.document
 
   val pp_args : t -> string
+
+  val to_lc : t -> Sym.t -> LC.t
 end
 
 module type T = sig
@@ -89,7 +91,7 @@ module type T = sig
   val abs_assign : (IT.t * Sctypes.t) * IT.t -> t -> t
 
   (** Check truthiness *)
-  val to_it : t -> IT.t
+  val to_lc : t -> LC.t
 
   (** Whether meet is associative (allows optimization) *)
   val is_meet_assoc : bool

lib/testGeneration/bennet/stage4/smtPruning.ml

@@ -75,6 +75,22 @@ 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)
+        ->
+        let@ () = add_l x bt' (loc, lazy (Sym.pp x)) in
+        let@ gt_rest = aux new_constraint gt_rest in
+        return
+          (let open Option in
+           let@ gt_rest in
+           return (Term.let_star_ ((x, gt_inner), gt_rest) () loc))
+      | `LetStar ((x, (Annot (`ArbitraryDomain ad, _, bt', _) as gt_inner)), gt_rest) ->
+        let@ () = add_l x bt' (loc, lazy (Sym.pp x)) in
+        let@ () = add_c loc (AD.Relative.to_lc ad x) in
+        let@ gt_rest = aux new_constraint gt_rest in
+        return
+          (let open Option in
+           let@ gt_rest in
+           return (Term.let_star_ ((x, gt_inner), gt_rest) () loc))
       | `LetStar ((x, gt_inner), gt_rest) ->
         let@ gt_inner = pure (aux new_constraint gt_inner) in
         (match gt_inner with
@@ -104,12 +120,26 @@ module Make (AD : Domain.T) = struct
           (let open Option in
            let@ gt_rest in
            return (if redundant then gt_rest else Term.assert_ (lc, gt_rest) () loc))
-      | `AssertDomain (domain, gt_rest) ->
+      | `AssertDomain (ad, gt_rest) ->
+        let@ check = provable loc in
+        let@ redundant =
+          let lc = AD.to_lc ad in
+          if remove_redundant then (
+            match check lc with
+            | `True -> return true
+            | `False ->
+              let@ () = add_c loc lc in
+              return false)
+          else
+            let@ () = add_c loc lc in
+            return false
+        in
         let@ gt_rest = aux true gt_rest in
         return
           (let open Option in
            let@ gt_rest in
-           return (Term.assert_domain_ (domain, gt_rest) () loc))
+           return
+             (if redundant then gt_rest else Term.assert_domain_ (ad, gt_rest) () loc))
       | `ITE (it_if, gt_then, gt_else) ->
         let@ check = provable loc in
         let@ ogt_then =

lib/testGeneration/bennet/stage7/convert.ml

@@ -861,8 +861,8 @@ module Make (AD : Domain.T) = struct
         transform_term filename sigma ctx name gt_rest
       else (
         (* Filter abstract domain to only include in-scope variables *)
-        let it = AD.to_it ad in
-        let b_cond, s_cond, e_cond = transform_it filename sigma name it in
+        let lc = AD.to_lc ad in
+        let b_cond, s_cond, e_cond = transform_lc filename sigma lc in
         let s_begin =
           A.
             [ AilSexpr