[sledge] Change: Arithmetic comparison formulas to unary

Summary:
The unary forms are primitive in ICS, and in uncoming changes which
involve considering the product of a term and an equality relation, it
is more efficient to have unary constructors since the product is then
linear instead of quadratic in the size of the equality relation.

Reviewed By: jvillard

Differential Revision: D22571138

fbshipit-source-id: e0b745cc8

sledge/src/exec.ml

@@ -87,7 +87,7 @@ let gen_spec us specm =
  * Instruction small axioms
  *)
 
-let null_eq ptr = Sh.pure (Formula.eq Term.zero ptr)
+let null_eq ptr = Sh.pure (Formula.eq0 ptr)
 
 let eq_concat (siz, seq) ms =
   Formula.eq (Term.sized ~siz ~seq)
@@ -156,8 +156,7 @@ let memcpy_eq_spec dst src len =
   let+ seg = Fresh.seg dst ~len in
   let dst_heap = Sh.seg seg in
   let foot =
-    Sh.and_ (Formula.eq dst src)
+    Sh.and_ (Formula.eq dst src) (Sh.and_ (Formula.eq0 len) dst_heap)
-      (Sh.and_ (Formula.eq len Term.zero) dst_heap)
   in
   let post = dst_heap in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
@@ -336,7 +335,7 @@ let malloc_spec reg siz =
  * { r=0 ∨ ∃α'. r-[r;sΘ)->⟨sΘ,α'⟩ }
  *)
 let mallocx_spec reg siz =
-  let foot = Sh.pure (Formula.dq siz Term.zero) in
+  let foot = Sh.pure (Formula.dq0 siz) in
   let* sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:(Term.fv siz) in
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
@@ -410,7 +409,7 @@ let realloc_spec reg ptr siz =
   let+ a2 = Fresh.var "a" in
   let post =
     Sh.or_
