[inferbo] Inequality for iterator alias target

Summary:
This diff introduces inequality for the iterator alias target, as we
did for the size target before.

Reviewed By: ezgicicek

Differential Revision: D17879208

fbshipit-source-id: cc2f6a723

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -411,6 +411,10 @@ module Val = struct
 
   let prune_ge_one : t -> t = lift_prune1 Itv.prune_ge_one
 
+  let prune_length_le : t -> Itv.t -> t =
+   fun x y -> lift_prune_length1 (fun x -> Itv.prune_le x y) x
+
+
   let prune_length_lt : t -> Itv.t -> t =
    fun x y -> lift_prune_length1 (fun x -> Itv.prune_lt x y) x
 
@@ -865,7 +869,7 @@ module AliasTarget = struct
     | Empty of Loc.t
     | Size of {alias_typ: alias_typ; l: Loc.t; i: IntLit.t; java_tmp: Loc.t option}
     | Fgets of Loc.t
-    | IteratorOffset of {l: Loc.t; i: IntLit.t; java_tmp: Loc.t option}
+    | IteratorOffset of {alias_typ: alias_typ; l: Loc.t; i: IntLit.t; java_tmp: Loc.t option}
     | IteratorHasNext of {l: Loc.t; java_tmp: Loc.t option}
     | Top
   [@@deriving compare]
@@ -889,9 +893,9 @@ module AliasTarget = struct
             Loc.pp l pp_intlit i
       | Fgets l ->
           F.fprintf fmt "%t=fgets(%a)" pp_key Loc.pp l
-      | IteratorOffset {l; i; java_tmp} ->
+      | IteratorOffset {alias_typ; l; i; java_tmp} ->
-          F.fprintf fmt "iterator offset(%t%a)=length(%a)%a" pp_key pp_java_tmp java_tmp Loc.pp l
+          F.fprintf fmt "iterator offset(%t%a)%alength(%a)%a" pp_key pp_java_tmp java_tmp
-            pp_intlit i
+            alias_typ_pp alias_typ Loc.pp l pp_intlit i
       | IteratorHasNext {l; java_tmp} ->
           F.fprintf fmt "%t%a=hasNext(%a)" pp_key pp_java_tmp java_tmp Loc.pp l
       | Top ->
@@ -933,9 +937,9 @@ module AliasTarget = struct
         Option.map (f l) ~f:(fun l -> Size {alias_typ; l; i; java_tmp})
     | Fgets l ->
         Option.map (f l) ~f:(fun l -> Fgets l)
-    | IteratorOffset {l; i; java_tmp} ->
+    | IteratorOffset {alias_typ; l; i; java_tmp} ->
         let java_tmp = Option.bind java_tmp ~f in
-        Option.map (f l) ~f:(fun l -> IteratorOffset {l; i; java_tmp})
+        Option.map (f l) ~f:(fun l -> IteratorOffset {alias_typ; l; i; java_tmp})
     | IteratorHasNext {l; java_tmp} ->
         let java_tmp = Option.bind java_tmp ~f in
         Option.map (f l) ~f:(fun l -> IteratorHasNext {l; java_tmp})
@@ -948,7 +952,9 @@ module AliasTarget = struct
     ||
     match (lhs, rhs) with
     | ( Size {alias_typ= _; l= l1; i= i1; java_tmp= java_tmp1}
-      , Size {alias_typ= Le; l= l2; i= i2; java_tmp= java_tmp2} ) ->
+      , Size {alias_typ= Le; l= l2; i= i2; java_tmp= java_tmp2} )
+    | ( IteratorOffset {alias_typ= _; l= l1; i= i1; java_tmp= java_tmp1}
+      , IteratorOffset {alias_typ= Le; l= l2; i= i2; java_tmp= java_tmp2} ) ->
         (* (a=size(l)+2) <= (a>=size(l)+1)  *)
         (* (a>=size(l)+2) <= (a>=size(l)+1)  *)
         Loc.equal l1 l2 && IntLit.geq i1 i2 && Option.equal Loc.equal java_tmp1 java_tmp2
@@ -956,27 +962,38 @@ module AliasTarget = struct
         false
 
 
