[inferbo] Model Java collections using arrays

Reviewed By: ezgicicek, skcho

Differential Revision: D13190960

fbshipit-source-id: fba435f34

infer/src/bufferoverrun/arrayBlk.ml

@@ -180,6 +180,17 @@ module ArrInfo = struct
         Top
 
 
+  let transform_length : f:(Itv.t -> Itv.t) -> t -> t =
+   fun ~f arr ->
+    match arr with
+    | C {offset; size; stride} ->
+        C {offset; size= f size; stride}
+    | Java {length} ->
+        Java {length= f length}
+    | Top ->
+        Top
+
+
   (* Set new stride only when the previous stride is a constant interval. *)
   let set_stride : Z.t -> t -> t =
    fun new_stride arr ->
@@ -320,3 +331,7 @@ let lift_cmp_itv cmp_itv cmp_loc arr1 arr2 =
           (Allocsite.eq as1 as2))
   | _ ->
       Boolean.Top
+
+
+let transform_length : f:(Itv.t -> Itv.t) -> t -> t =
+ fun ~f a -> map (ArrInfo.transform_length ~f) a

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -45,15 +45,10 @@ module Init = struct
             ?stride ~inst_num ~represents_multiple_values ~dimension mem
       | Typ.Tstruct typname -> (
         match TypModels.dispatch tenv typname with
-        | Some typ_model -> (
-          match typ_model with
-          | CArray {element_typ; length} ->
-              BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc element_typ
-                ~length:(Some length) ~inst_num ~represents_multiple_values ~dimension mem
-          | JavaCollection ->
-              BoUtils.Exec.decl_local_collection pname ~node_hash location loc ~inst_num
-                ~represents_multiple_values ~dimension mem )
-        | None ->
+        | Some (CArray {element_typ; length}) ->
+            BoUtils.Exec.decl_local_array ~decl_local pname ~node_hash location loc element_typ
+              ~length:(Some length) ~inst_num ~represents_multiple_values ~dimension mem
+        | Some JavaCollection | None ->
             (mem, inst_num) )
       | _ ->
           (mem, inst_num)

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -352,6 +352,13 @@ module Val = struct
     ; traces= Trace.(Set.add_elem location ArrayDeclaration) length.traces }
 
 
+  let transform_array_length : Location.t -> f:(Itv.t -> Itv.t) -> t -> t =
+   fun location ~f v ->
+    { v with
+      arrayblk= ArrayBlk.transform_length ~f v.arrayblk
+    ; traces= Trace.(Set.add_elem location Through) v.traces }
+
+
   let set_array_stride : Z.t -> t -> t =
    fun new_stride v ->
     PhysEqual.optim1 v ~res:{v with arrayblk= ArrayBlk.set_stride new_stride v.arrayblk}
@@ -408,7 +415,14 @@ module Val = struct
           let offset = Itv.zero in
           let size = Itv.of_int_lit length in
           of_c_array_alloc allocsite ~stride:None ~offset ~size ~traces
-      | Some JavaCollection | None ->
+      | Some JavaCollection ->
+          let deref_path = SPath.deref ~deref_kind:Deref_ArrayIndex path in
+          let l = Loc.of_path deref_path in
+          let traces = TraceSet.singleton location (Trace.Parameter l) in
+          let allocsite = Allocsite.make_symbol deref_path in
+          let length = Itv.of_length_path path in
+          of_java_array_alloc allocsite ~length ~traces
+      | None ->
           let l = Loc.of_path path in
           let traces = TraceSet.singleton location (Trace.Parameter l) in
           of_loc ~traces l )
@@ -458,8 +472,6 @@ module Val = struct
 
     let nat = of_itv Itv.nat
 
-    let one = of_itv Itv.one
-
     let pos = of_itv Itv.pos
 
     let top = of_itv Itv.top

infer/src/bufferoverrun/bufferOverrunField.ml

@@ -10,20 +10,29 @@ module F = Format
 (**
   If fn is empty, prints [pp_lhs_alone lhs]
   Otherwise prints [pp_lhs lhs ^ sep ^ fn]
+
+  Create invisible phantom fields by giving them a name ending in '.'
+  The name preceeding the '.' will be used in debug mode.
 *)
 let pp ~pp_lhs ~pp_lhs_alone ~sep f lhs fn =
   let fieldname = Typ.Fieldname.to_flat_string fn in
