From 6d25b0990ded4399470f6977e9795f7bc7b6d389 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Tue, 16 Apr 2019 02:59:30 -0700 Subject: [PATCH] [cost,purity] Model java's Map as Collections Reviewed By: jeremydubreil, mbouaziz Differential Revision: D14935325 fbshipit-source-id: 798feb68e --- .../src/bufferoverrun/bufferOverrunModels.ml | 25 +++++++++++++++- infer/src/checkers/invariantModels.ml | 1 + .../java/performance/MapTest.java | 30 +++++++++++++++++++ .../codetoanalyze/java/performance/issues.exp | 4 +++ 4 files changed, 59 insertions(+), 1 deletion(-) create mode 100644 infer/tests/codetoanalyze/java/performance/MapTest.java diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index c00847372..f7de755cd 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/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 diff --git a/infer/src/checkers/invariantModels.ml b/infer/src/checkers/invariantModels.ml index 6d42bd9b1..02b22baf2 100644 --- a/infer/src/checkers/invariantModels.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/java/performance/MapTest.java b/infer/tests/codetoanalyze/java/performance/MapTest.java new file mode 100644 index 000000000..703d673f1 --- /dev/null +++ b/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 map) { + for (String name : map.keySet()) {} + } + + public void entrySet_linear(Map map) { + for (Map.Entry entry : map.entrySet()) {} + } + + public void values_linear(Map map) { + map.put("hi", 0); + for (Integer name : map.values()) {} + } + + public void putAll_linear(Map map) { + Map newmap = new HashMap<>(); + newmap.putAll(map); + for (Integer name : newmap.values()) {} + } +} diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 068f0f12b..f82b3f3f9 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/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, [,Assignment,,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,,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]