[cost] Add modeled range

Summary:
`ModeledRange` represents how many times the interval value can be updated by modeled functions.  This
domain is to support the case where there are mismatches between value of a control variable and
actual number of loop iterations.  For example,

```
while((c = file_channel.read(buf)) != -1) { ... }
```

the loop will iterates as the file size, but the control variable `c` does not have that value.  In
these cases, it assigns a symbolic value of the file size to the modeled range of `c`, then which
is used when calculating the overall cost.

Reviewed By: jvillard

Differential Revision: D17476621

fbshipit-source-id: 9a81376e8

infer/src/absint/PatternMatch.ml

@@ -76,6 +76,8 @@ let implements_inject class_name = implements ("javax.inject." ^ class_name)
 
 let implements_io class_name = implements ("java.io." ^ class_name)
 
+let implements_nio class_name = implements ("java.nio." ^ class_name)
+
 let implements_map = implements "java.util.Map"
 
 let implements_set = implements "java.util.Set"

infer/src/absint/PatternMatch.mli

@@ -61,6 +61,9 @@ val implements_inject : string -> Tenv.t -> string -> bool
 val implements_io : string -> Tenv.t -> string -> bool
 (** Check whether class implements a Java IO *)
 
+val implements_nio : string -> Tenv.t -> string -> bool
+(** Check whether class implements a Java nio *)
+
 val implements_map : Tenv.t -> string -> bool
 (** Check whether class implements a Java's Map *)
 

infer/src/bufferoverrun/bounds.ml

@@ -1132,6 +1132,8 @@ module BoundTrace = struct
 
   let compare t1 t2 = [%compare: int * t] (length t1, t1) (length t2, t2)
 
+  let join x y = if length x <= length y then x else y
+
   let rec pp f = function
     | Loop loc ->
         F.fprintf f "Loop (%a)" Location.pp loc
@@ -1162,6 +1164,16 @@ end
 module NonNegativeBound = struct
   type t = Bound.t * BoundTrace.t [@@deriving compare]
 
+  let ( <= ) ~lhs:(bound_lhs, _) ~rhs:(bound_rhs, _) = Bound.le bound_lhs bound_rhs
+
+  let join (bound_x, trace_x) (bound_y, trace_y) =
+    (Bound.overapprox_max bound_x bound_y, BoundTrace.join trace_x trace_y)
+
+
+  let widen ~prev:(bound_prev, trace_prev) ~next:(bound_next, trace_next) ~num_iters:_ =
+    (Bound.widen_u bound_prev bound_next, BoundTrace.join trace_prev trace_next)
+
+
   let make_err_trace (b, t) =
     let b = F.asprintf "{%a}" Bound.pp b in
     (b, BoundTrace.make_err_trace ~depth:0 t)

infer/src/bufferoverrun/bounds.mli

@@ -132,6 +132,12 @@ type ('c, 's, 't) valclass = Constant of 'c | Symbolic of 's | ValTop of 't
 module NonNegativeBound : sig
   type t [@@deriving compare]
 
+  val ( <= ) : lhs:t -> rhs:t -> bool
+
+  val join : t -> t -> t
+
+  val widen : prev:t -> next:t -> num_iters:int -> t
+
   val of_loop_bound : Location.t -> Bound.t -> t
 
   val of_modeled_function : string -> Location.t -> Bound.t -> t

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -30,10 +30,32 @@ module ItvThresholds = AbstractDomain.FiniteSet (struct
   let pp = pp_print
 end)
 
+(* ModeledRange represents how many times the interval value can be updated by modeled functions.
+   This domain is to support the case where there are mismatches between value of a control variable
+   and actual number of loop iterations.  For example,
+
+   [while((c = file_channel.read(buf)) != -1) { ... }]
+
+   the loop will iterates as the file size, but the control variable [c] does not have that value.
+   In these cases, it assigns a symbolic value of the file size to the modeled range of [c], then
+   which it is used when calculating the overall cost.  *)
+module ModeledRange = struct
+  include AbstractDomain.BottomLifted (struct
+    include Bounds.NonNegativeBound
+
+    let pp = pp ~hum:true
+  end)
+
+  let of_modeled_function pname location bound =
+    let pname = Typ.Procname.to_simplified_string pname in
+    NonBottom (Bounds.NonNegativeBound.of_modeled_function pname location bound)
+end
+
 module Val = struct
   type t =
     { itv: Itv.t
     ; itv_thresholds: ItvThresholds.t
+    ; modeled_range: ModeledRange.t
     ; sym: Relation.Sym.t
     ; powloc: PowLoc.t
     ; arrayblk: ArrayBlk.t
@@ -44,6 +66,7 @@ module Val = struct
   let bot : t =
     { itv= Itv.bot
     ; itv_thresholds= ItvThresholds.empty
+    ; modeled_range= ModeledRange.bottom
     ; sym= Relation.Sym.bot
     ; powloc= PowLoc.bot
     ; arrayblk= ArrayBlk.bot
@@ -60,12 +83,16 @@ module Val = struct
     let relation_sym_pp fmt sym =
       if Option.is_some Config.bo_relational_domain then F.fprintf fmt ", %a" Relation.Sym.pp sym
     in
+    let modeled_range_pp fmt range =
+      if not (ModeledRange.is_bottom range) then
+        F.fprintf fmt " (modeled_range:%a)" ModeledRange.pp range
+    in
     let trace_pp fmt traces =
       if Config.bo_debug >= 1 then F.fprintf fmt ", %a" TraceSet.pp traces
     in
-    F.fprintf fmt "(%a%a%a, %a, %a%a%a%a)" Itv.pp x.itv itv_thresholds_pp x.itv_thresholds
+    F.fprintf fmt "(%a%a%a%a, %a, %a%a%a%a)" Itv.pp x.itv itv_thresholds_pp x.itv_thresholds
-      relation_sym_pp x.sym PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk relation_sym_pp x.offset_sym
+      relation_sym_pp x.sym modeled_range_pp x.modeled_range PowLoc.pp x.powloc ArrayBlk.pp
-      relation_sym_pp x.size_sym trace_pp x.traces
+      x.arrayblk relation_sym_pp x.offset_sym relation_sym_pp x.size_sym trace_pp x.traces
 
 
   let unknown_from : callee_pname:_ -> location:_ -> t =
@@ -73,6 +100,7 @@ module Val = struct
     let traces = Trace.(Set.singleton_final location (UnknownFrom callee_pname)) in
     { itv= Itv.top
     ; itv_thresholds= ItvThresholds.empty
+    ; modeled_range= ModeledRange.bottom
     ; sym= Relation.Sym.top
     ; powloc= PowLoc.unknown
     ; arrayblk= ArrayBlk.unknown
@@ -86,6 +114,7 @@ module Val = struct
     else
       Itv.( <= ) ~lhs:lhs.itv ~rhs:rhs.itv
       && ItvThresholds.( <= ) ~lhs:lhs.itv_thresholds ~rhs:rhs.itv_thresholds
+      && ModeledRange.( <= ) ~lhs:lhs.modeled_range ~rhs:rhs.modeled_range
       && Relation.Sym.( <= ) ~lhs:lhs.sym ~rhs:rhs.sym
       && PowLoc.( <= ) ~lhs:lhs.powloc ~rhs:rhs.powloc
       && ArrayBlk.( <= ) ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk
@@ -102,6 +131,8 @@ module Val = struct
             ~thresholds:(ItvThresholds.elements itv_thresholds)
             ~prev:prev.itv ~next:next.itv ~num_iters
       ; itv_thresholds
+      ; modeled_range=
+          ModeledRange.widen ~prev:prev.modeled_range ~next:next.modeled_range ~num_iters
       ; sym= Relation.Sym.widen ~prev:prev.sym ~next:next.sym ~num_iters
       ; powloc= PowLoc.widen ~prev:prev.powloc ~next:next.powloc ~num_iters
       ; arrayblk= ArrayBlk.widen ~prev:prev.arrayblk ~next:next.arrayblk ~num_iters
@@ -116,6 +147,7 @@ module Val = struct
     else
       { itv= Itv.join x.itv y.itv
       ; itv_thresholds= ItvThresholds.join x.itv_thresholds y.itv_thresholds
+      ; modeled_range= ModeledRange.join x.modeled_range y.modeled_range
       ; sym= Relation.Sym.join x.sym y.sym
       ; powloc= PowLoc.join x.powloc y.powloc
       ; arrayblk= ArrayBlk.join x.arrayblk y.arrayblk
@@ -126,6 +158,8 @@ module Val = struct
 
   let get_itv : t -> Itv.t = fun x -> x.itv
 
+  let get_modeled_range : t -> ModeledRange.t = fun x -> x.modeled_range
+
   let get_sym : t -> Relation.Sym.t = fun x -> x.sym
 
   let get_sym_var : t -> Relation.Var.t option = fun x -> Relation.Sym.get_var x.sym
@@ -189,6 +223,8 @@ module Val = struct
     of_itv (Itv.set_lb_zero (Itv.of_int max_char))
 
 
+  let set_modeled_range range x = {x with modeled_range= range}
+
   let unknown_bit : t -> t = fun x -> {x with itv= Itv.top; sym= Relation.Sym.top}
 
   let neg : t -> t = fun x -> {x with itv= Itv.neg x.itv; sym= Relation.Sym.top}
@@ -199,6 +235,7 @@ module Val = struct
    fun f ?f_trace x y ->
     let itv = f x.itv y.itv in
     let itv_thresholds = ItvThresholds.join x.itv_thresholds y.itv_thresholds in
+    let modeled_range = ModeledRange.join x.modeled_range y.modeled_range in
     let traces =
       match f_trace with
       | Some f_trace ->
@@ -212,7 +249,7 @@ module Val = struct
         | true, true | false, false ->
             TraceSet.join x.traces y.traces )
     in
-    {bot with itv; itv_thresholds; traces}
+    {bot with itv; itv_thresholds; modeled_range; traces}
 
 
   let lift_cmp_itv : (Itv.t -> Itv.t -> Boolean.t) -> Boolean.EqualOrder.t -> t -> t -> t =
@@ -632,7 +669,13 @@ module MemPure = struct
             let itv = Val.get_itv v in
             if Itv.has_only_non_int_symbols itv then acc
             else
-              let range1 = Itv.range loop_head_loc itv |> Itv.ItvRange.to_top_lifted_polynomial in
+              let range1 =
+                match Val.get_modeled_range v with
+                | NonBottom range ->
+                    Polynomials.NonNegativePolynomial.of_non_negative_bound range
+                | Bottom ->
+                    Itv.range loop_head_loc itv |> Itv.ItvRange.to_top_lifted_polynomial
+              in
               if Polynomials.NonNegativePolynomial.is_top range1 then
                 L.d_printfln_escaped "Range of %a (loc:%a) became top at %a." Itv.pp itv Loc.pp loc
                   ProcCfg.Normal.Node.pp_id node_id ;

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -1119,6 +1119,36 @@ module InputStream = struct
     {exec; check= no_check}
 end
 
+module FileChannel = struct
+  (* https://docs.oracle.com/javase/7/docs/api/java/io/InputStream.html#read(byte[],%20int,%20int) *)
+  let read buf_exp =
+    let exec {pname; location} ~ret:(ret_id, ret_typ) mem =
+      let buf_locs = Sem.eval_locs buf_exp mem in
+      let buf_v = Dom.Mem.find_set buf_locs mem in
+      let range =
+        Symb.SymbolPath.of_callsite ~ret_typ (CallSite.make pname location)
+        |> Bounds.Bound.of_modeled_path Symb.Symbol.make_onevalue
+        |> Dom.ModeledRange.of_modeled_function pname location
+      in
+      let mem = Dom.Mem.add_heap_set buf_locs (Dom.Val.set_modeled_range range buf_v) mem in
+      let v =
+        Dom.Val.of_itv (Itv.set_lb Itv.Bound.mone Itv.nat) |> Dom.Val.set_modeled_range range
+      in
+      model_by_value v ret_id mem
+    in
+    {exec; check= no_check}
+end
+
+module ByteBuffer = struct
+  let get_int buf_exp =
+    let exec _ ~ret:(ret_id, _) mem =
+      let range = Dom.Mem.find_set (Sem.eval_locs buf_exp mem) mem |> Dom.Val.get_modeled_range in
+      let v = Dom.Val.of_itv Itv.nat |> Dom.Val.set_modeled_range range in
+      model_by_value v ret_id mem
+    in
+    {exec; check= no_check}
+end
+
 module Call = struct
   let dispatch : (Tenv.t, model) ProcnameDispatcher.Call.dispatcher =
     let open ProcnameDispatcher.Call in
@@ -1350,5 +1380,13 @@ module Call = struct
         &:: "intValue" <>$ capt_exp $--> JavaInteger.intValue
       ; +PatternMatch.implements_lang "Integer" &:: "valueOf" <>$ capt_exp $--> JavaInteger.valueOf
       ; +PatternMatch.implements_io "InputStream"
-        &:: "read" <>$ any_arg $+ any_arg $+ any_arg $+ capt_exp $--> InputStream.read ]
+        &:: "read" <>$ any_arg $+ any_arg $+ any_arg $+ capt_exp $--> InputStream.read
+      ; +PatternMatch.implements_nio "channels.FileChannel"
+        &:: "read" <>$ any_arg $+ capt_exp $+ any_arg $--> FileChannel.read
+      ; +PatternMatch.implements_nio "ByteBuffer" &:: "get" <>$ capt_exp $--> ByteBuffer.get_int
+      ; +PatternMatch.implements_nio "ByteBuffer"
+        &:: "getShort" <>$ capt_exp $--> ByteBuffer.get_int
+      ; +PatternMatch.implements_nio "ByteBuffer" &:: "getInt" <>$ capt_exp $--> ByteBuffer.get_int
+      ; +PatternMatch.implements_nio "ByteBuffer"
+        &:: "getLong" <>$ capt_exp $--> ByteBuffer.get_int ]
 end

infer/tests/codetoanalyze/java/performance/Loops.java

@@ -6,6 +6,10 @@
  */
 package codetoanalyze.java.performance;
 
+import java.io.IOException;
+import java.nio.ByteBuffer;
+import java.nio.channels.FileChannel;
+
 public class Loops {
 
   static int do_while_independent_of_p(int p) {
@@ -110,4 +114,17 @@ public class Loops {
   void charsequence_length_linear(CharSequence seq) {
     for (int i = 0; i < seq.length(); i++) {}
   }
+
+  void modeled_range_linear(FileChannel fc, ByteBuffer bb) throws IOException {
+    int i;
+    int offset = 0;
+    do {
+      int numBytesRead = fc.read(bb, offset);
+      if (numBytesRead == -1) {
+        break;
+      }
+      i = bb.getInt();
+      offset += 8;
+    } while (i != 0);
+  }
 }

infer/tests/codetoanalyze/java/performance/issues.exp

@@ -150,18 +150,20 @@ codetoanalyze/java/performance/ListTest.java, ListTest.asList_linear(java.lang.S
 codetoanalyze/java/performance/ListTest.java, ListTest.indexOfImpl_linear(java.util.List,java.lang.Object):int, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 11 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 16,{list.length},Loop at line 16]
 codetoanalyze/java/performance/ListTest.java, ListTest.sort_comparator_nlogn(java.util.List):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 List.sort,{people.length},Modeled call to List.sort]
 codetoanalyze/java/performance/ListTest.java, ListTest.sublist(java.util.List):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 11 + 8 ⋅ (filesList.length - 1) + 3 ⋅ filesList.length, O(filesList.length), degree = 1,{filesList.length},Loop at line 30,{filesList.length - 1},Loop at line 30]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.charsequence_length_linear(java.lang.CharSequence):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ seq.length + 3 ⋅ (seq.length + 1), O(seq.length), degree = 1,{seq.length + 1},Loop at line 111,{seq.length},Loop at line 111]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.charsequence_length_linear(java.lang.CharSequence):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ seq.length + 3 ⋅ (seq.length + 1), O(seq.length), degree = 1,{seq.length + 1},Loop at line 115,{seq.length},Loop at line 115]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.do_while_independent_of_p(int):int, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 250, O(1), degree = 0]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 25 ⋅ (length - 1), O(length), degree = 1,{length - 1},Loop at line 40]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumb0(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 25 ⋅ (length - 1), O(length), degree = 1,{length - 1},Loop at line 44]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.dumbSort(long[],long[],int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + 59 ⋅ (length - 1) × (length - 1) + 8 ⋅ length, O(length × 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, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 + 59 ⋅ (length - 1) × (length - 1) + 8 ⋅ length, O(length × length), degree = 2,{length},Loop at line 54,{length - 1},Loop at line 55,{length - 1},Loop at line 54]
 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.linear(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x, O(x), degree = 1,{x},Loop at line 82]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.linear(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ x, O(x), degree = 1,{x},Loop at line 86]
-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 at line 30]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.modeled_range_linear(java.nio.channels.FileChannel,java.nio.ByteBuffer):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 14 ⋅ FileChannel.read(...).modeled, O(FileChannel.read(...).modeled), degree = 1,{FileChannel.read(...).modeled},Modeled call to read(...)]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.modeled_range_linear(java.nio.channels.FileChannel,java.nio.ByteBuffer):void, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,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 at line 34]
 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, no_bucket, ERROR, [with estimated cost 16 + 26 ⋅ x.length, O(x.length), degree = 1,{x.length},Loop at line 73]
