[purity, hoisting] Keep track of modified args

Reviewed By: mbouaziz

Differential Revision: D12921871

fbshipit-source-id: 17ba48895

infer/src/checkers/loopInvariant.ml

@@ -23,18 +23,19 @@ let is_defined_outside loop_nodes reaching_defs var =
   |> Option.value ~default:true
 
 
-let is_fun_pure tenv ~is_inv_by_default callee_pname params =
+let get_purity tenv ~is_inv_by_default callee_pname args =
   (* Take into account purity behavior of modeled functions *)
-  match Models.Call.dispatch tenv callee_pname params with
+  let all_params_modified = PurityDomain.all_params_modified args in
+  match Models.Call.dispatch tenv callee_pname args with
   | Some inv ->
-      InvariantModels.is_invariant inv
+      PurityDomain.with_purity (InvariantModels.is_invariant inv) all_params_modified
   | None -> (
     (* If there is no model, invoke purity analysis to see if function is pure *)
     match Ondemand.analyze_proc_name callee_pname with
-    | Some {Summary.payloads= {Payloads.purity= Some is_pure}} ->
-        is_pure
+    | Some {Summary.payloads= {Payloads.purity= Some purity_summary}} ->
+        purity_summary
     | _ ->
-        is_inv_by_default )
+        PurityDomain.with_purity is_inv_by_default all_params_modified )
 
 
 let is_non_primitive typ = Typ.is_pointer typ || Typ.is_struct typ
@@ -57,10 +58,10 @@ let is_def_unique_and_satisfy tenv var (loop_nodes : LoopNodes.t) ~is_inv_by_def
               | Sil.Store (exp_lhs, _, exp_rhs, _)
                 when Exp.equal exp_lhs (Var.to_exp var) && is_exp_invariant exp_rhs ->
                   true
-              | Sil.Call ((id, _), Const (Cfun callee_pname), params, _, _) when equals_var id ->
-                  is_fun_pure tenv ~is_inv_by_default callee_pname params
+              | Sil.Call ((id, _), Const (Cfun callee_pname), args, _, _) when equals_var id ->
+                  PurityDomain.is_pure (get_purity tenv ~is_inv_by_default callee_pname args)
                   && (* check if all params are invariant *)
-                     List.for_all ~f:(fun (exp, _) -> is_exp_invariant exp) params
+                     List.for_all ~f:(fun (exp, _) -> is_exp_invariant exp) args
               | _ ->
                   false ) )
        loop_nodes
@@ -140,16 +141,20 @@ let get_ptr_vars_in_defn_path node loop_head var =
   aux node var ProcessedPairSet.empty
 
 
-let get_vars_to_invalidate node loop_head params invalidated_vars : InvalidatedVars.t =
-  List.fold ~init:invalidated_vars
-    ~f:(fun acc (arg_exp, typ) ->
+let get_vars_to_invalidate node loop_head args modified_params invalidated_vars : InvalidatedVars.t
+    =
+  List.foldi ~init:invalidated_vars
+    ~f:(fun i acc (arg_exp, typ) ->
+      if PurityDomain.ModifiedParamIndices.mem i modified_params then (
+        debug "Invalidate %a \n" Exp.pp arg_exp ;
         Var.get_all_vars_in_exp arg_exp
         |> Sequence.fold ~init:acc ~f:(fun acc var ->
                if is_non_primitive typ then
                  let dep_vars = get_ptr_vars_in_defn_path node loop_head var in
                  InvalidatedVars.union dep_vars (InvalidatedVars.add var acc)
                else acc ) )
-    params
+      else acc )
+    args
 
 
 (* If there is a call to an impure function in the loop, invalidate
@@ -161,10 +166,12 @@ let get_invalidated_vars_in_loop tenv loop_head ~is_inv_by_default loop_nodes =
       Procdesc.Node.get_instrs node
       |> Instrs.fold ~init:acc ~f:(fun acc instr ->
              match instr with
-             | Sil.Call ((id, _), Const (Cfun callee_pname), params, _, _)
-               when not (is_fun_pure tenv ~is_inv_by_default callee_pname params) ->
-                 get_vars_to_invalidate node loop_head params
-                   (InvalidatedVars.add (Var.of_id id) acc)
+             | Sil.Call ((id, _), Const (Cfun callee_pname), args, _, _) ->
+                 let purity = get_purity tenv ~is_inv_by_default callee_pname args in
+                 Option.value_map (PurityDomain.get_modified_params purity) ~default:acc
+                   ~f:(fun modified_params ->
+                     get_vars_to_invalidate node loop_head args modified_params
+                       (InvalidatedVars.add (Var.of_id id) acc) )
              | _ ->
                  acc ) )
     loop_nodes InvalidatedVars.empty

infer/src/checkers/purity.ml

@@ -7,6 +7,7 @@
 open! IStd
 module F = Format
 module L = Logging
+module ModifiedVarSet = Caml.Set.Make (Var)
 
 let debug fmt = L.(debug Analysis Verbose fmt)
 
@@ -22,9 +23,24 @@ end)
 
 module TransferFunctions (CFG : ProcCfg.S) = struct
   module CFG = CFG
