From 69a979612b5f30482bb496e9fdcf9a273916d474 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 12 Jan 2021 04:25:22 -0800 Subject: [PATCH] [sledge] Use unsat context and ff pure constraints in unsat symbolic heaps Summary: Sh operations usually detect inconsistency where needed. But some operations such as Context.inter must treat the unsat case specially. This diff increases robustness by not relying on Sh to detect inconsistency in order to get the correct context or pure constraints, or to use the fast-paths through Context or Formula operations. Reviewed By: jvillard Differential Revision: D25756550 fbshipit-source-id: 091439ff6 --- sledge/src/fol/context.mli | 3 + sledge/src/sh.ml | 228 +++++++++++++++++---------------- sledge/src/test/solver_test.ml | 4 +- 3 files changed, 125 insertions(+), 110 deletions(-) diff --git a/sledge/src/fol/context.mli b/sledge/src/fol/context.mli index e594aceac..3d245b44a 100644 --- a/sledge/src/fol/context.mli +++ b/sledge/src/fol/context.mli @@ -27,6 +27,9 @@ include Invariant.S with type t := t val empty : t (** The empty context of assumptions. *) +val unsat : t +(** An unsatisfiable context of assumptions. *) + val add : Var.Set.t -> Formula.t -> t -> Var.Set.t * t (** Add (that is, conjoin) an assumption to a context. *) diff --git a/sledge/src/sh.ml b/sledge/src/sh.ml index 97ab11891..b208705cc 100644 --- a/sledge/src/sh.ml +++ b/sledge/src/sh.ml @@ -37,7 +37,8 @@ let emp = ; heap= [] ; djns= [] } -let false_ us = {emp with us; djns= [[]]} +let false_ us = + {emp with us; ctx= Context.unsat; pure= Formula.ff; djns= [[]]} (** Traversals *) @@ -186,43 +187,46 @@ let rec pp_ ?var_strength ?vs ancestor_xs parent_ctx fs Format.pp_open_hvbox fs 0 ; let x v = Option.bind ~f:(fun (_, m) -> Var.Map.find v m) var_strength in pp_us ~pre:"@<2>∀ " ?vs () fs us ; - let vs = Option.value vs ~default:Var.Set.empty in - let xs_d_vs, xs_i_vs = - Var.Set.diff_inter - (Var.Set.filter xs ~f:(fun v -> Poly.(x v <> Some `Anonymous))) - vs - in - if not (Var.Set.is_empty xs_i_vs) then ( - Format.fprintf fs "@<3>∃↑ @[%a@] ." (Var.Set.ppx x) xs_i_vs ; - if not (Var.Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ; - if not (Var.Set.is_empty xs_d_vs) then - Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ; - let first = - if Option.is_some var_strength then - Context.ppx_diff x fs parent_ctx pure ctx - else ( - Format.fprintf fs "@[ %a@ @<2>∧ %a@]" Context.pp ctx Formula.pp - pure ; - false ) - in - if List.is_empty heap then - Format.fprintf fs - ( if first then if List.is_empty djns then " emp" else "" - else "@ @<5>∧ emp" ) - else - pp_heap x - ~pre:(if first then " " else "@ @<2>∧ ") - (if Option.is_some var_strength then ctx else emp.ctx) - fs heap ; - let first = first && List.is_empty heap in - List.pp - ~pre:(if first then " " else "@ * ") - "@ * " - (pp_djn ?var_strength - (Var.Set.union vs (Var.Set.union us xs)) - (Var.Set.union ancestor_xs xs) - ctx) - fs djns ; + ( match djns with + | [[]] when Option.is_some var_strength -> Format.fprintf fs "false" + | _ -> + let vs = Option.value vs ~default:Var.Set.empty in + let xs_d_vs, xs_i_vs = + Var.Set.diff_inter + (Var.Set.filter xs ~f:(fun v -> Poly.(x v <> Some `Anonymous))) + vs + in + if not (Var.Set.is_empty xs_i_vs) then ( + Format.fprintf fs "@<3>∃↑ @[%a@] ." (Var.Set.ppx x) xs_i_vs ; + if not (Var.Set.is_empty xs_d_vs) then Format.fprintf fs "@ " ) ; + if not (Var.Set.is_empty xs_d_vs) then + Format.fprintf fs "@<2>∃ @[%a@] .@ " (Var.Set.ppx x) xs_d_vs ; + let first = + if Option.is_some var_strength then + Context.ppx_diff x fs parent_ctx pure ctx + else ( + Format.fprintf fs "@[ %a@ @<2>∧ %a@]" Context.pp ctx Formula.pp + pure ; + false ) + in + if List.is_empty heap then + Format.fprintf fs + ( if first then if List.is_empty djns then " emp" else "" + else "@ @<5>∧ emp" ) + else + pp_heap x + ~pre:(if first then " " else "@ @<2>∧ ") + (if Option.is_some var_strength then ctx else emp.ctx) + fs heap ; + let first = first && List.is_empty heap in + List.pp + ~pre:(if first then " " else "@ * ") + "@ * " + (pp_djn ?var_strength + (Var.Set.union vs (Var.Set.union us xs)) + (Var.Set.union ancestor_xs xs) + ctx) + fs djns ) ; Format.pp_close_box fs () and pp_djn ?var_strength vs xs ctx fs = function @@ -260,9 +264,6 @@ let fv ?ignore_ctx ?ignore_pure q = in fv_union q Var.Set.empty -let invariant_pure p = assert (not Formula.(equal ff p)) -let invariant_seg _ = () - let rec invariant q = let@ () = Invariant.invariant [%here] q [%sexp_of: t] in let {us; xs; ctx; pure; heap; djns} = q in @@ -278,12 +279,13 @@ let rec invariant q = Context.invariant ctx ; ( match djns with | [[]] -> - assert (Context.is_empty ctx) ; - assert (Formula.(equal tt pure)) ; + assert (Context.is_unsat ctx) ; + assert (Formula.equal Formula.ff pure) ; assert (List.is_empty heap) - | _ -> assert (not (Context.is_unsat ctx)) ) ; - invariant_pure pure ; - List.iter heap ~f:invariant_seg ; + | _ -> + assert (not (Context.is_unsat ctx)) ; + assert (not (Formula.equal Formula.ff pure)) ; + assert (not (List.exists djns ~f:List.is_empty)) ) ; List.iter djns ~f:(fun djn -> List.iter djn ~f:(fun sjn -> assert (Var.Set.subset sjn.us ~of_:(Var.Set.union us xs)) ; @@ -293,6 +295,41 @@ let rec invariant q = [%Trace.info "%a" pp_raw q] ; Printexc.raise_with_backtrace exc bt +(** Query *) + +(** syntactically empty: empty heap and no pure constraints *) +let is_emp q = + Context.is_empty q.ctx + && Formula.equal Formula.tt q.pure + && List.is_empty q.heap + && List.is_empty q.djns + +(** (incomplete syntactic) test that all satisfying heaps are empty *) +let rec is_empty q = + List.is_empty q.heap && List.for_all ~f:(List.for_all ~f:is_empty) q.djns + +(** syntactically inconsistent *) +let is_false q = match q.djns with [[]] -> true | _ -> false + +(** first-order approximation of heap constraints *) +let rec pure_approx q = + Formula.andN + ( [q.pure] + |> List.fold q.heap ~f:(fun seg p -> Formula.dq0 seg.loc :: p) + |> List.fold q.djns ~f:(fun djn p -> + Formula.orN (List.map djn ~f:pure_approx) :: p ) ) + +let pure_approx q = + [%Trace.call fun {pf} -> pf "%a" pp q] + ; + pure_approx q + |> + [%Trace.retn fun {pf} -> pf "%a" Formula.pp] + +(** test if pure constraints are inconsistent with first-order consequences + of spatial constraints *) +let is_unsat q = Context.refutes q.ctx (pure_approx q) + (** Quantification and Vocabulary *) let exists_fresh xs q = @@ -330,19 +367,23 @@ let elim_exists xs q = let map ~f_sjn ~f_ctx ~f_trm ~f_fml ({us; xs= _; ctx; pure; heap; djns} as q) = let pure = f_fml pure in - if Formula.(equal ff pure) then false_ us + if Formula.equal Formula.ff pure then false_ us else let xs, ctx = f_ctx ctx in - let heap = List.map_endo heap ~f:(map_seg ~f:f_trm) in - let djns = List.map_endo djns ~f:(List.map_endo ~f:f_sjn) in - if - ctx == q.ctx - && pure == q.pure - && heap == q.heap - && djns == q.djns - && Var.Set.is_empty xs - then q - else exists_fresh xs {q with ctx; pure; heap; djns} + if Context.is_unsat ctx then false_ us + else + let djns = List.map_endo djns ~f:(List.map_endo ~f:f_sjn) in + if List.exists ~f:List.is_empty djns then false_ us + else + let heap = List.map_endo heap ~f:(map_seg ~f:f_trm) in + if + ctx == q.ctx + && pure == q.pure + && heap == q.heap + && djns == q.djns + && Var.Set.is_empty xs + then q + else exists_fresh xs {q with ctx; pure; heap; djns} (** primitive application of a substitution, ignores us and xs, may violate invariant *) @@ -437,9 +478,7 @@ let and_ctx_ ctx q = let and_ctx ctx q = [%Trace.call fun {pf} -> pf "%a@ %a" Context.pp ctx pp q] ; - ( match q.djns with - | [[]] -> q - | _ -> and_ctx_ ctx (extend_us (Context.fv ctx) q) ) + (if is_false q then q else and_ctx_ ctx (extend_us (Context.fv ctx) q)) |> [%Trace.retn fun {pf} q -> pf "%a" pp q ; @@ -453,30 +492,23 @@ let star q1 q2 = invariant q ; assert (Var.Set.equal q.us (Var.Set.union q1.us q2.us)) ) @@ fun () -> - match (q1, q2) with - | {djns= [[]]; _}, _ | _, {djns= [[]]; _} -> - false_ (Var.Set.union q1.us q2.us) - | {us= _; xs= _; ctx; pure; heap= []; djns= []}, _ - when Context.is_empty ctx && Formula.(equal tt pure) -> - let us = Var.Set.union q1.us q2.us in - if us == q2.us then q2 else {q2 with us} - | _, {us= _; xs= _; ctx; pure; heap= []; djns= []} - when Context.is_empty ctx && Formula.(equal tt pure) -> - let us = Var.Set.union q1.us q2.us in - if us == q1.us then q1 else {q1 with us} - | _ -> - let us = Var.Set.union q1.us q2.us in - let q1 = freshen_xs q1 ~wrt:(Var.Set.union us q2.xs) in - let q2 = freshen_xs q2 ~wrt:(Var.Set.union us q1.xs) in - let {us= us1; xs= xs1; ctx= c1; pure= p1; heap= h1; djns= d1} = q1 in - let {us= us2; xs= xs2; ctx= c2; pure= p2; heap= h2; djns= d2} = q2 in - assert (Var.Set.equal us (Var.Set.union us1 us2)) ; - let xs, ctx = - Context.union (Var.Set.union us (Var.Set.union xs1 xs2)) c1 c2 - in + if is_false q1 || is_false q2 then false_ (Var.Set.union q1.us q2.us) + else if is_emp q1 then extend_us q1.us q2 + else if is_emp q2 then extend_us q2.us q1 + else + let us = Var.Set.union q1.us q2.us in + let q1 = freshen_xs q1 ~wrt:(Var.Set.union us q2.xs) in + let q2 = freshen_xs q2 ~wrt:(Var.Set.union us q1.xs) in + let {us= us1; xs= xs1; ctx= c1; pure= p1; heap= h1; djns= d1} = q1 in + let {us= us2; xs= xs2; ctx= c2; pure= p2; heap= h2; djns= d2} = q2 in + assert (Var.Set.equal us (Var.Set.union us1 us2)) ; + let xs, ctx = + Context.union (Var.Set.union us (Var.Set.union xs1 xs2)) c1 c2 + in + if Context.is_unsat ctx then false_ us + else let pure = Formula.and_ p1 p2 in - if Formula.equal Formula.ff pure || Context.is_unsat ctx then - false_ us + if Formula.equal Formula.ff pure then false_ us else exists_fresh xs { us @@ -495,8 +527,8 @@ let or_ q1 q2 = [%Trace.call fun {pf} -> pf "(%a)@ (%a)" pp_raw q1 pp_raw q2] ; ( match (q1, q2) with - | {djns= [[]]; _}, _ -> extend_us q1.us q2 - | _, {djns= [[]]; _} -> extend_us q2.us q1 + | _ when is_false q1 -> extend_us q1.us q2 + | _ when is_false q2 -> extend_us q2.us q1 | ( ({djns= []; _} as q) , ({us= _; xs; ctx= _; pure; heap= []; djns= [djn]} as d) ) when Var.Set.is_empty xs && Formula.(equal tt pure) -> @@ -529,7 +561,8 @@ let pure (p : Formula.t) = Iter.fold (Context.dnf p) (false_ Var.Set.empty) ~f:(fun (xs, pure, ctx) q -> let us = Formula.fv pure in - if Context.is_unsat ctx then extend_us us q + if Context.is_unsat ctx || Formula.equal Formula.ff pure then + extend_us us q else or_ q (exists_fresh xs {emp with us; ctx; pure}) ) |> [%Trace.retn fun {pf} q -> @@ -578,28 +611,7 @@ let rem_seg seg q = let filter_heap ~f q = {q with heap= List.filter q.heap ~f} |> check invariant -(** Query *) - -let rec is_empty q = - List.is_empty q.heap && List.for_all ~f:(List.for_all ~f:is_empty) q.djns - -let rec pure_approx q = - Formula.andN - ( [q.pure] - |> List.fold q.heap ~f:(fun seg p -> Formula.dq0 seg.loc :: p) - |> List.fold q.djns ~f:(fun djn p -> - Formula.orN (List.map djn ~f:pure_approx) :: p ) ) - -let pure_approx q = - [%Trace.call fun {pf} -> pf "%a" pp q] - ; - pure_approx q - |> - [%Trace.retn fun {pf} -> pf "%a" Formula.pp] - -(** test if pure constraints are inconsistent with first-order consequences - of spatial constraints *) -let is_unsat q = Context.refutes q.ctx (pure_approx q) +(** Disjunctive-Normal Form *) let fold_dnf ~conj ~disj sjn (xs, conjuncts) disjuncts = let rec add_disjunct pending_splits sjn (xs, conjuncts) disjuncts = diff --git a/sledge/src/test/solver_test.ml b/sledge/src/test/solver_test.ml index 41b7d31f7..2de7aff7c 100644 --- a/sledge/src/test/solver_test.ml +++ b/sledge/src/test/solver_test.ml @@ -66,8 +66,8 @@ let%test_module _ = check_frame (Sh.false_ Var.Set.empty) [] Sh.emp ; [%expect {| - ( infer_frame: false \- emp - ) infer_frame: false |}] + ( infer_frame: false \- emp + ) infer_frame: false |}] let%expect_test _ = check_frame Sh.emp [n_; m_] (Sh.and_ (Formula.eq m n) Sh.emp) ;