[purity] Mark unmodeled functions as modifying global state

Reviewed By: mbouaziz

Differential Revision: D13941653

fbshipit-source-id: 02a15b29c

infer/src/checkers/loopInvariant.ml

@@ -23,12 +23,16 @@ let is_defined_outside loop_nodes reaching_defs var =
   |> Option.value ~default:true
 
 
+let is_not_modeled tenv callee_pname =
+  match Models.ProcName.dispatch tenv callee_pname with Some _ -> false | None -> true
+
+
 let get_purity tenv ~is_inv_by_default callee_pname args =
   (* Take into account purity behavior of modeled functions *)
-  let all_params_modified = PurityDomain.all_params_modified args in
   match Models.ProcName.dispatch tenv callee_pname with
   | Some inv ->
-      PurityDomain.with_purity (InvariantModels.is_invariant inv) all_params_modified
+      PurityDomain.(
+        if InvariantModels.is_invariant inv then pure else impure_params (all_params_modified args))
   | None -> (
       debug "No model for %a \n" Typ.Procname.pp callee_pname ;
       (* If there is no model, invoke purity analysis to see if function is pure *)
@@ -36,7 +40,7 @@ let get_purity tenv ~is_inv_by_default callee_pname args =
       | Some {Summary.payloads= {Payloads.purity= Some purity_summary}} ->
           purity_summary
       | _ ->
-          PurityDomain.with_purity is_inv_by_default all_params_modified )
+          if is_inv_by_default then PurityDomain.pure else PurityDomain.impure_global )
 
 
 let is_non_primitive typ = Typ.is_pointer typ || Typ.is_struct typ
@@ -154,13 +158,14 @@ let get_vars_to_invalidate node loop_head args modified_params invalidated_vars
     args
 
 
-let all_modified loop_nodes =
+let all_unmodeled_modified tenv 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, _), _, _, _, _) ->
+             | Sil.Call ((id, _), Const (Cfun callee_pname), _, _, _)
+               when is_not_modeled tenv callee_pname ->
                  InvalidatedVars.add (Var.of_id id) acc
              | _ ->
                  acc ) )
@@ -171,7 +176,7 @@ let all_modified loop_nodes =
    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
+  let all_unmodeled_modified = lazy (all_unmodeled_modified tenv loop_nodes) in
   LoopNodes.fold
     (fun node acc ->
       Procdesc.Node.get_instrs node
@@ -184,10 +189,11 @@ let get_invalidated_vars_in_loop tenv loop_head ~is_inv_by_default loop_nodes =
                    | AbstractDomain.Types.Top ->
                        (* modified global *)
                        (* if one of the callees modifies a global static
-                          variable, invalidate all the function calls *)
+                          variable, invalidate all unmodeled function calls *)
-                       InvalidatedVars.union acc (force all_modified)
+                       InvalidatedVars.union acc (force all_unmodeled_modified)
                    | AbstractDomain.Types.NonTop modified_params ->
-                       if ModifiedParamIndices.is_empty modified_params then (*pure*) acc
+                       if ModifiedParamIndices.is_empty modified_params then (*pure*)
+                         acc
                        else
                          get_vars_to_invalidate node loop_head args modified_params
                            (InvalidatedVars.add (Var.of_id id) acc)) )

infer/src/checkers/purity.ml

@@ -143,22 +143,22 @@ module TransferFunctions = struct
     | Assign (ae, _, _) when is_heap_access ae ->
         track_modified_params inferbo_mem formals ae |> Domain.join astate
     | Call (_, Direct called_pname, args, _, _) ->
-        let matching_modified =
-          lazy
-            (find_params_matching_modified_args inferbo_mem formals args
-               (Domain.all_params_modified args))
-        in
         Domain.join astate
           ( match InvariantModels.ProcName.dispatch tenv called_pname with
           | Some inv ->
-              Domain.with_purity (InvariantModels.is_invariant inv) (Lazy.force matching_modified)
+              if InvariantModels.is_invariant inv then Domain.pure
+              else
+                find_params_matching_modified_args inferbo_mem formals args
+                  (Domain.all_params_modified args)
+                |> Domain.impure_params
           | None -> (
             match Payload.read pdesc called_pname with
             | Some summary ->
                 debug "Reading from %a \n" Typ.Procname.pp called_pname ;
                 find_modified_if_impure inferbo_mem formals args summary
             | None ->
-                Domain.impure_params (Lazy.force matching_modified) ) )
+                if Typ.Procname.is_constructor called_pname then Domain.pure
+                else Domain.impure_global ) )
     | Call (_, Indirect _, _, _, _) ->
         (* This should never happen in Java. Fail if it does. *)
         L.(die InternalError) "Unexpected indirect call %a" HilInstr.pp instr

