[pulse][join] first stab at joining formulas

Summary:
First half of joining formulas: forget facts from one side that conflict
with the other side. Adding non-conflicting facts from both sides is
TODO, right now we only keep (a subset of) one side instead.

Reviewed By: skcho

Differential Revision: D66710907

fbshipit-source-id: 2e85346b0e42c9f17c5ac0056ab9f23ef05890e6

infer/src/istd/UnionFind.ml

@@ -24,7 +24,7 @@ struct
   (** the union-find backing data structure: maps elements to their representatives *)
   module UF : sig
     (** to get a little bit of type safety *)
-    type repr = private X.t
+    type repr = private X.t [@@deriving compare, equal]
 
     type t [@@deriving compare, equal]
 
@@ -43,7 +43,7 @@ struct
 
     module Map : Stdlib.Map.S with type key = repr
   end = struct
-    type repr = X.t
+    type repr = X.t [@@deriving compare, equal]
 
     type t = X.t XMap.t [@@deriving compare, equal]
 
@@ -74,7 +74,7 @@ struct
     module Map = XMap
   end
 
-  type repr = UF.repr
+  type repr = UF.repr [@@deriving compare, equal]
 
   module Classes = struct
     let find classes (x : UF.repr) = UF.Map.find_opt x classes |> Option.value ~default:XSet.empty
@@ -230,6 +230,8 @@ struct
     {reprs; classes}
 
 
+  let remove x uf = filter uf ~f:(fun y -> not (X.equal x y))
+
   let fold_elements uf ~init ~f =
     fold_congruences uf ~init ~f:(fun acc (repr, xs) ->
         XSet.fold (Fn.flip f) xs (f acc (repr :> X.t)) )

infer/src/istd/UnionFind.mli

@@ -25,7 +25,7 @@ module Make
 
   val pp : (F.formatter -> X.t -> unit) -> F.formatter -> t -> unit
 
-  type repr = private X.t
+  type repr = private X.t [@@deriving compare, equal]
 
   val empty : t
 
@@ -53,6 +53,8 @@ module Make
       smallest representative not in the domain of [subst] for each class. Classes without any such
       elements are kept intact. *)
 
+  val remove : X.t -> t -> t
+
   val filter : f:(X.t -> bool) -> t -> t
   (** only keep items satisfying [f] *)
 

infer/src/pulse/PulseFormula.ml

@@ -2259,6 +2259,10 @@ module Formula = struct
 
     val set_intervals : intervals -> t -> t
 
+    val join : t -> t -> t
+
+    val remove_conditions_for_join : Atom.t list -> t -> t -> t
+
     val unsafe_mk :
          var_eqs:var_eqs
       -> const_eqs:Term.t Var.Map.t
@@ -2781,6 +2785,98 @@ module Formula = struct
       ; tableau_occurrences
       ; term_eqs_occurrences
       ; atoms_occurrences }
