[inferbo] Update relation between iterator and integer value on Call

Summary:
This diff updates the relation between iterator (offset) and integer value not only at
assignments (`x += 1`), but also at function calls (`foo()`) that increase integer values by one in
their side effects.

Reviewed By: ezgicicek

Differential Revision: D19163214

fbshipit-source-id: 47e52f939

infer/src/bufferoverrun/bounds.ml

@@ -374,6 +374,15 @@ module Bound = struct
         is_symbolic x || is_symbolic y
 
 
+  let is_incr_of path = function
+    | Linear (i, se) ->
+        Z.(equal i one)
+        && Option.value_map (SymLinear.get_one_symbol_opt se) ~default:false ~f:(fun sym ->
+               Symb.SymbolPath.equal (Symb.SymbolPath.normal path) (Symb.Symbol.path sym) )
+    | _ ->
+        false
+
+
   let mk_MinMax (c, sign, m, d, s) =
     if Symb.Symbol.is_unsigned s && Z.(d <= zero) then
       match m with

infer/src/bufferoverrun/bounds.mli

@@ -132,6 +132,9 @@ module Bound : sig
   val is_same_one_symbol : t -> t -> bool
   (** It returns [true] when the two bounds are linear expressions of the same one symbol [1⋅s]. *)
 
+  val is_incr_of : Symb.SymbolPath.partial -> t -> bool
+  (** Check if [bound] is [path+1] when called [is_incr_of path bound] *)
+
   val exists_str : f:(string -> bool) -> t -> bool
 end
 

infer/src/bufferoverrun/bufferOverrunAnalysis.ml

@@ -167,8 +167,13 @@ module TransferFunctions = struct
       Sem.mk_eval_sym_trace integer_type_widths callee_formals params caller_mem
         ~mode:Sem.EvalNormal
     in
-    instantiate_mem_reachable ret callee_formals callee_pname ~callee_exit_mem eval_sym_trace
-      caller_mem location
+    let mem =
+      instantiate_mem_reachable ret callee_formals callee_pname ~callee_exit_mem eval_sym_trace
+        caller_mem location
+    in
+    if Language.curr_language_is Java then
+      Dom.Mem.incr_iterator_simple_alias_on_call eval_sym_trace ~callee_exit_mem mem
+    else mem
 
 
   let rec is_array_access_exp = function

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -500,6 +500,10 @@ module Val = struct
 
   let is_mone x = Itv.is_mone (get_itv x)
 
+  let is_incr_of l {itv} =
+    Option.value_map (Loc.get_path l) ~default:false ~f:(fun path -> Itv.is_incr_of path itv)
+
+
   let cast typ v = {v with powloc= PowLoc.cast typ v.powloc}
 
   let of_path tenv ~may_last_field integer_type_widths location typ path =
@@ -686,6 +690,8 @@ module MVal = struct
   let get_rep_multi (represents_multiple_values, _) = represents_multiple_values
 
   let get_val (_, v) = v
+
+  let is_incr_of l (m, v) = (not m) && Val.is_incr_of l v
 end
 
 module MemPure = struct
@@ -773,6 +779,11 @@ module MemPure = struct
 
   let is_rep_multi_loc l m = Option.value_map ~default:false (find_opt l m) ~f:MVal.get_rep_multi
 
+  (** Collect the location that was increased by one, i.e., [x -> x+1] *)
+  let get_incr_locs m =
+    fold (fun l v acc -> if MVal.is_incr_of l v then PowLoc.add l acc else acc) m PowLoc.empty
+
+
   let find_opt l m = Option.map (find_opt l m) ~f:MVal.get_val
 
   let add ?(represents_multiple_values = false) l v m =
@@ -1163,6 +1174,18 @@ module AliasMap = struct
     M.fold accum_tgts prev x
 
 
+  let incr_iterator_simple_alias_on_call {eval_locpath} ~callee_locs x =
+    let accum_increased_alias callee_loc acc =
+      Option.value_map (Loc.get_path callee_loc) ~default:acc ~f:(fun callee_path ->
+          match PowLoc.is_singleton_or_more (eval_locpath callee_path) with
+          | IContainer.Singleton loc ->
+              incr_iterator_simple_alias ~prev:x loc IntLit.one acc
+          | IContainer.Empty | IContainer.More ->
+              acc )
+    in
+    PowLoc.fold accum_increased_alias callee_locs x
+
+
   let store_n ~prev loc id n x =
     let accum_size_alias rhs tgt acc =
       match tgt with
