From 7e3275dcc864aafa1498bd725e3e857300728185 Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 19 Dec 2019 07:07:36 -0800 Subject: [PATCH] [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 --- .../src/bufferoverrun/bufferOverrunDomain.ml | 153 ++++++++++++------ .../src/bufferoverrun/bufferOverrunDomain.mli | 13 +- .../src/bufferoverrun/bufferOverrunModels.ml | 2 +- .../bufferoverrun/bufferOverrunSemantics.ml | 20 ++- .../java/performance/ListTest.java | 24 +++ .../codetoanalyze/java/performance/issues.exp | 5 + 6 files changed, 154 insertions(+), 63 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 601491437..2545f30a4 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/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 accum_incr_iterator_offset_alias rhs tgt acc = - match tgt with - | AliasTarget.IteratorOffset ({i; java_tmp} as tgt) -> - let i = IntLit.(add i one) in - let acc = - 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 ) + let incr_iterator_offset_alias = + let apply_i ~f = function + | AliasTarget.IteratorSimple ({i} as tgt) -> + AliasTarget.IteratorSimple {tgt with i= f i} + | AliasTarget.IteratorOffset ({i} as tgt) -> + AliasTarget.IteratorOffset {tgt with i= f i} | _ -> - acc + assert false in - match M.find_opt (KeyLhs.of_id id) x with - | Some tgts -> - AliasTargets.fold accum_incr_iterator_offset_alias tgts x - | _ -> - x + let java_tmp_none = function + | AliasTarget.IteratorSimple tgt -> + AliasTarget.IteratorSimple {tgt with java_tmp= None} + | AliasTarget.IteratorOffset tgt -> + 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 arr_locs = - let add_arr l v acc = if Itv.is_zero (Val.array_sizeof v) then PowLoc.add l acc else acc in - MemPure.fold add_arr m.mem_pure PowLoc.empty + let add_iterator_alias_common ~cond ~alias_add id m = + let locs = + let accum_loc l v acc = if cond v then PowLoc.add l acc else acc in + 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 = - fun id -> map ~f:(MemReach.add_iterator_offset_alias id) - + let add_iterator_alias : Ident.t -> t -> t = fun id -> map ~f:(MemReach.add_iterator_alias id) let incr_iterator_offset_alias : Exp.t -> t -> t = fun iterator m -> diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.mli b/infer/src/bufferoverrun/bufferOverrunDomain.mli index e4bb3d775..62327d42e 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.mli +++ b/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 - (** Add [AliasTarget.IteratorOffset] alias when [Iteratable.iterator()] is called *) + val add_iterator_alias : Ident.t -> t -> t + (** 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 *) diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 57be1d243..caf5c33d2 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/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} diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index b2d605398..98d17647b 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/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 v = Mem.find arr_loc mem in - let v = - let prune_f = + let prune_f v length = + let 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 diff --git a/infer/tests/codetoanalyze/java/performance/ListTest.java b/infer/tests/codetoanalyze/java/performance/ListTest.java index 958edced5..a5156d77e 100644 --- a/infer/tests/codetoanalyze/java/performance/ListTest.java +++ b/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 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 a) { + MyOwnObj o = new MyOwnObj(); + for (Integer i : a) { + o.my_put(); + } + for (int i = 0; i < o.my_size; i++) {} + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 94980384f..41c8bae44 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/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,,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_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]