Add support for Java's ArrayLists.add*

Reviewed By: mbouaziz

Differential Revision: D8806285

fbshipit-source-id: 34c2838ac

infer/src/IR/ProcnameDispatcher.ml

@@ -450,6 +450,14 @@ module Call = struct
     let typ (_, ty) = ty
 
     let exp (e, _) = e
+
+    let get_var_exn arg =
+      match exp arg with
+      | Exp.Var v ->
+          v
+      | e ->
+          Logging.(die InternalError)
+            "Expected Lvar, got %a:%a" Exp.pp e (Typ.pp Pp.text) (typ arg)
   end
 
   type ('f_in, 'f_out, 'captured_types) proc_matcher =
@@ -684,6 +692,13 @@ module Call = struct
     {get_captured_value; do_capture}
 
 
+  (** Capture the argument local var or fail *)
+  let capture_arg_var_exn : (Ident.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f) arg_capture =
+    let get_captured_value arg = FuncArg.get_var_exn arg in
+    let do_capture f v = f v in
+    {get_captured_value; do_capture}
+
+
   let mandatory_arg =
     let on_empty _do_capture _f = None in
     let wrapper = Fn.id in
@@ -728,6 +743,10 @@ module Call = struct
     {one_arg_matcher= match_any_arg; capture= capture_arg_exp}
 
 
+  let capt_var_exn : (Ident.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg =
+    {one_arg_matcher= match_any_arg; capture= capture_arg_var_exn}
+
+
   let capt_arg_of_typ m = {one_arg_matcher= match_typ (m <...>! ()); capture= capture_arg}
 
   let capt_exp_of_typ m = {one_arg_matcher= match_typ (m <...>! ()); capture= capture_arg_exp}

infer/src/IR/ProcnameDispatcher.mli

@@ -217,6 +217,9 @@ module Call : sig
     -> (Exp.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg
   (** Captures one arg expression of the given type *)
 
+  val capt_var_exn : (Ident.t, 'wrapped_arg, 'wrapped_arg -> 'f, 'f, _, _) one_arg
+  (** Captures one arg Var. Fails with an internal error if the expression is not a Var *)
+
   val typ1 : 'marker -> (unit, _, 'f, 'f, 'marker mtyp * _, 'marker * _) one_arg
   (** Matches first captured type *)
 

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -57,6 +57,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
               |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
             in
             Dom.Mem.add_heap loc v mem
+        (* Temporary fix for ArrayLists in Java, need a better way to handle parameters, see T31498711 *)
+        | Typ.Tptr (typ, _)
+          when Language.curr_language_is Java ->
+            decl_sym_val pname path tenv ~node_hash location ~depth ~may_last_field loc typ mem
         | Typ.Tptr (typ, _) ->
             BoUtils.Exec.decl_sym_arr ~decl_sym_val:(decl_sym_val ~may_last_field) pname path tenv
               ~node_hash location ~depth loc typ ~inst_num ~new_sym_num ~new_alloc_num mem
@@ -279,6 +283,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                   declare_local ~decl_local model_env loc ~inst_num ~dimension mem
               | None ->
                   (mem, inst_num) )
+            (* Temporary fix for ArrayLists in Java, need a better
+                 way to handle local vars, see T31498711 *)
+            | Typ.Tptr (typ, _)
+              when Language.curr_language_is Java ->
+                decl_local pname ~node_hash location loc typ ~inst_num ~dimension mem
             | _ ->
                 (mem, inst_num)
           in

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -244,9 +244,11 @@ module Val = struct
 
 
   module Itv = struct
+    let m1_255 = of_itv Itv.m1_255
+
     let nat = of_itv Itv.nat
 
-    let m1_255 = of_itv Itv.m1_255
+    let one = of_itv Itv.one
 
     let top = of_itv Itv.top
 

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -290,6 +290,82 @@ module StdArray = struct
     {declare_local; declare_symbolic}
 end
 
+(* Java's ArrayLists are represented by their size. 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 ArrayList = struct
+  let typ =
+    let declare_local ~decl_local:_ {pname; node_hash; location} loc ~inst_num ~dimension mem =
+      BoUtils.Exec.decl_local_arraylist pname ~node_hash location loc ~inst_num ~dimension mem
+    in
+    let declare_symbolic ~decl_sym_val:_ path {pname; node_hash; location} ~depth:_ loc ~inst_num
+        ~new_sym_num ~new_alloc_num mem =
+      BoUtils.Exec.decl_sym_arraylist pname path ~node_hash location loc ~inst_num ~new_sym_num
+        ~new_alloc_num mem
+    in
+    {declare_local; declare_symbolic}
+
+
+  let new_list _ =
+    let exec {pname; node_hash; location} ~ret:(id, _) mem =
+      let loc = Loc.of_id id in
+      let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num:0 ~dimension:1 in
+      let alloc_loc = Loc.of_allocsite allocsite in
+      let init_size = Dom.Val.of_int 0 in
+      let traces = TraceSet.add_elem (Trace.ArrDecl location) (Dom.Val.get_traces init_size) in
+      let v = Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) |> Dom.Val.set_traces traces in
+      mem |> Dom.Mem.add_stack loc v |> Dom.Mem.add_heap alloc_loc init_size
+    in
+    {exec; check= no_check}
+
+
+  let increment_size_by extra_size alist_id _ ~ret:_ mem =
+    let alist_v = Dom.Mem.find_stack (Loc.of_id alist_id) mem in
+    let locs = Dom.Val.get_pow_loc alist_v in
+    Dom.Mem.transform_mem ~f:(fun a -> Dom.Val.plus_a a extra_size) locs mem
+
+
+  let add alist_id = {exec= increment_size_by Dom.Val.Itv.one alist_id; check= no_check}
+
+  let get_size alist mem = BoUtils.Exec.get_alist_size (Sem.eval alist mem) mem
+
+  let size array_exp =
+    let exec _ ~ret mem =
+      let size = get_size array_exp mem in
+      model_by_value size ret mem
+    in
+    {exec; check= no_check}
+
+
+  let addAll alist_id alist_to_add =
+    let exec _model_env ~ret mem =
+      let to_add_length = get_size alist_to_add mem in
+      increment_size_by to_add_length alist_id _model_env ~ret mem
+    in
+    {exec; check= no_check}
+
+
+  let add_at_index (alist_id: Ident.t) index_exp =
+    let check {pname; location} mem cond_set =
+      let array_exp = Exp.Var alist_id in
+      BoUtils.Check.lindex ~array_exp ~index_exp ~is_arraylist_add:true mem pname location cond_set
+    in
+    {exec= increment_size_by Dom.Val.Itv.one alist_id; check}
+
+
+  let addAll_at_index alist_id index_exp alist_to_add =
+    let exec _model_env ~ret mem =
+      let to_add_length = get_size alist_to_add mem in
+      increment_size_by to_add_length alist_id _model_env ~ret mem
+    in
+    let check {pname; location} mem cond_set =
+      let array_exp = Exp.Var alist_id in
+      BoUtils.Check.lindex ~array_exp ~is_arraylist_add:true ~index_exp mem pname location cond_set
+    in
+    {exec; check}
+end
+
 module Call = struct
   let dispatch : model ProcnameDispatcher.Call.dispatcher =
     let open ProcnameDispatcher.Call in
@@ -304,6 +380,7 @@ module Call = struct
       ; -"fgetc" <>--> by_value Dom.Val.Itv.m1_255
       ; -"infer_print" <>$ capt_exp $!--> infer_print
       ; -"malloc" <>$ capt_exp $+...$--> malloc
+      ; -"__new" <>$ capt_exp_of_typ (-"java.util.ArrayList") $+...$--> ArrayList.new_list
       ; -"__new" <>$ capt_exp $+...$--> malloc
       ; -"__new_array" <>$ capt_exp $+...$--> malloc
       ; -"__placement_new" <>$ any_arg $+ capt_exp $!--> placement_new
@@ -319,7 +396,13 @@ module Call = struct
       ; std_array2 >:: "at" $ capt_arg $+ capt_arg $!--> StdArray.at
       ; std_array2 >:: "operator[]" $ capt_arg $+ capt_arg $!--> StdArray.at
       ; -"std" &:: "array" &::.*--> StdArray.no_model
-      ; -"java.util.ArrayList" &:: "size" <>$ capt_exp $!--> get_array_length ]
+      ; -"java.util.ArrayList" &:: "add" <>$ capt_var_exn $+ any_arg $--> ArrayList.add
+      ; -"java.util.ArrayList" &:: "add" <>$ capt_var_exn $+ capt_exp $+ any_arg
+        $!--> ArrayList.add_at_index
+      ; -"java.util.ArrayList" &:: "addAll" <>$ capt_var_exn $+ capt_exp $--> ArrayList.addAll
+      ; -"java.util.ArrayList" &:: "addAll" <>$ capt_var_exn $+ capt_exp $+ capt_exp
+        $!--> ArrayList.addAll_at_index
+      ; -"java.util.ArrayList" &:: "size" <>$ capt_exp $!--> ArrayList.size ]
 end
 
 module TypName = struct