-  module Domain = PurityDomain.Pure
+  module Domain = PurityDomain
+
+  type extras = Var.t list
+
+  let get_modified_params formals ~f =
+    List.foldi ~init:Domain.ModifiedParamIndices.empty
+      ~f:(fun i modified_acc var ->
+        if f var then Domain.ModifiedParamIndices.add i modified_acc else modified_acc )
+      formals
+
+
+  (* given a heap access to ae, find which parameter indices of pdesc
+     it modifies *)
+  let track_modified_params formals ae =
+    let base_var, _ = AccessExpression.get_base ae in
+    let modified_params = get_modified_params formals ~f:(Var.equal base_var) in
+    Domain.impure modified_params
 
-  type extras = ProcData.no_extras
 
   let rec is_heap_access ae =
     match (ae : AccessExpression.t) with
@@ -36,26 +52,62 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         false
 
 
-  let exec_instr (astate : Domain.astate) {ProcData.pdesc; tenv} _ (instr : HilInstr.t) =
-    if astate then
+  (* given the purity of the callee and the respective args, find
+     parameters of the current pdesc that match, i.e have been
+     modified by the callee.
+
+     E.g. : for the below call to 'impure_fun' in 'foo', we return 2
+     (i.e. index of a).
+
+     void foo (int x, Object a, Object b){
+        for (...){
+           impure_fun(b, 10, a); // modifies only 4th argument, i.e. a
+        }
+     }
+  *)
+  let find_params_matching_modified_args formals args callee_summary =
+    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 ->
+              if Domain.ModifiedParamIndices.mem i callee_modified_params then (
+                debug "Argument %a is modified.\n" HilExp.pp arg_exp ;
+                HilExp.get_access_exprs arg_exp
+                |> List.fold ~init:modified_acc ~f:(fun modified_acc ae ->
+                       ModifiedVarSet.add (AccessExpression.get_base ae |> fst) modified_acc ) )
+              else modified_acc )
+            args
+        in
+        Domain.impure
+          ((* 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 ))
+    | None ->
+        Domain.pure
+
+
+  let exec_instr (astate : Domain.astate) {ProcData.pdesc; tenv; ProcData.extras= formals} _
+      (instr : HilInstr.t) =
     match instr with
-      | Assign (ae, _, _) ->
-          not (is_heap_access ae)
-      | Call (_, Direct called_pname, _, _, _) -> (
-        match InvariantModels.Call.dispatch tenv called_pname [] with
+    | 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
+        Domain.join astate
+          ( match InvariantModels.Call.dispatch tenv called_pname [] with
           | Some inv ->
-            InvariantModels.is_invariant inv
+              Domain.with_purity (InvariantModels.is_invariant inv) all_params_modified
           | None ->
               Payload.read pdesc called_pname
-            |> Option.value_map ~default:false ~f:(fun summary ->
+              |> Option.value_map ~default:(Domain.impure all_params_modified) ~f:(fun summary ->
                      debug "Reading from %a \n" Typ.Procname.pp called_pname ;
-                   summary ) )
+                     find_params_matching_modified_args 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
     | _ ->
         astate
-    else astate
 
 
   let pp_session_name _node fmt = F.pp_print_string fmt "purity checker"
@@ -63,11 +115,10 @@ end
 
 module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Normal) (TransferFunctions)
 
-let should_report is_pure pdesc =
+let should_report pdesc =
   match Procdesc.get_proc_name pdesc with
   | Typ.Procname.Java java_pname as proc_name ->
-      is_pure
-      && (not (Typ.Procname.is_constructor proc_name))
+      (not (Typ.Procname.is_constructor proc_name))
       && (not (Typ.Procname.Java.is_class_initializer java_pname))
       && not (Typ.Procname.Java.is_access_method java_pname)
   | _ ->
@@ -75,19 +126,27 @@ let should_report is_pure pdesc =
 
 
 let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
-  let initial = true in
   let proc_name = Procdesc.get_proc_name proc_desc in
-  let proc_data = ProcData.make_default proc_desc tenv in
+  let formals =
+    Procdesc.get_formals proc_desc
+    |> List.map ~f:(fun (mname, _) -> Var.of_pvar (Pvar.mk mname proc_name))
+  in
+  let proc_data = ProcData.make proc_desc tenv formals in
   let report_pure () =
     let loc = Procdesc.get_loc proc_desc in
     let exp_desc = F.asprintf "Side-effect free function %a" Typ.Procname.pp proc_name in
     let ltr = [Errlog.make_trace_element 0 loc exp_desc []] in
     Reporting.log_error summary ~loc ~ltr IssueType.pure_function exp_desc
   in
-  match Analyzer.compute_post proc_data ~initial with
-  | Some is_pure ->
-      if should_report is_pure proc_desc then report_pure () ;
-      Payload.update_summary is_pure summary
+  match Analyzer.compute_post proc_data ~initial:PurityDomain.pure with
+  | Some astate ->
+      ( match PurityDomain.get_modified_params astate with
+      | Some modified_params ->
+          debug "Modified parameter indices of %a: %a \n" Typ.Procname.pp proc_name
+            PurityDomain.ModifiedParamIndices.pp modified_params
+      | None ->
+          if should_report proc_desc then report_pure () ) ;
+      Payload.update_summary astate summary
   | None ->
       L.internal_error "Analyzer failed to compute purity information for %a@." Typ.Procname.pp
         proc_name ;

infer/src/checkers/purityDomain.ml

@@ -6,8 +6,34 @@
  *)
 open! IStd
 module F = Format