+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, no_bucket, ERROR, [with estimated cost 16 + 26 ⋅ x.length, O(x.length), degree = 1,{x.length},Loop at line 77]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.string_concat_linear(java.lang.String,java.lang.String):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + 5 ⋅ (p.length + s.length) + 3 ⋅ (p.length + s.length + 1), O((p.length + s.length)), degree = 1,{p.length + s.length + 1},Loop at line 99,{p.length + s.length},Loop at line 99]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.string_concat_linear(java.lang.String,java.lang.String):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + 5 ⋅ (p.length + s.length) + 3 ⋅ (p.length + s.length + 1), O((p.length + s.length)), degree = 1,{p.length + s.length + 1},Loop at line 103,{p.length + s.length},Loop at line 103]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.string_length_linear(java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ s.length + 3 ⋅ (s.length + 1), O(s.length), degree = 1,{s.length + 1},Loop at line 94,{s.length},Loop at line 94]
+codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.string_length_linear(java.lang.String):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ s.length + 3 ⋅ (s.length + 1), O(s.length), degree = 1,{s.length + 1},Loop at line 98,{s.length},Loop at line 98]
-codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol():void, 0, INFINITE_EXECUTION_TIME, 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, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded value x,call to void Loops.linear(int),Loop at line 86]
 codetoanalyze/java/performance/Loops.java, codetoanalyze.java.performance.Loops.unboundedSymbol():void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6996, O(1), 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)` ]