[inferbo] Add relation between iterator and integer value

Summary: This diff extends the domain to express the relation between iterator's offset and integer value.

Reviewed By: ezgicicek

Differential Revision: D19143670

fbshipit-source-id: 6223bc934

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -409,6 +409,8 @@ module Val = struct
 
   let prune_ne : t -> t -> t = lift_prune2 Itv.prune_ne ArrayBlk.prune_ne
 
+  let prune_lt : t -> t -> t = prune_binop Binop.Lt
+
   let is_pointer_to_non_array x = (not (PowLoc.is_bot x.powloc)) && ArrayBlk.is_bot x.arrayblk
 
   (* In the pointer arithmetics, it returns top, if we cannot
@@ -804,37 +806,12 @@ module AliasTarget = struct
         F.pp_print_string fmt ">="
 
 
-  (* Relations between values of logical variables(registers) and program variables
-
-     "Simple relation": Since Sil distinguishes logical and program variables, we need a relation for
-     pruning values of program variables.  For example, a C statement [if(x){...}] is translated to
-     [%r=load(x); if(%r){...}] in Sil.  At the load statement, we record the alias between the
-     values of [%r] and [x], then we can prune not only the value of [%r], but also that of [x]
-     inside the if branch.  The [java_tmp] field is an additional slot for keeping one more alias of
-     temporary variable in Java.  The [i] field is to express [%r=load(x)+i].
-
-     "Empty relation": For pruning [vector.length] with [vector::empty()] results, we adopt a specific
-     relation between [%r] and [v->elements], where [%r=v.empty()].  So, if [%r!=0], [v]'s array
-     length ([v->elements->length]) is pruned by [=0].  On the other hand, if [%r==0], [v]'s array
-     length is pruned by [>=1].
-
-     "Size relation": This is for pruning vector's length.  When there is a function call,
-     [%r=x.size()], the alias target for [%r] becomes [AliasTarget.size {l=x.elements}].  The
-     [java_tmp] field is an additional slot for keeping one more alias of temporary variable in
-     Java.  The [i] field is to express [%r=x.size()+i], which is required to follow the semantics
-     of [Array.add] inside loops precisely.
-
-     "Iterator offset relation": This is for tracking a relation between an iterator offset and a
-     length of array.  If [%r] has an alias to [IteratorOffset {l; i}], which means that [%r's
-     iterator offset] is same to [length(l)+i].
-
-     "HasNext relation": This is for tracking return values of the [hasNext] function.  If [%r] has an
-     alias to [HasNext {l}], which means that [%r] is a [hasNext] results of the iterator [l]. *)
   type t =
     | Simple of {i: IntLit.t; java_tmp: Loc.t option}
     | Empty
     | Size of {alias_typ: alias_typ; i: IntLit.t; java_tmp: Loc.t option}
     | Fgets
+    | IteratorSimple of {i: IntLit.t; java_tmp: Loc.t option}
     | IteratorOffset of {alias_typ: alias_typ; i: IntLit.t; java_tmp: Loc.t option}
     | IteratorHasNext of {java_tmp: Loc.t option}
     | Top
@@ -863,6 +840,8 @@ module AliasTarget = struct
             pp_intlit i
       | Fgets ->
           F.fprintf fmt "%t=fgets(%t)" pp_lhs pp_rhs
+      | IteratorSimple {i; java_tmp} ->
+          F.fprintf fmt "iterator offset(%t%a)=%t%a" pp_lhs pp_java_tmp java_tmp pp_rhs pp_intlit i
       | IteratorOffset {alias_typ; i; java_tmp} ->
           F.fprintf fmt "iterator offset(%t%a)%alength(%t)%a" pp_lhs pp_java_tmp java_tmp
             alias_typ_pp alias_typ pp_rhs pp_intlit i
@@ -880,6 +859,7 @@ module AliasTarget = struct
   let get_locs = function
     | Simple {java_tmp= Some tmp}
     | Size {java_tmp= Some tmp}
+    | IteratorSimple {java_tmp= Some tmp}
     | IteratorOffset {java_tmp= Some tmp}
     | IteratorHasNext {java_tmp= Some tmp} ->
         PowLoc.singleton tmp
@@ -887,6 +867,7 @@ module AliasTarget = struct
     | Size {java_tmp= None}
     | Empty
     | Fgets
+    | IteratorSimple {java_tmp= None}
     | IteratorOffset {java_tmp= None}
     | IteratorHasNext {java_tmp= None}
     | Top ->
@@ -905,6 +886,8 @@ module AliasTarget = struct
         Size {alias_typ; i; java_tmp= Option.bind java_tmp ~f}
     | Fgets ->
         Fgets
+    | IteratorSimple {i; java_tmp} ->
+        IteratorSimple {i; java_tmp= Option.bind java_tmp ~f}
     | IteratorOffset {alias_typ; i; java_tmp} ->
         IteratorOffset {alias_typ; i; java_tmp= Option.bind java_tmp ~f}
     | IteratorHasNext {java_tmp} ->
@@ -994,6 +977,8 @@ module AliasTarget = struct
   let set_java_tmp loc = function
     | Size a ->
         Size {a with java_tmp= Some loc}
+    | IteratorSimple a ->
+        IteratorSimple {a with java_tmp= Some loc}
     | IteratorOffset a ->
         IteratorOffset {a with java_tmp= Some loc}
     | IteratorHasNext _ ->
@@ -1162,6 +1147,22 @@ module AliasMap = struct
 
   let forget_size_alias arr_locs x = M.map (AliasTargets.forget_size_alias arr_locs) x
 
+  let incr_iterator_simple_alias ~prev loc n x =
+    let accum_tgt ~lhs ~rhs tgt acc =
+      if Loc.equal rhs loc then
+        match tgt with
+        | AliasTarget.IteratorSimple {i; java_tmp} ->
+            add_alias ~lhs ~rhs (AliasTarget.IteratorSimple {i= IntLit.sub i n; java_tmp}) acc
+        | _ ->
+            acc
+      else acc
+    in
+    let accum_tgts lhs tgts acc =
+      AliasTargets.fold (fun rhs tgts acc -> accum_tgt ~lhs ~rhs tgts acc) tgts acc
+    in
+    M.fold accum_tgts prev x
+
+
   let store_n ~prev loc id n x =
     let accum_size_alias rhs tgt acc =
       match tgt with
@@ -1172,7 +1173,19 @@ module AliasMap = struct
       | _ ->
           acc
     in
-    AliasTargets.fold accum_size_alias (find_id id prev) x
+    let tgts = find_id id prev in
+    let x = AliasTargets.fold accum_size_alias tgts x in
+    match AliasTargets.find_simple_alias tgts with
+    | Some loc' when Loc.equal loc loc' ->
+        incr_iterator_simple_alias ~prev loc n x
+    | _ ->
+        x
+
+
+  let add_iterator_simple_alias id int x =
+    add_alias ~lhs:(KeyLhs.of_id id) ~rhs:int
+      (AliasTarget.IteratorSimple {i= IntLit.zero; java_tmp= None})
+      x
 
 
   let add_iterator_offset_alias id arr x =
@@ -1181,31 +1194,45 @@ module AliasMap = struct
       x
 
 
-  let incr_iterator_offset_alias id x =
+  let incr_iterator_offset_alias =
-    let accum_incr_iterator_offset_alias rhs tgt acc =
+    let apply_i ~f = function
-      match tgt with
+      | AliasTarget.IteratorSimple ({i} as tgt) ->
-      | AliasTarget.IteratorOffset ({i; java_tmp} as tgt) ->
+          AliasTarget.IteratorSimple {tgt with i= f i}
-          let i = IntLit.(add i one) in
+      | AliasTarget.IteratorOffset ({i} as tgt) ->
-          let acc =
+          AliasTarget.IteratorOffset {tgt with i= f i}
-            add_alias ~lhs:(KeyLhs.of_id id) ~rhs (AliasTarget.IteratorOffset {tgt with i}) acc
-          in
-          Option.value_map java_tmp ~default:x ~f:(fun java_tmp ->
-              add_alias ~lhs:(KeyLhs.of_loc java_tmp) ~rhs
-                (AliasTarget.IteratorOffset {tgt with i; java_tmp= None})
-                acc )
       | _ ->
-          acc
+          assert false
     in
-    match M.find_opt (KeyLhs.of_id id) x with
+    let java_tmp_none = function
-    | Some tgts ->
+      | AliasTarget.IteratorSimple tgt ->
-        AliasTargets.fold accum_incr_iterator_offset_alias tgts x
+          AliasTarget.IteratorSimple {tgt with java_tmp= None}
-    | _ ->
+      | AliasTarget.IteratorOffset tgt ->
-        x
+          AliasTarget.IteratorOffset {tgt with java_tmp= None}
+      | _ ->
+          assert false
+    in
+    fun id x ->
+      let accum_incr_iterator_offset_alias rhs tgt acc =
+        match tgt with
+        | AliasTarget.IteratorSimple {java_tmp} | AliasTarget.IteratorOffset {java_tmp} ->
+            let tgt = apply_i tgt ~f:IntLit.(add one) in
+            let acc = add_alias ~lhs:(KeyLhs.of_id id) ~rhs tgt acc in
+            Option.value_map java_tmp ~default:x ~f:(fun java_tmp ->
+                add_alias ~lhs:(KeyLhs.of_loc java_tmp) ~rhs (java_tmp_none tgt) acc )
+        | _ ->
+            acc
+      in
+      match M.find_opt (KeyLhs.of_id id) x with
+      | Some tgts ->
+          AliasTargets.fold accum_incr_iterator_offset_alias tgts x
+      | _ ->
+          x
 
 
   let add_iterator_has_next_alias ~ret_id ~iterator x =
     let accum_has_next_alias _rhs tgt acc =
       match tgt with
+      | AliasTarget.IteratorSimple {java_tmp= Some java_tmp}
       | AliasTarget.IteratorOffset {java_tmp= Some java_tmp} ->
           add_alias ~lhs:(KeyLhs.of_id ret_id) ~rhs:java_tmp
             (AliasTarget.IteratorHasNext {java_tmp= None})
@@ -1315,6 +1342,14 @@ module Alias = struct
     List.fold arr_locs ~init:(lift_map (AliasMap.forget loc) prev) ~f:accum_size_alias
 
 
+  let add_iterator_simple_alias : Ident.t -> PowLoc.t -> t -> t =
+   fun id int_locs a ->
+    let accum_iterator_simple_alias int_loc acc =
+      lift_map (AliasMap.add_iterator_simple_alias id int_loc) acc
+    in
+    PowLoc.fold accum_iterator_simple_alias int_locs a
+
+
   let add_iterator_offset_alias : Ident.t -> PowLoc.t -> t -> t =
    fun id arr_locs a ->
     let accum_iterator_offset_alias arr_loc acc =
@@ -1865,13 +1900,27 @@ module MemReach = struct
 
   let incr_or_not_size_alias locs m = {m with alias= Alias.incr_or_not_size_alias locs m.alias}
 
-  let add_iterator_offset_alias id m =
+  let add_iterator_alias_common ~cond ~alias_add id m =
-    let arr_locs =
+    let locs =
-      let add_arr l v acc = if Itv.is_zero (Val.array_sizeof v) then PowLoc.add l acc else acc in
+      let accum_loc l v acc = if cond v then PowLoc.add l acc else acc in
-      MemPure.fold add_arr m.mem_pure PowLoc.empty
+      MemPure.fold accum_loc m.mem_pure PowLoc.empty
     in
-    {m with alias= Alias.add_iterator_offset_alias id arr_locs m.alias}
+    {m with alias= alias_add id locs m.alias}
+
 
+  let add_iterator_simple_alias =
+    add_iterator_alias_common
+      ~cond:(fun v -> Itv.is_zero (Val.get_itv v))
+      ~alias_add:Alias.add_iterator_simple_alias
+
+
+  let add_iterator_offset_alias =
+    add_iterator_alias_common
+      ~cond:(fun v -> Itv.is_zero (Val.array_sizeof v))
+      ~alias_add:Alias.add_iterator_offset_alias
+
+
+  let add_iterator_alias id m = add_iterator_offset_alias id m |> add_iterator_simple_alias id
 
   let incr_iterator_offset_alias id m = {m with alias= Alias.incr_iterator_offset_alias id m.alias}
 
@@ -2232,9 +2281,7 @@ module Mem = struct
 
   let incr_or_not_size_alias locs = map ~f:(MemReach.incr_or_not_size_alias locs)
 
-  let add_iterator_offset_alias : Ident.t -> t -> t =
+  let add_iterator_alias : Ident.t -> t -> t = fun id -> map ~f:(MemReach.add_iterator_alias id)
-   fun id -> map ~f:(MemReach.add_iterator_offset_alias id)
-
 
   let incr_iterator_offset_alias : Exp.t -> t -> t =
    fun iterator m ->

infer/src/bufferoverrun/bufferOverrunDomain.mli

@@ -214,6 +214,10 @@ module Val : sig
   (** Pruning semantics for [Binop.Ne]. This prunes value of [x] when given [x != y], i.e.,
       [prune_ne x y]. *)
 
+  val prune_lt : t -> t -> t
+  (** Pruning semantics for [Binop.Lt]. This prunes value of [x] when given [x < y], i.e.,
+      [prune_lt x y]. *)
+
   val prune_ne_zero : t -> t
   (** Prune value of [x] when given [x != 0] *)
 
@@ -313,6 +317,10 @@ module AliasTarget : sig
     | Fgets
         (** This is for pruning return values of [fgets]. If the result of [fgets] is not null, the
             length of return value will be pruned to greater than or equal to 1. *)
+    | IteratorSimple of {i: IntLit.t; java_tmp: AbsLoc.Loc.t option}
+        (** This is for tracking a relation between an iterator offset and an integer value. If [%r]
+            has an alias to [IteratorSimple {l; i}], which means that [%r's iterator offset] is same
+            to [l]. *)
     | IteratorOffset of {alias_typ: alias_typ; i: IntLit.t; java_tmp: AbsLoc.Loc.t option}
         (** This is for tracking a relation between an iterator offset and the length of the
             underlying collection. If [%r] has an alias to [IteratorOffset {l; i}], which means that
@@ -565,8 +573,9 @@ module Mem : sig
   val add_iterator_has_next_alias : Ident.t -> Exp.t -> t -> t
   (** Add an [AliasTarget.IteratorHasNext] alias when [ident = iterator.hasNext()] is called *)
 
-  val add_iterator_offset_alias : Ident.t -> t -> t
+  val add_iterator_alias : Ident.t -> t -> t
-  (** Add [AliasTarget.IteratorOffset] alias when [Iteratable.iterator()] is called *)
+  (** Add [AliasTarget.IteratorSimple] and [AliasTarget.IteratorOffset] aliases when
+      [Iteratable.iterator()] is called *)
 
   val incr_iterator_offset_alias : Exp.t -> t -> t
   (** Update iterator offset alias when [iterator.next()] is called *)

infer/src/bufferoverrun/bufferOverrunModels.ml

@@ -887,7 +887,7 @@ module Collection = struct
   let iterator coll_exp =
     let exec {integer_type_widths} ~ret:(ret_id, _) mem =
       let itr = Sem.eval integer_type_widths coll_exp mem in
-      model_by_value itr ret_id mem |> Dom.Mem.add_iterator_offset_alias ret_id
+      model_by_value itr ret_id mem |> Dom.Mem.add_iterator_alias ret_id
     in
     {exec; check= no_check}
 

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -518,19 +518,25 @@ module Prune = struct
 
 
   let prune_has_next ~true_branch iterator ({mem} as astate) =
-    let accum_pruned arr_loc tgt acc =
+    let accum_prune_common ~prune_f loc acc =
+      let length = collection_length_of_iterator iterator mem in
+      let v = prune_f (Mem.find loc mem) length in
+      update_mem_in_prune loc v acc
+    in
+    let accum_pruned loc tgt acc =
       match tgt with
+      | AliasTarget.IteratorSimple {i} when IntLit.(eq i zero) ->
+          let prune_f = if true_branch then Val.prune_lt else Val.prune_eq in
+          accum_prune_common ~prune_f loc acc
       | AliasTarget.IteratorOffset {alias_typ; i} when IntLit.(eq i zero) ->
-          let length = collection_length_of_iterator iterator mem |> Val.get_itv in
+          let prune_f v length =
-          let v = Mem.find arr_loc mem in
+            let f =
-          let v =
-            let prune_f =
               if true_branch then Val.prune_length_lt
               else match alias_typ with Eq -> Val.prune_length_eq | Le -> Val.prune_length_le
             in
-            prune_f v length
+            f v (Val.get_itv length)
           in
-          update_mem_in_prune arr_loc v acc
+          accum_prune_common ~prune_f loc acc
       | _ ->
           acc
     in

infer/tests/codetoanalyze/java/performance/ListTest.java

@@ -98,4 +98,28 @@ class ListTest {
     a.addAll(l);
     for (Integer i : a) {}
   }
+
+  void iter_relation_with_var(List<Integer> a) {
+    int k = 0;
+    for (Integer i : a) {
+      k += 1;
+    }
+    for (int i = 0; i < k; i++) {}
+  }
+
+  class MyOwnObj {
+    int my_size = 0;
+
+    void my_put() {
+      my_size += 1;
+    }
+  }
+
+  void iter_my_own_obj_FP(List<Integer> a) {
+    MyOwnObj o = new MyOwnObj();
+    for (Integer i : a) {
+      o.my_put();
+    }
+    for (int i = 0; i < o.my_size; i++) {}
+  }
 }

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

@@ -164,6 +164,11 @@ codetoanalyze/java/performance/ListTest.java, ListTest.indexOfImpl_linear(java.u
 codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list1_linear(java.util.List,java.util.List):void, 6, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 17 + 12 ⋅ (l2.length + l1.length) + 3 ⋅ (l2.length + l1.length + 1), O((l2.length + l1.length)), degree = 1,{l2.length + l1.length + 1},Loop at line 76,{l2.length + l1.length},Loop at line 76]
 codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list2_linear(java.util.List,java.util.List):void, 5, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 14 + 8 ⋅ (l2.length + l1.length) + 3 ⋅ (l2.length + l1.length + 1), O((l2.length + l1.length)), degree = 1,{l2.length + l1.length + 1},Loop at line 88,{l2.length + l1.length},Loop at line 88]
 codetoanalyze/java/performance/ListTest.java, ListTest.iter_multiple_list3_linear(java.util.List,java.util.List,java.util.List):void, 6, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 18 + 8 ⋅ (l2.length + l1.length + a.length) + 3 ⋅ (l2.length + l1.length + a.length + 1), O((l2.length + l1.length + a.length)), degree = 1,{l2.length + l1.length + a.length + 1},Loop at line 99,{l2.length + l1.length + a.length},Loop at line 99]
