From 3d087ff5e566ae5594514460e1a04eb9c51cc29d Mon Sep 17 00:00:00 2001
From: Sungkeun Cho <scho@fb.com>
Date: Thu, 19 Dec 2019 07:07:40 -0800
Subject: [PATCH] [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 | 9 +++++
infer/src/bufferoverrun/bounds.mli | 3 ++
.../bufferoverrun/bufferOverrunAnalysis.ml | 9 ++++-
.../src/bufferoverrun/bufferOverrunDomain.ml | 39 +++++++++++++++++++
.../src/bufferoverrun/bufferOverrunDomain.mli | 3 ++
infer/src/bufferoverrun/itv.ml | 4 ++
infer/src/bufferoverrun/itv.mli | 3 ++
infer/src/bufferoverrun/symb.mli | 1 +
.../java/performance/ListTest.java | 2 +-
.../codetoanalyze/java/performance/issues.exp | 5 +--
10 files changed, 71 insertions(+), 7 deletions(-)
diff --git a/infer/src/bufferoverrun/bounds.ml b/infer/src/bufferoverrun/bounds.ml
index 5c044957f..5cc4265f1 100644
--- a/infer/src/bufferoverrun/bounds.ml
+++ b/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
diff --git a/infer/src/bufferoverrun/bounds.mli b/infer/src/bufferoverrun/bounds.mli
index 92f40e348..87bcc85e5 100644
--- a/infer/src/bufferoverrun/bounds.mli
+++ b/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
diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
index 78481fa25..8bb7169ce 100644
--- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml
+++ b/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
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml
index 2545f30a4..cea7ad454 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.ml
+++ b/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 =
diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli
index 62327d42e..962f76e5f 100644
--- a/infer/src/bufferoverrun/bufferOverrunDomain.mli
+++ b/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 *)
diff --git a/infer/src/bufferoverrun/itv.ml b/infer/src/bufferoverrun/itv.ml
index 1cc3f5590..5b4bff8c8 100644
--- a/infer/src/bufferoverrun/itv.ml
+++ b/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)
diff --git a/infer/src/bufferoverrun/itv.mli b/infer/src/bufferoverrun/itv.mli
index 55939f109..b6db80f25 100644
--- a/infer/src/bufferoverrun/itv.mli
+++ b/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] *)
diff --git a/infer/src/bufferoverrun/symb.mli b/infer/src/bufferoverrun/symb.mli
index 8c890bc4b..92fba38f6 100644
--- a/infer/src/bufferoverrun/symb.mli
+++ b/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
diff --git a/infer/tests/codetoanalyze/java/performance/ListTest.java b/infer/tests/codetoanalyze/java/performance/ListTest.java
index a5156d77e..a95c6aa71 100644
--- a/infer/tests/codetoanalyze/java/performance/ListTest.java
+++ b/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();
diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp
index 41c8bae44..5bea6da14 100644
--- a/infer/tests/codetoanalyze/java/performance/issues.exp
+++ b/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]