-  if String.is_empty fieldname then pp_lhs_alone f lhs
+  if String.is_empty fieldname then
+    if Config.bo_debug > 0 then
+      let fieldname =
+        Option.value ~default:""
+          (Typ.Fieldname.to_simplified_string fn |> String.chop_suffix ~suffix:".")
+      in
+      F.fprintf f "%a%s%s" pp_lhs lhs sep fieldname
+    else pp_lhs_alone f lhs
   else F.fprintf f "%a%s%s" pp_lhs lhs sep fieldname
 
 
 let mk, get_type =
   let classname = "__infer__" in
   let types = ref Typ.Fieldname.Map.empty in
-  let mk name typ_desc =
+  let mk name typ =
     let fullname = Format.sprintf "%s.%s" classname name in
     let fieldname = Typ.Fieldname.Java.from_string fullname in
-    let typ = Typ.mk typ_desc in
     types := Typ.Fieldname.Map.add fieldname typ !types ;
     fieldname
   in
@@ -31,5 +40,4 @@ let mk, get_type =
   (mk, get_type)
 
 
-let java_collection_length =
-  mk "java.collection.length" Typ.(Tint IUInt (* wrong: we need IInt but with unsigned symbol *))
+let java_collection_internal_array = mk "java.collection.$elements." Typ.(mk_array void)

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -205,18 +205,19 @@ let infer_print e =
   {exec; check= no_check}
 
 
+let eval_array_locs_length arr_locs mem =
+  if PowLoc.is_empty arr_locs then Dom.Val.Itv.top
+  else
+    let arr = Dom.Mem.find_set arr_locs mem in
+    let traces = Dom.Val.get_traces arr in
+    let length = arr |> Dom.Val.get_array_blk |> ArrayBlk.sizeof in
+    Dom.Val.of_itv ~traces length
+
+
 (* Java only *)
 let get_array_length array_exp =
   let exec _ ~ret mem =
-    let arr_locs = Sem.eval_locs array_exp mem in
-    let result =
-      if PowLoc.is_empty arr_locs then Dom.Val.Itv.top
-      else
-        let arr = Dom.Mem.find_set arr_locs mem in
-        let traces = Dom.Val.get_traces arr in
-        let length = arr |> Dom.Val.get_array_blk |> ArrayBlk.sizeof in
-        Dom.Val.of_itv ~traces length
-    in
+    let result = eval_array_locs_length (Sem.eval_locs array_exp mem) mem in
     model_by_value result ret mem
   in
   {exec; check= no_check}
@@ -309,123 +310,133 @@ module StdArray = struct
     {exec; check= no_check}
 end
 
-(* Java's Collections are represented by their size. We don't care about the elements.
+(* Java's Collections are represented like arrays. But we don't care about the elements.
 - when they are constructed, we set the size to 0
 - each time we add an element, we increase the length of the array
 - each time we delete an element, we decrease the length of the array *)
 module Collection = struct
   let new_collection _ =
     let exec {pname; node_hash; location} ~ret:(id, _) mem =
-      let loc = Loc.of_id id in
-      let path = Option.bind (Dom.Mem.find_simple_alias id mem) ~f:Loc.get_path in
-      let allocsite =
-        Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path
-          ~represents_multiple_values:true
-      in
-      let alloc_loc = Loc.of_allocsite allocsite in
-      let init_length = Dom.Val.of_int 0 in
+      let represents_multiple_values = true in
       let traces = Trace.(Set.singleton location ArrayDeclaration) in
-      let v = Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) ~traces in
-      let length_loc = Loc.append_field alloc_loc ~fn:BufferOverrunField.java_collection_length in
-      mem |> Dom.Mem.add_stack loc v |> Dom.Mem.add_heap length_loc init_length
+      let coll_allocsite =
+        Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:1 ~path:None
+          ~represents_multiple_values
+      in
+      let internal_array =
+        let allocsite =
+          Allocsite.make pname ~node_hash ~inst_num:1 ~dimension:1 ~path:None
+            ~represents_multiple_values
+        in
+        Dom.Val.of_java_array_alloc allocsite ~length:Itv.zero ~traces
+      in
+      let coll_loc = Loc.of_allocsite coll_allocsite in
+      let internal_array_loc =
+        Loc.append_field coll_loc ~fn:BufferOverrunField.java_collection_internal_array
+      in
+      mem
+      |> Dom.Mem.add_heap internal_array_loc internal_array
+      |> Dom.Mem.add_stack (Loc.of_id id)
+           (coll_loc |> PowLoc.singleton |> Dom.Val.of_pow_loc ~traces)
     in
     {exec; check= no_check}
 
 
