[backend] Keep common constraints in pure join

Summary:
This changes the algorithm for pure join to keep the constraints that,
after normalization, occur in both arguments.  Previously pure join
would normalize, filter, and then union the constraints of the
arguments.

Reviewed By: sblackshear

Differential Revision: D3970394

fbshipit-source-id: 3dc1672

infer/src/backend/dom.ml

@@ -1501,9 +1501,9 @@ let rec sigma_partial_join' tenv mode (sigma_acc: Prop.sigma)
         assert false (* Should be handled by a guarded case *)
 
   with Todo.Empty ->
-    match sigma1_in, sigma2_in with
+  match sigma1_in, sigma2_in with
-    | _:: _, _:: _ -> L.d_strln "todo is empty, but the sigmas are not"; raise IList.Fail
+  | _:: _, _:: _ -> L.d_strln "todo is empty, but the sigmas are not"; raise IList.Fail
-    | _ -> sigma_acc, sigma1_in, sigma2_in
+  | _ -> sigma_acc, sigma1_in, sigma2_in
 
 let sigma_partial_join tenv mode (sigma1: Prop.sigma) (sigma2: Prop.sigma)
   : (Prop.sigma * Prop.sigma * Prop.sigma) =
@@ -1555,9 +1555,9 @@ let rec sigma_partial_meet' tenv (sigma_acc: Prop.sigma) (sigma1_in: Prop.sigma)
         (L.d_strln "failure reason 65"; raise IList.Fail)
 
   with Todo.Empty ->
-    match sigma1_in, sigma2_in with
+  match sigma1_in, sigma2_in with
-    | [], [] -> sigma_acc
+  | [], [] -> sigma_acc
-    | _, _ -> L.d_strln "todo is empty, but the sigmas are not"; raise IList.Fail
+  | _, _ -> L.d_strln "todo is empty, but the sigmas are not"; raise IList.Fail
 
 let sigma_partial_meet tenv (sigma1: Prop.sigma) (sigma2: Prop.sigma) : Prop.sigma =
   sigma_partial_meet' tenv [] sigma1 sigma2
@@ -1574,11 +1574,6 @@ let pi_partial_join tenv mode
     (ep1: Prop.exposed Prop.t) (ep2: Prop.exposed Prop.t)
     (pi1: Prop.pi) (pi2: Prop.pi) : Prop.pi
   =
-  let exp_is_const = function
-    (* | Exp.Var id -> is_normal id *)
-    | Exp.Const _ -> true
-    (* | Exp.Lvar _ -> true *)
-    | _ -> false in
   let get_array_len prop =
     (* find some array length in the prop, to be used as heuritic for upper bound in widening *)
     let len_list = ref [] in
@@ -1666,18 +1661,6 @@ let pi_partial_join tenv mode
               | None -> atom_list
               | Some a' -> a' :: atom_list))
     | Some a' -> a' :: atom_list in
