[pulse] change the API of `simplify` to take `~can_be_pruned ~keep`

Summary: I should have listened to skcho on D28002725 (7207e05682). Needed for the next diff.

Reviewed By: skcho

Differential Revision: D28121203

fbshipit-source-id: 96c01b141

infer/src/pulse/PulseAbductiveDomain.ml

@@ -871,13 +871,13 @@ let filter_for_summary tenv astate0 =
   let astate = restore_formals_for_summary astate_before_filter in
   let astate = {astate with topl= PulseTopl.filter_for_summary astate.path_condition astate.topl} in
   let astate, pre_live_addresses, post_live_addresses, _ = discard_unreachable astate in
+  let live_addresses = AbstractValue.Set.union pre_live_addresses post_live_addresses in
   let+ path_condition, new_eqs =
     PathCondition.simplify tenv
       ~get_dynamic_type:
         (BaseAddressAttributes.get_dynamic_type (astate_before_filter.post :> BaseDomain.t).attrs)
-      ~keep_pre:pre_live_addresses ~keep_post:post_live_addresses astate.path_condition
+      ~can_be_pruned:pre_live_addresses ~keep:live_addresses astate.path_condition
   in
-  let live_addresses = AbstractValue.Set.union pre_live_addresses post_live_addresses in
   ({astate with path_condition; topl= PulseTopl.simplify ~keep:live_addresses astate.topl}, new_eqs)
 
 

infer/src/pulse/PulseFormula.ml

@@ -1704,10 +1704,10 @@ let and_fold_subst_variables phi0 ~up_to_f:phi_foreign ~init ~f:f_var =
 
 
 module QuantifierElimination : sig
