[Cost] More precise traces for Top

Reviewed By: ezgicicek

Differential Revision: D14350180

fbshipit-source-id: 2cb8b0cd0

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) =

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

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 =

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]

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]

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, [<LHS trace>,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, [<LHS trace>,Assignment,<RHS trace>,Assignment,Binary operation: ([-oo, +oo] + [0, +oo]):signed32]
 codetoanalyze/c/performance/cost_test.c, infinite_FN, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,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]

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);
+  }
 }

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, [<Length trace>,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, [<Length trace>,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, [<LHS trace>,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, [<Length trace>,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, [<Length trace>,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, [<Length trace>,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, [<Length trace>,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, [<Length trace>,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, [<LHS trace>,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, [<Offset trace>,Assignment,<Length trace>,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, [<Length trace>,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, [<LHS trace>,Parameter `x`,<RHS trace>,Parameter `x`,Binary operation: (x × x):signed32]
 codetoanalyze/java/performance/CantHandle.java, CantHandle.quadratic_FP(int):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,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, [<LHS trace>,Assignment,<RHS trace>,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, [<LHS trace>,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, [<LHS trace>,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, [<LHS trace>,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, [<LHS trace>,Assignment,Assignment,<RHS trace>,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, [<LHS trace>,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, [<LHS trace>,Parameter `x`,<RHS trace>,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, [<LHS trace>,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, [<LHS trace>,Parameter `a[*]`,<RHS trace>,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, [<LHS trace>,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, [<LHS trace>,Assignment,<RHS trace>,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,<LHS trace>,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, [<LHS trace>,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]