[hoisting] Make invalidation stop at already explored (var,node) pairs

Reviewed By: mbouaziz

Differential Revision: D12957025

fbshipit-source-id: b51f81966

infer/src/checkers/loopInvariant.ml

@@ -102,32 +102,42 @@ let get_vars_in_loop loop_nodes =
     loop_nodes VarsInLoop.empty
 
 
+module ProcessedPair = struct
+  type t = Var.t * Procdesc.Node.t [@@deriving compare]
+end
+
+module ProcessedPairSet = Caml.Set.Make (ProcessedPair)
+
 (* get all the ptr variables (and their dependencies) occurring on the
    RHS of the definition of a given variable. *)
 let get_ptr_vars_in_defn_path node loop_head var =
-  let rec aux node var =
+  let rec aux node var processed_pairs =
-    let invalidate_exp exp_rhs init =
+    if ProcessedPairSet.mem (var, node) processed_pairs then InvalidatedVars.empty
-      Var.get_all_vars_in_exp exp_rhs
+    else
-      |> Sequence.fold ~init ~f:(fun acc var ->
+      let invalidate_exp exp_rhs init =
-             List.fold_left ~init:(InvalidatedVars.add var acc)
+        let node_list =
-               ~f:(fun acc node -> InvalidatedVars.union (aux node var) acc)
+          node :: (if Procdesc.Node.equal node loop_head then [] else Procdesc.Node.get_preds node)
-               ( node
+        in
-               :: (if Procdesc.Node.equal node loop_head then [] else Procdesc.Node.get_preds node)
+        let processed_pairs' = ProcessedPairSet.add (var, node) processed_pairs in
-               ) )
+        Var.get_all_vars_in_exp exp_rhs
-    in
+        |> Sequence.fold ~init ~f:(fun acc rhs_var ->
-    Procdesc.Node.get_instrs node
+               List.fold_left ~init:(InvalidatedVars.add rhs_var acc)
-    |> Instrs.fold ~init:InvalidatedVars.empty ~f:(fun acc instr ->
+                 ~f:(fun acc node -> InvalidatedVars.union (aux node rhs_var processed_pairs') acc)
-           match instr with
+                 node_list )
-           | Sil.Load (id, exp_rhs, typ, _)
+      in
-             when Var.equal var (Var.of_id id) && is_non_primitive typ ->
+      Procdesc.Node.get_instrs node
-               invalidate_exp exp_rhs acc
+      |> Instrs.fold ~init:InvalidatedVars.empty ~f:(fun acc instr ->
-           | Sil.Store (Exp.Lvar pvar, typ, exp_rhs, _)
+             match instr with
-             when Var.equal var (Var.of_pvar pvar) && is_non_primitive typ ->
+             | Sil.Load (id, exp_rhs, typ, _)
-               invalidate_exp exp_rhs acc
+               when Var.equal var (Var.of_id id) && is_non_primitive typ ->
-           | _ ->
+                 invalidate_exp exp_rhs acc
-               acc )
+             | Sil.Store (Exp.Lvar pvar, typ, exp_rhs, _)
+               when Var.equal var (Var.of_pvar pvar) && is_non_primitive typ ->
+                 invalidate_exp exp_rhs acc
+             | _ ->
+                 acc )
   in
-  aux node var
+  aux node var ProcessedPairSet.empty
 
 
 let get_vars_to_invalidate node loop_head params invalidated_vars : InvalidatedVars.t =

infer/tests/codetoanalyze/java/hoisting/HoistInvalidate.java

@@ -13,4 +13,17 @@ class HoistInvalidate<T extends Tree> {
   void loop_over_sun_list_dont_hoist(List<T> list) {
     for (List<T> item = list; item.nonEmpty(); item = item.tail) {}
   }
+
+  class Item {
+
+    public Item next;
+
+    public void while_dont_hoist(Item in1, Item in2) {
+
+      while (in1.next != null) {
+        in1 = in1.next;
+        if (in1.equals(in2)) {}
+      }
+    }
+  }
 }