-  val eliminate_vars : keep_pre:Var.Set.t -> keep_post:Var.Set.t -> t -> t SatUnsat.t
+  val eliminate_vars : keep:Var.Set.t -> t -> t SatUnsat.t
-  (** [eliminate_vars ~keep_pre ~keep_post φ] substitutes every variable [x] in [φ] with [x']
+  (** [eliminate_vars ~keep φ] substitutes every variable [x] in [φ] with [x'] whenever [x'] is a
-      whenever [x'] is a distinguished representative of the equivalence class of [x] in [φ] such
+      distinguished representative of the equivalence class of [x] in [φ] such that
-      that [x' ∈ keep_pre ∪ keep_post] *)
+      [x' ∈ keep_pre ∪ keep_post] *)
 end = struct
   exception Contradiction
 
@@ -1749,12 +1749,8 @@ end = struct
     ; both= subst_var_formula subst phi.both }
 
 
-  let eliminate_vars ~keep_pre ~keep_post phi =
+  let eliminate_vars ~keep phi =
-    let subst =
+    let subst = VarUF.reorient ~should_keep:(fun x -> Var.Set.mem x keep) phi.known.var_eqs in
-      VarUF.reorient
-        ~should_keep:(fun x -> Var.Set.mem x keep_pre || Var.Set.mem x keep_post)
-        phi.known.var_eqs
-    in
     try Sat (subst_var subst phi) with Contradiction -> Unsat
 end
 
@@ -1841,18 +1837,18 @@ module DeadVariables = struct
 
 
   (** Get rid of atoms when they contain only variables that do not appear in atoms mentioning
-      variables in [keep_pre] or [keep_post], or variables appearing in atoms together with
+      variables in [keep], or variables appearing in atoms together with variables in these sets,
-      variables in these sets, and so on. In other words, the variables to keep are all the ones
+      and so on. In other words, the variables to keep are all the ones transitively reachable from
-      transitively reachable from variables in [keep_pre ∪ keep_post] in the graph connecting two
+      variables in [keep] in the graph connecting two variables whenever they appear together in a
-      variables whenever they appear together in a same atom of the formula. *)
+      same atom of the formula. *)
-  let eliminate ~keep_pre ~keep_post phi =
+  let eliminate ~can_be_pruned ~keep phi =
     (* We only consider [phi.both] when building the relation. Considering [phi.known] and
        [phi.pruned] as well could lead to us keeping more variables around, but that's not necessarily
        a good idea. Ignoring them means we err on the side of reporting potentially slightly more
        issues than we would otherwise, as some atoms in [phi.pruned] may vanish unfairly as a
        result. *)
     let var_graph = build_var_graph phi.both in
-    let vars_to_keep = get_reachable_from var_graph (Var.Set.union keep_pre keep_post) in
+    let vars_to_keep = get_reachable_from var_graph keep in
     L.d_printfln "Reachable vars: %a" Var.Set.pp vars_to_keep ;
     let simplify_phi phi =
       let var_eqs =
@@ -1877,24 +1873,24 @@ module DeadVariables = struct
     let known = simplify_phi phi.known in
     let both = simplify_phi phi.both in
     let pruned =
-      (* discard atoms that callers have no way of influencing, i.e. those that do not contain
+      (* discard atoms that callers have no way of influencing, i.e. more or less those that do not
-         variables related to variables in the pre *)
+         contain variables related to variables in the pre *)
-      let vars_to_keep_pre = get_reachable_from var_graph keep_pre in
+      let closed_prunable_vars = get_reachable_from var_graph can_be_pruned in
-      Atom.Set.filter (fun atom -> not (Atom.has_var_notin vars_to_keep_pre atom)) phi.pruned
+      Atom.Set.filter (fun atom -> not (Atom.has_var_notin closed_prunable_vars atom)) phi.pruned
     in
     {known; pruned; both}
 end
 
-let simplify tenv ~get_dynamic_type ~keep_pre ~keep_post phi =
+let simplify tenv ~get_dynamic_type ~can_be_pruned ~keep phi =
   let open SatUnsat.Import in
   let* phi, new_eqs = normalize tenv ~get_dynamic_type phi in
-  L.d_printfln_escaped "@[Simplifying %a@,wrt %a (pre) and %a (post)@]" pp phi Var.Set.pp keep_pre
+  L.d_printfln_escaped "@[Simplifying %a@,wrt %a (keep), with prunables=%a@]" pp phi Var.Set.pp keep
-    Var.Set.pp keep_post ;
+    Var.Set.pp can_be_pruned ;
   (* get rid of as many variables as possible *)
-  let+ phi = QuantifierElimination.eliminate_vars ~keep_pre ~keep_post phi in
+  let+ phi = QuantifierElimination.eliminate_vars ~keep phi in
   (* TODO: doing [QuantifierElimination.eliminate_vars; DeadVariables.eliminate] a few times may
      eliminate even more variables *)
-  let phi = DeadVariables.eliminate ~keep_pre ~keep_post phi in
+  let phi = DeadVariables.eliminate ~can_be_pruned ~keep phi in
   (phi, new_eqs)
 
 

infer/src/pulse/PulseFormula.mli

@@ -59,8 +59,8 @@ val normalize : Tenv.t -> get_dynamic_type:(Var.t -> Typ.t option) -> t -> (t *
 val simplify :
      Tenv.t
   -> get_dynamic_type:(Var.t -> Typ.t option)
-  -> keep_pre:Var.Set.t
+  -> can_be_pruned:Var.Set.t
-  -> keep_post:Var.Set.t
+  -> keep:Var.Set.t
   -> t
   -> (t * new_eqs) SatUnsat.t
 

infer/src/pulse/PulsePathCondition.ml

@@ -107,11 +107,11 @@ let and_eq_vars v1 v2 phi =
   ({is_unsat; bo_itvs; citvs; formula}, new_eqs)
 
 
-let simplify tenv ~keep_pre ~keep_post ~get_dynamic_type phi =
+let simplify tenv ~can_be_pruned ~keep ~get_dynamic_type phi =
   let result =
     let+ {is_unsat; bo_itvs; citvs; formula} = phi in
-    let+| formula, new_eqs = Formula.simplify tenv ~keep_pre ~keep_post ~get_dynamic_type formula in
+    let+| formula, new_eqs = Formula.simplify tenv ~can_be_pruned ~keep ~get_dynamic_type formula in
-    let is_in_keep v _ = AbstractValue.Set.mem v keep_pre || AbstractValue.Set.mem v keep_post in
+    let is_in_keep v _ = AbstractValue.Set.mem v keep in
     ( { is_unsat
       ; bo_itvs= BoItvs.filter is_in_keep bo_itvs
       ; citvs= CItvs.filter is_in_keep citvs

infer/src/pulse/PulsePathCondition.mli

@@ -36,13 +36,14 @@ val and_eq_vars : AbstractValue.t -> AbstractValue.t -> t -> t * new_eqs
 
 val simplify :
      Tenv.t
-  -> keep_pre:AbstractValue.Set.t
+  -> can_be_pruned:AbstractValue.Set.t
-  -> keep_post:AbstractValue.Set.t
+  -> keep:AbstractValue.Set.t
   -> get_dynamic_type:(AbstractValue.t -> Typ.t option)
   -> t
   -> (t * new_eqs) SatUnsat.t
-(** [simplify ~keep phi] attempts to get rid of as many variables in [fv phi] but not in [keep] as
+(** [simplify ~can_be_pruned ~keep phi] attempts to get rid of as many variables in [fv phi] but not
-    possible *)
+    in [keep] as possible, and tries to eliminate variables not in [can_be_pruned] from the "pruned"
+    part of the formula *)
 
 val simplify_instanceof : Tenv.t -> get_dynamic_type:(AbstractValue.t -> Typ.t option) -> t -> t
 

infer/src/pulse/unit/PulseFormulaTest.ml

@@ -129,11 +129,11 @@ let dummy_get_dynamic_type _ = None
 let normalize phi = test ~f:(normalize dummy_tenv ~get_dynamic_type:dummy_get_dynamic_type) phi
 
 let simplify ~keep phi =
+  let keep = AbstractValue.Set.of_list keep in
   test phi ~f:(fun phi ->
       (* keep variables as if they were in the pre-condition, which makes [simplify] keeps the most
          facts (eg atoms in [pruned] may be discarded if their variables are not in the pre) *)
-      simplify dummy_tenv ~get_dynamic_type:dummy_get_dynamic_type
+      simplify dummy_tenv ~get_dynamic_type:dummy_get_dynamic_type ~can_be_pruned:keep ~keep phi )
-        ~keep_pre:(AbstractValue.Set.of_list keep) ~keep_post:AbstractValue.Set.empty phi )
 
 
 let%test_module "normalization" =