-module Pure = AbstractDomain.BooleanAnd
+module ModifiedParamIndices = AbstractDomain.FiniteSet (Int)
+module Domain = AbstractDomain.BottomLifted (ModifiedParamIndices)
+include Domain
 
-type summary = Pure.astate
+let pure = AbstractDomain.Types.Bottom
 
-let pp_summary fmt summary = F.fprintf fmt "@\n Purity summary: %a @\n" Pure.pp summary
+let is_pure = Domain.is_empty
+
+let impure modified_args = AbstractDomain.Types.NonBottom modified_args
+
+let with_purity is_pure modified_args =
+  if is_pure then AbstractDomain.Types.Bottom else impure modified_args
+
+
+let all_params_modified args =
+  List.foldi ~init:ModifiedParamIndices.empty
+    ~f:(fun i acc _ -> ModifiedParamIndices.add i acc)
+    args
+
+
+let get_modified_params astate =
+  match astate with
+  | AbstractDomain.Types.NonBottom modified_args ->
+      Some modified_args
+  | AbstractDomain.Types.Bottom ->
+      None
+
+
+type summary = Domain.astate
+
+let pp_summary fmt astate = F.fprintf fmt "@\n Purity summary: %a @\n" Domain.pp astate

infer/tests/codetoanalyze/java/hoisting/ByteBufferTest.java