-  let join x y =
+  let join =
-    if equal x y then x
+    let locs_eq ~l1 ~java_tmp1 ~l2 ~java_tmp2 =
-    else
+      Loc.equal l1 l2 && Option.equal Loc.equal java_tmp1 java_tmp2
-      match (x, y) with
+    in
-      | ( Size {alias_typ= _; l= l1; i= i1; java_tmp= java_tmp1}
+    fun x y ->
-        , Size {alias_typ= _; l= l2; i= i2; java_tmp= java_tmp2} )
+      if equal x y then x
-        when Loc.equal l1 l2 && Option.equal Loc.equal java_tmp1 java_tmp2 ->
+      else
-          (* (a=size(l)+1) join (a=size(l)+2) is (a>=size(l)+1) *)
+        match (x, y) with
-          (* (a=size(l)+1) join (a>=size(l)+2) is (a>=size(l)+1) *)
+        | ( Size {alias_typ= _; l= l1; i= i1; java_tmp= java_tmp1}
-          Size {alias_typ= Le; l= l1; i= IntLit.min i1 i2; java_tmp= java_tmp1}
+          , Size {alias_typ= _; l= l2; i= i2; java_tmp= java_tmp2} )
-      | _, _ ->
+          when locs_eq ~l1 ~java_tmp1 ~l2 ~java_tmp2 ->
-          Top
+            (* (a=size(l)+1) join (a=size(l)+2) is (a>=size(l)+1) *)
+            (* (a=size(l)+1) join (a>=size(l)+2) is (a>=size(l)+1) *)
+            Size {alias_typ= Le; l= l1; i= IntLit.min i1 i2; java_tmp= java_tmp1}
+        | ( IteratorOffset {alias_typ= _; l= l1; i= i1; java_tmp= java_tmp1}
+          , IteratorOffset {alias_typ= _; l= l2; i= i2; java_tmp= java_tmp2} )
+          when locs_eq ~l1 ~java_tmp1 ~l2 ~java_tmp2 ->
+            IteratorOffset {alias_typ= Le; l= l1; i= IntLit.min i1 i2; java_tmp= java_tmp1}
+        | _, _ ->
+            Top
 
 
   let widen ~prev ~next ~num_iters:_ =
     if equal prev next then prev
     else
       match (prev, next) with
-      | Size {alias_typ= Eq}, Size {alias_typ= _} ->
+      | Size {alias_typ= Eq}, Size {alias_typ= _}
+      | IteratorOffset {alias_typ= Eq}, IteratorOffset {alias_typ= _} ->
           join prev next
-      | Size {alias_typ= Le; i= i1}, Size {alias_typ= _; i= i2} when IntLit.eq i1 i2 ->
+      | Size {alias_typ= Le; i= i1}, Size {alias_typ= _; i= i2}
+      | IteratorOffset {alias_typ= Le; i= i1}, IteratorOffset {alias_typ= _; i= i2}
+        when IntLit.eq i1 i2 ->
           join prev next
       | _, _ ->
           Top
@@ -988,8 +1005,8 @@ module AliasTarget = struct
     match x with
     | Size {alias_typ; l; i} when Loc.equal l loc ->
         Size {alias_typ; l; i= IntLit.(add i minus_one); java_tmp= None}
-    | IteratorOffset {l; i; java_tmp} when Loc.equal l loc ->
+    | IteratorOffset {alias_typ; l; i; java_tmp} when Loc.equal l loc ->
-        IteratorOffset {l; i= IntLit.(add i minus_one); java_tmp}
+        IteratorOffset {alias_typ; l; i= IntLit.(add i minus_one); java_tmp}
     | _ ->
         x
 end
@@ -1102,7 +1119,9 @@ module AliasMap = struct
 
 
   let add_iterator_offset_alias id arr x =
-    add (Key.of_id id) (AliasTarget.IteratorOffset {l= arr; i= IntLit.zero; java_tmp= None}) x
+    add (Key.of_id id)
+      (AliasTarget.IteratorOffset {alias_typ= Eq; l= arr; i= IntLit.zero; java_tmp= None})
+      x
 
 
   let incr_iterator_offset_alias id x =

