From 22e25fda769e4b30a7f0abc4b815c6f6a407e58a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Wed, 16 Sep 2020 02:48:24 -0700 Subject: [PATCH] [inferbo] Ignore symbolic values in ranges when upper bound is constant Summary: Handle the case of - computing the range of `[lb, ub]` where `lb` contains length path and `ub` is constant. E.g. `[a.length, 2]` would give `3` range - simplifying `c1 +/- min(c2, a.length)` to `c1 +/- min(c2, 0)` since the length of a collection/array is always nonnegative. This also removes some existing FPs in tests results. Facebook Context: we stumbled upon this issue in ObjC results TV109717121 which is corresponding to the added test case. Reviewed By: skcho Differential Revision: D23648807 fbshipit-source-id: 1e89ea246 --- infer/src/bufferoverrun/bounds.ml | 36 +++++++++++++++++++ infer/src/bufferoverrun/bounds.mli | 6 ++++ infer/src/bufferoverrun/itv.ml | 9 +++++ infer/src/bufferoverrun/symb.ml | 9 +++++ infer/src/bufferoverrun/symb.mli | 4 +++ .../codetoanalyze/java/performance/Loops.java | 11 ++++++ .../java/performance/StringTest.java | 2 +- .../java/performance/cost-issues.exp | 11 +++--- .../codetoanalyze/java/performance/issues.exp | 1 + 9 files changed, 83 insertions(+), 6 deletions(-) diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index 69a5c8dec..0e3de67a1 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -105,6 +105,12 @@ module SymLinear = struct let neg : t -> t = fun x -> M.map NonZeroInt.( ~- ) x + let remove_positive_length_symbol : t -> t = + M.filter (fun symb coeff -> + let path = Symb.Symbol.path symb in + not (NonZeroInt.is_positive coeff && Symb.SymbolPath.is_length path) ) + + let plus : t -> t -> t = fun x y -> let plus_coeff _ c1 c2 = NonZeroInt.plus c1 c2 in @@ -614,6 +620,22 @@ module Bound = struct mk_MultB (Z.neg c, neg x, y) + let rec remove_positive_length_symbol b = + match b with + | MInf | PInf -> + b + | Linear (c, x) -> + Linear (c, SymLinear.remove_positive_length_symbol x) + | MinMax (c, sign, min_max, d, x) -> + if Symb.Symbol.is_length x then + Linear (Sign.eval_big_int sign c (MinMax.eval_big_int min_max d Z.zero), SymLinear.empty) + else b + | MinMaxB (m, x, y) -> + mk_MinMaxB (m, remove_positive_length_symbol x, remove_positive_length_symbol y) + | MultB (c, x, y) -> + mk_MultB (c, remove_positive_length_symbol x, remove_positive_length_symbol y) + + let exact_min : otherwise:(t -> t -> t) -> t -> t -> t = fun ~otherwise b1 b2 -> if le b1 b2 then b1 @@ -1227,6 +1249,20 @@ module Bound = struct if phys_equal a a' && phys_equal b b' then x else mk_MultB (c, a', b') + let simplify_minimum_length x = + match x with + | MultB _ | Linear _ | MInf | PInf | MinMaxB _ -> + x + | MinMax (c1, sign, Min, c2, symb) -> + let path = Symb.Symbol.path symb in + if Symb.SymbolPath.is_length path then + let z = Sign.eval_big_int sign c1 (Z.min c2 Z.zero) in + Linear (z, SymLinear.empty) + else x + | MinMax _ -> + x + + let get_same_one_symbol b1 b2 = match (b1, b2) with | Linear (n1, se1), Linear (n2, se2) when Z.(equal n1 zero) && Z.(equal n2 zero) -> diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index 96067ce97..8aba1f5d6 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -126,6 +126,12 @@ module Bound : sig val simplify_min_one : t -> t + val simplify_minimum_length : t -> t + (** Simplifies c1 +/- min(c2, length) to c1 +- min(0,c2) *) + + val remove_positive_length_symbol : t -> t + (** Removes positive symbols that are coming from length paths *) + val get_same_one_symbol : t -> t -> Symb.SymbolPath.t option (** It returns a symbol [s] when the two bounds are all linear expressions of the symbol [1⋅s]. *) diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 455e86d1b..76234609c 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -22,9 +22,18 @@ module ItvRange = struct let of_bounds : loop_head_loc:Location.t -> lb:Bound.t -> ub:Bound.t -> t = fun ~loop_head_loc ~lb ~ub -> + let lb = + (* Handle the case of[s, c] where s contains positive length path and c + is constant. E.g [len, 2] would give 3 since len is always + nonnegative *) + if Bound.is_symbolic lb && not (Bound.is_symbolic ub) then + Bound.remove_positive_length_symbol lb + else lb + in Bound.plus_u ~weak:true ub Bound.one |> Bound.plus_u ~weak:true (Bound.neg lb) |> Bound.simplify_min_one |> Bound.simplify_bound_ends_from_paths + |> Bound.simplify_minimum_length |> Bounds.NonNegativeBound.of_loop_bound loop_head_loc diff --git a/infer/src/bufferoverrun/symb.ml b/infer/src/bufferoverrun/symb.ml index d650d6843..2887b0db8 100644 --- a/infer/src/bufferoverrun/symb.ml +++ b/infer/src/bufferoverrun/symb.ml @@ -233,6 +233,8 @@ module SymbolPath = struct false + let is_length = function Length _ -> true | _ -> false + let is_global = function Normal p | Offset {p} | Length {p} | Modeled {p} -> is_global_partial p end @@ -353,6 +355,13 @@ module Symbol = struct path + let is_length = function + | ForeignVariable _ -> + false + | OneValue {path} | BoundEnd {path} -> + SymbolPath.is_length path + + (* NOTE: This may not be satisfied in the cost checker for simplifying its results. *) let check_bound_end s be = if Config.bo_debug >= 3 then diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli index 826e2f6c5..44823aa6c 100644 --- a/infer/src/bufferoverrun/symb.mli +++ b/infer/src/bufferoverrun/symb.mli @@ -80,6 +80,8 @@ module SymbolPath : sig val is_cpp_vector_elem : partial -> bool val is_global_partial : partial -> bool + + val is_length : t -> bool end module Symbol : sig @@ -95,6 +97,8 @@ module Symbol : sig val is_global : t -> bool + val is_length : t -> bool + val pp_mark : markup:bool -> F.formatter -> t -> unit val equal : t -> t -> bool diff --git a/infer/tests/codetoanalyze/java/performance/Loops.java b/infer/tests/codetoanalyze/java/performance/Loops.java index 85f520a01..3a946047d 100644 --- a/infer/tests/codetoanalyze/java/performance/Loops.java +++ b/infer/tests/codetoanalyze/java/performance/Loops.java @@ -10,6 +10,7 @@ import android.app.Activity; import java.io.IOException; import java.nio.ByteBuffer; import java.nio.channels.FileChannel; +import java.util.ArrayList; public class Loops { @@ -171,4 +172,14 @@ public class Loops { } } } + + int loop_prune_constant(ArrayList list) { + int k = 0; + for (int i = 0; i < 3; ++i) { + if (list.size() >= i + 1) { + k++; + } + } + return k; + } } diff --git a/infer/tests/codetoanalyze/java/performance/StringTest.java b/infer/tests/codetoanalyze/java/performance/StringTest.java index 5392bd289..ed10e5e13 100644 --- a/infer/tests/codetoanalyze/java/performance/StringTest.java +++ b/infer/tests/codetoanalyze/java/performance/StringTest.java @@ -98,7 +98,7 @@ class StringTest { boolean unknown_bool; - public void last_index_of_linear_FP(String s) { + public void last_index_of_linear_FN(String s) { int i = s.lastIndexOf('/'); while (i > 0) { int j = s.lastIndexOf('/', i - 1); diff --git a/infer/tests/codetoanalyze/java/performance/cost-issues.exp b/infer/tests/codetoanalyze/java/performance/cost-issues.exp index a894a3b54..4c308d8fd 100644 --- a/infer/tests/codetoanalyze/java/performance/cost-issues.exp +++ b/infer/tests/codetoanalyze/java/performance/cost-issues.exp @@ -285,6 +285,7 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops. codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_simple_linear(codetoanalyze.java.performance.Loops$MyLinkedList):void, 3 + 10 ⋅ (p.linked_list_length + 1), OnUIThread:false, [{p.linked_list_length + 1},Loop] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.linked_list_model_linear(android.app.Activity):void, 3 + 7 ⋅ (p.linked_list_length + 1), OnUIThread:false, [{p.linked_list_length + 1},Loop] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.loop_linear(int):void, 5 + 5 ⋅ x, OnUIThread:false, [{x},Loop] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.loop_prune_constant(java.util.ArrayList):int, 42, OnUIThread:false, [] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.modeled_range_linear_FP(java.nio.channels.FileChannel,java.nio.ByteBuffer):void, 6 + 14 ⋅ FileChannel.read(...).modeled², OnUIThread:false, [{FileChannel.read(...).modeled},Modeled call to read(...),{FileChannel.read(...).modeled},Modeled call to read(...)] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, ⊤, OnUIThread:false, [Unbounded loop,Loop] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar_linear(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 47 + 26 ⋅ x.length, OnUIThread:false, [{x.length},Loop] @@ -305,13 +306,13 @@ codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.Mat codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.linear(int):void, 5 + 5 ⋅ p, OnUIThread:false, [{p},Loop] codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.max2_symbolic(int,int):void, 9 + 9 ⋅ (max(x, y)), OnUIThread:false, [{max(x, y)},Loop] codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.max_symbolic(int[]):void, 5 + 5 ⋅ arr.length + 4 ⋅ (arr.length + 1), OnUIThread:false, [{arr.length + 1},Loop,{arr.length},Loop] -codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.min_constant(int[]):void, 5 + 5 ⋅ (min(3, arr.length)) + 4 ⋅ (1+min(3, arr.length)), OnUIThread:false, [{1+min(3, arr.length)},Loop,{min(3, arr.length)},Loop] +codetoanalyze/java/performance/MathTest.java, codetoanalyze.java.performance.MathTest.min_constant(int[]):void, 14, OnUIThread:false, [] codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest$Constant.(PreconditionTest), 6, OnUIThread:false, [] codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.(), 3, OnUIThread:false, [] -codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.checkArgument_constant(java.util.ArrayList):void, 16 + 5 ⋅ (min(2, list.length)) + 3 ⋅ (1+min(2, list.length)), OnUIThread:false, [{1+min(2, list.length)},Loop,{min(2, list.length)},Loop] +codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.checkArgument_constant(java.util.ArrayList):void, 24, OnUIThread:false, [] codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.checkNotNull_linear(java.util.ArrayList,java.lang.Object):void, 13 + 8 ⋅ list.length + 3 ⋅ (list.length + 1), OnUIThread:false, [{list.length + 1},Loop,{list.length},Loop] -codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.checkState_constant(java.util.ArrayList):void, 16 + 5 ⋅ (min(2, list.length)) + 3 ⋅ (1+min(2, list.length)), OnUIThread:false, [{1+min(2, list.length)},Loop,{min(2, list.length)},Loop] -codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.constant_array(int[]):void, 20 + 17 ⋅ (min(5, a.length)), OnUIThread:false, [{min(5, a.length)},Loop] +codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.checkState_constant(java.util.ArrayList):void, 24, OnUIThread:false, [] +codetoanalyze/java/performance/PreconditionTest.java, PreconditionTest.constant_array(int[]):void, 37, OnUIThread:false, [] codetoanalyze/java/performance/StringBuilderTest.java, StringBuilderTest.(), 3, OnUIThread:false, [] codetoanalyze/java/performance/StringBuilderTest.java, StringBuilderTest.append_linear(java.lang.String):void, 25 + 5 ⋅ (s.length + 2) + 3 ⋅ (s.length + 3), OnUIThread:false, [{s.length + 3},Call to void StringBuilderTest.new_linear(String),Loop,{s.length + 2},Call to void StringBuilderTest.new_linear(String),Loop] codetoanalyze/java/performance/StringBuilderTest.java, StringBuilderTest.new_capacity_constant():void, 24, OnUIThread:false, [] @@ -329,7 +330,7 @@ codetoanalyze/java/performance/StringTest.java, StringTest.indexof_from_linear(j codetoanalyze/java/performance/StringTest.java, StringTest.indexof_linear(java.lang.String):int, 5 + m.length, OnUIThread:false, [{m.length},Modeled call to String.indexOf] codetoanalyze/java/performance/StringTest.java, StringTest.indexof_quadratic(java.lang.String,java.lang.String):int, 6 + m.length × n.length, OnUIThread:false, [{n.length},Modeled call to String.indexOf,{m.length},Modeled call to String.indexOf] codetoanalyze/java/performance/StringTest.java, StringTest.last_index_of_linear(java.lang.String):void, 8 + 5 ⋅ (s.length - 1), OnUIThread:false, [{s.length - 1},Loop] -codetoanalyze/java/performance/StringTest.java, StringTest.last_index_of_linear_FP(java.lang.String):void, 8 + 6 ⋅ (s.length - 1) × (s.length + 1) + 4 ⋅ (1+min(1, s.length))², OnUIThread:false, [{1+min(1, s.length)},Loop,{1+min(1, s.length)},Loop,{s.length + 1},Loop,{s.length - 1},Loop] +codetoanalyze/java/performance/StringTest.java, StringTest.last_index_of_linear_FN(java.lang.String):void, 24, OnUIThread:false, [] codetoanalyze/java/performance/StringTest.java, StringTest.replace_linear(java.lang.String):void, 8 + 5 ⋅ s.length + 3 ⋅ (s.length + 1), OnUIThread:false, [{s.length + 1},Loop,{s.length},Loop] codetoanalyze/java/performance/StringTest.java, StringTest.split_linear(java.lang.String):void, 9 + 6 ⋅ (-1+max(2, s.length)), OnUIThread:false, [{-1+max(2, s.length)},Loop] codetoanalyze/java/performance/StringTest.java, StringTest.split_with_limit_linear(java.lang.String,int):void, 10 + 6 ⋅ (max(1, limit)), OnUIThread:false, [{max(1, limit)},Loop] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 7e05837bf..c1c0eed03 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -66,6 +66,7 @@ codetoanalyze/java/performance/JsonUtils.java, libraries.marauder.analytics.util codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded value x,Call to void Loops.loop_linear(int),Loop] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.length_of_linked_list_linear_FP(codetoanalyze.java.performance.Loops$MyLinkedList):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Assignment,Call,,Parameter `x`,Binary operation: ([0, +oo] + 1):signed32 by call to `void Loops.loop_linear(int)` ] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.loop_prune_constant(java.util.ArrayList):int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.modeled_range_linear_FP(java.nio.channels.FileChannel,java.nio.ByteBuffer):void, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 8):signed32] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 8, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32]