[purity] Fix wrong invalidation of all params

Reviewed By: ddino

Differential Revision: D13119156

fbshipit-source-id: a766c16be

infer/src/checkers/purity.ml

@@ -52,22 +52,21 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         false
 
 
-  (* given the purity of the callee and the respective args, find
+  (* given the modified parameters and the args of the callee, find
-     parameters of the current pdesc that match, i.e have been
+     parameter indices of the current procedure that match, i.e have
-     modified by the callee.
+     been modified by the callee. Note that index counting starts from
+     0, reserved for the implicit parameter (formal) this .
 
      E.g. : for the below call to 'impure_fun' in 'foo', we return 2
-     (i.e. index of a).
+     (i.e. index of a wrt. foo's formals).
 
      void foo (int x, Object a, Object b){
         for (...){
-           impure_fun(b, 10, a); // modifies only 4th argument, i.e. a
+           impure_fun(b, 10, a); // modifies only 3rd argument, i.e. a
         }
      }
   *)
-  let find_params_matching_modified_args formals args callee_summary =
+  let find_params_matching_modified_args formals callee_args callee_modified_params =
-    match Domain.get_modified_params callee_summary with
-    | Some callee_modified_params ->
     let vars_of_modified_args =
       List.foldi ~init:ModifiedVarSet.empty
         ~f:(fun i modified_acc arg_exp ->
@@ -77,12 +76,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             |> List.fold ~init:modified_acc ~f:(fun modified_acc ae ->
                    ModifiedVarSet.add (AccessExpression.get_base ae |> fst) modified_acc ) )
           else modified_acc )
-            args
+        callee_args
     in
-        Domain.impure
+    (* find the respective parameter of the proc, matching the modified vars *)
-          ((* find the respective parameter of pdesc, matching the modified vars *)
     get_modified_params formals ~f:(fun formal_var ->
-               ModifiedVarSet.mem formal_var vars_of_modified_args ))
+        ModifiedVarSet.mem formal_var vars_of_modified_args )
+
+
+  (* if the callee is impure, find the parameters that have been modified by the callee *)
+  let find_modified_if_impure formals args callee_summary =
+    match Domain.get_modified_params callee_summary with
+    | Some callee_modified_params ->
+        debug "Callee modified params %a \n" Domain.ModifiedParamIndices.pp callee_modified_params ;
+        Domain.impure (find_params_matching_modified_args formals args callee_modified_params)
     | None ->
         Domain.pure
 
@@ -93,16 +99,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Assign (ae, _, _) when is_heap_access ae ->
         track_modified_params formals ae |> Domain.join astate
     | Call (_, Direct called_pname, args, _, _) ->
-        let all_params_modified = Domain.all_params_modified args in
+        let matching_modified =
+          find_params_matching_modified_args formals args (Domain.all_params_modified args)
+        in
         Domain.join astate
           ( match InvariantModels.Call.dispatch tenv called_pname [] with
           | Some inv ->
-              Domain.with_purity (InvariantModels.is_invariant inv) all_params_modified
+              Domain.with_purity (InvariantModels.is_invariant inv) matching_modified
           | None ->
               Payload.read pdesc called_pname
-              |> Option.value_map ~default:(Domain.impure all_params_modified) ~f:(fun summary ->
+              |> Option.value_map ~default:(Domain.impure matching_modified) ~f:(fun summary ->
                      debug "Reading from %a \n" Typ.Procname.pp called_pname ;
-                     find_params_matching_modified_args formals args summary ) )
+                     find_modified_if_impure formals args summary ) )
     | Call (_, Indirect _, _, _, _) ->
         (* This should never happen in Java. Fail if it does. *)
         L.(die InternalError) "Unexpected indirect call %a" HilInstr.pp instr

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

@@ -6,9 +6,11 @@
  */
 import com.sun.source.tree.Tree;
 import com.sun.tools.javac.util.List;
+import java.util.ArrayList;
 
 class HoistInvalidate<T extends Tree> {
 
+  int x = 0;
   // item will be invalidated
   void loop_over_sun_list_dont_hoist(List<T> list) {
     for (List<T> item = list; item.nonEmpty(); item = item.tail) {}
@@ -26,4 +28,37 @@ class HoistInvalidate<T extends Tree> {
       }
     }
   }
+
+  public void add_to_head(ArrayList<Integer> list, int[] array) {
+    list.add(0);
+  }
+
+  int get_length(int[] array) {
+    return array.length;
+  }
+
+  int get_x(int[] array) {
+    return array[x];
+  }
+
+  int effectful_get_length(int[] array) {
+    x = 0;
+    return array.length;
+  }
+
+  public void loop_indirect_hoist(ArrayList<Integer> list, int x, int[] array) {
+    for (int i = 0; i < 10; i++) {
+      add_to_head(list, array); // invalidate only list
+      get_length(array); // ok to hoist
+    }
+  }
+
+  // to deal with the FN, we need to track which global arguments are read
+  public void loop_indirect_hoist_FN(ArrayList<Integer> list, int x, int[] array) {
+    for (int i = 0; i < 10; i++) {
+      get_length(array); // ok to hoist
+      get_x(array); // not ok to hoist since it reads this.x
+      effectful_get_length(array); // here, we invalidate *this* (implicit arg)
+    }
+  }
 }

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

@@ -18,6 +18,7 @@ codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.indirect_this_modi
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.irvar_independent_hoist(int[][],int,int[]):void, 2, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect.double_me(int) at line 212]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.this_modification_outside_hoist(int):int, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect.get() at line 127]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.unmodified_arg_hoist(int[][],int,int[]):void, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect.regionFirst(int[]) at line 222]
+codetoanalyze/java/hoisting/HoistInvalidate.java, HoistInvalidate.loop_indirect_hoist(java.util.ArrayList,int,int[]):void, 3, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistInvalidate.get_length(int[]) at line 52]
 codetoanalyze/java/hoisting/HoistModeled.java, HoistModeled.deserialize_hoist(com.fasterxml.jackson.databind.JsonDeserializer,com.fasterxml.jackson.core.JsonParser,com.fasterxml.jackson.databind.DeserializationContext):void, 8, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to Object JsonDeserializer.deserialize(JsonParser,DeserializationContext) at line 33]
 codetoanalyze/java/hoisting/HoistModeled.java, HoistModeled.list_contains_hoist(java.util.List,java.lang.String):int, 3, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to String String.substring(int,int) at line 18]
 codetoanalyze/java/hoisting/HoistModeled.java, HoistModeled.list_contains_hoist(java.util.List,java.lang.String):int, 3, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to boolean List.contains(Object) at line 18]