@@ -327,5 +410,6 @@ module TypName = struct
     let open ProcnameDispatcher.TypName in
     make_dispatcher
       [ -"std" &:: "array" < capt_typ `T &+ capt_int >--> StdArray.typ
+      ; -"java.util.ArrayList" &::.*--> ArrayList.typ
       ; -"std" &:: "array" &::.*--> StdArray.no_typ_model ]
 end

infer/src/bufferoverrun/bufferOverrunProofObligations.ml

@@ -201,12 +201,16 @@ module ArrayAccessCondition = struct
 
 
   (* check buffer overrun and return its confidence *)
-  let check : t -> checked_condition =
-   fun c ->
-    (* idx = [il, iu], size = [sl, su], we want to check that 0 <= idx < size *)
+  let check : is_arraylist_add:bool -> t -> checked_condition =
+   fun ~is_arraylist_add c ->
+    (* idx = [il, iu], size = [sl, su], 
+       For arrays : we want to check that 0 <= idx < size
+       For adding into arraylists: we want to check that 0 <= idx <= size *)
     let c' = set_size_pos c in
     (* if sl < 0, use sl' = 0 *)
-    let not_overrun = ItvPure.lt_sem c'.idx c'.size in
+    let not_overrun =
+      if is_arraylist_add then ItvPure.le_sem c'.idx c'.size else ItvPure.lt_sem c'.idx c'.size
+    in
     let not_underrun = ItvPure.le_sem ItvPure.zero c'.idx in
     (* il >= 0 and iu < sl, definitely not an error *)
     if Itv.Boolean.is_true not_overrun && Itv.Boolean.is_true not_underrun then
@@ -245,43 +249,48 @@ module ArrayAccessCondition = struct
 end
 
 module Condition = struct
-  type t = AllocSize of AllocSizeCondition.t | ArrayAccess of ArrayAccessCondition.t
+  type t =
+    | AllocSize of AllocSizeCondition.t
+    | ArrayAccess of {is_arraylist_add: bool; c: ArrayAccessCondition.t}
 
   let make_alloc_size = Option.map ~f:(fun c -> AllocSize c)
 
-  let make_array_access = Option.map ~f:(fun c -> ArrayAccess c)
+  let make_array_access ~is_arraylist_add =
+    Option.map ~f:(fun c -> ArrayAccess {is_arraylist_add; c})
+
 
   let get_symbols = function
     | AllocSize c ->
         AllocSizeCondition.get_symbols c
-    | ArrayAccess c ->
+    | ArrayAccess {c} ->
         ArrayAccessCondition.get_symbols c
 
 
   let subst bound_map = function
     | AllocSize c ->
         AllocSizeCondition.subst bound_map c |> make_alloc_size
-    | ArrayAccess c ->
-        ArrayAccessCondition.subst bound_map c |> make_array_access
+    | ArrayAccess {is_arraylist_add; c} ->
+        ArrayAccessCondition.subst bound_map c |> make_array_access ~is_arraylist_add
 
 
   let have_similar_bounds c1 c2 =
     match (c1, c2) with
     | AllocSize c1, AllocSize c2 ->
         AllocSizeCondition.have_similar_bounds c1 c2
-    | ArrayAccess c1, ArrayAccess c2 ->
+    | ArrayAccess {c= c1}, ArrayAccess {c= c2} ->
         ArrayAccessCondition.have_similar_bounds c1 c2
     | _ ->
         false
 
 
-  let has_infty = function ArrayAccess c -> ArrayAccessCondition.has_infty c | _ -> false
+  let has_infty = function ArrayAccess {c} -> ArrayAccessCondition.has_infty c | _ -> false
 
   let xcompare ~lhs ~rhs =
     match (lhs, rhs) with
     | AllocSize lhs, AllocSize rhs ->
         AllocSizeCondition.xcompare ~lhs ~rhs
-    | ArrayAccess lhs, ArrayAccess rhs ->
+    | ArrayAccess {is_arraylist_add= b1; c= lhs}, ArrayAccess {is_arraylist_add= b2; c= rhs}
+      when Bool.equal b1 b2 ->
         ArrayAccessCondition.xcompare ~lhs ~rhs
     | _ ->
         `NotComparable
@@ -290,22 +299,22 @@ module Condition = struct
   let pp fmt = function
     | AllocSize c ->
         AllocSizeCondition.pp fmt c
-    | ArrayAccess c ->
+    | ArrayAccess {c} ->
         ArrayAccessCondition.pp fmt c
 
 
   let pp_description fmt = function
     | AllocSize c ->
         AllocSizeCondition.pp_description fmt c
-    | ArrayAccess c ->
+    | ArrayAccess {c} ->
         ArrayAccessCondition.pp_description fmt c
 
 
   let check = function
     | AllocSize c ->
         AllocSizeCondition.check c
-    | ArrayAccess c ->
-        ArrayAccessCondition.check c
+    | ArrayAccess {is_arraylist_add; c} ->
+        ArrayAccessCondition.check ~is_arraylist_add c
 end
 
 module ConditionTrace = struct
@@ -486,8 +495,8 @@ module ConditionSet = struct
         join [cwt] condset
 
 
-  let add_array_access pname location ~idx ~size val_traces condset =
-    ArrayAccessCondition.make ~idx ~size |> Condition.make_array_access
+  let add_array_access pname location ~idx ~size ~is_arraylist_add val_traces condset =
+    ArrayAccessCondition.make ~idx ~size |> Condition.make_array_access ~is_arraylist_add
     |> add_opt pname location val_traces condset
 
 

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -16,6 +16,11 @@ module Trace = BufferOverrunTrace
 module TraceSet = Trace.Set
 
 module Exec = struct
+  let get_alist_size alist mem =
+    let size_powloc = Dom.Val.get_pow_loc alist in
+    Dom.Mem.find_heap_set size_powloc mem
+
+
   let load_val id val_ mem =
     let locs = val_ |> Dom.Val.get_all_locs in
     let v = Dom.Mem.find_heap_set locs mem in
@@ -48,6 +53,24 @@ module Exec = struct
     (mem, inst_num + 1)
 
 
+  let decl_local_arraylist
+      : Typ.Procname.t -> node_hash:int -> Location.t -> Loc.t -> inst_num:int -> dimension:int
+        -> Dom.Mem.astate -> Dom.Mem.astate * int =
+   fun pname ~node_hash location loc ~inst_num ~dimension mem ->
+    let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension in
+    let alloc_loc = Loc.of_allocsite allocsite in
+    let alist =
+      Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc)
+      |> Dom.Val.add_trace_elem (Trace.ArrDecl location)
+    in
+    let size = Dom.Val.of_int 0 in
+    let mem =
+      if Int.equal dimension 1 then Dom.Mem.add_stack loc alist mem
+      else Dom.Mem.add_heap loc alist mem |> Dom.Mem.add_heap alloc_loc size
+    in
+    (mem, inst_num + 1)
+
+
   type decl_sym_val =
     Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t -> node_hash:int -> Location.t -> depth:int
     -> Loc.t -> Typ.t -> Dom.Mem.astate -> Dom.Mem.astate