+
+
+    let join phi1 _phi2 =
+      (* TODO: do phi1 /\ phi2 *)
+      phi1
+
+
+    let scramble_var phi_rhs phi v =
+      let remove_if_different mem_lhs test_equal find remove lhs rhs =
+        if (not mem_lhs) || test_equal (find v lhs) (find v rhs) then (lhs, false)
+        else (remove v lhs, true)
+      in
+      let var_eqs, _removed =
+        remove_if_different true VarUF.equal_repr
+          (fun v var_eqs -> VarUF.find var_eqs v)
+          VarUF.remove phi.var_eqs phi_rhs.var_eqs
+      in
+      let const_eqs, _removed =
+        remove_if_different (Var.Map.mem v phi.const_eqs) (Option.equal Term.equal) Var.Map.find_opt
+          Var.Map.remove phi.const_eqs phi_rhs.const_eqs
+      in
+      let type_constraints, _removed =
+        remove_if_different
+          (Var.Map.mem v phi.type_constraints)
+          (Option.equal InstanceOf.equal_instance_fact)
+          Var.Map.find_opt Var.Map.remove phi.type_constraints phi_rhs.type_constraints
+      in
+      let linear_eqs, removed_linear_eqs =
+        remove_if_different (Var.Map.mem v phi.linear_eqs) (Option.equal LinArith.equal)
+          Var.Map.find_opt Var.Map.remove phi.linear_eqs phi_rhs.linear_eqs
+      in
+      let linear_eqs_occurrences =
+        if removed_linear_eqs then Var.Map.remove v phi.linear_eqs_occurrences
+        else phi.linear_eqs_occurrences
+      in
+      let tableau, removed_tableau =
+        remove_if_different (Var.Map.mem v phi.tableau) (Option.equal LinArith.equal)
+          Var.Map.find_opt Var.Map.remove phi.tableau phi_rhs.tableau
+      in
+      let tableau_occurrences =
+        if removed_tableau then Var.Map.remove v phi.tableau_occurrences
+        else phi.tableau_occurrences
+      in
+      let intervals, _removed =
+        remove_if_different (Var.Map.mem v phi.intervals) (Option.equal CItv.equal) Var.Map.find_opt
+          Var.Map.remove phi.intervals phi_rhs.intervals
+      in
+      let atoms, atoms_occurrences =
+        match Var.Map.find_opt v phi.atoms_occurrences with
+        | None ->
+            (phi.atoms, phi.atoms_occurrences)
+        | Some atoms_v ->
+            Atom.Set.fold
+              (fun atom_v (atoms, atoms_occurrences) ->
+                if Atom.Set.mem atom_v phi_rhs.atoms then (atoms, atoms_occurrences)
+                else remove_atom_ atom_v atoms atoms_occurrences )
+              atoms_v
+              (phi.atoms, phi.atoms_occurrences)
+      in
+      let term_eqs, term_eqs_occurrences =
+        match Var.Map.find_opt v phi.term_eqs_occurrences with
+        | None ->
+            (phi.term_eqs, phi.term_eqs_occurrences)
+        | Some term_eqs_v ->
+            TermDomainOrRange.Set.fold
+              (fun (term_v, _) (term_eqs, term_eqs_occurrences) ->
+                if Term.VarMap.find_opt term_v phi_rhs.term_eqs |> Option.exists ~f:(Var.equal v)
+                then (term_eqs, term_eqs_occurrences)
+                else remove_term_eq_ term_v v term_eqs term_eqs_occurrences )
+              term_eqs_v
+              (phi.term_eqs, phi.term_eqs_occurrences)
+      in
+      { var_eqs
+      ; const_eqs
+      ; type_constraints
+      ; linear_eqs
+      ; term_eqs
+      ; tableau
+      ; intervals
+      ; atoms
+      ; linear_eqs_occurrences
+      ; tableau_occurrences
+      ; term_eqs_occurrences
+      ; atoms_occurrences }
+
+
+    let remove_condition_for_join atom phi_lhs phi_rhs =
+      Atom.fold_variables atom ~init:phi_lhs ~f:(scramble_var phi_rhs)
+
+
+    let remove_conditions_for_join atoms phi_lhs phi_rhs =
+      List.fold atoms ~init:phi_lhs ~f:(fun phi atom -> remove_condition_for_join atom phi phi_rhs)
   end
 
   include Unsafe
@@ -4735,3 +4831,53 @@ let pp_formula_explained pp_var fmt {phi} =
 let pp_conditions_explained pp_var fmt {conditions} =
   if not (Atom.Map.is_empty conditions) then
     F.fprintf fmt "@;∧ %a" (pp_conditions pp_var) conditions
