diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml index b4e94b8fc..42dfde127 100644 --- a/infer/src/bufferoverrun/bounds.ml +++ b/infer/src/bufferoverrun/bounds.ml @@ -1038,20 +1038,18 @@ module BoundTrace = struct let call ~callee_pname ~location callee_trace = Call {callee_pname; callee_trace; location} - let make_err_trace = - let rec aux depth trace = - match trace with - | Loop loop_head_loc -> - let desc = F.asprintf "Loop at %a" Location.pp loop_head_loc in - [Errlog.make_trace_element depth loop_head_loc desc []] - | Call {callee_pname; location; callee_trace} -> - let desc = F.asprintf "call to %a" Typ.Procname.pp callee_pname in - Errlog.make_trace_element depth location desc [] :: aux (depth + 1) callee_trace - | ModeledFunction {pname; location} -> - let desc = F.asprintf "Modeled call to %s" pname in - [Errlog.make_trace_element depth location desc []] - in - fun trace -> aux 0 trace + let rec make_err_trace ~depth trace = + match trace with + | Loop loop_head_loc -> + let desc = F.asprintf "Loop at %a" Location.pp loop_head_loc in + [Errlog.make_trace_element depth loop_head_loc desc []] + | Call {callee_pname; location; callee_trace} -> + let desc = F.asprintf "call to %a" Typ.Procname.pp callee_pname in + Errlog.make_trace_element depth location desc [] + :: make_err_trace ~depth:(depth + 1) callee_trace + | ModeledFunction {pname; location} -> + let desc = F.asprintf "Modeled call to %s" pname in + [Errlog.make_trace_element depth location desc []] end (** A NonNegativeBound is a Bound that is either non-negative or symbolic but will be evaluated to a non-negative value once instantiated *) @@ -1060,7 +1058,7 @@ module NonNegativeBound = struct let make_err_trace (b, t) = let b = F.asprintf "{%a}" Bound.pp b in - (b, BoundTrace.make_err_trace t) + (b, BoundTrace.make_err_trace ~depth:0 t) let pp ~hum fmt (bound, t) = diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli index 355e4cf95..322e47269 100644 --- a/infer/src/bufferoverrun/bounds.mli +++ b/infer/src/bufferoverrun/bounds.mli @@ -117,9 +117,9 @@ end module BoundTrace : sig include PrettyPrintable.PrintableOrderedType - val call : callee_pname:Typ.Procname.t -> location:Location.t -> t -> t + val length : t -> int - val make_err_trace : t -> Errlog.loc_trace + val make_err_trace : depth:int -> t -> Errlog.loc_trace end type ('c, 's, 't) valclass = Constant of 'c | Symbolic of 's | ValTop of 't diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml index 3af84adac..9388e7c0c 100644 --- a/infer/src/bufferoverrun/polynomials.ml +++ b/infer/src/bufferoverrun/polynomials.ml @@ -9,7 +9,6 @@ open! IStd open! AbstractDomain.Types module Bound = Bounds.Bound open Ints -module TopTrace = Bounds.BoundTrace module DegreeKind = struct type t = Linear | Log [@@deriving compare] @@ -57,7 +56,7 @@ end module type NonNegativeSymbol = sig type t [@@deriving compare] - val classify : t -> (Ints.NonNegativeInt.t, t, TopTrace.t) Bounds.valclass + val classify : t -> (Ints.NonNegativeInt.t, t, Bounds.BoundTrace.t) Bounds.valclass val int_lb : t -> NonNegativeInt.t @@ -68,7 +67,7 @@ module type NonNegativeSymbol = sig -> Location.t -> t -> Bound.eval_sym - -> (NonNegativeInt.t, t, TopTrace.t) Bounds.valclass + -> (NonNegativeInt.t, t, Bounds.BoundTrace.t) Bounds.valclass val pp : hum:bool -> F.formatter -> t -> unit end @@ -317,7 +316,7 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct let subst callee_pname location = - let exception ReturnTop of TopTrace.t in + let exception ReturnTop of (S.t * Bounds.BoundTrace.t) in (* avoids top-lifting everything *) let rec subst {const; terms} eval_sym = M.fold @@ -332,14 +331,14 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct mult_const_positive p c |> plus acc ) | ValTop trace -> let p = subst p eval_sym in - if is_zero p then acc else raise (ReturnTop trace) + if is_zero p then acc else raise (ReturnTop (s, trace)) | Symbolic s -> let p = subst p eval_sym in mult_symb p s |> plus acc ) terms (of_non_negative_int const) in fun p eval_sym -> - match subst p eval_sym with p -> Below p | exception ReturnTop trace -> Above trace + match subst p eval_sym with p -> Below p | exception ReturnTop s_trace -> Above s_trace (** Emit a pair (d,t) where d is the degree of the polynomial and t is the first term with such degree *) @@ -414,11 +413,63 @@ end module NonNegativeBoundWithDegreeKind = MakeSymbolWithDegreeKind (Bounds.NonNegativeBound) module NonNegativeNonTopPolynomial = MakePolynomial (NonNegativeBoundWithDegreeKind) +module TopTrace = struct + module S = NonNegativeBoundWithDegreeKind + + type t = + | UnboundedLoop of {bound_trace: Bounds.BoundTrace.t} + | UnboundedSymbol of {location: Location.t; symbol: S.t; bound_trace: Bounds.BoundTrace.t} + | Call of {location: Location.t; callee_pname: Typ.Procname.t; callee_trace: t} + [@@deriving compare] + + let rec length = function + | UnboundedLoop {bound_trace} | UnboundedSymbol {bound_trace} -> + 1 + Bounds.BoundTrace.length bound_trace + | Call {callee_trace} -> + 1 + length callee_trace + + + let compare t1 t2 = [%compare: int * t] (length t1, t1) (length t2, t2) + + let unbounded_loop bound_trace = UnboundedLoop {bound_trace} + + let unbounded_symbol ~location ~symbol bound_trace = + UnboundedSymbol {location; symbol; bound_trace} + + + let call ~location ~callee_pname callee_trace = Call {location; callee_pname; callee_trace} + + let rec pp f = function + | UnboundedLoop {bound_trace} -> + F.fprintf f "%a -> UnboundedLoop" Bounds.BoundTrace.pp bound_trace + | UnboundedSymbol {location; symbol; bound_trace} -> + F.fprintf f "%a -> UnboundedSymbol (%a): %a" Bounds.BoundTrace.pp bound_trace Location.pp + location (S.pp ~hum:false) symbol + | Call {callee_pname; callee_trace; location} -> + F.fprintf f "%a -> Call `%a` (%a)" pp callee_trace Typ.Procname.pp callee_pname Location.pp + location + + + let rec make_err_trace ~depth trace = + match trace with + | UnboundedLoop {bound_trace} -> + let bound_err_trace = Bounds.BoundTrace.make_err_trace ~depth bound_trace in + [("Unbounded loop", bound_err_trace)] |> Errlog.concat_traces + | UnboundedSymbol {location; symbol; bound_trace} -> + let desc = F.asprintf "Unbounded value %a" (S.pp ~hum:true) symbol in + Errlog.make_trace_element depth location desc [] + :: Bounds.BoundTrace.make_err_trace ~depth bound_trace + | Call {location; callee_pname; callee_trace} -> + let desc = F.asprintf "Call to %a" Typ.Procname.pp callee_pname in + Errlog.make_trace_element depth location desc [] + :: make_err_trace ~depth:(depth + 1) callee_trace +end + module TopTraces = struct include AbstractDomain.MinReprSet (TopTrace) let make_err_trace traces = - match min_elt traces with None -> [] | Some trace -> TopTrace.make_err_trace trace + match min_elt traces with None -> [] | Some trace -> TopTrace.make_err_trace ~depth:0 trace end module NonNegativePolynomial = struct @@ -453,13 +504,16 @@ module NonNegativePolynomial = struct let of_int_exn i = Below (NonNegativeNonTopPolynomial.of_int_exn i) - let make_trace_set = AbstractDomain.StackedUtils.map ~f_below:Fn.id ~f_above:TopTraces.singleton + let make_trace_set ~map_above = + AbstractDomain.StackedUtils.map ~f_below:Fn.id ~f_above:(fun above -> + TopTraces.singleton (map_above above) ) + let of_non_negative_bound ?(degree_kind = DegreeKind.Linear) b = b |> NonNegativeBoundWithDegreeKind.make degree_kind |> NonNegativeBoundWithDegreeKind.classify |> NonNegativeNonTopPolynomial.of_valclass - |> make_trace_set + |> make_trace_set ~map_above:TopTrace.unbounded_loop let is_symbolic = function @@ -496,7 +550,9 @@ module NonNegativePolynomial = struct (fun callee_trace -> TopTrace.call ~callee_pname ~location callee_trace) callee_traces) | Below p -> - NonNegativeNonTopPolynomial.subst callee_pname location p eval_sym |> make_trace_set + NonNegativeNonTopPolynomial.subst callee_pname location p eval_sym + |> make_trace_set ~map_above:(fun (symbol, bound_trace) -> + TopTrace.unbounded_symbol ~location ~symbol bound_trace ) let degree p = diff --git a/infer/tests/build_systems/differential_of_costs_report/introduced.exp b/infer/tests/build_systems/differential_of_costs_report/introduced.exp index c25d07d89..829386765 100644 --- a/infer/tests/build_systems/differential_of_costs_report/introduced.exp +++ b/infer/tests/build_systems/differential_of_costs_report/introduced.exp @@ -1,3 +1,3 @@ -INFINITE_EXECUTION_TIME_CALL, no_bucket, src/DiffExample.java, DiffExample.f1(int):void, 0, [Loop at line 26] +INFINITE_EXECUTION_TIME_CALL, no_bucket, src/DiffExample.java, DiffExample.f1(int):void, 0, [Unbounded loop,Loop at line 26] PERFORMANCE_VARIATION, no_bucket, src/DiffExample.java, DiffExample.f4(int):int, 0, [Updated Cost is 6 + 5 ⋅ k (degree is 1),{k},Loop at line 45] PERFORMANCE_VARIATION, no_bucket, src/DiffExample.java, DiffExample.f5(java.util.ArrayList):void, 0, [Updated Cost is 2 + list.length × log(list.length) (degree is 1 + 1⋅log),{list.length},Modeled call to List.length,{list.length},Modeled call to List.length] diff --git a/infer/tests/build_systems/differential_of_costs_report/preexisting.exp b/infer/tests/build_systems/differential_of_costs_report/preexisting.exp index 5f021e7da..576624911 100644 --- a/infer/tests/build_systems/differential_of_costs_report/preexisting.exp +++ b/infer/tests/build_systems/differential_of_costs_report/preexisting.exp @@ -1 +1 @@ -INFINITE_EXECUTION_TIME_CALL, no_bucket, src/DiffExample.java, DiffExample.f7(int):void, 0, [call to void DiffExample.f1(int),Loop at line 26] +INFINITE_EXECUTION_TIME_CALL, no_bucket, src/DiffExample.java, DiffExample.f7(int):void, 0, [Call to void DiffExample.f1(int),Unbounded loop,Loop at line 26] diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index b7382e9fa..99c9cdd90 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -15,13 +15,13 @@ codetoanalyze/c/performance/compound_loop_guard.c, simulated_nested_loop_with_an codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_shortcut, 5, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/performance/compound_loop_guard.c, simulated_while_with_and, 11, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 3 ⋅ p + 4 ⋅ (1+max(0, p)), degree = 1,{1+max(0, p)},Loop at line 43, column 3,{p},Loop at line 43, column 3] -codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 63, column 3] +codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded loop,Loop at line 63, column 3] codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/c/performance/compound_loop_guard.c, while_and_or, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/c/performance/cost_test.c, alias_OK, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Binary operation: ([-oo, +oo] + 1):signed32] -codetoanalyze/c/performance/cost_test.c, call_infinite, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [call to infinite,Loop at line 143, column 3] +codetoanalyze/c/performance/cost_test.c, call_infinite, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Call to infinite,Unbounded loop,Loop at line 143, column 3] codetoanalyze/c/performance/cost_test.c, call_while_upto20_minus100_bad, 0, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 726, degree = 0] -codetoanalyze/c/performance/cost_test.c, infinite, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 143, column 3] +codetoanalyze/c/performance/cost_test.c, infinite, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded loop,Loop at line 143, column 3] codetoanalyze/c/performance/cost_test.c, infinite, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: ([-oo, +oo] + [0, +oo]):signed32] codetoanalyze/c/performance/cost_test.c, infinite_FN, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: ([-oo, +oo] + [0, +oo]):signed32] codetoanalyze/c/performance/cost_test.c, loop0_bad, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1104, degree = 0] diff --git a/infer/tests/codetoanalyze/java/performance/Loops.java b/infer/tests/codetoanalyze/java/performance/Loops.java index 29d16e7f8..64e09fae7 100644 --- a/infer/tests/codetoanalyze/java/performance/Loops.java +++ b/infer/tests/codetoanalyze/java/performance/Loops.java @@ -77,4 +77,16 @@ public class Loops { } return true; } + + static void linear(int x) { + for (int i = 0; i < x; i++) {} + } + + static void unboundedSymbol() { + int infinite = 9; + for (int i = 0; i < 999; i++) { + infinite *= infinite; + } + linear(infinite); + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 3b6a958fa..a04618bfb 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -5,14 +5,14 @@ codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void, codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 883, degree = 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add3_overrun_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Through,Through,Through,Array access: Offset added: 4 Size: 3] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_addAll_bad():void, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Through,Through,Through,Array access: Offset added: 5 Size: 4] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 53] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded loop,Loop at line 53] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_FP():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_overrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: 1 Size: 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset added: -1 Size: 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Through,Array access: Offset: 2 Size: 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_get_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Through,Through,Through,Array access: Offset: 1 Size: 1] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 164] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded loop,Loop at line 164] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_in_loop_Good_FP():void, 6, BUFFER_OVERRUN_L5, no_bucket, ERROR, [,Assignment,,Array declaration,Array access: Offset: [0, +oo] Size: [0, +oo]] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remove_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Through,Array access: Offset: 1 Size: 1] @@ -36,13 +36,13 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sortArrayList(j codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 10 + 7 ⋅ 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_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 ⋅ 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_CALL, 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)), 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] -codetoanalyze/java/performance/CantHandle.java, CantHandle.quadratic_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 31] +codetoanalyze/java/performance/CantHandle.java, CantHandle.quadratic_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded loop,Loop at line 31] codetoanalyze/java/performance/CantHandle.java, CantHandle.quadratic_FP(int):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `x`,,Parameter `x`,Binary operation: (x × x):signed32] codetoanalyze/java/performance/CantHandle.java, CantHandle.quadratic_FP(int):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `x`,Binary operation: ([0, +oo] + 1):signed32] -codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 17] +codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded loop,Loop at line 17] codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_FP(int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: ([0, +oo] × [0, +oo]):signed32] codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_FP(int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] -codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_variant_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 25] +codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_variant_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded loop,Loop at line 25] codetoanalyze/java/performance/CantHandle.java, CantHandle.square_root_variant_FP(int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `x`,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.ensure_call(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 11 + 5 ⋅ list.length, degree = 1,{list.length},call to void CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection),Loop at line 16] codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_call_quad(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 4 + 18 ⋅ (list.length - 1) + 5 ⋅ (list.length - 1) × list.length + 3 ⋅ list.length, degree = 2,{list.length},Loop at line 47,{list.length},call to void CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection),Loop at line 16,{list.length - 1},Loop at line 47] @@ -57,7 +57,7 @@ codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performanc codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.nested_while_and_or(int):int, 3, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.nested_while_and_or(int):int, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.nested_while_and_or(int):int, 4, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] -codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 24] +codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded loop,Loop at line 24] codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/java/performance/Compound_loop.java, codetoanalyze.java.performance.Compound_loop.while_and_or(int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Continue.java, codetoanalyze.java.performance.Continue.continue_outer_loop():int, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7963049, degree = 0] @@ -79,10 +79,10 @@ codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performan codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.real_while():int, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Assignment,,Assignment,Binary operation: ([0, +oo] + [0, 29]):signed32] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([3, +oo] + 1):signed32] codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 7, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 545, degree = 0] -codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 15] +codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded loop,Loop at line 15] codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ test.a, degree = 1,{test.a},Loop at line 16] codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 3 ⋅ (k - 1) + 4 ⋅ (max(1, k)), degree = 1,{max(1, k)},Loop at line 58,{k - 1},Loop at line 58] -codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 31] +codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded loop,Loop at line 31] codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `x`,,Parameter `x`,Binary operation: (size + [-oo, +oo]):signed32] codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 6, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `x`,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Invariant.java, Invariant.list_size_invariant(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ items.length + 3 ⋅ (items.length + 1), degree = 1,{items.length + 1},Loop at line 66,{items.length},Loop at line 66] @@ -105,9 +105,14 @@ codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops. codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 25 ⋅ (length - 1), degree = 1,{length - 1},Loop at line 40] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 3 + 59 ⋅ (length - 1) × (length - 1) + 8 ⋅ length, degree = 2,{length},Loop at line 50,{length - 1},Loop at line 51,{length - 1},Loop at line 50] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `a[*]`,,Parameter `b[*]`,Binary operation: (a[*] × b[*]):signed64] -codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 30] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.linear(int):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x, degree = 1,{x},Loop at line 82] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.nested_do_while_FP(int):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded loop,Loop at line 30] 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] codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.similar(codetoanalyze.java.performance.Loops$C[],codetoanalyze.java.performance.Loops$C[]):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 16 + 26 ⋅ x.length, degree = 1,{x.length},Loop at line 73] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol():void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded value x,call to void Loops.linear(int),Loop at line 82] +codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol():void, 2, EXPENSIVE_EXECUTION_TIME_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/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_TIME_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] @@ -115,7 +120,7 @@ codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.call_loop codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_linear(org.json.JSONArray):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ JSONArray.length().ub, degree = 1,{JSONArray.length().ub},Loop at line 18] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.jsonArray_quadratic(org.json.JSONArray):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ JSONArray.length().ub² + 3 ⋅ (1+max(0, JSONArray.length().ub)), degree = 2,{1+max(0, JSONArray.length().ub)},Loop at line 24,{JSONArray.length().ub},Loop at line 24,{JSONArray.length().ub},Loop at line 24] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.loop_over_charArray(java.lang.StringBuilder,java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 12 ⋅ String.toCharArray().length.ub, degree = 1,{String.toCharArray().length.ub},Loop at line 52] -codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Loop at line 47] +codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, [Unbounded loop,Loop at line 47] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_max_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_cost(java.io.InputStream,byte[],int,int,java.util.ArrayList):int, 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 15 + 6 ⋅ (Math.min(...).ub + InputStream.read(...).ub), degree = 1,{Math.min(...).ub + InputStream.read(...).ub},Loop at line 33] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ list.length + 3 ⋅ (list.length + 1), degree = 1,{list.length + 1},Loop at line 62,{list.length},Loop at line 62]