-  let change_size_by ~size_f collection_id _ ~ret:_ mem =
-    let collection_v = Dom.Mem.find (Loc.of_id collection_id) mem in
-    let collection_locs = Dom.Val.get_pow_loc collection_v in
-    let length_locs =
-      PowLoc.append_field collection_locs ~fn:BufferOverrunField.java_collection_length
-    in
-    Dom.Mem.transform_mem ~f:size_f length_locs mem
+  let eval_collection_internal_array_locs coll_exp mem =
+    Sem.eval_locs coll_exp mem
+    |> PowLoc.append_field ~fn:BufferOverrunField.java_collection_internal_array
+
 
+  let get_collection_internal_array_locs coll_id mem =
+    let coll = Dom.Mem.find (Loc.of_id coll_id) mem in
+    Dom.Val.get_pow_loc coll
+    |> PowLoc.append_field ~fn:BufferOverrunField.java_collection_internal_array
 
-  let incr_size = Dom.Val.plus_a Dom.Val.Itv.one
 
-  let decr_size size = Dom.Val.minus_a size Dom.Val.Itv.one
+  let eval_collection_length coll_exp mem =
+    let arr_locs = eval_collection_internal_array_locs coll_exp mem in
+    eval_array_locs_length arr_locs mem
 
-  let add alist_id = {exec= change_size_by ~size_f:incr_size alist_id; check= no_check}
 
-  let get_size integer_type_widths alist mem =
-    BoUtils.Exec.get_java_collection_length (Sem.eval integer_type_widths alist mem) mem
+  let change_size_by ~size_f coll_id {location} ~ret:_ mem =
+    Dom.Mem.transform_mem
+      ~f:(Dom.Val.transform_array_length location ~f:size_f)
+      (get_collection_internal_array_locs coll_id mem)
+      mem
 
 
-  let size array_exp =
-    let exec {integer_type_widths} ~ret mem =
-      let size = get_size integer_type_widths array_exp mem in
-      model_by_value size ret mem
+  let add coll_id = {exec= change_size_by ~size_f:Itv.incr coll_id; check= no_check}
+
+  let size coll_exp =
+    let exec _ ~ret mem =
+      let result = eval_collection_length coll_exp mem in
+      model_by_value result ret mem
     in
     {exec; check= no_check}
 
 
-  let iterator alist =
+  let iterator coll_exp =
     let exec {integer_type_widths} ~ret mem =
-      let itr = Sem.eval integer_type_widths alist mem in
+      let itr = Sem.eval integer_type_widths coll_exp mem in
       model_by_value itr ret mem
     in
     {exec; check= no_check}
 
 
   let hasNext iterator =
-    let exec {integer_type_widths} ~ret mem =
+    let exec _ ~ret mem =
       (* Set the size of the iterator to be [0, size-1], so that range
          will be size of the collection. *)
-      let collection_size =
-        get_size integer_type_widths iterator mem |> Dom.Val.get_iterator_itv
-      in
+      let collection_size = eval_collection_length iterator mem |> Dom.Val.get_iterator_itv in
       model_by_value collection_size ret mem
     in
     {exec; check= no_check}
 
 
-  let addAll alist_id alist_to_add =
-    let exec ({integer_type_widths} as model_env) ~ret mem =
-      let to_add_length = get_size integer_type_widths alist_to_add mem in
-      change_size_by ~size_f:(Dom.Val.plus_a to_add_length) alist_id model_env ~ret mem
+  let addAll coll_id coll_to_add =
+    let exec model_env ~ret mem =
+      let to_add_length = eval_collection_length coll_to_add mem |> Dom.Val.get_itv in
+      change_size_by ~size_f:(Itv.plus to_add_length) coll_id model_env ~ret mem
     in
     {exec; check= no_check}
 
 