+
+
+let join_conditions conditions_lhs conditions_rhs =
+  let conditions_join =
+    Atom.Map.merge
+      (fun _atom depth1 depth2 ->
+        (* keep only atoms present on both sides, with the min of their call depths *)
+        Option.both depth1 depth2 |> Option.map ~f:(fun (depth1, depth2) -> Int.min depth1 depth2)
+        )
+      conditions_lhs conditions_rhs
+  in
+  let atoms_not_in ~not_in:atoms_not_in atoms =
+    Atom.Map.merge
+      (fun _atom atom_depth not_in ->
+        match (atom_depth, not_in) with
+        | Some _, None ->
+            atom_depth
+        | None, _ | Some _, Some _ ->
+            None )
+      atoms atoms_not_in
+    |> Atom.Map.bindings |> List.map ~f:fst
+  in
+  let kill_conditions_lhs = atoms_not_in ~not_in:conditions_join conditions_lhs in
+  let kill_conditions_rhs = atoms_not_in ~not_in:conditions_join conditions_rhs in
+  (conditions_join, kill_conditions_lhs, kill_conditions_rhs)
+
+
+(* This relies on the idea that two formulas for the same procedure must be different only because
+   the path conditions are different. All other variables not involved in the path conditions are
+   the results of being created fresh to hold some intermediate values created by the program and so
+   can be handled with a conjunction (since they will appear only on one side).
+
+   Given that, the strategy is to compute the conditions that are common to both sides, and those
+   that are present only on one side need to be removed from the formulas. The removal of facts is
+   done brutally by forgetting all facts involving any variable present in these conditions. This
+   should be a valid over-approximation.
+
+   NOTE: It would be good to know which variables were created fresh in [phi1] and in [phi2] and
+   automatically keep information about these, since they cannot appear in the other formula and
+   their valuation doesn't matter for the formula where they don't belong. Instead, we rely on
+   conditions to tell which variables need to be forgotten about but that is over-approximate (and
+   fragile: it could be that some consequences are not completely cleaned up this way). *)
+let join {conditions= conditions_lhs; phi= phi_lhs} {conditions= conditions_rhs; phi= phi_rhs} =
+  let conditions_join, killed_conditions_lhs, killed_conditions_rhs =
+    join_conditions conditions_lhs conditions_rhs
+  in
+  let phi_lhs = Formula.remove_conditions_for_join killed_conditions_lhs phi_lhs phi_rhs in
+  let phi_rhs = Formula.remove_conditions_for_join killed_conditions_rhs phi_rhs phi_lhs in
+  let phi_join = Formula.join phi_lhs phi_rhs in
+  {conditions= conditions_join; phi= phi_join}

infer/src/pulse/PulseFormula.mli

@@ -160,3 +160,5 @@ val pp_term : (F.formatter -> Var.t -> unit) -> F.formatter -> term -> unit
 val pp_conditions_explained : (F.formatter -> Var.t -> unit) -> F.formatter -> t -> unit
 
 val pp_formula_explained : (F.formatter -> Var.t -> unit) -> F.formatter -> t -> unit
+
+val join : t -> t -> t

infer/src/pulse/PulseJoin.ml

@@ -345,9 +345,12 @@ let join_attributes join_state astate_lhs astate_rhs =
   (pre, post)
 
 
-let join_formulas _join_state _astate_lhs _astate_rhs =
-  (* TODO *)
-  Formula.ttrue
+let join_formulas _join_state astate_lhs astate_rhs =
+  let formula =
+    Formula.join astate_lhs.AbductiveDomain.path_condition astate_rhs.AbductiveDomain.path_condition
+  in
+  (* TODO: add info from [join_state.rev_subst] *)
+  formula
 
 
 let join_abductive astate_lhs astate_rhs =

infer/src/pulse/unit/PulseFormulaTest.ml

@@ -103,7 +103,7 @@ let ( = ) f1 f2 phi =
 let ( =. ) f1 f2 phi =
   let* phi, op1 = f1 phi in
   let* phi, op2 = f2 phi in
-  prune_binop ~negated:false Binop.Eq op1 op2 phi >>| fst
+  prune_binop ~negated:false Eq op1 op2 phi >>| fst
 
 
 let ( <> ) f1 f2 phi =
@@ -112,6 +112,12 @@ let ( <> ) f1 f2 phi =
   and_not_equal op1 op2 phi >>| fst
 
 
+let ( <>. ) f1 f2 phi =
+  let* phi, op1 = f1 phi in
+  let* phi, op2 = f2 phi in
+  prune_binop ~negated:false Ne op1 op2 phi >>| fst
+
+
 let ( < ) f1 f2 phi =
   let* phi, op1 = f1 phi in
   let* phi, op2 = f2 phi in
@@ -120,6 +126,12 @@ let ( < ) f1 f2 phi =
 
 let ( > ) f1 f2 phi = ( < ) f2 f1 phi
 
+let ( >. ) f1 f2 phi =
+  let* phi, op1 = f1 phi in
+  let* phi, op2 = f2 phi in
+  prune_binop ~negated:false Gt op1 op2 phi >>| fst
+
+
 let ( <= ) f1 f2 phi =
   let* phi, op1 = f1 phi in
   let* phi, op2 = f2 phi in