@@ -82,6 +105,22 @@ module Exec = struct
     decl_sym_val pname path tenv ~node_hash location ~depth deref_loc typ mem
 
 
+  let decl_sym_arraylist
+      : Typ.Procname.t -> Itv.SymbolPath.partial -> node_hash:int -> Location.t -> Loc.t
+        -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t
+        -> Dom.Mem.astate -> Dom.Mem.astate =
+   fun pname path ~node_hash location loc ~inst_num ~new_sym_num ~new_alloc_num mem ->
+    let alloc_num = Itv.Counter.next new_alloc_num in
+    let allocsite = Sem.get_allocsite pname ~node_hash ~inst_num ~dimension:alloc_num in
+    let alloc_loc = Loc.of_allocsite allocsite in
+    let size =
+      Itv.make_sym ~unsigned:true pname (Itv.SymbolPath.length path) new_sym_num |> Dom.Val.of_itv
+      |> Dom.Val.add_trace_elem (Trace.SymAssign (loc, location))
+    in
+    let alist = Dom.Val.of_pow_loc (PowLoc.singleton alloc_loc) in
+    mem |> Dom.Mem.add_heap loc alist |> Dom.Mem.add_heap alloc_loc size
+
+
   let init_array_fields tenv pname ~node_hash typ locs ?dyn_length mem =
     let rec init_field locs dimension ?dyn_length (mem, inst_num) (field_name, field_typ, _) =
       let field_loc = PowLoc.append_field locs ~fn:field_name in