@@ -1369,6 +1392,9 @@ module Alias = struct
   let remove_temp : Ident.t -> t -> t = fun temp -> lift_map (AliasMap.remove (KeyLhs.of_id temp))
 
   let forget_size_alias arr_locs = lift_map (AliasMap.forget_size_alias arr_locs)
+
+  let incr_iterator_simple_alias_on_call eval_sym_trace ~callee_locs =
+    lift_map (AliasMap.incr_iterator_simple_alias_on_call eval_sym_trace ~callee_locs)
 end
 
 module CoreVal = struct
@@ -1928,6 +1954,11 @@ module MemReach = struct
     {m with alias= Alias.add_iterator_has_next_alias ~ret_id ~iterator m.alias}
 
 
+  let incr_iterator_simple_alias_on_call eval_sym_trace ~callee_exit_mem m =
+    let callee_locs = MemPure.get_incr_locs callee_exit_mem.mem_pure in
+    {m with alias= Alias.incr_iterator_simple_alias_on_call eval_sym_trace ~callee_locs m.alias}
+
+
   let add_stack_loc : Loc.t -> t -> t = fun k m -> {m with stack_locs= StackLocs.add k m.stack_locs}
 
   let add_stack : ?represents_multiple_values:bool -> Loc.t -> Val.t -> t -> t =
@@ -2297,6 +2328,14 @@ module Mem = struct
         m
 
 
+  let incr_iterator_simple_alias_on_call eval_sym_trace ~callee_exit_mem m =
+    match (callee_exit_mem, m) with
+    | NonBottom callee_exit_mem, NonBottom m ->
+        NonBottom (MemReach.incr_iterator_simple_alias_on_call eval_sym_trace ~callee_exit_mem m)
+    | _, _ ->
+        m
+
+
   let add_stack_loc : Loc.t -> t -> t = fun k -> map ~f:(MemReach.add_stack_loc k)
 
   let add_stack : ?represents_multiple_values:bool -> Loc.t -> Val.t -> t -> t =

infer/src/bufferoverrun/bufferOverrunDomain.mli

@@ -573,6 +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 incr_iterator_simple_alias_on_call : eval_sym_trace -> callee_exit_mem:no_oenv_t -> t -> t
+  (** Update [AliasTarget.IteratorSimple] alias at function calls *)
+
   val add_iterator_alias : Ident.t -> t -> t
   (** Add [AliasTarget.IteratorSimple] and [AliasTarget.IteratorOffset] aliases when
       [Iteratable.iterator()] is called *)

infer/src/bufferoverrun/itv.ml

@@ -586,6 +586,8 @@ module ItvPure = struct
 
 
   let has_void_ptr_symb x = Bound.has_void_ptr_symb (lb x) || Bound.has_void_ptr_symb (ub x)
+
+  let is_incr_of path x = Bound.is_incr_of path (lb x) && Bound.is_incr_of path (ub x)
 end
 
 include AbstractDomain.BottomLifted (ItvPure)
@@ -827,3 +829,5 @@ let is_offset_path_of path = bind1_gen ~bot:false (ItvPure.is_offset_path_of pat
 let is_length_path_of path = bind1_gen ~bot:false (ItvPure.is_length_path_of path)
 
 let has_only_non_int_symbols = bind1bool ItvPure.has_only_non_int_symbols
+
+let is_incr_of path = bind1bool (ItvPure.is_incr_of path)

infer/src/bufferoverrun/itv.mli

@@ -268,3 +268,6 @@ val is_offset_path_of : Symb.SymbolPath.partial -> t -> bool
 val is_length_path_of : Symb.SymbolPath.partial -> t -> bool
 
 val has_only_non_int_symbols : t -> bool
+
+val is_incr_of : Symb.SymbolPath.partial -> t -> bool
+(** Check if [itv] is [path+1] when called [is_incr_of path itv] *)

infer/src/bufferoverrun/symb.mli

@@ -37,6 +37,7 @@ module SymbolPath : sig
     | Offset of {p: partial; is_void: bool}
     | Length of {p: partial; is_void: bool}
     | Modeled of partial
+  [@@deriving equal]
 
   val equal_partial : partial -> partial -> bool
 

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

@@ -115,7 +115,7 @@ class ListTest {
     }
   }
 
-  void iter_my_own_obj_FP(List<Integer> a) {
+  void iter_my_own_obj(List<Integer> a) {
     MyOwnObj o = new MyOwnObj();
     for (Integer i : a) {
       o.my_put();

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

@@ -164,10 +164,7 @@ 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_my_own_obj(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_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]