diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml index 357dba0b3..f587d5733 100644 --- a/infer/src/bufferoverrun/itv.ml +++ b/infer/src/bufferoverrun/itv.ml @@ -97,6 +97,8 @@ module Symbol = struct let equal = [%compare.equal : t] + let paths_equal s1 s2 = phys_equal s1.path s2.path + let make : unsigned:bool -> Typ.Procname.t -> SymbolPath.t -> BoundEnd.t -> int -> t = fun ~unsigned pname path bound_end id -> {id; pname; unsigned; path; bound_end} @@ -165,6 +167,10 @@ module NonZeroInt : sig val plus : t -> t -> t option val exact_div_exn : t -> t -> t + + val max : t -> t -> t + + val min : t -> t -> t end = struct type t = int [@@deriving compare] @@ -197,6 +203,11 @@ end = struct let exact_div_exn num den = if not (is_multiple num den) then raise DivisionNotExact ; num / den + + + let max = Int.max + + let min = Int.min end module Ints : sig @@ -419,6 +430,28 @@ module SymLinear = struct let int_lb x = if is_ge_zero x then Some 0 else None let int_ub x = if is_le_zero x then Some 0 else None + + (** When two following symbols are from the same path, simplify what would lead to a zero sum. E.g. 2 * x.lb - x.ub = x.lb *) + let simplify_bound_ends_from_paths : t -> t = + fun x -> + let f (prev_opt, to_add) symb coeff = + match prev_opt with + | Some (prev_coeff, prev_symb) + when Symbol.paths_equal prev_symb symb + && NonZeroInt.is_positive coeff <> NonZeroInt.is_positive prev_coeff -> + let add_coeff = + (if NonZeroInt.is_positive coeff then NonZeroInt.max else NonZeroInt.min) + prev_coeff (NonZeroInt.( ~- ) coeff) + in + let to_add = + to_add |> M.add symb add_coeff |> M.add prev_symb (NonZeroInt.( ~- ) add_coeff) + in + (None, to_add) + | _ -> + (Some (coeff, symb), to_add) + in + let _, to_add = fold x ~init:(None, zero) ~f in + plus x to_add end module Bound = struct @@ -1030,6 +1063,14 @@ module Bound = struct let subst_lb_exn x map = subst_exn ~subst_pos:BoundEnd.LowerBound x map let subst_ub_exn x map = subst_exn ~subst_pos:BoundEnd.UpperBound x map + + let simplify_bound_ends_from_paths x = + match x with + | MInf | PInf | MinMax _ -> + x + | Linear (c, se) -> + let se' = SymLinear.simplify_bound_ends_from_paths se in + if phys_equal se se' then x else Linear (c, se') end type ('c, 's) valclass = Constant of 'c | Symbolic of 's | ValTop @@ -1393,7 +1434,8 @@ module ItvRange = struct let of_bounds : lb:Bound.t -> ub:Bound.t -> t = fun ~lb ~ub -> - Bound.plus_u ub Bound.one |> Bound.plus_u (Bound.neg lb) |> NonNegativeBound.of_bound + Bound.plus_u ub Bound.one |> Bound.plus_u (Bound.neg lb) + |> Bound.simplify_bound_ends_from_paths |> NonNegativeBound.of_bound let to_top_lifted_polynomial : t -> NonNegativePolynomial.astate = diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index ce2958125..9abfd1e5c 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -42,9 +42,6 @@ codetoanalyze/c/performance/cost_test.c, loop1_bad, 6, EXPENSIVE_EXECUTION_TIME_ codetoanalyze/c/performance/cost_test.c, loop2_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 11 * k.ub] codetoanalyze/c/performance/cost_test.c, loop2_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 11 * k.ub] codetoanalyze/c/performance/cost_test.c, loop2_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 11 * k.ub] -codetoanalyze/c/performance/cost_test.c, loop3_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 11 * (-k.lb + k.ub + 15)] -codetoanalyze/c/performance/cost_test.c, loop3_bad, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 11 * (-k.lb + k.ub + 15)] -codetoanalyze/c/performance/cost_test.c, loop3_bad, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 11 * (-k.lb + k.ub + 15)] codetoanalyze/c/performance/cost_test.c, main_bad, 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 211] codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 5 * (-m.lb + 20)] codetoanalyze/c/performance/cost_test.c, while_upto20_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 5 * (-m.lb + 20)] diff --git a/infer/tests/codetoanalyze/java/performance/Cost_test.java b/infer/tests/codetoanalyze/java/performance/Cost_test.java index cf8088804..a4ccc81d5 100644 --- a/infer/tests/codetoanalyze/java/performance/Cost_test.java +++ b/infer/tests/codetoanalyze/java/performance/Cost_test.java @@ -7,116 +7,113 @@ package codetoanalyze.java.performance; -public class Cost_test{ +public class Cost_test { -// Cost: 5 -private static int foo_OK() { - int i, j; - i = 17; - j = 31; + // Cost: 5 + private static int foo_OK() { + int i, j; + i = 17; + j = 31; - return i + j + 3 + 7; -} + return i + j + 3 + 7; + } -// Cost: 17 -private static int bar_OK() { + // Cost: 17 + private static int bar_OK() { - int j = 0; + int j = 0; - j++; - j++; - j++; - j = foo_OK(); - j++; + j++; + j++; + j++; + j = foo_OK(); + j++; - return j; -} + return j; + } -// Cost: 25 -private static int cond_OK(int i) { - int x; + // Cost: 25 + private static int cond_OK(int i) { + int x; - if (i < 0) { - x = bar_OK(); - } else { - x = 1; + if (i < 0) { + x = bar_OK(); + } else { + x = 1; + } + return x; } - return x; -} -// Cost: 5 -private static void alias_OK() { + // Cost: 5 + private static void alias_OK() { - int i = 0, j; + int i = 0, j; - j = i; - i = ++i; -} - -// Cost: 7 -private static void alias2_OK() { + j = i; + i = ++i; + } - int i = 0, j, z; + // Cost: 7 + private static void alias2_OK() { - j = 1; - z = 2; + int i = 0, j, z; - j = i; - i = z; -} + j = 1; + z = 2; -// Cost: 1101 -private static int loop0_bad() { - - for (int i = 0; i < 100; i++) { - alias2_OK(); + j = i; + i = z; } - return 0; -} -// Cost: 1203 -private static int loop1_bad() { + // Cost: 1101 + private static int loop0_bad() { - int k = 100; - for (int i = 0; i < k; i++) { - alias2_OK(); + for (int i = 0; i < 100; i++) { + alias2_OK(); + } + return 0; } - return 0; -} -// Expected: Linear bound -private static int FN_loop2(int k) { + // Cost: 1203 + private static int loop1_bad() { - for (int i = 0; i < k; i++) { - alias2_OK(); + int k = 100; + for (int i = 0; i < k; i++) { + alias2_OK(); + } + return 0; } - return 0; -} -// Expected: constant, but the bound is a polynomial since we can't -// currently map variables to polynomial symbols -private static int FN_loop3(int k) { + // Expected: Linear bound + private static int FN_loop2(int k) { - for (int i = k; i < k + 15; i++) { - alias2_OK(); + for (int i = 0; i < k; i++) { + alias2_OK(); + } + return 0; } - return 0; -} -// Cost: 218 -// Shows that calling many times non expensive function can -// result in an expensive computation -private static int main_bad() { + // Expected: constant + private static int loop3(int k) { - int k1, k2, k3, k4; + for (int i = k; i < k + 18; i++) { + alias2_OK(); + } + return 0; + } - cond_OK(2); - k1 = bar_OK() + foo_OK() + cond_OK(15) * 2; - k2 = bar_OK() + foo_OK() + cond_OK(17) * 3; - k3 = bar_OK() + foo_OK() + cond_OK(11) * 3; - k4 = bar_OK() + foo_OK() + cond_OK(19) * 3; - return 0; -} + // Cost: 218 + // Shows that calling many times non expensive function can + // result in an expensive computation + private static int main_bad() { + int k1, k2, k3, k4; + cond_OK(2); + k1 = bar_OK() + foo_OK() + cond_OK(15) * 2; + k2 = bar_OK() + foo_OK() + cond_OK(17) * 3; + k3 = bar_OK() + foo_OK() + cond_OK(11) * 3; + k4 = bar_OK() + foo_OK() + cond_OK(19) * 3; + return 0; + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 023ad8c04..2852d3c17 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -20,12 +20,12 @@ codetoanalyze/java/performance/Compound_loop.java, void Compound_loop.while_and_ codetoanalyze/java/performance/Continue.java, int Continue.continue_outer_loop_FN(), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [] codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop2(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 * k.ub] codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop2(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 12 * k.ub] -codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop3(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 12 * (-k.lb + k.ub + 15)] -codetoanalyze/java/performance/Cost_test.java, int Cost_test.FN_loop3(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 12 * (-k.lb + k.ub + 15)] codetoanalyze/java/performance/Cost_test.java, int Cost_test.loop0_bad(), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1101] codetoanalyze/java/performance/Cost_test.java, int Cost_test.loop0_bad(), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1102] codetoanalyze/java/performance/Cost_test.java, int Cost_test.loop1_bad(), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1203] codetoanalyze/java/performance/Cost_test.java, int Cost_test.loop1_bad(), 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1202] +codetoanalyze/java/performance/Cost_test.java, int Cost_test.loop3(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 219] +codetoanalyze/java/performance/Cost_test.java, int Cost_test.loop3(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 218] codetoanalyze/java/performance/Cost_test.java, int Cost_test.main_bad(), 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 237] codetoanalyze/java/performance/Cost_test.java, int Cost_test.main_bad(), 8, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 205] codetoanalyze/java/performance/Cost_test.java, int Cost_test.main_bad(), 9, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 243]