[inferbo] Add size alias when i=1

Summary: Sometimes there is a code like `for(int i = 1; i < x; i++){ l.add(); }`, where the first element in a list is addressed specifically. This case was not analyzed precisely, because the alias value is added only when `i` is initialized by 0 by heuristic. This diff extends the heuristic, so it adds a size alias between `i` and `l.size()` when `i` is initialized by 0 or 1.

Reviewed By: ezgicicek

Differential Revision: D18351867

fbshipit-source-id: e7d19a4ec

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -1186,9 +1186,9 @@ module AliasMap = struct
     else x
 
 
-  let add_zero_size_alias ~size ~arr 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= IntLit.zero; java_tmp= None})
+      (AliasTarget.Size {alias_typ= Eq; i; java_tmp= None})
       x
 
 
@@ -1343,10 +1343,10 @@ 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 -> PowLoc.t -> t -> t =
+  let add_empty_size_alias : Loc.t -> IntLit.t -> PowLoc.t -> t -> t =
-   fun loc arr_locs prev ->
+   fun loc i arr_locs prev ->
     let accum_empty_size_alias arr_loc acc =
-      lift_map (AliasMap.add_zero_size_alias ~size:loc ~arr:arr_loc) acc
+      lift_map (AliasMap.add_zero_size_alias ~size:loc ~i ~arr:arr_loc) acc
     in
     PowLoc.fold accum_empty_size_alias arr_locs (lift_map (AliasMap.forget loc) prev)
 
@@ -1864,11 +1864,12 @@ module MemReach = struct
     fun k m -> AliasTargets.fold accum_simple_alias (Alias.find_id k m.alias) []
 
 
-  let find_size_alias : Ident.t -> _ t0 -> (AliasTarget.alias_typ * Loc.t * Loc.t option) list =
+  let find_size_alias :
+      Ident.t -> _ t0 -> (AliasTarget.alias_typ * Loc.t * IntLit.t * Loc.t option) list =
     let accum_size_alias l tgt acc =
       match tgt with
-      | AliasTarget.Size {alias_typ; java_tmp} ->
+      | AliasTarget.Size {alias_typ; i; java_tmp} ->
-          (alias_typ, l, java_tmp) :: acc
+          (alias_typ, l, i, java_tmp) :: acc
       | _ ->
           acc
     in
@@ -1884,14 +1885,14 @@ module MemReach = struct
   let store_simple_alias : Loc.t -> Exp.t -> t -> t =
    fun loc e m ->
     match e with
-    | Exp.Const (Const.Cint zero) when IntLit.iszero zero ->
+    | 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
           in
           MemPure.fold add_arr m.mem_pure PowLoc.empty
         in
-        {m with alias= Alias.add_empty_size_alias loc arr_locs m.alias}
+        {m with alias= Alias.add_empty_size_alias loc i arr_locs m.alias}
     | _ ->
         {m with alias= Alias.store_simple loc e m.alias}
 
@@ -2281,7 +2282,8 @@ module Mem = struct
    fun k -> f_lift_default ~default:[] (MemReach.find_simple_alias k)
 
 
-  let find_size_alias : Ident.t -> _ t0 -> (AliasTarget.alias_typ * Loc.t * Loc.t option) list =
+  let find_size_alias :
+      Ident.t -> _ t0 -> (AliasTarget.alias_typ * Loc.t * IntLit.t * Loc.t option) list =
    fun k -> f_lift_default ~default:[] (MemReach.find_size_alias k)
 
 

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -650,18 +650,23 @@ module Prune = struct
     let prune_alias_core ~val_prune_eq ~val_prune_le ~make_pruning_exp integer_type_widths x e
         ({mem} as astate) =
       List.fold (Mem.find_size_alias x mem) ~init:astate
-        ~f:(fun astate (alias_typ, lv, java_tmp) ->
+        ~f:(fun astate (alias_typ, lv, i, java_tmp) ->
           let array_v = Mem.find lv mem in
-          let size =
+          let lhs =
-            Val.get_array_blk array_v |> ArrayBlk.sizeof |> Val.of_itv
+            Val.get_array_blk array_v |> ArrayBlk.sizeof
-            |> Val.set_itv_updated_by_addition
+            |> Itv.plus (Itv.of_int_lit i)
+            |> Val.of_itv |> Val.set_itv_updated_by_addition
           in
           let rhs = eval integer_type_widths e mem in
           let prune_target val_prune astate =
-            let size' = val_prune size rhs in
+            let lhs' = val_prune lhs rhs in
-            let array_v' = Val.set_array_length Location.dummy ~length:size' array_v in
+            let array_v' =
-            let pruning_exp = make_pruning_exp ~lhs:size' ~rhs in
+              Val.set_array_length Location.dummy
-            (update_mem_in_prune lv array_v' ~pruning_exp astate, size', pruning_exp)
+                ~length:(Val.minus_a lhs' (Val.of_int_lit i))
+                array_v
+            in
+            let pruning_exp = make_pruning_exp ~lhs:lhs' ~rhs in
+            (update_mem_in_prune lv array_v' ~pruning_exp astate, lhs', pruning_exp)
           in
           match alias_typ with
           | AliasTarget.Eq ->

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

@@ -74,6 +74,26 @@ class ArrayListTest {
     int j = b.get(a.size());
   }
 
+  void add_in_loop_by_param3_ok(ArrayList<Integer> b) {
+    ArrayList<Integer> a = new ArrayList<>();
+    if (b.size() > 0) {
+      for (int i = 1; i < b.size(); i++) {
+        a.add(0);
+      }
+      int j = a.get(b.size() - 2);
+    }
+  }
+
+  void add_in_loop_by_param3_bad(ArrayList<Integer> b) {
+    ArrayList<Integer> a = new ArrayList<>();
+    if (b.size() > 0) {
+      for (int i = 1; i < b.size(); i++) {
+        a.add(0);
+      }
+      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

@@ -10,6 +10,7 @@ codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Ar
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_and_remove_bad(java.util.ArrayList):void, 6, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: 0]
 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_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]