From f3311dfd985d4464388941e5a03ef1d593b5f0eb Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Thu, 25 Jul 2019 10:47:31 -0700 Subject: [PATCH] [inferbo] Weak update on array contents Summary: The `represents_multiple_values` flag was adopted to decide whether updating abstract value strongly or weakly. However, the flag was included in the `Val` domain, which is strange, because it is a property of abstract locations, rather than abstract values. This makes the behavior of memory update function depend on the abstract value to update, making its code complicated. This diff detach the `represents_multiple_values` flag from the `Value` domain, thus the memory update does not depend on the abstract value. Since this is a refactoring, I believe the diff should not make many semantic changes. Reviewed By: ezgicicek Differential Revision: D16441734 fbshipit-source-id: 4c10779d7 --- infer/src/bufferoverrun/absLoc.ml | 9 ++ .../bufferoverrun/bufferOverrunAnalysis.ml | 30 ++-- .../src/bufferoverrun/bufferOverrunDomain.ml | 133 ++++++++++-------- infer/src/bufferoverrun/bufferOverrunUtils.ml | 16 +-- .../codetoanalyze/java/performance/Array.java | 17 +++ .../codetoanalyze/java/performance/issues.exp | 5 + 6 files changed, 130 insertions(+), 80 deletions(-) diff --git a/infer/src/bufferoverrun/absLoc.ml b/infer/src/bufferoverrun/absLoc.ml index 06b6534e7..d9b0d140d 100644 --- a/infer/src/bufferoverrun/absLoc.ml +++ b/infer/src/bufferoverrun/absLoc.ml @@ -248,6 +248,13 @@ module Loc = struct false + let is_java_collection_internal_array = function + | Field (_, fn) -> + Typ.Fieldname.equal fn BufferOverrunField.java_collection_internal_array + | _ -> + false + + let rec is_pretty = function | Var _ -> true @@ -333,6 +340,8 @@ module Loc = struct false | Allocsite allocsite -> Allocsite.represents_multiple_values allocsite + | Field _ as x when is_c_strlen x || is_java_collection_internal_array x -> + false | Field (l, _) -> represents_multiple_values l | StarField _ -> diff --git a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml index f9bd742c8..b8efbc2f0 100644 --- a/infer/src/bufferoverrun/bufferOverrunAnalysis.ml +++ b/infer/src/bufferoverrun/bufferOverrunAnalysis.ml @@ -216,23 +216,21 @@ module TransferFunctions = struct else mem in let mem = - if not v.represents_multiple_values then - match PowLoc.is_singleton_or_more locs with - | IContainer.Singleton loc_v -> ( - let pname = Summary.get_proc_name summary in - match Typ.Procname.get_method pname with - | "__inferbo_empty" when Loc.is_return loc_v -> ( - match Procdesc.get_pvar_formals (Summary.get_proc_desc summary) with - | [(formal, _)] -> - let formal_v = Dom.Mem.find (Loc.of_pvar formal) mem in - Dom.Mem.store_empty_alias formal_v loc_v mem - | _ -> - assert false ) + match PowLoc.is_singleton_or_more locs with + | IContainer.Singleton loc_v -> ( + let pname = Summary.get_proc_name summary in + match Typ.Procname.get_method pname with + | "__inferbo_empty" when Loc.is_return loc_v -> ( + match Procdesc.get_pvar_formals (Summary.get_proc_desc summary) with + | [(formal, _)] -> + let formal_v = Dom.Mem.find (Loc.of_pvar formal) mem in + Dom.Mem.store_empty_alias formal_v loc_v mem | _ -> - Dom.Mem.store_simple_alias loc_v exp2 mem ) - | _ -> - mem - else mem + assert false ) + | _ -> + Dom.Mem.store_simple_alias loc_v exp2 mem ) + | _ -> + mem in let mem = Dom.Mem.update_latest_prune ~updated_locs:locs exp1 exp2 mem in mem diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index f43a4f52c..75db28840 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -39,8 +39,7 @@ module Val = struct ; arrayblk: ArrayBlk.t ; offset_sym: Relation.Sym.t ; size_sym: Relation.Sym.t - ; traces: TraceSet.t - ; represents_multiple_values: bool } + ; traces: TraceSet.t } let bot : t = { itv= Itv.bot @@ -50,8 +49,7 @@ module Val = struct ; arrayblk= ArrayBlk.bot ; offset_sym= Relation.Sym.bot ; size_sym= Relation.Sym.bot - ; traces= TraceSet.bottom - ; represents_multiple_values= false } + ; traces= TraceSet.bottom } let pp fmt x = @@ -65,14 +63,9 @@ module Val = struct let trace_pp fmt traces = if Config.bo_debug >= 1 then F.fprintf fmt ", %a" TraceSet.pp traces in - let represents_multiple_values_str = if x.represents_multiple_values then "M" else "" in - F.fprintf fmt "%s(%a%a%a, %a, %a%a%a%a)" represents_multiple_values_str Itv.pp x.itv - itv_thresholds_pp x.itv_thresholds relation_sym_pp x.sym PowLoc.pp x.powloc ArrayBlk.pp - x.arrayblk relation_sym_pp x.offset_sym relation_sym_pp x.size_sym trace_pp x.traces - - - let sets_represents_multiple_values : represents_multiple_values:bool -> t -> t = - fun ~represents_multiple_values x -> {x with represents_multiple_values} + F.fprintf fmt "(%a%a%a, %a, %a%a%a%a)" Itv.pp x.itv itv_thresholds_pp x.itv_thresholds + relation_sym_pp x.sym PowLoc.pp x.powloc ArrayBlk.pp x.arrayblk relation_sym_pp x.offset_sym + relation_sym_pp x.size_sym trace_pp x.traces let unknown_from : callee_pname:_ -> location:_ -> t = @@ -85,8 +78,7 @@ module Val = struct ; arrayblk= ArrayBlk.unknown ; offset_sym= Relation.Sym.top ; size_sym= Relation.Sym.top - ; traces - ; represents_multiple_values= false } + ; traces } let ( <= ) ~lhs ~rhs = @@ -99,7 +91,6 @@ module Val = struct && ArrayBlk.( <= ) ~lhs:lhs.arrayblk ~rhs:rhs.arrayblk && Relation.Sym.( <= ) ~lhs:lhs.offset_sym ~rhs:rhs.offset_sym && Relation.Sym.( <= ) ~lhs:lhs.size_sym ~rhs:rhs.size_sym - && Bool.( <= ) lhs.represents_multiple_values rhs.represents_multiple_values let widen ~prev ~next ~num_iters = @@ -116,9 +107,7 @@ module Val = struct ; arrayblk= ArrayBlk.widen ~prev:prev.arrayblk ~next:next.arrayblk ~num_iters ; offset_sym= Relation.Sym.widen ~prev:prev.offset_sym ~next:next.offset_sym ~num_iters ; size_sym= Relation.Sym.widen ~prev:prev.size_sym ~next:next.size_sym ~num_iters - ; traces= TraceSet.join prev.traces next.traces - ; represents_multiple_values= - prev.represents_multiple_values || next.represents_multiple_values } + ; traces= TraceSet.join prev.traces next.traces } let join : t -> t -> t = @@ -132,8 +121,7 @@ module Val = struct ; arrayblk= ArrayBlk.join x.arrayblk y.arrayblk ; offset_sym= Relation.Sym.join x.offset_sym y.offset_sym ; size_sym= Relation.Sym.join x.size_sym y.size_sym - ; traces= TraceSet.join x.traces y.traces - ; represents_multiple_values= x.represents_multiple_values || y.represents_multiple_values } + ; traces= TraceSet.join x.traces y.traces } let get_itv : t -> Itv.t = fun x -> x.itv @@ -291,21 +279,10 @@ module Val = struct let lor_sem : t -> t -> t = lift_cmp_itv Itv.lor_sem Boolean.EqualOrder.top - (* TODO: get rid of those cases *) - let warn_against_pruning_multiple_values : t -> t = - fun x -> - if x.represents_multiple_values && Config.write_html then - L.d_printfln_escaped ~color:Pp.Red "Pruned %a that represents multiple values" pp x ; - x - - - let lift_prune1 : (Itv.t -> Itv.t) -> t -> t = - fun f x -> warn_against_pruning_multiple_values {x with itv= f x.itv} - + let lift_prune1 : (Itv.t -> Itv.t) -> t -> t = fun f x -> {x with itv= f x.itv} let lift_prune_length1 : (Itv.t -> Itv.t) -> t -> t = - fun f x -> - warn_against_pruning_multiple_values {x with arrayblk= ArrayBlk.transform_length ~f x.arrayblk} + fun f x -> {x with arrayblk= ArrayBlk.transform_length ~f x.arrayblk} let lift_prune2 : @@ -326,9 +303,7 @@ module Val = struct && phys_equal arrayblk x.arrayblk then (* x hasn't changed, don't join traces *) x - else - warn_against_pruning_multiple_values - {x with itv; itv_thresholds; arrayblk; traces= TraceSet.join x.traces y.traces} + else {x with itv; itv_thresholds; arrayblk; traces= TraceSet.join x.traces y.traces} let prune_eq_zero : t -> t = lift_prune1 Itv.prune_eq_zero @@ -588,8 +563,28 @@ module StackLocs = struct let bot = empty end +(* MultiLocs denotes whether abstract locations represent one or multiple concrete locations. If + the value is true, the abstract location may represent multiple concrete locations, thus it + should be updated weakly. *) +module MultiLocs = AbstractDomain.BooleanOr + +module MVal = struct + include AbstractDomain.Pair (MultiLocs) (Val) + + let pp fmt (represents_multiple_values, v) = + if represents_multiple_values then F.fprintf fmt "M" ; + Val.pp fmt v + + + let on_demand ~default ?typ oenv l = + (Loc.represents_multiple_values l, Val.on_demand ~default ?typ oenv l) + + + let get_val (_, v) = v +end + module MemPure = struct - include AbstractDomain.Map (Loc) (Val) + include AbstractDomain.Map (Loc) (MVal) let bot = empty @@ -597,7 +592,7 @@ module MemPure = struct filter_loc:(Loc.t -> LoopHeadLoc.t option) -> t -> Polynomials.NonNegativePolynomial.t = fun ~filter_loc mem -> fold - (fun loc v acc -> + (fun loc (_, v) acc -> match filter_loc loc with | Some loop_head_loc -> v |> Val.get_itv |> Itv.range loop_head_loc |> Itv.ItvRange.to_top_lifted_polynomial @@ -614,10 +609,10 @@ module MemPure = struct (fun l v1_opt v2_opt -> match (v1_opt, v2_opt) with | Some v1, Some v2 -> - Some (Val.join v1 v2) + Some (MVal.join v1 v2) | Some v1, None | None, Some v1 -> - let v2 = Val.on_demand ~default:Val.bot oenv l in - Some (Val.join v1 v2) + let v2 = MVal.on_demand ~default:Val.bot oenv l in + Some (MVal.join v1 v2) | None, None -> None ) astate1 astate2 @@ -630,16 +625,35 @@ module MemPure = struct (fun l v1_opt v2_opt -> match (v1_opt, v2_opt) with | Some v1, Some v2 -> - Some (Val.widen ~prev:v1 ~next:v2 ~num_iters) + Some (MVal.widen ~prev:v1 ~next:v2 ~num_iters) | Some v1, None -> - let v2 = Val.on_demand ~default:Val.bot oenv l in - Some (Val.widen ~prev:v1 ~next:v2 ~num_iters) + let v2 = MVal.on_demand ~default:Val.bot oenv l in + Some (MVal.widen ~prev:v1 ~next:v2 ~num_iters) | None, Some v2 -> - let v1 = Val.on_demand ~default:Val.bot oenv l in - Some (Val.widen ~prev:v1 ~next:v2 ~num_iters) + let v1 = MVal.on_demand ~default:Val.bot oenv l in + Some (MVal.widen ~prev:v1 ~next:v2 ~num_iters) | None, None -> None ) prev next + + + let find_opt l m = Option.map (find_opt l m) ~f:MVal.get_val + + let add ?(represents_multiple_values = false) l v m = + let f = function + | None -> + Some (represents_multiple_values || Loc.represents_multiple_values l, v) + | Some (represents_multiple_values', v') -> + let represents_multiple_values = + represents_multiple_values || represents_multiple_values' + in + let v = if represents_multiple_values then Val.join v' v else v in + Some (represents_multiple_values, v) + in + update l f m + + + let fold f m init = fold (fun k range acc -> f k (MVal.get_val range) acc) m init end module AliasTarget = struct @@ -1335,17 +1349,19 @@ module MemReach = struct let add_stack_loc : Loc.t -> t -> t = fun k m -> {m with stack_locs= StackLocs.add k m.stack_locs} - let add_stack : Loc.t -> Val.t -> t -> t = - fun k v m -> - {m with stack_locs= StackLocs.add k m.stack_locs; mem_pure= MemPure.add k v m.mem_pure} + let add_stack : ?represents_multiple_values:bool -> Loc.t -> Val.t -> t -> t = + fun ?represents_multiple_values k v m -> + { m with + stack_locs= StackLocs.add k m.stack_locs + ; mem_pure= MemPure.add ?represents_multiple_values k v m.mem_pure } let replace_stack : Loc.t -> Val.t -> t -> t = fun k v m -> {m with mem_pure= MemPure.add k v m.mem_pure} - let add_heap : Loc.t -> Val.t -> t -> t = - fun x v m -> + let add_heap : ?represents_multiple_values:bool -> Loc.t -> Val.t -> t -> t = + fun ?represents_multiple_values x v m -> let v = let sym = if Itv.is_bottom (Val.get_itv v) then Relation.Sym.bot else Relation.Sym.of_loc x @@ -1356,7 +1372,7 @@ module MemReach = struct in {v with Val.sym; Val.offset_sym; Val.size_sym} in - {m with mem_pure= MemPure.add x v m.mem_pure} + {m with mem_pure= MemPure.add ?represents_multiple_values x v m.mem_pure} let add_unknown_from : @@ -1377,7 +1393,8 @@ module MemReach = struct let transform_mem1 l m = let add, find = if is_stack_loc l m then (replace_stack, find_stack) - else (add_heap, find_heap_default ~default:Val.bot ?typ:None) + else + (add_heap ~represents_multiple_values:false, find_heap_default ~default:Val.bot ?typ:None) in add l (f l (find l m)) m in @@ -1639,9 +1656,15 @@ module Mem = struct let add_stack_loc : Loc.t -> t -> t = fun k -> map ~f:(MemReach.add_stack_loc k) - let add_stack : Loc.t -> Val.t -> t -> t = fun k v -> map ~f:(MemReach.add_stack k v) + let add_stack : ?represents_multiple_values:bool -> Loc.t -> Val.t -> t -> t = + fun ?represents_multiple_values k v -> + map ~f:(MemReach.add_stack ?represents_multiple_values k v) + + + let add_heap : ?represents_multiple_values:bool -> Loc.t -> Val.t -> t -> t = + fun ?represents_multiple_values k v -> + map ~f:(MemReach.add_heap ?represents_multiple_values k v) - let add_heap : Loc.t -> Val.t -> t -> t = fun k v -> map ~f:(MemReach.add_heap k v) let add_unknown_from : Ident.t -> callee_pname:Typ.Procname.t -> location:Location.t -> t -> t = fun id ~callee_pname ~location -> diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index b3f8a8246..15f0fe26d 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -35,13 +35,11 @@ module Exec = struct let load_locs id typ locs mem = let v = Dom.Mem.find_set ~typ locs mem in let mem = Dom.Mem.add_stack (Loc.of_id id) v mem in - if not v.represents_multiple_values then - match PowLoc.is_singleton_or_more locs with - | IContainer.Singleton loc -> - Dom.Mem.load_simple_alias id loc mem - | _ -> - mem - else mem + match PowLoc.is_singleton_or_more locs with + | IContainer.Singleton loc -> + Dom.Mem.load_simple_alias id loc mem + | _ -> + mem let rec decl_local_loc ({tenv} as model_env) loc typ ~inst_num ~represents_multiple_values @@ -80,9 +78,9 @@ module Exec = struct | Language.Java -> (Dom.Val.of_java_array_alloc allocsite ~length:size ~traces, None) in - let arr = Dom.Val.sets_represents_multiple_values arr ~represents_multiple_values in let mem = Dom.Mem.init_array_relation allocsite ~offset_opt ~size ~size_exp_opt:None mem in - if Int.equal dimension 1 then Dom.Mem.add_stack loc arr mem else Dom.Mem.add_heap loc arr mem + if Int.equal dimension 1 then Dom.Mem.add_stack ~represents_multiple_values loc arr mem + else Dom.Mem.add_heap ~represents_multiple_values loc arr mem in let loc = Loc.of_allocsite allocsite in let mem, _ = diff --git a/infer/tests/codetoanalyze/java/performance/Array.java b/infer/tests/codetoanalyze/java/performance/Array.java index ab25e50bf..e36e2eb2a 100644 --- a/infer/tests/codetoanalyze/java/performance/Array.java +++ b/infer/tests/codetoanalyze/java/performance/Array.java @@ -70,4 +70,21 @@ public class Array { String[] arr = new String[i]; Arrays.binarySearch(arr, "u"); } + + String[] gen_and_iter_types(int length) { + String[] result = new String[length]; + for (int i = 0; i < length; i++) {} + return result; + } + + void call_gen_and_iter_types(int x) { + String[] r = gen_and_iter_types(x); + for (int i = 0; i < r.length; i++) {} + } + + void call_gen_and_iter_types_linear_FP(int x, int y) { + String[] r1 = gen_and_iter_types(x); + String[] r2 = gen_and_iter_types(y); + for (int i = 0; i < r2.length; i++) {} // should not be infinite execution time + } } diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 037327381..ec87add98 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -4,9 +4,14 @@ codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array. codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.array_access_weird_ok(long[],int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ length, degree = 1,{length},Loop at line 30] codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.binary_search_log(java.lang.String[]):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + log(arr.length), degree = 0 + 1⋅log,{arr.length},Modeled call to Arrays.binarySearch] codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.bsearch_log(int):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + log(i), degree = 0 + 1⋅log,{i},Modeled call to Arrays.binarySearch] +codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.call_gen_and_iter_types(int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 13 + 5 ⋅ x, degree = 1,{x},call to java.lang.String[] Array.gen_and_iter_types(int),Loop at line 76] +codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.call_gen_and_iter_types_linear_FP(int,int):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 88] +codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.call_gen_and_iter_types_linear_FP(int,int):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 13 + 5 ⋅ x, degree = 1,{x},call to java.lang.String[] Array.gen_and_iter_types(int),Loop at line 76] +codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.call_gen_and_iter_types_linear_FP(int,int):void, 3, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.copyOf_linear(java.lang.String[]):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + arr.length, degree = 1,{arr.length},Modeled call to Arrays.copyOf] codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.fill_big_constant():void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 307, degree = 0] codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.fill_linear(java.lang.String[]):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + arr.length, degree = 1,{arr.length},Modeled call to Arrays.fill] +codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.gen_and_iter_types(int):java.lang.String[], 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ length, degree = 1,{length},Loop at line 76] codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.init_array_linear():void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2564, degree = 0] codetoanalyze/java/performance/Array.java, codetoanalyze.java.performance.Array.sort_array_nlogn(int):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + size × log(size), degree = 1 + 1⋅log,{size},Modeled call to Arrays.sort,{size},Modeled call to Arrays.sort] codetoanalyze/java/performance/ArrayCost.java, ArrayCost.ArrayCost(int[]):void, 5, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ mag.length, degree = 1,{mag.length},Loop at line 15]