[cost,purity] Model java's Map as Collections

Reviewed By: jeremydubreil, mbouaziz

Differential Revision: D14935325

fbshipit-source-id: 798feb68e

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -713,6 +713,18 @@ module Collection = struct
     {exec; check= no_check}
 
 
+  (** increase the size by [0, |collection_to_add|] because put replaces the value
+     rather than add a new one when the key is found in the map *)
+  let putAll coll_id coll_to_add =
+    let exec model_env ~ret mem =
+      let to_add_length =
+        eval_collection_length coll_to_add mem |> Dom.Val.get_itv |> Itv.set_lb_zero
+      in
+      change_size_by ~size_f:(Itv.plus to_add_length) coll_id model_env ~ret mem
+    in
+    {exec; check= no_check}
+
+
   let check_index ~last_included coll_id index_exp {location; integer_type_widths} mem cond_set =
     let arr =
       let arr_locs = get_collection_internal_array_locs coll_id mem in
@@ -782,6 +794,9 @@ module Call = struct
       ; -"__new"
         <>$ capt_exp_of_typ (+PatternMatch.implements_collection)
         $+...$--> Collection.new_collection
+      ; -"__new"
+        <>$ capt_exp_of_typ (+PatternMatch.implements_map)
+        $+...$--> Collection.new_collection
       ; -"__new" <>$ capt_exp $+...$--> malloc ~can_be_zero:true
       ; -"__new_array" <>$ capt_exp $+...$--> malloc ~can_be_zero:true
       ; -"__placement_new" <>$ capt_exp $+ capt_arg $+? capt_arg $!--> placement_new
@@ -876,11 +891,19 @@ module Call = struct
         &:: "add" <>$ capt_var_exn $+ capt_exp $+ any_arg $!--> Collection.add_at_index
       ; +PatternMatch.implements_lang "Iterable"
         &:: "iterator" <>$ capt_exp $!--> Collection.iterator
+      ; +PatternMatch.implements_map &:: "entrySet" <>$ capt_exp $!--> Collection.iterator
+      ; +PatternMatch.implements_map &:: "keySet" <>$ capt_exp $!--> Collection.iterator
+      ; +PatternMatch.implements_map &:: "values" <>$ capt_exp $!--> Collection.iterator
+      ; +PatternMatch.implements_map &:: "put" <>$ capt_var_exn $+ any_arg $+ any_arg
+        $--> Collection.put
+      ; +PatternMatch.implements_map &:: "putAll" <>$ capt_var_exn $+ capt_exp
+        $--> Collection.putAll
       ; +PatternMatch.implements_iterator &:: "hasNext" <>$ capt_exp $!--> Collection.hasNext
       ; +PatternMatch.implements_collection
         &:: "addAll" <>$ capt_var_exn $+ capt_exp $--> Collection.addAll
       ; +PatternMatch.implements_collection
         &:: "addAll" <>$ capt_var_exn $+ capt_exp $+ capt_exp $!--> Collection.addAll_at_index
       ; +PatternMatch.implements_collection &:: "size" <>$ capt_exp $!--> Collection.size
-      ; +PatternMatch.implements_pseudo_collection &:: "size" <>$ capt_exp $!--> Collection.size ]
+      ; +PatternMatch.implements_pseudo_collection &:: "size" <>$ capt_exp $!--> Collection.size
+      ; +PatternMatch.implements_map &:: "size" <>$ capt_exp $!--> Collection.size ]
 end

infer/src/checkers/invariantModels.ml

@@ -54,6 +54,7 @@ module ProcName = struct
       ; +PatternMatch.implements_iterator &:: "next" <>--> Variant
       ; +PatternMatch.implements_iterator &:: "remove" <>--> Variant
       ; +PatternMatch.implements_collection &:: "size" <>--> Invariant
+      ; +PatternMatch.implements_map &:: "size" <>--> Invariant
       ; +PatternMatch.implements_collection &:: "add" <>--> Variant
       ; +PatternMatch.implements_collection &:: "addAll" <>--> Variant
       ; +PatternMatch.implements_collection &:: "remove" <>--> Variant

infer/tests/codetoanalyze/java/performance/MapTest.java

@@ -0,0 +1,30 @@
+/*
+ * 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.
+ */
+import java.util.HashMap;
+import java.util.Map;
+
+class MapTest {
+
+  public void keySet_linear(Map<String, Integer> map) {
+    for (String name : map.keySet()) {}
+  }
+
+  public void entrySet_linear(Map<String, Integer> map) {
+    for (Map.Entry<String, Integer> entry : map.entrySet()) {}
+  }
+
+  public void values_linear(Map<String, Integer> map) {
+    map.put("hi", 0);
+    for (Integer name : map.values()) {}
+  }
+
+  public void putAll_linear(Map<String, Integer> map) {
+    Map<String, Integer> newmap = new HashMap<>();
+    newmap.putAll(map);
+    for (Integer name : newmap.values()) {}
+  }
+}

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

@@ -128,6 +128,10 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol():void, 2, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 6996, degree = 0]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol():void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([-oo, +oo] × [-oo, +oo]):signed32]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Call,<LHS trace>,Parameter `x`,Binary operation: ([0, +oo] + 1):signed32 by call to `void Loops.linear(int)` ]
+codetoanalyze/java/performance/MapTest.java, MapTest.entrySet_linear(java.util.Map):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 7 + 8 ⋅ (map.length - 1) + 3 ⋅ map.length, degree = 1,{map.length},Loop at line 17,{map.length - 1},Loop at line 17]
+codetoanalyze/java/performance/MapTest.java, MapTest.keySet_linear(java.util.Map):void, 1, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 7 + 8 ⋅ (map.length - 1) + 3 ⋅ map.length, degree = 1,{map.length},Loop at line 13,{map.length - 1},Loop at line 13]
+codetoanalyze/java/performance/MapTest.java, MapTest.putAll_linear(java.util.Map):void, 3, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 13 + 8 ⋅ (map.length - 1) + 3 ⋅ map.length, degree = 1,{map.length},Loop at line 28,{map.length - 1},Loop at line 28]
+codetoanalyze/java/performance/MapTest.java, MapTest.values_linear(java.util.Map):void, 2, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 13 + 8 ⋅ map.length + 3 ⋅ (map.length + 1), degree = 1,{map.length + 1},Loop at line 22,{map.length},Loop at line 22]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.test_switch():int, 3, EXPENSIVE_EXECUTION_CALL, no_bucket, ERROR, [with estimated cost 798, degree = 0]
 codetoanalyze/java/performance/Switch.java, codetoanalyze.java.performance.Switch.vanilla_switch(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]