@@ -141,28 +180,41 @@ module Exec = struct
 end
 
 module Check = struct
+  let check_access ~size ~idx ~arr ~idx_traces ?(is_arraylist_add= false) pname location cond_set =
+    let arr_traces = Dom.Val.get_traces arr in
+    match (size, idx) with
+    | NonBottom length, NonBottom idx ->
+        let traces = TraceSet.merge ~arr_traces ~idx_traces location in
+        PO.ConditionSet.add_array_access pname location ~size:length ~idx ~is_arraylist_add traces
+          cond_set
+    | _ ->
+        cond_set
+
+
   let array_access ~arr ~idx ~is_plus pname location cond_set =
     let arr_blk = Dom.Val.get_array_blk arr in
-    let arr_traces = Dom.Val.get_traces arr in
     let size = ArrayBlk.sizeof arr_blk in
     let offset = ArrayBlk.offsetof arr_blk in
     let idx_itv = Dom.Val.get_itv idx in
     let idx_traces = Dom.Val.get_traces idx in
     let idx_in_blk = (if is_plus then Itv.plus else Itv.minus) offset idx_itv in
-    L.(debug BufferOverrun Verbose) "@[<v 2>Add condition :@," ;
-    L.(debug BufferOverrun Verbose) "array: %a@," ArrayBlk.pp arr_blk ;
-    L.(debug BufferOverrun Verbose) "  idx: %a@," Itv.pp idx_in_blk ;
-    L.(debug BufferOverrun Verbose) "@]@." ;
-    match (size, idx_in_blk) with
-    | NonBottom size, NonBottom idx ->
-        let traces = TraceSet.merge ~arr_traces ~idx_traces location in
-        PO.ConditionSet.add_array_access pname location ~size ~idx traces cond_set
-    | _ ->
-        cond_set
+    L.(debug BufferOverrun Verbose)
+      "@[<v 2>Add condition :@,array: %a@,  idx: %a@,@]@." ArrayBlk.pp arr_blk Itv.pp idx_in_blk ;
+    check_access ~size ~idx:idx_in_blk ~arr ~idx_traces pname location cond_set
 
 
-  let lindex ~array_exp ~index_exp mem pname location cond_set =
-    let arr = Sem.eval_arr array_exp mem in
+  let add_arraylist ~array_exp ~idx mem pname location cond_set =
+    let arr = Sem.eval array_exp mem in
+    let idx_traces = Dom.Val.get_traces idx in
+    let size = Exec.get_alist_size arr mem |> Dom.Val.get_itv in
+    let idx = Dom.Val.get_itv idx in
+    check_access ~size ~idx ~arr ~idx_traces ~is_arraylist_add:true pname location cond_set
+
+
+  let lindex ~array_exp ~index_exp ?(is_arraylist_add= false) mem pname location cond_set =
     let idx = Sem.eval index_exp mem in
