[purity] Mark functions that write to global static vars as impure

Reviewed By: ngorogiannis

Differential Revision: D13434587

fbshipit-source-id: 6fb3cf917

infer/src/checkers/loopInvariant.ml

@@ -154,10 +154,24 @@ let get_vars_to_invalidate node loop_head args modified_params invalidated_vars
     args
 
 
+let all_modified loop_nodes =
+  LoopNodes.fold
+    (fun node acc ->
+      Procdesc.Node.get_instrs node
+      |> Instrs.fold ~init:acc ~f:(fun acc instr ->
+             match instr with
+             | Sil.Call ((id, _), _, _, _, _) ->
+                 InvalidatedVars.add (Var.of_id id) acc
+             | _ ->
+                 acc ) )
+    loop_nodes InvalidatedVars.empty
+
+
 (* If there is a call to an impure function in the loop, invalidate
    all its non-primitive arguments. Once invalidated, it should be
    never added again. *)
 let get_invalidated_vars_in_loop tenv loop_head ~is_inv_by_default loop_nodes =
+  let all_modified = lazy (all_modified loop_nodes) in
   LoopNodes.fold
     (fun node acc ->
       Procdesc.Node.get_instrs node
@@ -167,8 +181,15 @@ let get_invalidated_vars_in_loop tenv loop_head ~is_inv_by_default loop_nodes =
                  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) )
+                     let acc' =
+                       get_vars_to_invalidate node loop_head args modified_params
+                         (InvalidatedVars.add (Var.of_id id) acc)
+                     in
+                     (* if one of the callees modifies a global static
+                        variable, invalidate all the function calls *)
+                     if PurityDomain.contains_global modified_params then
+                       InvalidatedVars.union acc' (force all_modified)
+                     else acc' )
              | _ ->
                  acc ) )
     loop_nodes InvalidatedVars.empty

infer/src/checkers/purity.ml

@@ -38,7 +38,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
      it modifies *)
   let track_modified_params formals ae =
     let base_var, _ = HilExp.AccessExpression.get_base ae in
-    let modified_params = get_modified_params formals ~f:(Var.equal base_var) in
+    (* treat writes to global (static) variables separately since they
+       are not considered to be explicit parameters. *)
+    let modified_params =
+      if Var.is_global base_var then Domain.ModifiedParamIndices.singleton Domain.global
+      else get_modified_params formals ~f:(Var.equal base_var)
+    in
     Domain.impure modified_params
 
 
@@ -78,9 +83,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           else modified_acc )
         callee_args
     in
-    (* find the respective parameter of the proc, matching the modified vars *)
-    get_modified_params formals ~f:(fun formal_var ->
-        ModifiedVarSet.mem formal_var vars_of_modified_args )
+    (* find the respective parameter of the caller, matching the modified vars *)
+    let caller_modified_params =
+      get_modified_params formals ~f:(fun formal_var ->
+          ModifiedVarSet.mem formal_var vars_of_modified_args )
+    in
+    (* if callee modified global, caller also indirectly does so*)
+    if Domain.contains_global callee_modified_params then
+      Domain.ModifiedParamIndices.add Domain.global caller_modified_params
+    else caller_modified_params
 
 
   (* if the callee is impure, find the parameters that have been modified by the callee *)

infer/src/checkers/purityDomain.ml

@@ -10,6 +10,10 @@ module ModifiedParamIndices = AbstractDomain.FiniteSet (Int)
 module Domain = AbstractDomain.BottomLifted (ModifiedParamIndices)
 include Domain
 
+let global = -1
+
+let contains_global modified_params = ModifiedParamIndices.mem global modified_params
+
 let pure = AbstractDomain.Types.Bottom
 
 let is_pure = Domain.is_empty

infer/tests/codetoanalyze/java/hoisting/HoistGlobal.java

