From 0aec8a04e99ee37cc4c31db5328a9e9903f9d5bb Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 14 Nov 2019 06:57:44 -0800 Subject: [PATCH] [inferbo] Substitution of array block of default case in Java Summary: There was a precision loss during the substitution of array block. For example: Callee's abstract memory includes an array block as follows, where `a` is a parameter. ``` a.elements -> { a.elements[*] with a.elements.size } ``` Callers' abstract memory includes a pointer that may point to multiple array blocks. ``` c -> { x, y } x.elements -> { x.elements[*] with x.elements.size } y.elements -> { y.elements[*] with y.elements.size } ``` When the callee is called with the parameter `c`, the callees memory is substituted to: ``` x.elements -> { x.elements[*] with top , y.elements[*] with top } y.elements -> { x.elements[*] with top , y.elements[*] with top } ``` because `a.elements[*]` was substituted to `{ x.elements[*] , y.elements[*] }` and `a.elements.size` was substituted to `top ( = x.elements.size join y.elements.size )`. This diff tries to keep the precision in the specific case, not to join the sizes of array blocks. So now the same callee's abstract memory is substituted to: ``` x.elements -> { x.elements[*] with x.elements.size } y.elements -> { y.elements[*] with y.elements.size } ``` Reviewed By: ngorogiannis Differential Revision: D18480585 fbshipit-source-id: b70e63c22 --- infer/src/bufferoverrun/arrayBlk.ml | 12 ++++++++++++ .../java/performance/ArrayListTest.java | 18 ++++++++++++++++++ .../codetoanalyze/java/performance/issues.exp | 2 ++ 3 files changed, 32 insertions(+) diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index d0f3d3ea7..0d5b7d36f 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -270,6 +270,14 @@ module ArrInfo = struct cmp_itv Itv.zero Itv.zero | _ -> Boolean.Top + + + let is_symbolic_length_of_path path info = + match (path, info) with + | Symb.SymbolPath.Deref (_, prefix), Java {length} -> + Itv.is_length_path_of prefix length + | _ -> + false end include AbstractDomain.Map (Allocsite) (ArrInfo) @@ -333,6 +341,10 @@ let subst : t -> Bound.eval_sym -> PowLoc.eval_locpath -> PowLoc.t * t = let locs = eval_locpath path in let add_allocsite l (powloc_acc, acc) = match l with + | Loc.Allocsite (Symbol (Symb.SymbolPath.Deref (_, prefix)) as a) + when ArrInfo.is_symbolic_length_of_path path info -> + let length = Itv.of_length_path ~is_void:false prefix in + (powloc_acc, add a (ArrInfo.make_java ~length) acc) | Loc.Allocsite a -> (powloc_acc, add a info' acc) | _ -> diff --git a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java index d5ba96fbc..9d00f1c91 100644 --- a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java +++ b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java @@ -316,6 +316,24 @@ public class ArrayListTest { HashMap m = init_with_put_linear(a); for (HashMap.Entry e : m.entrySet()) {} } + + boolean unknown_bool; + + void id(ArrayList a) { + a.add(0); + a.remove(0); + } + + void substitute_array_block_linear(ArrayList a, ArrayList b) { + ArrayList c; + if (unknown_bool) { + c = a; + } else { + c = b; + } + id(c); + iterate_over_arraylist(a); + } } class LexicographicComparator implements java.util.Comparator { diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 0c884d552..82ca3ebfe 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -52,6 +52,8 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.max_linear(java codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ this.list.length + 3 ⋅ (this.list.length + 1), O(this.list.length), degree = 1,{this.list.length + 1},Loop at line 221,{this.list.length},Loop at line 221] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + list.length × log(list.length), O(list.length × log(list.length)), degree = 1 + 1⋅log,{list.length},Modeled call to Collections.sort,{list.length},Modeled call to Collections.sort] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sort_comparator_nlogn(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + people.length × log(people.length), O(people.length × log(people.length)), degree = 1 + 1⋅log,{people.length},Modeled call to Collections.sort,{people.length},Modeled call to Collections.sort] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.substitute_array_block_linear(java.util.ArrayList,java.util.ArrayList):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 33 + 5 ⋅ (b.length + a.length), O((b.length + a.length)), degree = 1,{b.length + a.length},call to void ArrayListTest.iterate_over_arraylist(ArrayList),Loop at line 15] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.substitute_array_block_linear(java.util.ArrayList,java.util.ArrayList):void, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Parameter `b.elements[*]`,Call,Parameter `a.elements[*]`,Through,Through,Call,,Assignment,Binary operation: ([0, +oo] + 1):signed32 by call to `void ArrayListTest.iterate_over_arraylist(ArrayList)` ] codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 7 ⋅ p, O(p), degree = 1,{p},call to int Break.break_loop(int,int),Loop at line 12] codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_loop(int,int):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 7 ⋅ p, O(p), degree = 1,{p},Loop at line 12] codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_outer_loop_MaybeInfinite(int,int):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 4 ⋅ maxI + 3 ⋅ maxI × (min(12, maxJ)) + 5 ⋅ maxI × (12-max(0, maxJ)) + 5 ⋅ (min(11, maxI)) × (min(11, maxJ)), O(maxI × maxJ), degree = 2,{min(11, maxJ)},Loop at line 37,{min(11, maxI)},Loop at line 35,{12-max(0, maxJ)},Loop at line 35,{min(12, maxJ)},Loop at line 37,{maxI},Loop at line 35]