infer/src/checkers/purityDomain.ml

@@ -24,8 +24,6 @@ let is_pure astate =
 
 let impure_params modified_params = AbstractDomain.Types.NonTop modified_params
 
-let with_purity is_pure modified_params = if is_pure then pure else impure_params modified_params
-
 let all_params_modified args =
   List.foldi ~init:ModifiedParamIndices.empty
     ~f:(fun i acc _ -> ModifiedParamIndices.add i acc)

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

@@ -4,6 +4,8 @@
  * This source code is licensed under the MIT license found in the
  * LICENSE file in the root directory of this source tree.
  */
+import java.util.ArrayList;
+
 class HoistGlobal {
 
   public static int svar = 0;
@@ -12,6 +14,10 @@ class HoistGlobal {
     return svar;
   }
 
+  int return_one() {
+    return 1;
+  }
+
   class Foo {
     void set() {
       svar = 5;
@@ -20,6 +26,10 @@ class HoistGlobal {
     int read_global() {
       return svar;
     }
+
+    int return_zero() {
+      return 0;
+    }
   }
 
   int global_modification_dont_hoist(int size) {
@@ -33,6 +43,17 @@ class HoistGlobal {
     return d;
   }
 
+  int global_modification_hoist_FN(ArrayList<?> list) {
+    Foo f = new Foo();
+    int d = 0;
+    for (int i = 0; i < list.size(); i++) {
+      d += return_one(); // ok to hoist
+      f.set(); // don't invalidate size()
+      f.return_zero(); // ok to hoist since doesn't read global
+    }
+    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/HoistUnmodeled.java

@@ -0,0 +1,29 @@
+/*
+ * Copyright (c) 2019-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 HoistUnmodeled {
+
+  // Any unmodeled (e.g. timing) call is assumed to be modifying global
+  // state
+  void timing_calls_dont_hoist() {
+    for (int i = 0; i < 10; i++) {
+      System.nanoTime();
+    }
+  }
+
+  // doesn't read from global state or call any unmodeled function, a
+  // harmless pure function
+  void harmless_pure() {}
+
+  // It should be ok to hoist harmless_pure() since it doesn't read
+  // from global state.
+  void harmless_hoist_FN() {
+    for (int i = 0; i < 10; i++) {
+      timing_calls_dont_hoist(); // don't hoist
+      harmless_pure(); // ok to hoist
+    }
+  }
+}

infer/tests/codetoanalyze/java/performance/UnknownCallsTest.java

@@ -55,4 +55,12 @@ class UnknownCallsTest {
   private static void call_loop_over_charArray(StringBuilder out, String in) {
     loop_over_charArray(out, in);
   }
+
+  // hashCode is impure but we don't invalidate all other library
+  // calls such as size()
+  void unmodeled_impure_linear(ArrayList<Integer> list) {
+    for (int i = 0; i < list.size(); i++) {
+      list.get(i).hashCode();
+    }
+  }
 }

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

@@ -206,3 +206,7 @@ codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 17 + 6 ⋅ (Math.min(...).ub + InputStream.read(...).ub), degree = 1]
 codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 16 + 6 ⋅ (Math.min(...).ub + InputStream.read(...).ub), degree = 1]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 15 ⋅ list.length + 4 ⋅ (list.length + 1), degree = 1]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 ⋅ list.length + 4 ⋅ (list.length + 1), degree = 1]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: __cast,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 15 ⋅ list.length + 4 ⋅ (list.length + 1), degree = 1]

infer/tests/codetoanalyze/java/purity/Test.java

@@ -84,9 +84,8 @@ class Test {
     return new ArrayList<Integer>();
   }
 
-  // All unknown calls that don't have any argument, will be marked as
+  // All unmodeled calls will be marked as modifying global state
-  // pure by default even though they may have side-effects!
+  static long systemNanoTime_bad() {
-  static long systemNanoTime_bad_FP() {
     return System.nanoTime();
   }
 }

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

@@ -3,4 +3,3 @@ codetoanalyze/java/purity/Test.java, Test.emptyList_bad_FP():java.util.ArrayList
 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)]
 codetoanalyze/java/purity/Test.java, Test.local_write_ok(int,int):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Test.local_write_ok(int,int)]
 codetoanalyze/java/purity/Test.java, Test.parameter_field_access_ok(Test):int, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function int Test.parameter_field_access_ok(Test)]
-codetoanalyze/java/purity/Test.java, Test.systemNanoTime_bad_FP():long, 0, PURE_FUNCTION, no_bucket, ERROR, [Side-effect free function long Test.systemNanoTime_bad_FP()]