+codetoanalyze/java/performance/ListTest.java, ListTest.iter_my_own_obj_FP(java.util.List):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 123]
+codetoanalyze/java/performance/ListTest.java, ListTest.iter_my_own_obj_FP(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 15 + 14 ⋅ a.length + 3 ⋅ (a.length + 1), O(a.length), degree = 1,{a.length + 1},Loop at line 120,{a.length},Loop at line 120]
+codetoanalyze/java/performance/ListTest.java, ListTest.iter_my_own_obj_FP(java.util.List):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [Call,Assignment,Call,<LHS trace>,Parameter `this.my_size`,Binary operation: ([0, +oo] + 1):signed32 by call to `void ListTest$MyOwnObj.my_put()` ]
+codetoanalyze/java/performance/ListTest.java, ListTest.iter_my_own_obj_FP(java.util.List):void, 4, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,Binary operation: ([0, +oo] + 1):signed32]
+codetoanalyze/java/performance/ListTest.java, ListTest.iter_relation_with_var(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 10 ⋅ a.length + 3 ⋅ (a.length + 1), O(a.length), degree = 1,{a.length + 1},Loop at line 104,{a.length},Loop at line 104]
 codetoanalyze/java/performance/ListTest.java, ListTest.iterate_elements_linear(java.util.List):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 5 ⋅ l.length + 3 ⋅ (l.length + 1), O(l.length), degree = 1,{l.length + 1},Loop at line 59,{l.length},Loop at line 59]
 codetoanalyze/java/performance/ListTest.java, ListTest.sort_comparator_nlogn(java.util.List):void, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + people.length × log(people.length), O(people.length × log(people.length)), degree = 1 + 1⋅log,{people.length},Modeled call to List.sort,{people.length},Modeled call to List.sort]
 codetoanalyze/java/performance/ListTest.java, ListTest.sublist(java.util.List):void, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 11 + 8 ⋅ (filesList.length - 1) + 3 ⋅ filesList.length, O(filesList.length), degree = 1,{filesList.length},Loop at line 32,{filesList.length - 1},Loop at line 32]