[purity] Mark functions with empty modified params as pure

Reviewed By: mbouaziz, ngorogiannis

Differential Revision: D13452909

fbshipit-source-id: f0dc419b1

infer/src/checkers/purity.ml

@@ -8,6 +8,7 @@ open! IStd
 module F = Format
 module L = Logging
 module ModifiedVarSet = Caml.Set.Make (Var)
+module InstrCFG = ProcCfg.NormalOneInstrPerNode
 
 let debug fmt = L.(debug Analysis Verbose fmt)
 
@@ -21,11 +22,29 @@ module Payload = SummaryPayload.Make (struct
   let of_payloads (payloads : Payloads.t) = payloads.purity
 end)
 
-module TransferFunctions (CFG : ProcCfg.S) = struct
-  module CFG = CFG
+type purity_extras =
+  {inferbo_invariant_map: BufferOverrunChecker.invariant_map; formals: Var.t list}
+
+module TransferFunctions = struct
+  module CFG = ProcCfg.Normal
   module Domain = PurityDomain
 
-  type extras = Var.t list
+  type extras = purity_extras
+
+  let get_alias_set inferbo_mem var =
+    let default = ModifiedVarSet.empty in
+    let alias_v = BufferOverrunDomain.Mem.find (AbsLoc.Loc.of_var var) inferbo_mem in
+    let pow_locs = BufferOverrunDomain.Val.get_pow_loc alias_v in
+    AbsLoc.PowLoc.fold
+      (fun loc modified_acc ->
+        AbsLoc.Loc.get_path loc
+        |> Option.value_map ~default:modified_acc ~f:(fun path ->
+               Symb.SymbolPath.get_pvar path
+               |> Option.value_map ~default:modified_acc ~f:(fun pvar ->
+                      debug "Add alias of %a -> %a " Var.pp var (Pvar.pp Pp.text) pvar ;
+                      ModifiedVarSet.add (Var.of_pvar pvar) modified_acc ) ) )
+      pow_locs default
+
 
   let get_modified_params formals ~f =
     List.foldi ~init:Domain.ModifiedParamIndices.empty
@@ -36,13 +55,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
   (* given a heap access to ae, find which parameter indices of pdesc
      it modifies *)
-  let track_modified_params formals ae =
+  let track_modified_params inferbo_mem formals ae =
     let base_var, _ = HilExp.AccessExpression.get_base ae 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)
+      else
+        get_modified_params formals ~f:(fun var ->
+            Var.equal var base_var || ModifiedVarSet.mem var (get_alias_set inferbo_mem base_var)
+        )
     in
     Domain.impure modified_params
 
@@ -71,7 +93,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         }
      }
   *)
-  let find_params_matching_modified_args formals callee_args callee_modified_params =
+  let find_params_matching_modified_args inferbo_mem formals callee_args callee_modified_params =
     let vars_of_modified_args =
       List.foldi ~init:ModifiedVarSet.empty
         ~f:(fun i modified_acc arg_exp ->
@@ -79,7 +101,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             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 (HilExp.AccessExpression.get_base ae |> fst) modified_acc ) )
+                   let base_var, typ = HilExp.AccessExpression.get_base ae in
+                   let modified_acc' =
+                     if Typ.is_pointer typ then ModifiedVarSet.add base_var modified_acc
+                     else modified_acc
+                   in
+                   get_alias_set inferbo_mem base_var |> ModifiedVarSet.union modified_acc' ) )
           else modified_acc )
         callee_args
     in
@@ -95,23 +122,32 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
 
 
   (* if the callee is impure, find the parameters that have been modified by the callee *)
-  let find_modified_if_impure formals args callee_summary =
+  let find_modified_if_impure inferbo_mem 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)
+        Domain.impure
+          (find_params_matching_modified_args inferbo_mem formals args callee_modified_params)
     | None ->
         Domain.pure
 
 
-  let exec_instr (astate : Domain.t) {ProcData.pdesc; tenv; ProcData.extras= formals} _
+  let exec_instr (astate : Domain.t)
+      {ProcData.pdesc; tenv; ProcData.extras= {inferbo_invariant_map; formals}} (node : CFG.Node.t)
       (instr : HilInstr.t) =
+    let (node_id : InstrCFG.Node.id) =
+      CFG.Node.underlying_node node |> InstrCFG.last_of_underlying_node |> InstrCFG.Node.id
+    in
+    let inferbo_mem =
+      Option.value_exn (BufferOverrunChecker.extract_post node_id inferbo_invariant_map)
+    in
     match instr with
     | Assign (ae, _, _) when is_heap_access ae ->
-        track_modified_params formals ae |> Domain.join astate
+        track_modified_params inferbo_mem formals ae |> Domain.join astate
     | Call (_, Direct called_pname, args, _, _) ->
         let matching_modified =