+    if is_arraylist_add then add_arraylist ~array_exp ~idx mem pname location cond_set
+    else
+      let arr = Sem.eval_arr array_exp mem in
       array_access ~arr ~idx ~is_plus:true pname location cond_set
 end

infer/src/bufferoverrun/bufferOverrunUtils.mli

@@ -11,6 +11,8 @@ module Dom = BufferOverrunDomain
 module PO = BufferOverrunProofObligations
 
 module Exec : sig
+  val get_alist_size : Dom.Val.t -> Dom.Mem.astate -> Dom.Val.astate
+
   val load_val : Ident.t -> Dom.Val.astate -> Dom.Mem.astate -> Dom.Mem.astate
 
   type decl_local =
@@ -22,6 +24,10 @@ module Exec : sig
     -> length:IntLit.t option -> ?stride:int -> inst_num:int -> dimension:int -> Dom.Mem.astate
     -> Dom.Mem.astate * int
 
+  val decl_local_arraylist :
+    Typ.Procname.t -> node_hash:int -> Location.t -> Loc.t -> inst_num:int -> dimension:int
+    -> Dom.Mem.astate -> Dom.Mem.astate * int
+
   type decl_sym_val =
     Typ.Procname.t -> Itv.SymbolPath.partial -> Tenv.t -> node_hash:int -> Location.t -> depth:int
     -> Loc.t -> Typ.t -> Dom.Mem.astate -> Dom.Mem.astate
