[inferbo] Add size alias when array size is one

Summary: Following D18351867, this diff adds more size alias: when initial array size is one.

Reviewed By: ezgicicek

Differential Revision: D18530598

fbshipit-source-id: 26d57fe30

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -1186,9 +1186,9 @@ module AliasMap = struct
     else x
 
 
-  let add_zero_size_alias ~size ~i ~arr x =
-    add_alias ~lhs:(KeyLhs.of_loc size) ~rhs:arr
-      (AliasTarget.Size {alias_typ= Eq; i; java_tmp= None})
+  let add_size_alias ~lhs ~lhs_v ~arr ~arr_size x =
+    add_alias ~lhs:(KeyLhs.of_loc lhs) ~rhs:arr
+      (AliasTarget.Size {alias_typ= Eq; i= IntLit.sub lhs_v arr_size; java_tmp= None})
       x
 
 
@@ -1343,12 +1343,12 @@ module Alias = struct
     update_size_alias locs a ~f:(fun loc acc -> lift_map (AliasMap.incr_or_not_size_alias loc) acc)
 
 
-  let add_empty_size_alias : Loc.t -> IntLit.t -> PowLoc.t -> t -> t =
+  let add_size_alias : Loc.t -> IntLit.t -> (Loc.t * IntLit.t) list -> t -> t =
    fun loc i arr_locs prev ->
-    let accum_empty_size_alias arr_loc acc =
-      lift_map (AliasMap.add_zero_size_alias ~size:loc ~i ~arr:arr_loc) acc
+    let accum_size_alias acc (arr_loc, arr_size) =
+      lift_map (AliasMap.add_size_alias ~lhs:loc ~lhs_v:i ~arr:arr_loc ~arr_size) acc
     in
-    PowLoc.fold accum_empty_size_alias arr_locs (lift_map (AliasMap.forget loc) prev)
+    List.fold arr_locs ~init:(lift_map (AliasMap.forget loc) prev) ~f:accum_size_alias
 
 
   let add_iterator_offset_alias : Ident.t -> PowLoc.t -> t -> t =
@@ -1888,11 +1888,14 @@ module MemReach = struct
     | Exp.Const (Const.Cint i) when IntLit.iszero i || IntLit.isone i ->
         let arr_locs =
           let add_arr l v acc =
-            if Itv.is_zero (Val.array_sizeof v) then PowLoc.add l acc else acc
+            let size = Val.array_sizeof v in
+            if Itv.is_zero size then (l, IntLit.zero) :: acc
+            else if Itv.is_one size then (l, IntLit.one) :: acc
+            else acc
           in
-          MemPure.fold add_arr m.mem_pure PowLoc.empty
+          MemPure.fold add_arr m.mem_pure []
         in
-        {m with alias= Alias.add_empty_size_alias loc i arr_locs m.alias}
+        {m with alias= Alias.add_size_alias loc i arr_locs m.alias}
     | _ ->
         {m with alias= Alias.store_simple loc e m.alias}
 

infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java

@@ -94,6 +94,28 @@ class ArrayListTest {
     }
   }
 
+  void add_in_loop_by_param4_ok(ArrayList<Integer> b) {
+    ArrayList<Integer> a = new ArrayList<>();
+    a.add(0);
+    if (b.size() > 0) {
+      for (int i = 1; i < b.size(); i++) {
+        a.add(0);
+      } // a.size = b.size
+      int j = a.get(b.size() - 1);
+    }
+  }
+
+  void add_in_loop_by_param4_bad(ArrayList<Integer> b) {
+    ArrayList<Integer> a = new ArrayList<>();
+    a.add(0);
+    if (b.size() > 0) {
+      for (int i = 1; i < b.size(); i++) {
+        a.add(0);
+      } // a.size = b.size
+      int j = a.get(b.size() + 1);
+    }
+  }
+
   void add_in_loop_iterator_ok(ArrayList<Integer> b) {
     ArrayList<Integer> a = new ArrayList<>();
     for (Integer i : b) {

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

@@ -11,6 +11,7 @@ codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_and_remov
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_bad():void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 6 Size: 5]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_by_param2_bad(java.util.ArrayList):void, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Array declaration,Assignment,<Length trace>,Assignment,Array declaration,Array access: Offset: [0, b.length] Size: b.length]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_by_param3_bad(java.util.ArrayList):void, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Array declaration,Assignment,<Length trace>,Array declaration,Assignment,Array declaration,Array access: Offset: [-1+max(1, b.length), b.length - 1] Size: -1+max(1, b.length)]
+codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_by_param4_bad(java.util.ArrayList):void, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Array declaration,Assignment,<Length trace>,Array declaration,Assignment,Array declaration,Array access: Offset: [1+max(1, b.length), b.length + 1] Size: max(1, b.length)]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_by_param_bad(java.util.ArrayList):void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Assignment,Array declaration,Assignment,<Length trace>,Parameter `b.elements[*]`,Assignment,Array declaration,Array access: Offset: b.length + 1 Size: b.length]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_iterator2_bad(java.util.ArrayList):void, 7, BUFFER_OVERRUN_L2, no_bucket, ERROR, [<Offset trace>,Array declaration,Assignment,<Length trace>,Parameter `b.elements[*]`,Array access: Offset: [0, b.length] Size: b.length]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_iterator_bad(java.util.ArrayList):void, 5, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `b.elements[*]`,Assignment,<Length trace>,Array declaration,Array access: Offset: b.length + 1 Size: b.length]