-          find_params_matching_modified_args formals args (Domain.all_params_modified args)
+          find_params_matching_modified_args inferbo_mem formals args
+            (Domain.all_params_modified args)
         in
         Domain.join astate
           ( match InvariantModels.Call.dispatch tenv called_pname [] with
@@ -121,7 +157,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               Payload.read pdesc called_pname
               |> Option.value_map ~default:(Domain.impure matching_modified) ~f:(fun summary ->
                      debug "Reading from %a \n" Typ.Procname.pp called_pname ;
-                     find_modified_if_impure formals args summary ) )
+                     find_modified_if_impure inferbo_mem 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
@@ -132,7 +168,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let pp_session_name _node fmt = F.pp_print_string fmt "purity checker"
 end
 
-module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Normal))
+module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions)
 
 let should_report pdesc =
   (not Config.loop_hoisting)
@@ -146,13 +182,16 @@ let should_report pdesc =
       L.(die InternalError "Not supposed to run on non-Java code.")
 
 
-let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
+let checker ({Callbacks.tenv; summary; proc_desc} as callback_args) : Summary.t =
   let proc_name = Procdesc.get_proc_name proc_desc in
+  let inferbo_invariant_map, _ =
+    BufferOverrunChecker.compute_invariant_map_and_check callback_args
+  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 proc_data = ProcData.make proc_desc tenv {inferbo_invariant_map; 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
@@ -161,13 +200,16 @@ let checker {Callbacks.tenv; summary; proc_desc} : Summary.t =
   in
   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
+      let astate' =
+        PurityDomain.get_modified_params astate
+        |> Option.value_map ~default:astate ~f:(fun modified_params ->
+               debug "Modified parameter indices of %a: %a \n" Typ.Procname.pp proc_name
+                 PurityDomain.ModifiedParamIndices.pp modified_params ;
+               if PurityDomain.ModifiedParamIndices.is_empty modified_params then PurityDomain.pure
+               else astate )
+      in
+      if should_report proc_desc && PurityDomain.is_pure astate' 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/tests/codetoanalyze/java/hoisting/HoistIndirect.java

@@ -230,7 +230,7 @@ class HoistIndirect {
     new_arr[0] = 4;
   }
 
-  void alias_dont_hoist_FP(int[] arr) {
+  void alias_dont_hoist(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/HoistNoIndirectMod.java

@@ -4,6 +4,7 @@
  * 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 HoistNoIndirectMod {
 
@@ -37,4 +38,43 @@ class HoistNoIndirectMod {
     }
     return p;
   }
+
+  // modifies list indirectly via aliasing
+  public void set_first_to_zero(ArrayList<Integer> list) {
+    ArrayList<Integer> l = list;
+    if (l != null) {
+      l.set(0, 0);
+    }
+  }
+
+  public void call_set_first_to_zero(ArrayList<Integer> list) {
+    set_first_to_zero(list);
+  }
+
+  public void alias_call_set_first_to_zero(ArrayList<Integer> list) {
+    ArrayList<Integer> l = list;
+    set_first_to_zero(l);
+  }
+
+  public void indirect_mod_dont_hoist(Integer[] array, ArrayList<Integer> list) {
+    for (Integer element : array) {
+      set_first_to_zero(list);
+      call_set_first_to_zero(list);
+      alias_call_set_first_to_zero(list);
+    }
+  }
+
+  int avg(ArrayList<Integer> list) {
+    int sum = 0;
+    for (Integer element : list) {
+      sum += element;
+    }
+    return sum;
+  }
+
+  public void no_mod_hoist(Integer[] array, ArrayList<Integer> list) {
+    for (Integer element : array) {
+      avg(list);
+    }
+  }
 }

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

@@ -1,25 +1,41 @@
 codetoanalyze/java/hoisting/Hoist.java, Hoist.array_store_hoist(int,int[]):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 117 is loop-invariant]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.clash_function_calls_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 26 is loop-invariant]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.legit_hoist(int,int[]):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 73 is loop-invariant]
+codetoanalyze/java/hoisting/Hoist.java, Hoist.loop_guard_hoist(int,int[]):void, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.loop_guard_hoist(int,int[]):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 65 is loop-invariant]
+codetoanalyze/java/hoisting/Hoist.java, Hoist.nested_loop_hoist(int,int,int):void, 4, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.nested_loop_hoist(int,int,int):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 127 is loop-invariant]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.reassigned_temp_hoist(int):void, 5, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 45 is loop-invariant]
 codetoanalyze/java/hoisting/Hoist.java, Hoist.two_function_call_hoist(int):void, 4, INVARIANT_CALL, no_bucket, ERROR, [The call to int Hoist.foo(int,int) at line 35 is loop-invariant]
 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/Hoist.java, Hoist.x_not_invariant_dont_hoist(int,int,int):void, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: int Hoist.foo(int,int),Assignment,<RHS trace>,Parameter `y`,Binary operation: ([-oo, +oo] + y):signed32]