@@ -130,6 +142,12 @@ let ( >= ) f1 f2 phi = ( <= ) f2 f1 phi
 
 let ( && ) f1 f2 phi = f1 phi >>= f2
 
+let ( || ) f1 f2 phi =
+  let* phi1 = f1 phi in
+  let+ phi2 = f2 phi in
+  join phi1 phi2
+
+
 [@@@warning "+unused-value-declaration"]
 (* end of shorthand notations *)
 
@@ -708,3 +726,102 @@ let%test_module "non-numerical constants" =
              && const_eqs: x="prefix cannot match" ∧ y="hello"
              && term_eqs: "hello"=y∧"prefix cannot match"=x∧("hello"^z)=x |}]
   end )
+
+
+let%test_module "join" =
+  ( module struct
+    let%expect_test _ =
+      test (x =. i 42 || x =. i 42) ;
+      [%expect
+        {|
+        conditions: {x = 42} phi: linear_eqs: x = 42 && term_eqs: 42=x && intervals: x=42 |}]
+
+
+    let%expect_test _ =
+      test (x =. i 42 || x <>. i 42) ;
+      [%expect {|
+        conditions: (empty) phi: (empty) |}]
+
+
+    let%expect_test _ =
+      test (x =. y + i 1 || x =. y + i 1) ;
+      [%expect {|
+        conditions: (empty) phi: linear_eqs: x = y +1 && term_eqs: [y +1]=x |}]
+
+
+    let%expect_test _ =
+      test (z = y + i 1 && (x =. z || x <>. z)) ;
+      [%expect {|
+        conditions: (empty) phi: var_eqs: x=v6 |}]
+
+
+    let%expect_test _ =
+      test (x =. i 42 || x =. y) ;
+      [%expect {|
+        conditions: (empty) phi: (empty) |}]
+
+
+    let%expect_test _ =
+      test (x =. i 42 || (x <>. i 42 && x =. y)) ;
+      [%expect {|
+        conditions: (empty) phi: (empty) |}]
+
+
+    let%expect_test _ =
+      test ((x =. i 42 && y =. w) || (x =. z && y =. i 42)) ;
+      [%expect {|
+        conditions: (empty) phi: (empty) |}]
+
+
+    let%expect_test _ =
+      test (x =. y * z || i 0 = i 0) ;
+      [%expect {|
+        conditions: (empty) phi: (empty) |}]
+
+
+    let%expect_test _ =
+      test (w = y * z && (x =. w || x =. w)) ;
+      [%expect {|
+        conditions: {[x -w] = 0} phi: var_eqs: x=w=v6 && term_eqs: (y×z)=x |}]
+
+
+    (* doesn't work as well as the previous test when the non-linear term is evaluated (twice)
+       inside the conditionals *)
+    let%expect_test _ =
+      test (x =. y * z || x =. y * z) ;
+      [%expect {|
+        conditions: (empty) phi: (empty) |}]
+
+
+    let%expect_test _ =
+      test (w = y + z - i 4 && (x >. w || x >. w)) ;
+      [%expect
+        {|
+        conditions: {[-x +w] < 0}
+        phi: var_eqs: w=v7
+             && linear_eqs: x = v6 +a1 -3 ∧ y = -z +v6 ∧ w = v6 -4
+             && term_eqs: [v6 -4]=w∧[v6 +a1 -3]=x∧[-z +v6]=y |}]
+
+
+    (* doesn't work as well as the previous test when the term is evaluated (twice) inside the
+       conditionals *)
+    let%expect_test _ =
+      test (x >. y + z - i 4 || x >. y + z - i 4) ;
+      [%expect
+        {|
+        conditions: (empty)
+        phi: linear_eqs: y = -z +v7 +4 ∧ v6 = v7 +4 && term_eqs: [-z +v7 +4]=y∧[v7 +4]=v6 |}]
+
+
+    let%expect_test _ =
+      test (x =. s "toto" || x =. s "toto") ;
+      [%expect
+        {|
+        conditions: {x = "toto"} phi: const_eqs: x="toto" && term_eqs: "toto"=x |}]
+
+
+    let%expect_test _ =
+      test (x =. s "toto" || x =. s "titi") ;
+      [%expect {|
+        conditions: (empty) phi: (empty) |}]
+  end )