-  let add_at_index (alist_id : Ident.t) index_exp =
-    let check {location; integer_type_widths} mem cond_set =
-      let array_exp = Exp.Var alist_id in
-      BoUtils.Check.collection_access integer_type_widths ~array_exp ~index_exp ~last_included:true
-        mem location cond_set
+  let check_index ~last_included coll_id index_exp {location; integer_type_widths} mem cond_set =
+    let arr =
+      let arr_locs = get_collection_internal_array_locs coll_id mem in
+      Dom.Mem.find_set arr_locs mem
+    in
+    let idx = Sem.eval integer_type_widths index_exp mem in
+    let idx_sym_exp =
+      Relation.SymExp.of_exp ~get_sym_f:(Sem.get_sym_f integer_type_widths mem) index_exp
     in
-    {exec= change_size_by ~size_f:incr_size alist_id; check}
+    let relation = Dom.Mem.get_relation mem in
+    let latest_prune = Dom.Mem.get_latest_prune mem in
+    BoUtils.Check.array_access ~arr ~idx ~idx_sym_exp ~relation ~is_plus:true ~last_included
+      ~latest_prune location cond_set
 
 
-  let remove_at_index alist_id index_exp =
-    let check {location; integer_type_widths} mem cond_set =
-      let array_exp = Exp.Var alist_id in
-      BoUtils.Check.collection_access integer_type_widths ~array_exp ~index_exp
-        ~last_included:false mem location cond_set
-    in
-    {exec= change_size_by ~size_f:decr_size alist_id; check}
+  let add_at_index (coll_id : Ident.t) index_exp =
+    { exec= change_size_by ~size_f:Itv.incr coll_id
+    ; check= check_index ~last_included:true coll_id index_exp }
 
 
-  let addAll_at_index alist_id index_exp alist_to_add =
-    let exec ({integer_type_widths} as model_env) ~ret mem =
-      let to_add_length = get_size integer_type_widths alist_to_add mem in
-      change_size_by ~size_f:(Dom.Val.plus_a to_add_length) alist_id model_env ~ret mem
-    in
-    let check {location; integer_type_widths} mem cond_set =
-      let array_exp = Exp.Var alist_id in
-      BoUtils.Check.collection_access integer_type_widths ~index_exp ~array_exp ~last_included:true
-        mem location cond_set
+  let remove_at_index coll_id index_exp =
+    { exec= change_size_by ~size_f:Itv.decr coll_id
+    ; check= check_index ~last_included:false coll_id index_exp }
+
+
+  let addAll_at_index coll_id index_exp coll_to_add =
+    let exec model_env ~ret mem =
+      let to_add_length = eval_collection_length coll_to_add mem |> Dom.Val.get_itv in
+      change_size_by ~size_f:(Itv.plus to_add_length) coll_id model_env ~ret mem
     in
-    {exec; check}
+    {exec; check= check_index ~last_included:true coll_id index_exp}
 
 
-  let get_or_set_at_index alist_id index_exp =
+  let get_or_set_at_index coll_id index_exp =
     let exec _model_env ~ret:_ mem = mem in
-    let check {location; integer_type_widths} mem cond_set =
-      let array_exp = Exp.Var alist_id in
-      BoUtils.Check.collection_access integer_type_widths ~index_exp ~array_exp
-        ~last_included:false mem location cond_set
-    in
-    {exec; check}
+    {exec; check= check_index ~last_included:false coll_id index_exp}
 end
 
 module Call = struct

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -17,14 +17,6 @@ module Trace = BufferOverrunTrace
 module TraceSet = Trace.Set
 
 module Exec = struct
-  let get_java_collection_length alist mem =
-    let collection_locs = Dom.Val.get_pow_loc alist in
-    let length_locs =
-      PowLoc.append_field collection_locs ~fn:BufferOverrunField.java_collection_length
-    in
-    Dom.Mem.find_set length_locs mem
-
-
   let load_locs id locs mem =
     let v = Dom.Mem.find_set locs mem in
     let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in
@@ -95,39 +87,6 @@ module Exec = struct
     (mem, inst_num + 1)
 
 
