From 822a78c57682c765b2de15225f06ef5b7ff0f2b0 Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 20 Apr 2020 11:00:10 -0700 Subject: [PATCH] [pudge] lazily compute sledge stuff Summary: This is mostly just a type change for now, more changes to come. This doesn't make thing much faster yet because we force computations pretty often to check for unsatisfiability (each function call and PRUNE node). Next diff will build on that. Reviewed By: skcho Differential Revision: D21129758 fbshipit-source-id: 72200e2b1 --- infer/src/pulse/PulseAbductiveDomain.ml | 1 + infer/src/pulse/PulseDummyPathCondition.ml | 4 +-- infer/src/pulse/PulsePathCondition.ml | 39 +++++++++++++--------- 3 files changed, 26 insertions(+), 18 deletions(-) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index d3fae80d3..8abf3f976 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -418,6 +418,7 @@ let of_post pdesc astate = let astate = filter_for_summary astate in let astate, live_addresses, _ = discard_unreachable astate in let astate = + (* this also forces the lazy path condition for safe serialization *) {astate with path_condition= PathCondition.simplify ~keep:live_addresses astate.path_condition} in invalidate_locals pdesc astate diff --git a/infer/src/pulse/PulseDummyPathCondition.ml b/infer/src/pulse/PulseDummyPathCondition.ml index d7cd82a27..ddd6b5f7c 100644 --- a/infer/src/pulse/PulseDummyPathCondition.ml +++ b/infer/src/pulse/PulseDummyPathCondition.ml @@ -36,11 +36,11 @@ module Term = struct end (* same type as {!PulsePathCondition.t} to be nice to summary serialization *) -type t = {eqs: Sledge.Equality.t; non_eqs: Sledge.Term.t} +type t = {eqs: Sledge.Equality.t lazy_t; non_eqs: Sledge.Term.t lazy_t} let pp _ _ = () -let true_ = {eqs= Sledge.Equality.true_; non_eqs= Sledge.Term.true_} +let true_ = {eqs= Lazy.from_val Sledge.Equality.true_; non_eqs= Lazy.from_val Sledge.Term.true_} let and_eq () () phi = phi diff --git a/infer/src/pulse/PulsePathCondition.ml b/infer/src/pulse/PulsePathCondition.ml index ae3ce980a..cce4fc5d2 100644 --- a/infer/src/pulse/PulsePathCondition.ml +++ b/infer/src/pulse/PulsePathCondition.ml @@ -102,39 +102,46 @@ module Equality = struct let apply_subst subst r = let new_vars, r' = Sledge.Equality.apply_subst Var.Set.empty subst r in - assert_no_new_vars "Equality.and_" new_vars ; + assert_no_new_vars "Equality.apply_subst" new_vars ; r' end (** We distinguish between what the equality relation of sledge can express and the "non-equalities" terms that this relation ignores. We keep the latter around for completeness: we can still substitute known equalities into these and sometimes get contradictions back. *) -type t = {eqs: Equality.t; non_eqs: Term.t} +type t = {eqs: Equality.t lazy_t; non_eqs: Term.t lazy_t} + +let pp fmt {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} = + F.fprintf fmt "%a∧%a" Equality.pp eqs Term.pp non_eqs -let pp fmt {eqs; non_eqs} = F.fprintf fmt "%a∧%a" Equality.pp eqs Term.pp non_eqs -let true_ = {eqs= Equality.true_; non_eqs= Term.true_} +let true_ = {eqs= Lazy.from_val Equality.true_; non_eqs= Lazy.from_val Term.true_} -let and_eq t1 t2 phi = {phi with eqs= Equality.and_eq t1 t2 phi.eqs} +let and_eq t1 t2 phi = {phi with eqs= lazy (Equality.and_eq t1 t2 (Lazy.force phi.eqs))} let and_term (t : Term.t) phi = (* add the term to the relation *) - let eqs = Equality.and_term t phi.eqs in + let eqs = lazy (Equality.and_term t (Lazy.force phi.eqs)) in (* [t] normalizes to [true_] so [non_eqs] never changes, do this regardless for now *) - let non_eqs = Term.and_ phi.non_eqs (Equality.normalize eqs t) in + let non_eqs = lazy (Term.and_ (Lazy.force phi.non_eqs) (Equality.normalize (Lazy.force eqs) t)) in {eqs; non_eqs} let and_ phi1 phi2 = - {eqs= Equality.and_ phi1.eqs phi2.eqs; non_eqs= Term.and_ phi1.non_eqs phi2.non_eqs} + { eqs= lazy (Equality.and_ (Lazy.force phi1.eqs) (Lazy.force phi2.eqs)) + ; non_eqs= lazy (Term.and_ (Lazy.force phi1.non_eqs) (Lazy.force phi2.non_eqs)) } -let is_known_zero t phi = Equality.entails_eq phi.eqs t Term.zero +let is_known_zero t phi = Equality.entails_eq (Lazy.force phi.eqs) t Term.zero (* NOTE: not normalizing non_eqs here gives imprecise results but is cheaper *) -let is_unsat {eqs; non_eqs} = Equality.is_false eqs || Term.is_false non_eqs +let is_unsat {eqs; non_eqs} = + Equality.is_false (Lazy.force eqs) || Term.is_false (Lazy.force non_eqs) + + +let fv {eqs= (lazy eqs); non_eqs= (lazy non_eqs)} = + Term.Var.Set.union (Equality.fv eqs) (Term.fv non_eqs) -let fv {eqs; non_eqs} = Term.Var.Set.union (Equality.fv eqs) (Term.fv non_eqs) let fold_map_variables phi ~init ~f = let term_fold_map t ~init ~f = @@ -145,15 +152,15 @@ let fold_map_variables phi ~init ~f = (acc', Term.var v') ) ) in let acc, eqs' = - Equality.classes phi.eqs + Equality.classes (Lazy.force phi.eqs) |> Term.Map.fold ~init:(init, Equality.true_) ~f:(fun ~key:t ~data:equal_ts (acc, eqs') -> let acc, t' = term_fold_map ~init:acc ~f t in List.fold equal_ts ~init:(acc, eqs') ~f:(fun (acc, eqs') equal_t -> let acc, t_mapped = term_fold_map ~init:acc ~f equal_t in (acc, Equality.and_eq t' t_mapped eqs') ) ) in - let acc, non_eqs' = term_fold_map ~init:acc ~f phi.non_eqs in - (acc, {eqs= eqs'; non_eqs= non_eqs'}) + let acc, non_eqs' = term_fold_map ~init:acc ~f (Lazy.force phi.non_eqs) in + (acc, {eqs= Lazy.from_val eqs'; non_eqs= Lazy.from_val non_eqs'}) let simplify ~keep phi = @@ -163,5 +170,5 @@ let simplify ~keep phi = (fun v keep_vs -> Term.Var.Set.add keep_vs (Var.of_absval v)) keep Term.Var.Set.empty in - let simpl_subst = Equality.solve_for_vars [keep_vs; all_vs] phi.eqs in - {phi with eqs= Equality.apply_subst simpl_subst phi.eqs} + let simpl_subst = Equality.solve_for_vars [keep_vs; all_vs] (Lazy.force phi.eqs) in + {phi with eqs= Lazy.from_val (Equality.apply_subst simpl_subst (Lazy.force phi.eqs))}