-  let filter_atom = function
-    | Sil.Aneq(e, e') | Sil.Aeq(e, e')
-      when (exp_is_const e && exp_is_const e') ->
-        true
-    | Sil.Aneq(Exp.Var _, e') | Sil.Aneq(e', Exp.Var _)
-    | Sil.Aeq(Exp.Var _, e') | Sil.Aeq(e', Exp.Var _)
-      when (exp_is_const e') ->
-        true
-    | Sil.Aneq _ -> false
-    | Sil.Aeq _ as e -> Prop.atom_is_inequality e
-    | Sil.Apred (_, es) | Anpred (_, es) ->
-        IList.for_all exp_is_const es in
   begin
     if Config.trace_join then begin
       L.d_str "pi1: "; Prop.d_pi pi1; L.d_ln ();
@@ -1687,18 +1670,15 @@ let pi_partial_join tenv mode
       let p2 = Prop.normalize tenv ep2 in
       IList.fold_left (handle_atom_with_widening Lhs p2 pi2) [] pi1 in
     if Config.trace_join then (L.d_str "atom_list1: "; Prop.d_pi atom_list1; L.d_ln ());
-    let atom_list_combined =
+    let atom_list2 =
       let p1 = Prop.normalize tenv ep1 in
-      IList.fold_left (handle_atom_with_widening Rhs p1 pi1) atom_list1 pi2 in
+      IList.fold_left (handle_atom_with_widening Rhs p1 pi1) [] pi2 in
     if Config.trace_join then
-      (L.d_str "atom_list_combined: "; Prop.d_pi atom_list_combined; L.d_ln ());
+      (L.d_str "atom_list2: "; Prop.d_pi atom_list2; L.d_ln ());
-    let atom_list_filtered =
+    let atom_list_combined = IList.inter Sil.atom_compare atom_list1 atom_list2 in
-      IList.filter filter_atom atom_list_combined in
     if Config.trace_join then
-      (L.d_str "atom_list_filtered: "; Prop.d_pi atom_list_filtered; L.d_ln ());
+      (L.d_str "atom_list_combined: "; Prop.d_pi atom_list_combined; L.d_ln ());
-    let atom_list_res =
+    atom_list_combined
-      IList.rev atom_list_filtered in
-    atom_list_res
   end
 
 let pi_partial_meet tenv (p: Prop.normal Prop.t) (ep1: 'a Prop.t) (ep2: 'b Prop.t) : Prop.normal Prop.t =

infer/src/base/IList.ml

@@ -199,6 +199,25 @@ let intersect compare l1 l2 =
         else f l1 l2' in
   f l1_sorted l2_sorted
 
+let inter compare xs ys =
+  let rev_sort xs = sort (fun x y -> compare y x) xs in
+  let rev_xs = rev_sort xs in
+  let rev_ys = rev_sort ys in
+  let rec inter_ is rev_xxs rev_yys =
+    match rev_xxs, rev_yys with
+    | ([], _) | (_, []) ->
+        is
+    | (x :: rev_xs, y :: rev_ys) ->
+        let c = compare x y in
+        if c = 0 then
+          inter_ (x :: is) rev_xs rev_ys
+        else if c < 0 then
+          inter_ is rev_xs rev_yys
+        else
+          inter_ is rev_xxs rev_ys
+  in
+  inter_ [] rev_xs rev_ys
+
 exception Fail
 
 (** Apply [f] to pairs of elements; raise [Fail] if the two lists have different lenghts. *)

infer/src/base/IList.mli

@@ -98,6 +98,9 @@ val merge_sorted_nodup : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list -> '
     The compare function is required to sort the lists. *)
 val intersect : ('a -> 'a -> int) -> 'a list -> 'a list -> bool
 
+(** [inter cmp xs ys] are the elements in both [xs] and [ys], sorted according to [cmp]. *)
+val inter : ('a -> 'a -> int) -> 'a list -> 'a list -> 'a list
+
 (** Like List.mem_assoc but without builtin equality *)
 val mem_assoc : ('a -> 'a -> bool) -> 'a -> ('a * 'b) list -> bool
 

infer/tests/codetoanalyze/java/infer/GuardedByExample.java

@@ -356,7 +356,7 @@ public class GuardedByExample {
 
   int n;
 
-  public void FP_withloop2() {
+  public void withloop2() {
     synchronized (mLock) {
       for (int i = 0; i<=n; i++) {
         f = 42;

infer/tests/codetoanalyze/java/infer/issues.exp

@@ -74,7 +74,6 @@ FilterOutputStreamLeaks.java, void FilterOutputStreamLeaks.printStreamNotClosedA
 GuardedByExample.java, Object GuardedByExample.byRefTrickyBad(), 5, UNSAFE_GUARDED_BY_ACCESS
 GuardedByExample.java, String GuardedByExample$3.readFromInnerClassBad1(), 2, UNSAFE_GUARDED_BY_ACCESS
 GuardedByExample.java, String GuardedByExample$4.readFromInnerClassBad2(), 1, UNSAFE_GUARDED_BY_ACCESS
-GuardedByExample.java, void GuardedByExample.FP_withloop2(), 3, UNSAFE_GUARDED_BY_ACCESS
 GuardedByExample.java, void GuardedByExample.readFAfterBlockBad(), 3, UNSAFE_GUARDED_BY_ACCESS
 GuardedByExample.java, void GuardedByExample.readFBad(), 1, UNSAFE_GUARDED_BY_ACCESS
 GuardedByExample.java, void GuardedByExample.readFBadWrongAnnotation(), 1, UNSAFE_GUARDED_BY_ACCESS