[inferbo] Add model for load of java.util.Collections.EMPTY_*

Reviewed By: skcho

Differential Revision: D19092281

fbshipit-source-id: c22fc96a7

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -238,6 +238,18 @@ module TransferFunctions = struct
               mem )
 
 
+  let modeled_load_of_empty_collection_opt =
+    let known_empty_collections = String.Set.of_list ["EMPTY_LIST"; "EMPTY_SET"; "EMPTY_MAP"] in
+    fun exp model_env ret mem ->
+      match exp with
+      | Exp.Lfield (_, fieldname, typ)
+        when String.Set.mem known_empty_collections (Typ.Fieldname.get_field_name fieldname)
+             && String.equal "java.util.Collections" (Typ.to_string typ) ->
+          Models.Collection.create_collection model_env ~ret mem ~length:Itv.zero |> Option.some
+      | _ ->
+          None
+
+
   let modeled_range_of_exp location exp mem =
     match exp with
     | Exp.Lindex (arr_exp, _) ->
@@ -272,16 +284,25 @@ module TransferFunctions = struct
           L.d_printfln_escaped "/!\\ Failed to get initializer name of global constant %a"
             (Pvar.pp Pp.text) pvar ;
           Dom.Mem.add_unknown id ~location mem )
-    | Load {id; e= exp; typ; loc= location} ->
+    | Load {id; e= exp; typ; loc= location} -> (
-        let mem =
+        let model_env =
-          if Language.curr_language_is Java then
+          let pname = Summary.get_proc_name summary in
-            join_java_static_final tenv get_proc_summary_and_formals exp mem
+          let node_hash = CFG.Node.hash node in
-          else mem
+          BoUtils.ModelEnv.mk_model_env pname ~node_hash location tenv integer_type_widths
         in
-        let represents_multiple_values = is_array_access_exp exp in
+        match modeled_load_of_empty_collection_opt exp model_env (id, typ) mem with
-        let modeled_range = modeled_range_of_exp location exp mem in
+        | Some mem' ->
-        BoUtils.Exec.load_locs ~represents_multiple_values ~modeled_range id typ
+            mem'
-          (Sem.eval_locs exp mem) mem
+        | None ->
+            let mem =
+              if Language.curr_language_is Java then
+                join_java_static_final tenv get_proc_summary_and_formals exp mem
+              else mem
+            in
+            let represents_multiple_values = is_array_access_exp exp in
+            let modeled_range = modeled_range_of_exp location exp mem in
+            BoUtils.Exec.load_locs ~represents_multiple_values ~modeled_range id typ
+              (Sem.eval_locs exp mem) mem )
     | Store {e2= Exn _} when Language.curr_language_is Java ->
         Dom.Mem.exc_raised
     | Store {e1= tgt_exp; e2= Const (Const.Cstr _) as src; loc= location}

infer/tests/codetoanalyze/java/performance/CollectionsTest.java

@@ -73,4 +73,8 @@ class CollectionsTest {
   void singletonMap_constant() {
     for (int i = 0; i < Collections.singletonMap(1, 1).size(); i++) {}
   }
+
+  void globalEmptyList_constant() {
+    for (int i = 0; i < java.util.Collections.EMPTY_LIST.size(); i++) {}
+  }
 }

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

@@ -76,6 +76,7 @@ codetoanalyze/java/performance/CollectionsTest.java, CollectionsTest.copy_linear
 codetoanalyze/java/performance/CollectionsTest.java, CollectionsTest.emptyList_constant():void, 1, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/java/performance/CollectionsTest.java, CollectionsTest.emptySet_zero():void, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/java/performance/CollectionsTest.java, CollectionsTest.fill_linear(java.util.List,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + list.length, O(list.length), degree = 1,{list.length},Modeled call to Collections.fill]
+codetoanalyze/java/performance/CollectionsTest.java, CollectionsTest.globalEmptyList_constant():void, 1, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/java/performance/CollectionsTest.java, CollectionsTest.reverse_linear(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + list.length, O(list.length), degree = 1,{list.length},Modeled call to Collections.reverse]
 codetoanalyze/java/performance/CollectionsTest.java, CollectionsTest.shuffle_linear(java.util.List,java.util.Random):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + list.length, O(list.length), degree = 1,{list.length},Modeled call to Collections.shuffle]
 codetoanalyze/java/performance/CollectionsTest.java, CollectionsTest.unmodifiable_linear(java.util.List):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 53,{list.length},Loop at line 53]