@@ -0,0 +1,36 @@
+/*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+class ByteBufferTest {
+
+  class ByteBuffer {
+    byte[] bufferBytes;
+
+    int limit = 10;
+    int pos = 0;
+
+    public int getInt() {
+      return bufferBytes[pos++];
+    }
+
+    public int remaining() {
+      return limit - pos;
+    }
+  }
+
+  public static int[] decodeMobileOnly(ByteBuffer buffer) {
+    int[] dataUsage = new int[3];
+    dataUsage[0] = buffer.getInt();
+    return dataUsage;
+  }
+
+  // don't hoist remaining()
+  void inner_change_don_hoist(ByteBuffer byteBuffer) {
+    while (byteBuffer.remaining() > 0) {
+      decodeMobileOnly(byteBuffer);
+    }
+  }
+}

infer/tests/codetoanalyze/java/hoisting/HoistIndirect.java

@@ -52,7 +52,6 @@ class HoistIndirect {
             return_only(t),
             size); // foo' and return_only's arguments are variant, hence don't hoist
       }
-      ;
     }
 
     // t changes deep in the call stack
@@ -66,8 +65,8 @@ class HoistIndirect {
       return d;
     }
 
-    // foo(3) is ok to hoist, but can't detect this right now
-    int indirect_modification_hoist_FN(int size) {
+    // foo(3) is ok to hoist
+    int indirect_modification_hoist(int size) {
       int d = 0;
       Test t = new Test();
       for (int i = 0; i < size; i++) {
@@ -76,6 +75,20 @@ class HoistIndirect {
       }
       return d;
     }
+
+    void set_only_first_param(Test test, Test no_mod) {
+      test.a = 5;
+    }
+
+    int indirect_modification_only_second_call_hoist(int size, Test t, Test no_mod_t) {
+      int d = 0;
+      for (int i = 0; i < size; i++) {
+        set_only_first_param(t, no_mod_t);
+        d = get_test(t); // don't hoist since t changes
+        d = get_test(no_mod_t); // hoist since no_mod_t doesn't change
+      }
+      return d;
+    }
   }
 
   void set() {
@@ -86,11 +99,12 @@ class HoistIndirect {
     return svar;
   }
 
-  int indirect_this_modification_dont_hoist(int size) {
+  // can't deal with static variables yet because they don't appear as parameters
+  int indirect_this_modification_dont_hoist_FP(int size) {
     int d = 0;
 
     for (int i = 0; i < size; i++) {
-      d = get(); // don't hoist since this.svar changes in the loop
+      d = get(); // don't hoist since HoistIndirect.svar changes in the loop
       set();
     }
     return d;
@@ -200,4 +214,28 @@ class HoistIndirect {
       }
     }
   }
+
+  void unmodified_arg_hoist(int[][] nextRegionM, int p, int[] tempRegion) {
+    for (int i = 0; i < 10; i++) {
+      if (i
+          < regionFirst(nextRegionM[p])
+              + regionFirst(tempRegion)) { // regionFirst(tempRegion) can be hoisted
+        sumDest(tempRegion, nextRegionM[p], i); // invalidate nextRegionM
+      }
+    }
+  }
+
+  // arr is modified via aliasing
+  void alias(int[] arr) {
+
+    int[] new_arr = arr;
+    new_arr[0] = 4;
+  }
+
+  void alias_dont_hoist_FP(int[] arr) {
+    for (int i = 0; i < 10; i++) {
+      alias(arr); // alias modifies arr
+      get_ith(0, arr); // don't hoist
+    }
+  }
 }

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

@@ -1,3 +1,4 @@
+codetoanalyze/java/hoisting/ByteBufferTest.java, ByteBufferTest$ByteBuffer.remaining():int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int ByteBufferTest$ByteBuffer.remaining()]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.array_store_hoist(int,int[]):void, 5, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int Hoist.foo(int,int) at line 117]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.bar(int):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Hoist.bar(int)]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.clash_function_calls_hoist(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Hoist.clash_function_calls_hoist(int)]
@@ -24,16 +25,21 @@ codetoanalyze/java/hoisting/Hoist.java, Hoist.x_not_invariant_dont_hoist(int,int
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.foo(int):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistIndirect$Test.foo(int)]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.get_sum_test(HoistIndirect$Test,int):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistIndirect$Test.get_sum_test(HoistIndirect$Test,int)]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.get_test(HoistIndirect$Test):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistIndirect$Test.get_test(HoistIndirect$Test)]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.indirect_modification_hoist(int):int, 5, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect$Test.foo(int) at line 74]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.indirect_modification_only_second_call_hoist(int,HoistIndirect$Test,HoistIndirect$Test):int, 5, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect$Test.get_test(HoistIndirect$Test) at line 88]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.return_only(HoistIndirect$Test):HoistIndirect$Test, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function HoistIndirect$Test HoistIndirect$Test.return_only(HoistIndirect$Test)]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.arg_modification_hoist(int,HoistIndirect$Test):int, 3, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect.get() at line 121]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.direct_this_modification_dont_hoist_FP(int):int, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect.get() at line 103]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.alias_dont_hoist_FP(int[]):void, 3, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect.get_ith(int,int[]) at line 238]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.arg_modification_hoist(int,HoistIndirect$Test):int, 3, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect.get() at line 135]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.direct_this_modification_dont_hoist_FP(int):int, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect.get() at line 117]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.double_me(int):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistIndirect.double_me(int)]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.get():int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistIndirect.get()]
 codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.get_ith(int,int[]):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistIndirect.get_ith(int,int[])]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.independent_hoist(int,HoistIndirect$Test):int, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect$Test.foo(int) at line 148]
-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 198]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.independent_hoist(int,HoistIndirect$Test):int, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect$Test.foo(int) at line 162]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.indirect_this_modification_dont_hoist_FP(int):int, 4, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistIndirect.get() at line 107]
+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.regionFirst(int[]):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistIndirect.regionFirst(int[])]
-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 113]
+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/HoistNoIndirectMod.java, HoistNoIndirectMod.calcNext():int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistNoIndirectMod.calcNext()]
 codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.calcSame():int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int HoistNoIndirectMod.calcSame()]
 codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.increment_dont_hoist_FP(int):int, 2, INVARIANT_CALL, no_bucket, ERROR, [Loop-invariant call to int HoistNoIndirectMod.calcNext() at line 27]