@@ -0,0 +1,41 @@
+/*
+ * 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 HoistGlobal {
+
+  public static int svar = 0;
+
+  int read_global() {
+    return svar;
+  }
+
+  class Foo {
+    void set() {
+      svar = 5;
+    }
+
+    int read_global() {
+      return svar;
+    }
+  }
+
+  int global_modification_dont_hoist(int size) {
+    Foo f = new Foo();
+    int d = 0;
+    for (int i = 0; i < size; i++) {
+      d += read_global(); // don't hoist since set() changes a global var in the loop
+      f.set();
+      f.read_global(); // don't hoist
+    }
+    return d;
+  }
+
+  void call_global_modification_dont_hoist(int size) {
+    for (int i = 0; i < size; i++) {
+      global_modification_dont_hoist(size);
+    }
+  }
+}

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

@@ -8,12 +8,12 @@
 class HoistIndirect {
 
   public static int svar = 0;
+  public int x = 0;
   int[] array;
 
   class Test {
 
     int a = 0;
-
     int[] test_array;
 
     int foo(int x) {
@@ -48,9 +48,7 @@ class HoistIndirect {
     void variant_arg_dont_hoist(int size, Test t) {
       for (int i = 0; i < size; i++) {
         set_test(t); // t is invalidated
-        get_sum_test(
-            return_only(t),
-            size); // foo' and return_only's arguments are variant, hence don't hoist
+        get_sum_test(return_only(t), size); // return_only's argument is variant, hence don't hoist
       }
     }
 
@@ -70,8 +68,8 @@ class HoistIndirect {
       int d = 0;
       Test t = new Test();
       for (int i = 0; i < size; i++) {
-        set_test(t); // this (and t) is invalidated here
-        d = foo(3); // foo becomes variant due to implicit arg. this being invalidated above
+        set_test(t); // t is invalidated here
+        d = foo(3); // foo is still invariant so it is ok to hoist
       }
       return d;
     }
@@ -99,8 +97,8 @@ class HoistIndirect {
     return svar;
   }
 
-  // can't deal with static variables yet because they don't appear as parameters
-  int indirect_this_modification_dont_hoist_FP(int size) {
+  //
+  int indirect_this_modification_dont_hoist(int size) {
     int d = 0;
 
     for (int i = 0; i < size; i++) {
@@ -238,4 +236,26 @@ class HoistIndirect {
       get_ith(0, arr); // don't hoist
     }
   }
+
+  int return_zero() {
+    return 0;
+  }
+
+  void set_x() {
+    x = 0;
+  }
+
+  // Since we don't keep track of what values are read in purity
+  // analysis, when we call set_x, we add implicit arg. "this" to
+  // modified arguments which prevents any other call in the loop to
+  // be hoisted
+  int indirect_this_modification_hoist_FN(int size) {
+    int d = 0;
+
+    for (int i = 0; i < size; i++) {
+      d = return_zero(); // OK to hoist
+      set_x();
+    }
+    return d;
+  }
 }

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

@@ -8,16 +8,15 @@ codetoanalyze/java/hoisting/Hoist.java, Hoist.two_function_call_hoist(int):void,
 codetoanalyze/java/hoisting/Hoist.java, Hoist.two_function_call_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.bar(int) at line 35 is loop-invariant]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.used_in_loop_body_before_def_temp_hoist(int,int[]):void, 6, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 57 is loop-invariant]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.void_hoist(int):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to void Hoist.dumb_foo() at line 183 is loop-invariant]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.indirect_modification_hoist(int):int, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect$Test.foo(int) at line 74 is loop-invariant]
-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, [The call to int HoistIndirect$Test.get_test(HoistIndirect$Test) at line 88 is loop-invariant]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.alias_dont_hoist_FP(int[]):void, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get_ith(int,int[]) at line 238 is loop-invariant]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.arg_modification_hoist(int,HoistIndirect$Test):int, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get() at line 135 is loop-invariant]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.direct_this_modification_dont_hoist_FP(int):int, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get() at line 117 is loop-invariant]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.independent_hoist(int,HoistIndirect$Test):int, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect$Test.foo(int) at line 162 is loop-invariant]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.indirect_this_modification_dont_hoist_FP(int):int, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get() at line 107 is loop-invariant]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.irvar_independent_hoist(int[][],int,int[]):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.double_me(int) at line 212 is loop-invariant]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.this_modification_outside_hoist(int):int, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get() at line 127 is loop-invariant]
-codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.unmodified_arg_hoist(int[][],int,int[]):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.regionFirst(int[]) at line 222 is loop-invariant]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect$Test.indirect_modification_hoist(int):int, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect$Test.foo(int) at line 72 is loop-invariant]
+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, [The call to int HoistIndirect$Test.get_test(HoistIndirect$Test) at line 86 is loop-invariant]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.alias_dont_hoist_FP(int[]):void, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get_ith(int,int[]) at line 236 is loop-invariant]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.arg_modification_hoist(int,HoistIndirect$Test):int, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get() at line 133 is loop-invariant]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.direct_this_modification_dont_hoist_FP(int):int, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get() at line 115 is loop-invariant]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.independent_hoist(int,HoistIndirect$Test):int, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect$Test.foo(int) at line 160 is loop-invariant]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.irvar_independent_hoist(int[][],int,int[]):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.double_me(int) at line 210 is loop-invariant]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.this_modification_outside_hoist(int):int, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.get() at line 125 is loop-invariant]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.unmodified_arg_hoist(int[][],int,int[]):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistIndirect.regionFirst(int[]) at line 220 is loop-invariant]
 codetoanalyze/java/hoisting/HoistInvalidate.java, HoistInvalidate.loop_indirect_hoist(java.util.ArrayList,int,int[]):void, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistInvalidate.get_length(int[]) at line 52 is loop-invariant]
 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, LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to Object JsonDeserializer.deserialize(JsonParser,DeserializationContext) at line 33 is loop-invariant]
 codetoanalyze/java/hoisting/HoistModeled.java, HoistModeled.list_contains_hoist(java.util.List,java.lang.String):int, 3, LOOP_INVARIANT_CALL, no_bucket, ERROR, [The call to String String.substring(int,int) at line 18 is loop-invariant]

infer/tests/codetoanalyze/java/purity/GlobalTest.java

@@ -0,0 +1,23 @@
+/*
+ * 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 GlobalTest {
+  public static int s = 0;
+
+  class Foo {
+
+    // modifies global var 's' hence impure
+    void set_bad() {
+      s = 10;
+    }
+  }
+
+  // calls foo which modifies global var
+  void call_set_bad() {
+    Foo f = new Foo();
+    f.set_bad();
+  }
+}