[purity] Fix global modification via argument passing

Reviewed By: mbouaziz

Differential Revision: D14208643

fbshipit-source-id: ddb3d435c

infer/src/checkers/purity.ml

@@ -7,7 +7,7 @@
 open! IStd
 module F = Format
 module L = Logging
-module ModifiedVarSet = Caml.Set.Make (Var)
+module ModifiedVarSet = PrettyPrintable.MakePPSet (Var)
 module InstrCFG = ProcCfg.NormalOneInstrPerNode
 
 let debug fmt = L.(debug Analysis Verbose fmt)
@@ -79,6 +79,27 @@ module TransferFunctions = struct
         false
 
 
+  exception Modified_Global
+
+  (* find all the variables occurring in the given modified argument exp,
+     unless the variable is a global (which makes all other function
+     calls impure since they may read from that modified global var ) *)
+  let get_modified_vars_unless_global inferbo_mem modified_acc modified_arg_exp =
+    debug "Argument %a is modified.\n" HilExp.pp modified_arg_exp ;
+    let ae_list = HilExp.get_access_exprs modified_arg_exp in
+    List.fold ae_list ~init:modified_acc ~f:(fun modified_acc ae ->
+        let base_var, typ = HilExp.AccessExpression.get_base ae in
+        let alias_set = get_alias_set inferbo_mem base_var in
+        debug "Alias set for %a : %a \n\n\n" Var.pp base_var ModifiedVarSet.pp alias_set ;
+        if Var.is_global base_var || ModifiedVarSet.exists Var.is_global alias_set then
+          raise Modified_Global
+        else
+          let modified_acc' =
+            if Typ.is_pointer typ then ModifiedVarSet.add base_var modified_acc else modified_acc
+          in
+          ModifiedVarSet.union modified_acc' alias_set )
+
+
   (* given the modified parameters and the args of the callee, find
      parameter indices of the current procedure that match, i.e have
      been modified by the callee. Note that index counting starts from
@@ -94,28 +115,22 @@ module TransferFunctions = struct
      }
   *)
   let find_params_matching_modified_args inferbo_mem formals callee_args callee_modified_params =
-    let vars_of_modified_args =
+    try
-      List.foldi ~init:ModifiedVarSet.empty
+      let vars_of_modified_args =
-        ~f:(fun i modified_acc arg_exp ->
+        List.foldi ~init:ModifiedVarSet.empty
-          if Domain.ModifiedParamIndices.mem i callee_modified_params then (
+          ~f:(fun i acc arg_exp ->
-            debug "Argument %a is modified.\n" HilExp.pp arg_exp ;
+            if Domain.ModifiedParamIndices.mem i callee_modified_params then
-            HilExp.get_access_exprs arg_exp
+              get_modified_vars_unless_global inferbo_mem acc arg_exp
-            |> List.fold ~init:modified_acc ~f:(fun modified_acc ae ->
+            else acc )
-                   let base_var, typ = HilExp.AccessExpression.get_base ae in
+          callee_args
-                   let modified_acc' =
+      in
-                     if Typ.is_pointer typ then ModifiedVarSet.add base_var modified_acc
+      (* find the respective parameter of the caller, matching the modified vars *)
-                     else modified_acc
+      let caller_modified_params =
-                   in
+        get_modified_params formals ~f:(fun formal_var ->
-                   get_alias_set inferbo_mem base_var |> ModifiedVarSet.union modified_acc' ) )
+            ModifiedVarSet.mem formal_var vars_of_modified_args )
-          else modified_acc )
+      in
-        callee_args
+      Domain.impure_params caller_modified_params
-    in
+    with Modified_Global -> Domain.impure_global
-    (* 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
-    caller_modified_params
 
 
   (* if the callee is impure, find the parameters that have been modified by the callee *)
@@ -127,9 +142,7 @@ module TransferFunctions = struct
         Domain.(
           debug "Callee modified params %a \n" ModifiedParamIndices.pp callee_modified_params ;
           if ModifiedParamIndices.is_empty callee_modified_params then pure
-          else
+          else find_params_matching_modified_args inferbo_mem formals args callee_modified_params)
-            impure_params
-              (find_params_matching_modified_args inferbo_mem formals args callee_modified_params))
 
 
   let exec_instr (astate : Domain.t)
@@ -152,7 +165,6 @@ module TransferFunctions = struct
               else
                 find_params_matching_modified_args inferbo_mem formals args
                   (Domain.all_params_modified args)
-                |> Domain.impure_params
           | None -> (
             match get_callee_summary called_pname with
             | Some summary ->

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

@@ -6,18 +6,40 @@
  */
 class GlobalTest {
   public static int s = 0;
+  public static Foo foo;
 
   class Foo {
 
+    int x = 0;
     // modifies global var 's' hence impure
     void set_bad() {
       s = 10;
     }
   }
 
+  void incr(Foo foo, int i) {
+    foo.x += i;
+  }
+
   // calls foo which modifies global var
   void call_set_bad() {
     Foo f = new Foo();
     f.set_bad();
   }
+
+  // foo is global which is modified by incr.
+  void global_mod_via_argument_passing_bad(int size, Foo f) {
+    for (int i = 0; i < size; i++) {
+      incr(foo, i);
+    }
+  }
+
+  // aliased_foo is aliasing a global and then is modified by incr.
+  void global_mod_via_argument_passing_bad_FP(int size, Foo f) {
+    Foo aliased_foo = foo; // Inferbo can't recognize aliasing here
+    // and assumes aliased_foo is in [-oo,+oo] not in foo
+    for (int i = 0; i < size; i++) {
+      incr(aliased_foo, i);
+    }
+  }
 }

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

@@ -1,3 +1,4 @@
+codetoanalyze/java/purity/GlobalTest.java, GlobalTest.global_mod_via_argument_passing_bad_FP(int,GlobalTest$Foo):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void GlobalTest.global_mod_via_argument_passing_bad_FP(int,GlobalTest$Foo)]
 codetoanalyze/java/purity/Test.java, Test.call_pure_ok(int):void, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function void Test.call_pure_ok(int)]
 codetoanalyze/java/purity/Test.java, Test.emptyList_bad_FP():java.util.ArrayList, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function ArrayList Test.emptyList_bad_FP()]
 codetoanalyze/java/purity/Test.java, Test.local_alloc_ok(int,int):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Test.local_alloc_ok(int,int)]