From 11af20ef86dad50ef0ae0415763427a3046fbc80 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Mon, 18 Feb 2019 00:58:10 -0800 Subject: [PATCH] [inferbo] Model list constructors with arguments Reviewed By: mbouaziz, ddino Differential Revision: D14083727 fbshipit-source-id: 13219330f --- .../src/bufferoverrun/bufferOverrunModels.ml | 34 ++++++++++++------- .../java/performance/ArrayListTest.java | 30 ++++++++++++++++ .../codetoanalyze/java/performance/issues.exp | 4 +++ 3 files changed, 56 insertions(+), 12 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index a694973fd..1e65fe2be 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -333,19 +333,19 @@ let variable_initialization (e, typ) = {exec; check= no_check} -let model_by_value value (id, _) mem = Dom.Mem.add_stack (Loc.of_id id) value mem +let model_by_value value id mem = Dom.Mem.add_stack (Loc.of_id id) value mem let by_value = - let exec ~value _ ~ret mem = model_by_value value ret mem in + let exec ~value _ ~ret:(ret_id, _) mem = model_by_value value ret_id mem in fun value -> {exec= exec ~value; check= no_check} let by_risky_value_from lib_fun = - let exec ~value {location} ~ret mem = + let exec ~value {location} ~ret:(ret_id, _) mem = let traces = Trace.(Set.add_elem location (through ~risky_fun:(Some lib_fun))) (Dom.Val.get_traces value) in - model_by_value {value with traces} ret mem + model_by_value {value with traces} ret_id mem in fun value -> {exec= exec ~value; check= no_check} @@ -376,9 +376,9 @@ let eval_array_locs_length arr_locs mem = (* Java only *) let get_array_length array_exp = - let exec _ ~ret mem = + let exec _ ~ret:(ret_id, _) mem = let result = eval_array_locs_length (Sem.eval_locs array_exp mem) mem in - model_by_value result ret mem + model_by_value result ret_id mem in {exec; check= no_check} @@ -634,27 +634,35 @@ module Collection = struct let add coll_id = {exec= change_size_by ~size_f:Itv.incr coll_id; check= no_check} let size coll_exp = - let exec _ ~ret mem = + let exec _ ~ret:(ret_id, _) mem = let result = eval_collection_length coll_exp mem in - model_by_value result ret mem + model_by_value result ret_id mem in {exec; check= no_check} let iterator coll_exp = - let exec {integer_type_widths} ~ret mem = + let exec {integer_type_widths} ~ret:(ret_id, _) mem = let itr = Sem.eval integer_type_widths coll_exp mem in - model_by_value itr ret mem + model_by_value itr ret_id mem + in + {exec; check= no_check} + + + let init lhs_id rhs_exp = + let exec {integer_type_widths} ~ret:_ mem = + let itr = Sem.eval integer_type_widths rhs_exp mem in + model_by_value itr lhs_id mem in {exec; check= no_check} let hasNext iterator = - let exec _ ~ret mem = + let exec _ ~ret:(ret_id, _) mem = (* Set the size of the iterator to be [0, size-1], so that range will be size of the collection. *) let collection_size = eval_collection_length iterator mem |> Dom.Val.get_iterator_itv in - model_by_value collection_size ret mem + model_by_value collection_size ret_id mem in {exec; check= no_check} @@ -792,6 +800,8 @@ module Call = struct $+ any_arg_of_typ (-"std" &:: "basic_string") $--> by_value Dom.Val.Itv.unknown_bool ; -"std" &:: "basic_string" &::.*--> no_model + ; +PatternMatch.implements_collection + &:: "" <>$ capt_var_exn $+ capt_exp $--> Collection.init ; +PatternMatch.implements_collection &:: "get" <>$ capt_var_exn $+ capt_exp $--> Collection.get_or_set_at_index ; +PatternMatch.implements_collection diff --git a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java index 1c7ff247b..ffb9ca0e9 100644 --- a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java +++ b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java @@ -221,4 +221,34 @@ public class ArrayListTest { } return false; } + + void constructor_linear(ArrayList list) { + ArrayList slist = new ArrayList<>(list); + for (int i = 0; i < slist.size(); i++) {} + } + + void constructor_modify(ArrayList list) { + // copying the reference here, so any change made to slist will + // affect list + ArrayList slist = new ArrayList<>(list); + slist.add("a"); + slist.add("b"); + slist.add("c"); + slist.add("d"); + for (int i = 0; i < list.size(); i++) {} + } + + void constructor_add_all(ArrayList list, ArrayList l) { + ArrayList slist = new ArrayList<>(list); + slist.addAll(l); // increments the size of both list and slist by + // l.length + for (int i = 0; i < list.size(); i++) {} + } + + void constructor_add_all_sym(ArrayList list, ArrayList l) { + ArrayList slist = new ArrayList<>(list); + list.addAll(l); // increments the size of both list and slist by + // l.length + for (int i = 0; i < slist.size(); i++) {} + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 3b1a814e0..5140904af 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -19,6 +19,10 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remov codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Through,Array access: Offset: 1 Size: 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.call_sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + list.length × log(list.length), degree = 1 + 1⋅log,{list.length},call to void ArrayListTest.sortArrayList(ArrayList),Modeled call to List.length,{list.length},call to void ArrayListTest.sortArrayList(ArrayList),Modeled call to List.length] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 11 + 5 ⋅ (l.length + list.length) + 4 ⋅ (l.length + list.length + 1), degree = 1,{l.length + list.length + 1},Loop at line 245,{l.length + list.length},Loop at line 245] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all_sym(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 11 + 5 ⋅ (l.length + list.length) + 4 ⋅ (l.length + list.length + 1), degree = 1,{l.length + list.length + 1},Loop at line 252,{l.length + list.length},Loop at line 252] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_linear(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length + 4 ⋅ (list.length + 1), degree = 1,{list.length + 1},Loop at line 227,{list.length},Loop at line 227] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_modify(java.util.ArrayList):void, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 22 + 5 ⋅ (list.length + 4) + 4 ⋅ (list.length + 5), degree = 1,{list.length + 5},Loop at line 238,{list.length + 4},Loop at line 238] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length, degree = 1,{list.length},Loop at line 14] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 13 ⋅ (list.length - 1) + 2 ⋅ (list.length - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length × (-Integer.intValue().lb + 11), degree = 2,{-Integer.intValue().lb + 11},Loop at line 193,{list.length},Loop at line 193,{-Integer.intValue().lb + 11},Loop at line 193,{list.length - 1},Loop at line 193] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: __cast,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]]