From 7567432afb18e96b2975177d66a58f4b1760f56d Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 19 Mar 2019 09:26:10 -0700 Subject: [PATCH] [sledge] Revise Sh.dnf to handle nested existentials Summary: The dnf implementation dates to before nested existentials were added. Updating it was overlooked, and it is just wrong. Reviewed By: ngorogiannis Differential Revision: D14481988 fbshipit-source-id: 9bba570f0 --- sledge/src/llair/exp_test.mli | 6 ++ sledge/src/symbheap/equality_test.mli | 6 ++ sledge/src/symbheap/sh.ml | 45 ++++++------- sledge/src/symbheap/sh.mli | 4 +- sledge/src/symbheap/sh_test.ml | 92 +++++++++++++++++++++++++++ sledge/src/symbheap/sh_test.mli | 6 ++ sledge/src/symbheap/solver_test.mli | 6 ++ 7 files changed, 141 insertions(+), 24 deletions(-) create mode 100644 sledge/src/llair/exp_test.mli create mode 100644 sledge/src/symbheap/equality_test.mli create mode 100644 sledge/src/symbheap/sh_test.ml create mode 100644 sledge/src/symbheap/sh_test.mli create mode 100644 sledge/src/symbheap/solver_test.mli diff --git a/sledge/src/llair/exp_test.mli b/sledge/src/llair/exp_test.mli new file mode 100644 index 000000000..1d6ea608c --- /dev/null +++ b/sledge/src/llair/exp_test.mli @@ -0,0 +1,6 @@ +(* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) diff --git a/sledge/src/symbheap/equality_test.mli b/sledge/src/symbheap/equality_test.mli new file mode 100644 index 000000000..1d6ea608c --- /dev/null +++ b/sledge/src/symbheap/equality_test.mli @@ -0,0 +1,6 @@ +(* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) diff --git a/sledge/src/symbheap/sh.ml b/sledge/src/symbheap/sh.ml index 025175eab..8a8cd75c0 100644 --- a/sledge/src/symbheap/sh.ml +++ b/sledge/src/symbheap/sh.ml @@ -311,6 +311,11 @@ let star q1 q2 = invariant q ; assert (Set.equal q.us (Set.union q1.us q2.us))] +let stars = function + | [] -> emp + | [q] -> q + | q :: qs -> List.fold ~f:star ~init:q qs + let or_ q1 q2 = [%Trace.call fun {pf} -> pf "(%a)@ (%a)" pp q1 pp q2] ; @@ -394,36 +399,32 @@ let rec pure_approx ({us; xs; cong; pure; heap= _; djns} as q) = if heap == q.heap && djns == q.djns then q else {us; xs; cong; pure; heap; djns} |> check invariant -let fold_disjunctions sjn ~init ~f = List.fold sjn.djns ~init ~f -let fold_disjuncts djn ~init ~f = List.fold djn ~init ~f - -let fold_dnf ~conj ~disj sjn conjuncts disjuncts = - let rec add_disjunct pending_splits sjn (conjuncts, disjuncts) = +let fold_dnf ~conj ~disj sjn (xs, conjuncts) disjuncts = + let rec add_disjunct pending_splits sjn (xs, conjuncts) disjuncts = + let ys, sjn = bind_exists sjn ~wrt:xs in + let xs = Set.union ys xs in + let djns = sjn.djns in + let sjn = {sjn with djns= []} in split_case - (fold_disjunctions sjn ~init:pending_splits - ~f:(fun pending_splits split -> split :: pending_splits )) - (conj {sjn with djns= []} conjuncts, disjuncts) - and split_case pending_splits (conjuncts, disjuncts) = + (List.rev_append djns pending_splits) + (xs, conj sjn conjuncts) + disjuncts + and split_case pending_splits (xs, conjuncts) disjuncts = match pending_splits with | split :: pending_splits -> - fold_disjuncts split ~init:disjuncts ~f:(fun disjuncts sjn -> - add_disjunct pending_splits sjn (conjuncts, disjuncts) ) - | [] -> disj conjuncts disjuncts + List.fold split ~init:disjuncts ~f:(fun disjuncts sjn -> + add_disjunct pending_splits sjn (xs, conjuncts) disjuncts ) + | [] -> disj (xs, conjuncts) disjuncts in - add_disjunct [] sjn (conjuncts, disjuncts) + add_disjunct [] sjn (xs, conjuncts) disjuncts let dnf q = [%Trace.call fun {pf} -> pf "%a" pp q] ; - let conj sjn conjuncts = - assert (List.is_empty sjn.djns) ; - assert (List.is_empty conjuncts.djns) ; - star conjuncts sjn - in - let disj conjuncts disjuncts = - assert (match conjuncts.djns with [] | [[]] -> true | _ -> false) ; - conjuncts :: disjuncts + let conj sjn conjuncts = sjn :: conjuncts in + let disj (xs, conjuncts) disjuncts = + exists xs (stars conjuncts) :: disjuncts in - fold_dnf ~conj ~disj q emp [] + fold_dnf ~conj ~disj q (Var.Set.empty, []) [] |> [%Trace.retn fun {pf} -> pf "%a" pp_djn] diff --git a/sledge/src/symbheap/sh.mli b/sledge/src/symbheap/sh.mli index 37999ef53..a51db5c4c 100644 --- a/sledge/src/symbheap/sh.mli +++ b/sledge/src/symbheap/sh.mli @@ -112,9 +112,9 @@ val pure_approx : t -> t val fold_dnf : conj:(starjunction -> 'conjuncts -> 'conjuncts) - -> disj:('conjuncts -> 'disjuncts -> 'disjuncts) + -> disj:(Var.Set.t * 'conjuncts -> 'disjuncts -> 'disjuncts) -> t - -> 'conjuncts + -> Var.Set.t * 'conjuncts -> 'disjuncts -> 'disjuncts (** Enumerate the cubes and clauses of a disjunctive-normal form expansion. *) diff --git a/sledge/src/symbheap/sh_test.ml b/sledge/src/symbheap/sh_test.ml new file mode 100644 index 000000000..37bf67f0d --- /dev/null +++ b/sledge/src/symbheap/sh_test.ml @@ -0,0 +1,92 @@ +(* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +let%test_module _ = + ( module struct + (* let () = Trace.init ~margin:68 ~config:all () *) + + let () = Trace.init ~margin:68 ~config:none () + let pp = Format.printf "@\n%a@." Sh.pp + let pp_djn = Format.printf "@\n%a@." Sh.pp_djn + let ( ~$ ) = Var.Set.of_list + let ( ! ) i = Exp.integer (Z.of_int i) Typ.siz + let ( = ) = Exp.eq + let wrt = Var.Set.empty + let x_, wrt = Var.fresh "x" ~wrt + let y_, _ = Var.fresh "y" ~wrt + let x = Exp.var x_ + let y = Exp.var y_ + + let%expect_test _ = + let p = Sh.(exists ~$[x_] (extend_us ~$[x_] emp)) in + let q = Sh.(pure (x = !0)) in + pp p ; + pp q ; + pp (Sh.star p q) ; + [%expect + {| + ∃ %x_1 . emp + + 0 = %x_1 ∧ emp + + 0 = %x_1 ∧ emp |}] + + let%expect_test _ = + let q = + Sh.( + or_ + (pure (x = !0)) + (exists + ~$[x_] + (or_ + (and_ (x = !1) (pure (y = !1))) + (exists ~$[x_] (pure (x = !2)))))) + in + pp q ; + pp_djn (Sh.dnf q) ; + [%expect + {| + emp + * ( ( 0 = %x_1 ∧ emp) + ∨ (∃ %x_1 .emp + * ( ( 1 = %x_1 = %y_2 ∧ emp) ∨ (∃ %x_1 . 2 = %x_1 ∧ emp) )) + ) + + ( (∃ %x_1, %x_2 . 2 = %x_2 ∧ emp) + ∨ (∃ %x_1 . 1 = %x_1 = %y_2 ∧ emp) + ∨ ( 0 = %x_1 ∧ emp) + ) |}] + + let%expect_test _ = + let q = + Sh.( + exists + ~$[x_] + (or_ + (pure (x = !0)) + (exists + ~$[x_] + (or_ + (and_ (x = !1) (pure (y = !1))) + (exists ~$[x_] (pure (x = !2))))))) + in + pp q ; + pp_djn (Sh.dnf q) ; + [%expect + {| + ∃ %x_1 . + emp + * ( ( 0 = %x_1 ∧ emp) + ∨ (∃ %x_1 .emp + * ( ( 1 = %x_1 = %y_2 ∧ emp) ∨ (∃ %x_1 . 2 = %x_1 ∧ emp) )) + ) + + ( (∃ %x_1, %x_3, %x_4 . 2 = %x_4 ∧ emp) + ∨ (∃ %x_1, %x_3 . 1 = %y_2 = %x_3 ∧ emp) + ∨ (∃ %x_1 . 0 = %x_1 ∧ emp) + ) |}] + end ) diff --git a/sledge/src/symbheap/sh_test.mli b/sledge/src/symbheap/sh_test.mli new file mode 100644 index 000000000..1d6ea608c --- /dev/null +++ b/sledge/src/symbheap/sh_test.mli @@ -0,0 +1,6 @@ +(* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) diff --git a/sledge/src/symbheap/solver_test.mli b/sledge/src/symbheap/solver_test.mli new file mode 100644 index 000000000..1d6ea608c --- /dev/null +++ b/sledge/src/symbheap/solver_test.mli @@ -0,0 +1,6 @@ +(* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *)