Add support for Java's ArrayList.set and ArrayList.get

Reviewed By: mbouaziz

Differential Revision: D8874675

fbshipit-source-id: aa96f5344

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -349,7 +349,8 @@ module ArrayList = struct
   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
+      BoUtils.Check.arraylist_access ~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}
 
@@ -361,7 +362,17 @@ module ArrayList = struct
     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
+      BoUtils.Check.arraylist_access ~index_exp ~array_exp ~is_arraylist_add:true mem pname
+        location cond_set
+    in
+    {exec; check}
+
+
+  let get_or_set_at_index alist_id index_exp =
+    let exec _model_env ~ret:_ mem = mem in
+    let check {pname; location} mem cond_set =
+      let array_exp = Exp.Var alist_id in
+      BoUtils.Check.arraylist_access ~index_exp ~array_exp mem pname location cond_set
     in
     {exec; check}
 end
@@ -396,6 +407,10 @@ 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" &:: "get" <>$ capt_var_exn $+ capt_exp
+        $--> ArrayList.get_or_set_at_index
+      ; -"java.util.ArrayList" &:: "set" <>$ capt_var_exn $+ capt_exp $+ any_arg
+        $--> ArrayList.get_or_set_at_index
       ; -"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

infer/src/bufferoverrun/bufferOverrunUtils.ml

@@ -203,18 +203,17 @@ module Check = struct
     check_access ~size ~idx:idx_in_blk ~arr ~idx_traces pname location cond_set
 
 
-  let add_arraylist ~array_exp ~idx mem pname location cond_set =
+  let arraylist_access ~array_exp ~index_exp ?(is_arraylist_add= false) mem pname location cond_set =
+    let idx = Sem.eval index_exp mem in
     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
+    check_access ~size ~idx ~arr ~idx_traces ~is_arraylist_add pname location cond_set
 
 
-  let lindex ~array_exp ~index_exp ?(is_arraylist_add= false) mem pname location cond_set =
+  let lindex ~array_exp ~index_exp 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

@@ -56,6 +56,10 @@ 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
+
+  val arraylist_access :
     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

@@ -92,4 +92,55 @@ public class ArrayListTest {
 
   }
 
+
+   public void arraylist_get_underrun_bad() {
+    ArrayList<Integer> list = new ArrayList<Integer>();
+    list.get(0);
+  }
+
+
+   public void arraylist_get_overrun_bad() {
+    ArrayList<Integer> list = new ArrayList<Integer>();
+    list.add(0);
+    list.get(2);
+  }
+
+
+   public void arraylist_get_ok() {
+    ArrayList<Integer> list = new ArrayList<Integer>();
+    list.add(0);
+    list.add(1);
+    list.add(2);
+
+    for (int i = 0, size = list.size(); i < size; ++i) {
+      list.get(i);
+    }
+
+   }
+
+
+    public void arraylist_set_ok() {
+    ArrayList<Integer> list = new ArrayList<Integer>();
+    list.add(0);
+    list.add(1);
+    list.add(2);
+    for (int i = 0, size = list.size(); i < size; ++i) {
+      list.set(i, i);
+    }
+
+   }
+
+
+   public void arraylist_set_underrun_bad() {
+    ArrayList<Integer> list = new ArrayList<Integer>();
+    list.set(0, 10);
+  }
+
+
+   public void arraylist_set_overrun_bad() {
+    ArrayList<Integer> list = new ArrayList<Integer>();
+    list.add(0);
+    list.set(1, 10);
+  }
+
 }

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

@@ -10,6 +10,10 @@ codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_
 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.arraylist_get_overrun_bad(), 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [2, 2] Size: [1, 1]]
+codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_get_underrun_bad(), 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] Size: [0, 0]]
+codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_set_overrun_bad(), 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [1, 1]]
+codetoanalyze/java/performance/ArrayListTest.java, void ArrayListTest.arraylist_set_underrun_bad(), 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 0] 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]