-  let decl_local_collection :
-         Typ.Procname.t
-      -> node_hash:int
-      -> Location.t
-      -> Loc.t
-      -> inst_num:int
-      -> represents_multiple_values:bool
-      -> dimension:int
-      -> Dom.Mem.t
-      -> Dom.Mem.t * int =
-   fun pname ~node_hash location loc ~inst_num ~represents_multiple_values ~dimension mem ->
-    let path = Loc.get_path loc in
-    let allocsite =
-      Allocsite.make pname ~node_hash ~inst_num ~dimension ~path ~represents_multiple_values:true
-    in
-    let alloc_loc = Loc.of_allocsite allocsite in
-    let traces = Trace.(Set.singleton location ArrayDeclaration) in
-    let mem =
-      let collection =
-        Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) ~traces
-        |> Dom.Val.sets_represents_multiple_values ~represents_multiple_values
-      in
-      if Int.equal dimension 1 then Dom.Mem.add_stack loc collection mem
-      else
-        let length = Dom.Val.of_itv ~traces Itv.zero in
-        let length_loc =
-          Loc.append_field alloc_loc ~fn:BufferOverrunField.java_collection_length
-        in
-        Dom.Mem.add_heap loc collection mem |> Dom.Mem.add_heap length_loc length
-    in
-    (mem, inst_num + 1)
-
-
   let init_c_array_fields tenv integer_type_widths pname path ~node_hash typ locs ?dyn_length mem =
     let rec init_field path locs dimension ?dyn_length (mem, inst_num) (field_name, field_typ, _) =
       let field_path = Option.map path ~f:(fun path -> Symb.SymbolPath.field path field_name) in
@@ -261,19 +220,6 @@ module Check = struct
       ~latest_prune location cond_set
 
 
-  let collection_access integer_type_widths ~array_exp ~index_exp ~last_included mem location
-      cond_set =
-    let idx = Sem.eval integer_type_widths index_exp mem in
-    let arr = Sem.eval integer_type_widths array_exp mem in
-    let idx_traces = Dom.Val.get_traces idx in
-    let size = Exec.get_java_collection_length arr mem |> Dom.Val.get_itv in
-    let idx = Dom.Val.get_itv idx in
-    let relation = Dom.Mem.get_relation mem in
-    let latest_prune = Dom.Mem.get_latest_prune mem in
-    check_access ~size ~idx ~size_sym_exp:None ~idx_sym_exp:None ~relation ~arr ~idx_traces
-      ~last_included ~latest_prune location cond_set
-
-
   let lindex integer_type_widths ~array_exp ~index_exp ~last_included mem location cond_set =
     let idx = Sem.eval integer_type_widths index_exp mem in
     let arr = Sem.eval_arr integer_type_widths array_exp mem in

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -12,8 +12,6 @@ module Relation = BufferOverrunDomainRelation
 module PO = BufferOverrunProofObligations
 
 module Exec : sig
-  val get_java_collection_length : Dom.Val.t -> Dom.Mem.t -> Dom.Val.t
-
   val load_locs : Ident.t -> PowLoc.t -> Dom.Mem.t -> Dom.Mem.t
 
   val load_val : Ident.t -> Dom.Val.t -> Dom.Mem.t -> Dom.Mem.t
@@ -45,17 +43,6 @@ module Exec : sig
     -> Dom.Mem.t
     -> Dom.Mem.t * int
 
-  val decl_local_collection :
-       Typ.Procname.t
-    -> node_hash:int
-    -> Location.t
-    -> Loc.t
-    -> inst_num:int
-    -> represents_multiple_values:bool
-    -> dimension:int
-    -> Dom.Mem.t
-    -> Dom.Mem.t * int
-
   val init_c_array_fields :
        Tenv.t
     -> Typ.IntegerWidths.t
@@ -114,16 +101,6 @@ module Check : sig
     -> PO.ConditionSet.checked_t
     -> PO.ConditionSet.checked_t
 
-  val collection_access :
-       Typ.IntegerWidths.t
-    -> array_exp:Exp.t
-    -> index_exp:Exp.t
-    -> last_included:bool
-    -> Dom.Mem.t
-    -> Location.t
-    -> PO.ConditionSet.checked_t
-    -> PO.ConditionSet.checked_t
-
   val binary_operation :
        Typ.IntegerWidths.t
     -> Binop.t

infer/src/bufferoverrun/itv.ml

@@ -553,6 +553,10 @@ let plus : t -> t -> t = lift2 ItvPure.plus
 
 let minus : t -> t -> t = lift2 ItvPure.minus
 
+let incr = plus one
+
+let decr x = minus x one
+
 let get_iterator_itv : t -> t = lift1 ItvPure.get_iterator_itv
 
 let is_const : t -> Z.t option = bind1zo ItvPure.is_const

infer/src/bufferoverrun/itv.mli

@@ -147,6 +147,10 @@ val get_bound : t -> Symb.BoundEnd.t -> Bound.t bottom_lifted
 
 val is_false : t -> bool
 