-      (Sh.and_ (Formula.eq loc Term.zero) (Sh.rename sub foot))
+      (Sh.and_ (Formula.eq0 loc) (Sh.rename sub foot))
       (Sh.and_
          (Formula.cond ~cnd:(Formula.le len siz)
             ~pos:(eq_concat (siz, a1) [|(len, a0); (Term.sub siz len, a2)|])
@@ -429,7 +428,7 @@ let rallocx_spec reg ptr siz =
   let* len = Fresh.var "m" in
   let* pseg = Fresh.seg ptr ~bas:ptr ~len ~siz:len in
   let pheap = Sh.seg pseg in
-  let foot = Sh.and_ (Formula.dq siz Term.zero) pheap in
+  let foot = Sh.and_ (Formula.dq0 siz) pheap in
   let* sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
@@ -439,7 +438,7 @@ let rallocx_spec reg ptr siz =
   let+ a2 = Fresh.var "a" in
   let post =
     Sh.or_
-      (Sh.and_ (Formula.eq loc Term.zero) (Sh.rename sub pheap))
+      (Sh.and_ (Formula.eq0 loc) (Sh.rename sub pheap))
       (Sh.and_
          (Formula.cond ~cnd:(Formula.le len siz)
             ~pos:(eq_concat (siz, a1) [|(len, a0); (Term.sub siz len, a2)|])
@@ -456,7 +455,7 @@ let rallocx_spec reg ptr siz =
 let xallocx_spec reg ptr siz ext =
   let* len = Fresh.var "m" in
   let* seg = Fresh.seg ptr ~bas:ptr ~len ~siz:len in
-  let foot = Sh.and_ (Formula.dq siz Term.zero) (Sh.seg seg) in
+  let foot = Sh.and_ (Formula.dq0 siz) (Sh.seg seg) in
   let* sub, ms =
     Fresh.assign ~ws:(Var.Set.of_ reg)
       ~rs:Var.Set.(union foot.us (union (Term.fv siz) (Term.fv ext)))
@@ -510,7 +509,7 @@ let malloc_usable_size_spec reg ptr =
  * { r=0 ∨ r=sΘ }
  *)
 let nallocx_spec reg siz =
-  let foot = Sh.pure (Formula.dq siz Term.zero) in
+  let foot = Sh.pure (Formula.dq0 siz) in
   let+ sub, ms = Fresh.assign ~ws:(Var.Set.of_ reg) ~rs:foot.us in
   let loc = Term.var reg in
   let siz = Term.rename sub siz in
@@ -528,9 +527,8 @@ let mallctl_read_spec r i w n =
   let* rseg = Fresh.seg r ~siz:iseg.seq in
   let+ a = Fresh.var "a" in
   let foot =
-    Sh.and_ (Formula.eq w Term.zero)
+    Sh.and_ (Formula.eq0 w)
-      (Sh.and_ (Formula.eq n Term.zero)
+      (Sh.and_ (Formula.eq0 n) (Sh.star (Sh.seg iseg) (Sh.seg rseg)))
-         (Sh.star (Sh.seg iseg) (Sh.seg rseg)))
   in
   let rseg' = {rseg with seq= a} in
   let post = Sh.star (Sh.seg rseg') (Sh.seg iseg) in
@@ -550,8 +548,8 @@ let mallctlbymib_read_spec p l r i w n =
   let const = Sh.star (Sh.seg pseg) (Sh.seg iseg) in
   let+ a = Fresh.var "a" in
   let foot =
-    Sh.and_ (Formula.eq w Term.zero)
+    Sh.and_ (Formula.eq0 w)
-      (Sh.and_ (Formula.eq n Term.zero) (Sh.star const (Sh.seg rseg)))
+      (Sh.and_ (Formula.eq0 n) (Sh.star const (Sh.seg rseg)))
   in
   let rseg' = {rseg with seq= a} in
   let post = Sh.star (Sh.seg rseg') const in
@@ -564,9 +562,7 @@ let mallctlbymib_read_spec p l r i w n =
 let mallctl_write_spec r i w n =
   let+ seg = Fresh.seg w ~siz:n in
   let post = Sh.seg seg in
-  let foot =
+  let foot = Sh.and_ (Formula.eq0 r) (Sh.and_ (Formula.eq0 i) post) in
-    Sh.and_ (Formula.eq r Term.zero) (Sh.and_ (Formula.eq i Term.zero) post)
-  in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
 (* { p-[_;_)->⟨W×l,_⟩ * r=0 * i=0 * w-[_;_)->⟨n,_⟩ }
@@ -579,9 +575,7 @@ let mallctlbymib_write_spec p l r i w n =
   let* pseg = Fresh.seg p ~siz:wl in
   let+ wseg = Fresh.seg w ~siz:n in
   let post = Sh.star (Sh.seg pseg) (Sh.seg wseg) in
-  let foot =
+  let foot = Sh.and_ (Formula.eq0 r) (Sh.and_ (Formula.eq0 i) post) in
-    Sh.and_ (Formula.eq r Term.zero) (Sh.and_ (Formula.eq i Term.zero) post)
-  in
   {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post}
 
 let mallctl_specs r i w n =

sledge/src/fol.ml

@@ -133,8 +133,12 @@ type fml =
   | Ff
   | Eq of trm * trm
   | Dq of trm * trm
-  | Lt of trm * trm
+  | Eq0 of trm  (** [Eq0(x)] iff x = 0 *)
-  | Le of trm * trm
+  | Dq0 of trm  (** [Dq0(x)] iff x ≠ 0 *)
+  | Gt0 of trm  (** [Gt0(x)] iff x > 0 *)
+  | Ge0 of trm  (** [Ge0(x)] iff x ≥ 0 *)
+  | Lt0 of trm  (** [Lt0(x)] iff x < 0 *)
+  | Le0 of trm  (** [Le0(x)] iff x ≤ 0 *)
   | And of fml * fml
   | Or of fml * fml
   | Iff of fml * fml
@@ -146,8 +150,12 @@ type fml =
 
 let _Eq x y = Eq (x, y)
 let _Dq x y = Dq (x, y)
-let _Lt x y = Lt (x, y)
+let _Eq0 x = Eq0 x
-let _Le x y = Le (x, y)
+let _Dq0 x = Dq0 x
+let _Gt0 x = Gt0 x
+let _Ge0 x = Ge0 x
+let _Lt0 x = Lt0 x
+let _Le0 x = Le0 x
 let _And p q = And (p, q)
 let _Or p q = Or (p, q)
 let _Iff p q = Iff (p, q)
@@ -461,8 +469,12 @@ let ppx_f strength fs fml =
     | Ff -> pf "ff"
     | Eq (x, y) -> pf "(%a@ = %a)" pp_t x pp_t y
     | Dq (x, y) -> pf "(%a@ @<2>≠ %a)" pp_t x pp_t y
-    | Lt (x, y) -> pf "(%a@ < %a)" pp_t x pp_t y
+    | Eq0 x -> pf "(0 = %a)" pp_t x
-    | Le (x, y) -> pf "(%a@ @<2>≤ %a)" pp_t x pp_t y
+    | Dq0 x -> pf "(0 @<2>≠ %a)" pp_t x
+    | Gt0 x -> pf "(0 < %a)" pp_t x
+    | Ge0 x -> pf "(0 @<2>≤ %a)" pp_t x
+    | Lt0 x -> pf "(0 > %a)" pp_t x
+    | Le0 x -> pf "(0 @<2>≥ %a)" pp_t x
     | And (x, y) -> pf "(%a@ @<2>∧ %a)" pp x pp y
     | Or (x, y) -> pf "(%a@ @<2>∨ %a)" pp x pp y
     | Iff (x, y) -> pf "(%a@ <=> %a)" pp x pp y
@@ -518,8 +530,8 @@ let rec fold_vars_t e ~init ~f =
 let rec fold_vars_f ~init p ~f =
   match (p : fml) with
   | Tt | Ff -> init
-  | Eq (x, y) | Dq (x, y) | Lt (x, y) | Le (x, y) ->
+  | Eq (x, y) | Dq (x, y) -> fold_vars_t ~f x ~init:(fold_vars_t ~f y ~init)
-      fold_vars_t ~f x ~init:(fold_vars_t ~f y ~init)
+  | Eq0 x | Dq0 x | Gt0 x | Ge0 x | Lt0 x | Le0 x -> fold_vars_t ~f x ~init
   | And (x, y) | Or (x, y) | Iff (x, y) | Xor (x, y) ->
       fold_vars_f ~f x ~init:(fold_vars_f ~f y ~init)
   | Cond {cnd; pos; neg} ->
@@ -582,8 +594,12 @@ let rec map_vars_f ~f e =
   | Tt | Ff -> e
   | Eq (x, y) -> map2 (map_vars_t ~f) e _Eq x y
   | Dq (x, y) -> map2 (map_vars_t ~f) e _Dq x y
-  | Lt (x, y) -> map2 (map_vars_t ~f) e _Lt x y
+  | Eq0 x -> map1 (map_vars_t ~f) e _Eq0 x
-  | Le (x, y) -> map2 (map_vars_t ~f) e _Le x y
+  | Dq0 x -> map1 (map_vars_t ~f) e _Dq0 x
+  | Gt0 x -> map1 (map_vars_t ~f) e _Gt0 x
+  | Ge0 x -> map1 (map_vars_t ~f) e _Ge0 x
+  | Lt0 x -> map1 (map_vars_t ~f) e _Lt0 x
+  | Le0 x -> map1 (map_vars_t ~f) e _Le0 x
   | And (x, y) -> map2 (map_vars_f ~f) e _And x y
   | Or (x, y) -> map2 (map_vars_f ~f) e _Or x y
   | Iff (x, y) -> map2 (map_vars_f ~f) e _Iff x y
@@ -699,6 +715,9 @@ let ap1 : (trm -> exp) -> exp -> exp =
 
 let ap1t : (trm -> trm) -> exp -> exp = fun f -> ap1 (fun x -> `Trm (f x))
 
+let ap1f : (trm -> fml) -> exp -> fml =
+ fun f x -> map_cnd _Cond f (embed_into_cnd x)
+
 (** Map a binary function on terms over conditional terms. This yields a
     conditional tree with the structure from the first argument where each
     leaf has been replaced by a conditional tree with the structure from the
@@ -908,8 +927,25 @@ module Formula = struct
 
   let eq = ap2f _Eq
   let dq = ap2f _Dq
-  let lt = ap2f _Lt
+  let eq0 = ap1f _Eq0
-  let le = ap2f _Le
+  let dq0 = ap1f _Dq0
+  let gt0 = ap1f _Gt0
+  let ge0 = ap1f _Ge0
+  let lt0 = ap1f _Lt0
+  let le0 = ap1f _Le0
+
+  let gt a b =
+    if a == Term.zero then lt0 b
+    else if b == Term.zero then gt0 a
+    else gt0 (Term.sub a b)
+
+  let ge a b =
+    if a == Term.zero then le0 b
+    else if b == Term.zero then ge0 a
+    else ge0 (Term.sub a b)
+
+  let lt a b = gt b a
+  let le a b = ge b a
 
   (* connectives *)
 
@@ -926,8 +962,12 @@ module Formula = struct
     | Ff -> Tt
     | Eq (x, y) -> Dq (x, y)
     | Dq (x, y) -> Eq (x, y)
-    | Lt (x, y) -> Le (y, x)
+    | Eq0 x -> Dq0 x
-    | Le (x, y) -> Lt (y, x)
+    | Dq0 x -> Eq0 x
+    | Gt0 x -> Le0 x
+    | Ge0 x -> Lt0 x
+    | Lt0 x -> Ge0 x
+    | Le0 x -> Gt0 x
     | And (x, y) -> Or (not_ x, not_ y)
     | Or (x, y) -> And (not_ x, not_ y)
     | Iff (x, y) -> Xor (x, y)
@@ -1043,8 +1083,12 @@ let rec f_to_ses : fml -> Ses.Term.t = function
   | Ff -> Ses.Term.false_
   | Eq (x, y) -> Ses.Term.eq (t_to_ses x) (t_to_ses y)
   | Dq (x, y) -> Ses.Term.dq (t_to_ses x) (t_to_ses y)
-  | Lt (x, y) -> Ses.Term.lt (t_to_ses x) (t_to_ses y)
+  | Eq0 x -> Ses.Term.eq Ses.Term.zero (t_to_ses x)
-  | Le (x, y) -> Ses.Term.le (t_to_ses x) (t_to_ses y)
+  | Dq0 x -> Ses.Term.dq Ses.Term.zero (t_to_ses x)
+  | Gt0 x -> Ses.Term.lt Ses.Term.zero (t_to_ses x)
+  | Ge0 x -> Ses.Term.le Ses.Term.zero (t_to_ses x)
+  | Lt0 x -> Ses.Term.lt (t_to_ses x) Ses.Term.zero
+  | Le0 x -> Ses.Term.le (t_to_ses x) Ses.Term.zero
   | And (p, q) -> Ses.Term.and_ (f_to_ses p) (f_to_ses q)
   | Or (p, q) -> Ses.Term.or_ (f_to_ses p) (f_to_ses q)
   | Iff (p, q) -> Ses.Term.eq (f_to_ses p) (f_to_ses q)
@@ -1467,13 +1511,13 @@ module Term_of_Llair = struct
         ap_fff (fun p q -> or_ p (not_ q)) p q
     | Ap2 (Eq, _, d, e) -> ap_ttf eq d e
     | Ap2 (Dq, _, d, e) -> ap_ttf dq d e
-    | Ap2 (Gt, _, d, e) -> ap_ttf lt e d
+    | Ap2 (Gt, _, d, e) -> ap_ttf gt d e
     | Ap2 (Lt, _, d, e) -> ap_ttf lt d e
-    | Ap2 (Ge, _, d, e) -> ap_ttf le e d
+    | Ap2 (Ge, _, d, e) -> ap_ttf ge d e
     | Ap2 (Le, _, d, e) -> ap_ttf le d e
-    | Ap2 (Ugt, typ, d, e) -> usap_ttf lt typ e d
+    | Ap2 (Ugt, typ, d, e) -> usap_ttf gt typ d e
     | Ap2 (Ult, typ, d, e) -> usap_ttf lt typ d e
-    | Ap2 (Uge, typ, d, e) -> usap_ttf le typ e d
+    | Ap2 (Uge, typ, d, e) -> usap_ttf ge typ d e
     | Ap2 (Ule, typ, d, e) -> usap_ttf le typ d e
     | Ap2 (Ord, _, d, e) -> ap_ttf (upos2 Ordered) d e
     | Ap2 (Uno, _, d, e) -> ap_ttf (uneg2 Ordered) d e

sledge/src/fol.mli

@@ -145,6 +145,14 @@ and Formula : sig
   (* comparisons *)
   val eq : Term.t -> Term.t -> t
   val dq : Term.t -> Term.t -> t
+  val eq0 : Term.t -> t
+  val dq0 : Term.t -> t
+  val gt0 : Term.t -> t
+  val ge0 : Term.t -> t
+  val lt0 : Term.t -> t
+  val le0 : Term.t -> t
+  val gt : Term.t -> Term.t -> t
+  val ge : Term.t -> Term.t -> t
   val lt : Term.t -> Term.t -> t
   val le : Term.t -> Term.t -> t
 

sledge/src/sh.ml

@@ -587,8 +587,7 @@ let rec pure_approx q =
   Formula.andN
     ( [q.pure]
     |> fun init ->
-    List.fold ~init q.heap ~f:(fun p seg ->
+    List.fold ~init q.heap ~f:(fun p seg -> Formula.dq0 seg.loc :: p)
-        Formula.dq Term.zero seg.loc :: p )
     |> fun init ->
     List.fold ~init q.djns ~f:(fun p djn ->
         Formula.orN (List.map djn ~f:pure_approx) :: p ) )

sledge/src/solver_test.ml

@@ -270,7 +270,7 @@ let%test_module _ =
       [%expect
         {|
         ( infer_frame:
-            (%n_9 ≤ 2)
+            (0 ≤ (2 + (-1 × %n_9)))
           ∧ %l_6
               -[ %l_6, 16 )-> ⟨(8 × %n_9),%a_2⟩^⟨(16 + (-8 × %n_9)),%a_3⟩
           \- ∃ %a_1, %m_8 .