From d8336ea906b1c153714c610346ab9c9853b9280a Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Sat, 8 Oct 2016 04:54:27 -0700 Subject: [PATCH] [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 | 44 +++++-------------- infer/src/base/IList.ml | 19 ++++++++ infer/src/base/IList.mli | 3 ++ .../java/infer/GuardedByExample.java | 2 +- .../tests/codetoanalyze/java/infer/issues.exp | 1 - 5 files changed, 35 insertions(+), 34 deletions(-) diff --git a/infer/src/backend/dom.ml b/infer/src/backend/dom.ml index c55418cfc..f23ca4083 100644 --- a/infer/src/backend/dom.ml +++ b/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 - | _:: _, _:: _ -> L.d_strln "todo is empty, but the sigmas are not"; raise IList.Fail - | _ -> sigma_acc, sigma1_in, sigma2_in + match sigma1_in, sigma2_in with + | _:: _, _:: _ -> L.d_strln "todo is empty, but the sigmas are not"; raise IList.Fail + | _ -> 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 - | [], [] -> sigma_acc - | _, _ -> L.d_strln "todo is empty, but the sigmas are not"; raise IList.Fail + match sigma1_in, sigma2_in with + | [], [] -> sigma_acc + | _, _ -> 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 ()); - let atom_list_filtered = - IList.filter filter_atom atom_list_combined in + (L.d_str "atom_list2: "; Prop.d_pi atom_list2; L.d_ln ()); + let atom_list_combined = IList.inter Sil.atom_compare atom_list1 atom_list2 in if Config.trace_join then - (L.d_str "atom_list_filtered: "; Prop.d_pi atom_list_filtered; L.d_ln ()); - let atom_list_res = - IList.rev atom_list_filtered in - atom_list_res + (L.d_str "atom_list_combined: "; Prop.d_pi atom_list_combined; L.d_ln ()); + atom_list_combined end let pi_partial_meet tenv (p: Prop.normal Prop.t) (ep1: 'a Prop.t) (ep2: 'b Prop.t) : Prop.normal Prop.t = diff --git a/infer/src/base/IList.ml b/infer/src/base/IList.ml index dccaf73e8..1e3a85c59 100644 --- a/infer/src/base/IList.ml +++ b/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. *) diff --git a/infer/src/base/IList.mli b/infer/src/base/IList.mli index a7d1c5edf..c8d2b98b7 100644 --- a/infer/src/base/IList.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/java/infer/GuardedByExample.java b/infer/tests/codetoanalyze/java/infer/GuardedByExample.java index ce63fec89..920a7e902 100644 --- a/infer/tests/codetoanalyze/java/infer/GuardedByExample.java +++ b/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; diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp index c5e6f3888..e626e0bb6 100644 --- a/infer/tests/codetoanalyze/java/infer/issues.exp +++ b/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