@@ -32,6 +38,11 @@ module Exec : sig
     -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate
     -> Dom.Mem.astate
 
+  val decl_sym_arraylist :
+    Typ.Procname.t -> Itv.SymbolPath.partial -> node_hash:int -> Location.t -> Loc.t
+    -> inst_num:int -> new_sym_num:Itv.Counter.t -> new_alloc_num:Itv.Counter.t -> Dom.Mem.astate
+    -> Dom.Mem.astate
+
   val init_array_fields :
     Tenv.t -> Typ.Procname.t -> node_hash:int -> Typ.t -> PowLoc.t -> ?dyn_length:Exp.t
     -> Dom.Mem.astate -> Dom.Mem.astate
@@ -45,6 +56,6 @@ module Check : sig
     -> PO.ConditionSet.t -> PO.ConditionSet.t
 
   val lindex :
-    array_exp:Exp.t -> index_exp:Exp.t -> Dom.Mem.astate -> Typ.Procname.t -> Location.t
-    -> PO.ConditionSet.t -> PO.ConditionSet.t
+    array_exp:Exp.t -> index_exp:Exp.t -> ?is_arraylist_add:bool -> Dom.Mem.astate
+    -> Typ.Procname.t -> Location.t -> PO.ConditionSet.t -> PO.ConditionSet.t
 end

infer/tests/codetoanalyze/java/performance/ArrayListTest.java

@@ -11,7 +11,85 @@ import java.util.ArrayList;
 public class ArrayListTest {
 
   public void iterate_over_arraylist(ArrayList<Integer> list) {
-    for (int i = 0, size = list.size(); i < size; ++i) {
+    for (int i = 0, size = list.size(); i < size; ++i) {}
   }
+
+   public void iterate_over_local_arraylist(ArrayList<Integer> list) {
+     ArrayList<Integer> local_list = list;
+     for (int i = 0, size = local_list.size(); i < size; ++i) {}
+  }
+
+  public void arraylist_empty_underrun_bad() {
+    ArrayList<Integer> list = new ArrayList<Integer>();
+    list.add(-1, 42);
+  }
+  public void arraylist_empty_ok() {
+    ArrayList<Integer> list = new ArrayList<Integer>();
+    list.add(0, 42);
+  }
+  public void arraylist_empty_overrun_bad() {
+    ArrayList<Integer> list = new ArrayList<Integer>();
+    list.add(1, 42);
+  }
+
+  public void arraylist_add3_overrun_bad() {
+    ArrayList<Integer> list = new ArrayList<Integer>();
+    list.add(42);
+    list.add(1337);
+    list.add(1984);
+    list.add(4, 666);
+  }
+
+
+  // we can't set the size of the list to 10 because it depends on how
+  // many times the loop is executed.Should be fixed once we have
+  // relational domain working.
+   public void arraylist_add_in_loop_FP() {
+    ArrayList<Integer> list = new ArrayList<Integer>();
+    for (int i = 0; i < 10; ++i) {
+      list.add(i);
+    }
+      for (int i = 0, size = list.size(); i < size; ++i) {}
+
    }
+
+  public void arraylist_add_in_loop_ok() {
+    ArrayList<Integer> list = new ArrayList<Integer>();
+      list.add(0);
+      list.add(1);
+      list.add(2);
+      list.add(3);
+      list.add(4);
+      list.add(5);
+      list.add(6);
+      list.add(7);
+      list.add(8);
+      list.add(9);
+      list.add(10);
+      list.add(11);
+      list.add(12);
+      list.add(13);
+      list.add(14);
+      list.add(15);
+
+      for (int i = 0, size = list.size(); i < size; ++i) {}
+
+
+  }
+
+
+   public void arraylist_addAll_bad() {
+    ArrayList<Integer> list = new ArrayList<Integer>();
+      list.add(2);
+      list.add(3);
+
+      ArrayList<Integer> list2 = new ArrayList<Integer>();
+      list2.add(0);
+      list2.add(1);
+
+      list2.addAll(0,list);
+      list2.addAll(5,list);
+
+  }
+
 }

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

@@ -4,8 +4,16 @@ codetoanalyze/java/performance/ArrayCost.java, boolean ArrayCost.isPowOfTwo_FP(i
 codetoanalyze/java/performance/ArrayCost.java, boolean ArrayCost.isPowOfTwo_FP(int), 12, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 889]
 codetoanalyze/java/performance/ArrayCost.java, void ArrayCost.ArrayCost(int[]), 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * mag.length.ub]
 codetoanalyze/java/performance/ArrayCost.java, void ArrayCost.ArrayCost(int[]), 5, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * mag.length.ub]
+codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_add3_overrun_bad(), 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [4, 4] Size: [3, 3]]
+codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_addAll_bad(), 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [5, 5] Size: [4, 4]]
+codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_add_in_loop_FP(), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_add_in_loop_ok(), 19, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 201]
+codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_empty_overrun_bad(), 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [0, 0]]
+codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_empty_underrun_bad(), 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [-1, -1] Size: [0, 0]]
 codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_over_arraylist(ArrayList), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 5 + 5 * list.length.ub]
 codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_over_arraylist(ArrayList), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 6 + 5 * list.length.ub]
+codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_over_local_arraylist(ArrayList), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 7 + 5 * list.length.ub]
+codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.iterate_over_local_arraylist(ArrayList), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 5 * list.length.ub]
 codetoanalyze/java/performance/Break.java, int Break.break_constant(int), 2, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 8 + 7 * p.ub]
 codetoanalyze/java/performance/Break.java, int Break.break_loop(int,int), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 7 * p.ub]
 codetoanalyze/java/performance/Break.java, int Break.break_loop(int,int), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 7 * p.ub]
@@ -48,16 +56,18 @@ codetoanalyze/java/performance/Cost_test_deps.java, int Cost_test_deps.two_loops
 codetoanalyze/java/performance/Cost_test_deps.java, void Cost_test_deps.if_bad(int), 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 608]
 codetoanalyze/java/performance/Cost_test_deps.java, void Cost_test_deps.if_bad(int), 6, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 607]
 codetoanalyze/java/performance/EvilCfg.java, void EvilCfg.foo(int,int,boolean), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
-codetoanalyze/java/performance/FieldAccess.java, void FieldAccess.iterate_upto_field_size(FieldAccess$Test), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 2 + 6 * test.a.ub]
-codetoanalyze/java/performance/FieldAccess.java, void FieldAccess.iterate_upto_field_size(FieldAccess$Test), 1, EXPENSIVE_EXECUTION_TIME_CALL, no_bucket, ERROR, [with estimated cost 1 + 6 * test.a.ub]
+codetoanalyze/java/performance/FieldAccess.java, void FieldAccess.iterate_upto_field_size(FieldAccess$Test), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonArray.java, void JsonArray.addStringEntry(String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/java/performance/JsonArray.java, void JsonArray.addStringEntry(String), 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: int StringBuilder.length(),ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,JsonType), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,JsonType), 6, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Call,Unknown value from: StringBuilder StringBuilder.append(String),Assignment,ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,Object), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,boolean), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,double), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonMap.java, void JsonMap.addEntry(String,long), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonMap.java, void JsonMap.addKeyToMap(String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
+codetoanalyze/java/performance/JsonMap.java, void JsonMap.addKeyToMap(String), 2, BUFFER_OVERRUN_U5, no_bucket, ERROR, [Unknown value from: int StringBuilder.length(),ArrayAccess: Offset: [-oo, +oo] Size: [0, +oo]]
 codetoanalyze/java/performance/JsonString.java, JsonString.<init>(String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonUtils.java, StringBuilder JsonUtils.serialize(String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []
 codetoanalyze/java/performance/JsonUtils.java, void JsonUtils.escape(StringBuilder,String), 0, INFINITE_EXECUTION_TIME_CALL, no_bucket, ERROR, []