infer/src/bufferoverrun/bufferOverrunSemantics.ml

@@ -527,11 +527,17 @@ module Prune = struct
 
   let prune_has_next ~true_branch iterator ({mem} as astate) =
     match Mem.find_alias_loc iterator mem with
-    | Some (IteratorOffset {l= arr_loc; i}) when IntLit.(eq i zero) ->
+    | Some (IteratorOffset {alias_typ; l= arr_loc; i}) when IntLit.(eq i zero) ->
         let length = collection_length_of_iterator iterator mem |> Val.get_itv in
         let v = Mem.find arr_loc mem in
-        let v' = (if true_branch then Val.prune_length_lt else Val.prune_length_eq) v length in
+        let v =
-        update_mem_in_prune arr_loc v' astate
+          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
+        in
+        update_mem_in_prune arr_loc v astate
     | _ ->
         astate
 

infer/src/bufferoverrun/itv.ml

@@ -658,6 +658,8 @@ let prune_comp : Binop.t -> t -> t -> t = fun comp -> bind2 (ItvPure.prune_comp
 
 let prune_lt : t -> t -> t = lift2 ItvPure.prune_lt
 
+let prune_le : t -> t -> t = lift2 ItvPure.prune_le
+
 let prune_eq : t -> t -> t = bind2 ItvPure.prune_eq
 
 let prune_ne : t -> t -> t = bind2 ItvPure.prune_ne

infer/src/bufferoverrun/itv.mli

@@ -233,6 +233,8 @@ val prune_ne : t -> t -> t
 
 val prune_lt : t -> t -> t
 
+val prune_le : t -> t -> t
+
 val subst : t -> Bound.eval_sym -> t
 
 val max_of_ikind : Typ.IntegerWidths.t -> Typ.ikind -> t

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

@@ -118,4 +118,26 @@ class ArrayListTest {
     } // a.size should be 0
     int j = a.get(0);
   }
+
+  void add_in_loop_iterator2_ok(ArrayList<Integer> b) {
+    ArrayList<Integer> a = new ArrayList<>();
+    for (Integer i : b) {
+      if (unknown_bool) {
+        a.add(i);
+      }
+    } // a.size should be [0, b.size]
+    if (a.size() > 0) {
+      int j = b.get(a.size() - 1);
+    }
+  }
+
+  void add_in_loop_iterator2_bad(ArrayList<Integer> b) {
+    ArrayList<Integer> a = new ArrayList<>();
+    for (Integer i : b) {
+      if (unknown_bool) {
+        a.add(i);
+      }
+    } // a.size should be [0, b.size]
+    int j = b.get(a.size());
+  }
 }

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_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_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]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alloc_is_negative_bad():void, 2, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1]
 codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.remove_in_loop_iterator_good_FP(java.util.ArrayList):void, 14, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `b.elements[*]`,Assignment,<Length trace>,Parameter `b.elements[*]`,Array access: Offset: b.length Size: b.length]

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

@@ -38,7 +38,7 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_mod
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.empty_list_constant(int):void, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ list.length, O(list.length), degree = 1,{list.length},Loop at line 14]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 11 ⋅ list.length + 2 ⋅ list.length × (11-max(10, list.elements)) + 3 ⋅ (list.length + 1) × (11-max(10, list.elements)), O(list.length × (-list.elements + 11)), degree = 2,{11-max(10, list.elements)},Loop at line 187,{list.length + 1},Loop at line 187,{11-max(10, list.elements)},Loop at line 187,{list.length},Loop at line 187]
-codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 11 ⋅ list1.length + 3 ⋅ (list1.length + 1), O(list1.length), degree = 1,{list1.length + 1},Loop at line 178,{list1.length},Loop at line 178]
+codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 14 ⋅ (list1.length + 1), O(list1.length), degree = 1,{list1.length + 1},Loop at line 178]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_local_arraylist(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length, O(list.length), degree = 1,{list.length},Loop at line 19]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 10 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 170,{list.length},Loop at line 170]
 codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 8 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 164,{list.length},Loop at line 164]