+val decr : t -> t
+
+val incr : t -> t
+
 val neg : t -> t
 
 val normalize : t -> t

infer/tests/codetoanalyze/java/bufferoverrun/Array.java

@@ -15,14 +15,9 @@ class Array {
     a.add(0, 100);
   }
 
-  ArrayList collection_add_zero_Bad() {
+  ArrayList collection_remove_from_empty_Bad() {
     ArrayList b = new ArrayList<>();
     b.remove(0);
     return b;
   }
-
-  void collection_add_zero2_Good() {
-    ArrayList b = collection_add_zero_Bad();
-    b.add(0, 100);
-  }
 }

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

@@ -1,2 +1,2 @@
-codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_add_zero_Bad():java.util.ArrayList, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
+codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_remove_from_empty_Bad():java.util.ArrayList, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: 0]
 codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy.ub - 1] × d.cci[*].s):signed32]

infer/tests/codetoanalyze/java/performance/CollectionTest.java

@@ -21,9 +21,9 @@ public class CollectionTest {
     for (MyCollection<Integer> list : mSubscribers) {}
   }
 
-  // Expected |mSubscribers| * |list| but we get T
+  // Expected |mSubscribers| * |list| but we get |mSubscribers|
   // because we are not tracking elements of collections
-  void iterate_over_mycollection_quad_FP(
+  void iterate_over_mycollection_quad_FN(
       ConcurrentLinkedQueue<MyCollection<Integer>> mSubscribers) {
     for (MyCollection<Integer> list : mSubscribers) {
       iterate_over_mycollection(list);

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

@@ -8,23 +8,23 @@ codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):bool
 codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 4, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 884, degree = 0]
 codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 883, degree = 0]
 codetoanalyze/java/performance/ArrayCost.java, ArrayCost.isPowOfTwo_FP(int):boolean, 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 890, degree = 0]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add3_overrun_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,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,Assignment,Array access: Offset added: 5 Size: 4]
+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, []
 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_add_in_loop_ok():void, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 202, degree = 0]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_add_in_loop_ok():void, 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201, degree = 0]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_empty_overrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,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,Assignment,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,Assignment,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,Assignment,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,Assignment,Array access: Offset: 1 Size: 1]
+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, []
 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,Assignment,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,Assignment,Array access: Offset: 1 Size: 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 1 Size: 1]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]
+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]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Through,Array access: Offset: 1 Size: 1]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_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.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length.ub, degree = 1]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length.ub, degree = 1]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 13 ⋅ (list.length.ub - 1) + 2 ⋅ (list.length.ub - 1) × (-Integer.intValue().lb + 11) + 4 ⋅ list.length.ub × (-Integer.intValue().lb + 11), degree = 2]
@@ -53,8 +53,8 @@ codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_
 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 6 + 21 ⋅ (list.length.ub - 1) + 5 ⋅ (list.length.ub - 1) × list.length.ub + 4 ⋅ list.length.ub, degree = 2]
 codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length.ub, degree = 1]
 codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length.ub, degree = 1]
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FP(java.util.concurrent.ConcurrentLinkedQueue):void, 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
-codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FP(java.util.concurrent.ConcurrentLinkedQueue):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32 by call to `void CollectionTest.iterate_over_mycollection(CollectionTest$MyCollection)` ]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FN(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 21 ⋅ (mSubscribers.length.ub - 1) + 4 ⋅ mSubscribers.length.ub, degree = 1]
+codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_mycollection_quad_FN(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 21 ⋅ (mSubscribers.length.ub - 1) + 4 ⋅ mSubscribers.length.ub, degree = 1]
 codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 9 ⋅ (mSubscribers.length.ub - 1) + 4 ⋅ mSubscribers.length.ub, degree = 1]
 codetoanalyze/java/performance/CollectionTest.java, CollectionTest.iterate_over_some_java_collection(java.util.concurrent.ConcurrentLinkedQueue):void, 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 9 ⋅ (mSubscribers.length.ub - 1) + 4 ⋅ mSubscribers.length.ub, degree = 1]
 codetoanalyze/java/performance/CollectionTest.java, CollectionTest.loop_over_call(int,CollectionTest$MyCollection):void, 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 17 ⋅ size.ub + 5 ⋅ size.ub × list.length.ub, degree = 2]