+codetoanalyze/java/hoisting/HoistGlobal.java, HoistGlobal.global_modification_dont_hoist(int):int, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int HoistGlobal.read_global(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
 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, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int HoistIndirect.get(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
 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, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int HoistIndirect.get(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
 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.independent_hoist(int,HoistIndirect$Test):int, 5, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int HoistIndirect.get_ith(int,int[]),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.irvar_independent_hoist(int[][],int,int[]):void, 2, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: int HoistIndirect.regionFirst(int[]),Assignment,<RHS trace>,Unknown value from: int HoistIndirect.double_me(int),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
 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.modified_array_dont_hoist(int,HoistIndirect$Test):int, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int HoistIndirect.get_ith(int,int[]),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.modified_inner_array_dont_hoist(int,HoistIndirect$Test):int, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int HoistIndirect$Test.foo(int),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
+codetoanalyze/java/hoisting/HoistIndirect.java, HoistIndirect.this_modification_outside_hoist(int):int, 4, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int HoistIndirect.get(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
 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, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Unknown value from: int HoistIndirect.regionFirst(int[]),Assignment,<RHS trace>,Unknown value from: int HoistIndirect.regionFirst(int[]),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
 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]
 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 boolean List.contains(Object) at line 18 is loop-invariant]
-codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.increment_dont_hoist_FP(int):int, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistNoIndirectMod.calcNext() at line 27 is loop-invariant]
-codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.modify_and_increment_dont_hoist_FP(int):int, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistNoIndirectMod.calcNext() at line 35 is loop-invariant]
+codetoanalyze/java/hoisting/HoistModeled.java, HoistModeled.list_contains_hoist(java.util.List,java.lang.String):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
+codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.avg(java.util.ArrayList):int, 3, BUFFER_OVERRUN_U5, no_bucket, ERROR, [<Length trace>,Unknown value from: __cast,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]
+codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.avg(java.util.ArrayList):int, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int Integer.intValue(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
+codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.increment_dont_hoist_FP(int):int, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistNoIndirectMod.calcNext() at line 28 is loop-invariant]
+codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.modify_and_increment_dont_hoist_FP(int):int, 3, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Unknown value from: int HoistNoIndirectMod.calcNext(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32]
+codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.modify_and_increment_dont_hoist_FP(int):int, 3, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistNoIndirectMod.calcNext() at line 36 is loop-invariant]
+codetoanalyze/java/hoisting/HoistNoIndirectMod.java, HoistNoIndirectMod.no_mod_hoist(java.lang.Integer[],java.util.ArrayList):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to int HoistNoIndirectMod.avg(ArrayList) at line 77 is loop-invariant]

infer/tests/codetoanalyze/java/hoistingExpensive/HoistExpensive.java

@@ -4,6 +4,7 @@
  * 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 HoistExpensive {
 
@@ -32,4 +33,19 @@ class HoistExpensive {
       cheap_dont_hoist(1);
     }
   }
+
+  // incr will not be hoisted since it is cheap
+  void cheap_iterator_dont_hoist(ArrayList<Integer> list) {
+    int x = 0;
+    for (Integer elem : list) {
+      incr(x);
+    }
+  }
+
+  // call to cheap_iterator_dont_hoist will be hoisted since it is expensive.
+  void symbolic_expensive_iterator_hoist(int size, ArrayList<Integer> list) {
+    for (int i = 0; i < size; i++) {
+      cheap_iterator_dont_hoist(list);
+    }
+  }
 }

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

@@ -1 +1,2 @@
-codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_hoist(int):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistExpensive.cheap_dont_hoist(int) at line 25 is loop-invariant]
+codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_hoist(int):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistExpensive.cheap_dont_hoist(int) at line 26 is loop-invariant]
+codetoanalyze/java/hoistingExpensive/HoistExpensive.java, HoistExpensive.symbolic_expensive_iterator_hoist(int,java.util.ArrayList):void, 2, INVARIANT_CALL, no_bucket, ERROR, [The call to void HoistExpensive.cheap_iterator_dont_hoist(ArrayList) at line 48 is loop-invariant]

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

@@ -42,8 +42,8 @@ class Test {
     }
   }
 
-  // as soon as we allocate with new, function is marked impure.
-  int local_alloc_bad_FP(int x, int y) {
+  // no change to outside state, the local allocation is ok.
+  int local_alloc_ok(int x, int y) {
     ArrayList<Integer> list = new ArrayList<Integer>(x + y);
     for (Integer el : list) {
       call_pure_ok(el);
@@ -71,4 +71,22 @@ class Test {
     array[i] = array[j];
     array[j] = tmp;
   }
+
+  void alias_bad(int[] array, int i, int j) {
+    int[] a = array;
+    a[j] = i;
+  }
+
+  // Currently, we can't distinguish between returning new Objects or
+  // creating new Objects locally. Ideally, the latter should be fine
+  // as long as it doesn't leak to the result.
+  public ArrayList<Integer> emptyList_bad_FP() {
+    return new ArrayList<Integer>();
+  }
+
+  // All unknown calls that don't have any argument, will be marked as
+  // pure by default even though they may have side-effects!
+  static long systemNanoTime_bad_FP() {
+    return System.nanoTime();
+  }
 }

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

@@ -1,3 +1,8 @@
 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)]
+codetoanalyze/java/purity/Test.java, Test.local_alloc_ok(int,int):int, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
+codetoanalyze/java/purity/Test.java, Test.local_alloc_ok(int,int):int, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 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()]