From 4da75ad2b0ebde49795ac3755bb4a52fed5038da Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sat, 15 Aug 2020 02:19:32 -0700 Subject: [PATCH] [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 | 34 +++++++--------- sledge/src/fol.ml | 84 +++++++++++++++++++++++++++++---------- sledge/src/fol.mli | 8 ++++ sledge/src/sh.ml | 3 +- sledge/src/solver_test.ml | 2 +- 5 files changed, 88 insertions(+), 43 deletions(-) diff --git a/sledge/src/exec.ml b/sledge/src/exec.ml index b9e99fbd6..e667f949a 100644 --- a/sledge/src/exec.ml +++ b/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 len Term.zero) dst_heap) + Sh.and_ (Formula.eq dst src) (Sh.and_ (Formula.eq0 len) 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.eq n Term.zero) - (Sh.star (Sh.seg iseg) (Sh.seg rseg))) + Sh.and_ (Formula.eq0 w) + (Sh.and_ (Formula.eq0 n) (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.eq n Term.zero) (Sh.star const (Sh.seg rseg))) + Sh.and_ (Formula.eq0 w) + (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 = - Sh.and_ (Formula.eq r Term.zero) (Sh.and_ (Formula.eq i Term.zero) post) - in + let foot = Sh.and_ (Formula.eq0 r) (Sh.and_ (Formula.eq0 i) 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 = - Sh.and_ (Formula.eq r Term.zero) (Sh.and_ (Formula.eq i Term.zero) post) - in + let foot = Sh.and_ (Formula.eq0 r) (Sh.and_ (Formula.eq0 i) post) in {foot; sub= Var.Subst.empty; ms= Var.Set.empty; post} let mallctl_specs r i w n = diff --git a/sledge/src/fol.ml b/sledge/src/fol.ml index 3087de7cb..cd921d26d 100644 --- a/sledge/src/fol.ml +++ b/sledge/src/fol.ml @@ -133,8 +133,12 @@ type fml = | Ff | Eq of trm * trm | Dq of trm * trm - | Lt of trm * trm - | Le of trm * trm + | Eq0 of trm (** [Eq0(x)] iff x = 0 *) + | 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 _Le x y = Le (x, y) +let _Eq0 x = Eq0 x +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 - | Le (x, y) -> pf "(%a@ @<2>≤ %a)" pp_t x pp_t y + | Eq0 x -> pf "(0 = %a)" pp_t x + | 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) -> - fold_vars_t ~f x ~init:(fold_vars_t ~f y ~init) + | Eq (x, y) | Dq (x, y) -> 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 - | Le (x, y) -> map2 (map_vars_t ~f) e _Le x y + | Eq0 x -> map1 (map_vars_t ~f) e _Eq0 x + | 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 le = ap2f _Le + let eq0 = ap1f _Eq0 + 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) - | Le (x, y) -> Lt (y, x) + | Eq0 x -> Dq0 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) - | Le (x, y) -> Ses.Term.le (t_to_ses x) (t_to_ses y) + | Eq0 x -> Ses.Term.eq Ses.Term.zero (t_to_ses x) + | 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 diff --git a/sledge/src/fol.mli b/sledge/src/fol.mli index 74b17f80b..b74838754 100644 --- a/sledge/src/fol.mli +++ b/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 diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index 6dfbbf924..fc2e78373 100644 --- a/sledge/src/sh.ml +++ b/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 -> - Formula.dq Term.zero seg.loc :: p ) + List.fold ~init q.heap ~f:(fun p seg -> Formula.dq0 seg.loc :: p) |> fun init -> List.fold ~init q.djns ~f:(fun p djn -> Formula.orN (List.map djn ~f:pure_approx) :: p ) ) diff --git a/sledge/src/solver_test.ml b/sledge/src/solver_test.ml index 7282cb815..a8dd4d0d9 100644 --- a/sledge/src/solver_test.ml +++ b/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 .