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 a) { + void iter_my_own_obj(List 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,,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, [,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]