From ebbc0fc7f295ba84964721db2956b4e0eb14fe8e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Fri, 28 Feb 2020 02:35:35 -0800 Subject: [PATCH] [cost] Add traces for ZERO_* issues Summary: The issue type `ZERO_EXECUTION_TIME` actually corresponds to bottom state but has been mistakenly used to mean - unreachable nodes (program never reaching exit state) - having zero cost (e.g. for allocations). Note that, for execution costs, the latter doesn't make sense since we always incur a unit cost for the start node. Hence, a function with empty body will have unit cost. For allocations or IO however, we only incur costs for specific primitives, so a function with no allocations/IO could have a zero cost. However, there is no point reporting functions with zero cost as a specific issue type. Instead, what we want to track is the former, i.e. functions whose cost becomes 0 due to program never reaching exit state. This diff aims to split these cases into two by only reporting on the latter and adds traces to bottom/unreachable cost by creating a special category in polynomials. Next diff will rename `ZERO_XXX` to `XXX_UNREACHABLE_AT_EXIT`. Reviewed By: skcho Differential Revision: D20005774 fbshipit-source-id: 46b9abd5a --- infer/src/absint/AbstractDomain.ml | 61 +++++-- infer/src/absint/AbstractDomain.mli | 40 +++-- infer/src/backend/Differential.ml | 16 +- infer/src/bufferoverrun/polynomials.ml | 156 ++++++++++++++---- infer/src/bufferoverrun/polynomials.mli | 20 ++- infer/src/cost/boundMap.ml | 10 +- infer/src/cost/cost.ml | 16 +- infer/src/cost/costDomain.ml | 5 +- infer/src/cost/costDomain.mli | 4 +- .../codetoanalyze/c/performance/issues.exp | 6 +- .../codetoanalyze/java/performance/issues.exp | 2 +- 11 files changed, 243 insertions(+), 93 deletions(-) diff --git a/infer/src/absint/AbstractDomain.ml b/infer/src/absint/AbstractDomain.ml index 109189e96..69fa1c11c 100644 --- a/infer/src/absint/AbstractDomain.ml +++ b/infer/src/absint/AbstractDomain.ml @@ -13,7 +13,7 @@ module Types = struct type 'astate top_lifted = Top | NonTop of 'astate - type ('below, 'above) below_above = Below of 'below | Above of 'above + type ('below, 'astate, 'above) below_above = Below of 'below | Above of 'above | Val of 'astate end open! Types @@ -256,65 +256,90 @@ module Flat (V : PrettyPrintable.PrintableEquatableType) = struct end module StackedUtils = struct - let compare x1 x2 ~cmp_below ~cmp_above = + let compare x1 x2 ~cmp_below ~cmp ~cmp_above = if phys_equal x1 x2 then 0 else match (x1, x2) with | Below b1, Below b2 -> cmp_below b1 b2 - | Below _, Above _ -> + | Below _, _ -> -1 - | Above _, Below _ -> + | _, Below _ -> 1 | Above a1, Above a2 -> cmp_above a1 a2 + | Above _, _ -> + 1 + | _, Above _ -> + -1 + | Val v1, Val v2 -> + cmp v1 v2 - let leq ~leq_below ~leq_above ~lhs ~rhs = + let leq ~leq_below ~leq ~leq_above ~lhs ~rhs = phys_equal lhs rhs || match (lhs, rhs) with | Below lhs, Below rhs -> leq_below ~lhs ~rhs - | Below _, Above _ -> + | Below _, _ -> true - | Above _, Below _ -> + | _, Below _ -> false | Above lhs, Above rhs -> leq_above ~lhs ~rhs + | Above _, _ -> + false + | _, Above _ -> + true + | Val lhs, Val rhs -> + leq ~lhs ~rhs - let combine ~dir x1 x2 ~f_below ~f_above = + let combine ~dir x1 x2 ~f_below ~f ~f_above = match (x1, x2) with | Below b1, Below b2 -> Below (f_below b1 b2) - | (Below _ as below), (Above _ as above) | (Above _ as above), (Below _ as below) -> ( - match dir with `Increasing -> above | `Decreasing -> below ) + | Val v1, Val v2 -> + Val (f v1 v2) | Above a1, Above a2 -> Above (f_above a1 a2) + | (Below _ as below), x | x, (Below _ as below) -> ( + match dir with `Increasing -> x | `Decreasing -> below ) + | x, (Above _ as above) | (Above _ as above), x -> ( + match dir with `Increasing -> above | `Decreasing -> x ) - let map x ~f_below ~f_above = - match x with Below b -> Below (f_below b) | Above a -> Above (f_above a) + let map x ~f_below ~f ~f_above = + match x with Below b -> Below (f_below b) | Above a -> Above (f_above a) | Val v -> Val (f v) - let pp ~pp_below ~pp_above f = function Below b -> pp_below f b | Above a -> pp_above f a + let pp ~pp_below ~pp ~pp_above f = function + | Below b -> + pp_below f b + | Above a -> + pp_above f a + | Val v -> + pp f v end -module Stacked (Below : S) (Above : S) = struct - type t = (Below.t, Above.t) below_above +module Stacked (Below : S) (Val : S) (Above : S) = struct + type t = (Below.t, Val.t, Above.t) below_above + + let leq = StackedUtils.leq ~leq_below:Below.leq ~leq:Val.leq ~leq_above:Above.leq - let leq = StackedUtils.leq ~leq_below:Below.leq ~leq_above:Above.leq + let join = + StackedUtils.combine ~dir:`Increasing ~f_below:Below.join ~f:Val.join ~f_above:Above.join - let join = StackedUtils.combine ~dir:`Increasing ~f_below:Below.join ~f_above:Above.join let widen ~prev ~next ~num_iters = StackedUtils.combine ~dir:`Increasing prev next ~f_below:(fun prev next -> Below.widen ~prev ~next ~num_iters) + ~f:(fun prev next -> Val.widen ~prev ~next ~num_iters) ~f_above:(fun prev next -> Above.widen ~prev ~next ~num_iters) - let pp = StackedUtils.pp ~pp_below:Below.pp ~pp_above:Above.pp + let pp = StackedUtils.pp ~pp_below:Below.pp ~pp:Val.pp ~pp_above:Above.pp end module MinReprSet (Element : PrettyPrintable.PrintableOrderedType) = struct diff --git a/infer/src/absint/AbstractDomain.mli b/infer/src/absint/AbstractDomain.mli index 223d9123b..218770ec2 100644 --- a/infer/src/absint/AbstractDomain.mli +++ b/infer/src/absint/AbstractDomain.mli @@ -12,7 +12,7 @@ module Types : sig type 'astate top_lifted = Top | NonTop of 'astate - type ('below, 'above) below_above = Below of 'below | Above of 'above + type ('below, 'astate, 'above) below_above = Below of 'below | Above of 'above | Val of 'astate end open! Types @@ -73,6 +73,10 @@ module BottomLifted (Domain : S) : sig val map : f:(Domain.t -> Domain.t) -> t -> t end +module BottomLiftedUtils : sig + val pp_bottom : Format.formatter -> unit +end + (** Create a domain with Top element from a pre-domain *) module TopLifted (Domain : S) : WithTop with type t = Domain.t top_lifted @@ -97,43 +101,53 @@ end include sig [@@@warning "-60"] - (** Stacked abstract domain: tagged union of [Below] and [Above] domains where all elements of - [Below] are strictly smaller than elements of [Above] *) - module Stacked (Below : S) (Above : S) : S with type t = (Below.t, Above.t) below_above + (** Stacked abstract domain: tagged union of [Below], [Val], and [Above] domains where all + elements of [Below] are strictly smaller than all elements of [Val] which are strictly smaller + than all elements of [Above] *) + module Stacked (Below : S) (Val : S) (Above : S) : + S with type t = (Below.t, Val.t, Above.t) below_above end module StackedUtils : sig val leq : leq_below:(lhs:'b -> rhs:'b -> bool) + -> leq:(lhs:'v -> rhs:'v -> bool) -> leq_above:(lhs:'a -> rhs:'a -> bool) - -> lhs:('b, 'a) below_above - -> rhs:('b, 'a) below_above + -> lhs:('b, 'v, 'a) below_above + -> rhs:('b, 'v, 'a) below_above -> bool val compare : - ('b, 'a) below_above - -> ('b, 'a) below_above + ('b, 'v, 'a) below_above + -> ('b, 'v, 'a) below_above -> cmp_below:('b -> 'b -> int) + -> cmp:('v -> 'v -> int) -> cmp_above:('a -> 'a -> int) -> int val pp : pp_below:(Format.formatter -> 'b -> unit) + -> pp:(Format.formatter -> 'v -> unit) -> pp_above:(Format.formatter -> 'a -> unit) -> Format.formatter - -> ('b, 'a) below_above + -> ('b, 'v, 'a) below_above -> unit val combine : dir:[`Increasing | `Decreasing] - -> ('b, 'a) below_above - -> ('b, 'a) below_above + -> ('b, 'v, 'a) below_above + -> ('b, 'v, 'a) below_above -> f_below:('b -> 'b -> 'b) + -> f:('v -> 'v -> 'v) -> f_above:('a -> 'a -> 'a) - -> ('b, 'a) below_above + -> ('b, 'v, 'a) below_above val map : - ('b, 'a) below_above -> f_below:('b -> 'b2) -> f_above:('a -> 'a2) -> ('b2, 'a2) below_above + ('b, 'v, 'a) below_above + -> f_below:('b -> 'b2) + -> f:('v -> 'v2) + -> f_above:('a -> 'a2) + -> ('b2, 'v2, 'a2) below_above end (** Abstracts a set of [Element]s by keeping its smallest representative only. The widening is diff --git a/infer/src/backend/Differential.ml b/infer/src/backend/Differential.ml index 4579eff5a..99b13eb0f 100644 --- a/infer/src/backend/Differential.ml +++ b/infer/src/backend/Differential.ml @@ -68,11 +68,9 @@ module CostsSummary = struct let count_aux t (e : CostDomain.BasicCost.t) = match CostDomain.BasicCost.degree e with | None -> - assert (CostDomain.BasicCost.is_top e) ; - {t with top= t.top + 1} - | Some d when CostDomain.BasicCost.is_zero e -> - assert (Polynomials.Degree.is_zero d) ; - {t with zero= t.zero + 1} + if CostDomain.BasicCost.is_top e then {t with top= t.top + 1} + else if CostDomain.BasicCost.is_unreachable e then {t with zero= t.zero + 1} + else (* a cost with no degree must be either T/bottom*) assert false | Some d -> let degrees = DegreeMap.update (Polynomials.Degree.encode_to_int d) incr t.degrees in {t with degrees} @@ -164,7 +162,7 @@ module CostItem = struct let is_top = lift ~f_poly:CostDomain.BasicCost.is_top ~f_deg:Option.is_none (* NOTE: incorrect when using [f_deg] *) - let is_zero = lift ~f_poly:CostDomain.BasicCost.is_zero ~f_deg:(fun _ -> false) + let is_unreachable = lift ~f_poly:CostDomain.BasicCost.is_unreachable ~f_deg:(fun _ -> false) (* NOTE: incorrect when using [f_deg] *) let is_one = lift ~f_poly:CostDomain.BasicCost.is_one ~f_deg:(fun _ -> false) @@ -226,7 +224,7 @@ let issue_of_cost kind CostIssues.{complexity_increase_issue; zero_issue; infini let source_file = SourceFile.create ~warn_on_error:false file in let issue_type = if CostItem.is_top curr_item then infinite_issue - else if CostItem.is_zero curr_item then zero_issue + else if CostItem.is_unreachable curr_item then zero_issue else let is_on_cold_start = ExternalPerfData.in_profiler_data_map procname in complexity_increase_issue ~is_on_cold_start ~is_on_ui_thread @@ -281,9 +279,11 @@ let issue_of_cost kind CostIssues.{complexity_increase_issue; zero_issue; infini match curr_degree_with_term with | None -> [] - | Some (Below (_, degree_term)) -> + | Some (Val (_, degree_term)) -> Polynomials.NonNegativeNonTopPolynomial.get_symbols degree_term |> List.map ~f:Bounds.NonNegativeBound.make_err_trace + | Some (Below traces) -> + [("", Polynomials.UnreachableTraces.make_err_trace traces)] | Some (Above traces) -> [("", Polynomials.TopTraces.make_err_trace traces)] in diff --git a/infer/src/bufferoverrun/polynomials.ml b/infer/src/bufferoverrun/polynomials.ml index 4adb4ac23..486ad85be 100644 --- a/infer/src/bufferoverrun/polynomials.ml +++ b/infer/src/bufferoverrun/polynomials.ml @@ -47,8 +47,6 @@ module Degree = struct (NonNegativeInt.to_int_exn d.linear * 100) + NonNegativeInt.to_int_exn d.log - let is_zero d = NonNegativeInt.is_zero d.linear && NonNegativeInt.is_zero d.log - let pp f d = NonNegativeInt.pp f d.linear ; if not (NonNegativeInt.is_zero d.log) then @@ -272,20 +270,22 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct mult_const p1 p2.const |> M.fold (fun s p acc -> plus (mult_symb (mult p p1) s) acc) p2.terms - let rec of_valclass : (NonNegativeInt.t, S.t, 't) Bounds.valclass -> (t, 't) below_above = + let rec of_valclass : (NonNegativeInt.t, S.t, 't) Bounds.valclass -> ('t, t, 't) below_above = function | ValTop trace -> Above trace | Constant i -> - Below (of_non_negative_int i) + Val (of_non_negative_int i) | Symbolic s -> ( match S.split_mult s with | None -> - Below {const= NonNegativeInt.zero; terms= M.singleton s one} + Val {const= NonNegativeInt.zero; terms= M.singleton s one} | Some (s1, s2) -> ( match (of_valclass (S.classify s1), of_valclass (S.classify s2)) with - | Below s1, Below s2 -> - Below (mult s1 s2) + | Val s1, Val s2 -> + Val (mult s1 s2) + | Below _, _ | _, Below _ -> + assert false | (Above _ as t), _ | _, (Above _ as t) -> t ) ) @@ -373,7 +373,7 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct terms (of_non_negative_int const) in fun p eval_sym -> - match subst p eval_sym with p -> Below p | exception ReturnTop s_trace -> Above s_trace + match subst p eval_sym with p -> Val p | exception ReturnTop s_trace -> Above s_trace (** Emit a pair (d,t) where d is the degree of the polynomial and t is the first term with such @@ -509,24 +509,79 @@ module TopTraces = struct match min_elt traces with None -> [] | Some trace -> TopTrace.make_err_trace ~depth:0 trace end +module UnreachableTrace = struct + type t = + | UnreachableNode of Location.t + | Call of {location: Location.t; callee_pname: Procname.t; callee_trace: t} + [@@deriving compare] + + let rec length = function + | UnreachableNode _ -> + 1 + | Call {callee_trace} -> + 1 + length callee_trace + + + let compare t1 t2 = [%compare: int * t] (length t1, t1) (length t2, t2) + + let unreachable_node node_loc = UnreachableNode node_loc + + let call ~location ~callee_pname callee_trace = Call {location; callee_pname; callee_trace} + + let rec pp f = function + | UnreachableNode node_loc -> + F.fprintf f "UnreachableNode (%a)" Location.pp node_loc + | Call {callee_pname; callee_trace; location} -> + F.fprintf f "%a -> Call `%a` (%a)" pp callee_trace Procname.pp callee_pname Location.pp + location + + + let rec make_err_trace ~depth trace = + match trace with + | UnreachableNode node_loc -> + [Errlog.make_trace_element depth node_loc "Unreachable node" []] + | Call {location; callee_pname; callee_trace} -> + let desc = F.asprintf "Call to %a" Procname.pp callee_pname in + Errlog.make_trace_element depth location desc [] + :: make_err_trace ~depth:(depth + 1) callee_trace +end + +module UnreachableTraces = struct + include AbstractDomain.MinReprSet (UnreachableTrace) + + let make_err_trace traces = + match min_elt traces with + | None -> + [] + | Some trace -> + UnreachableTrace.make_err_trace ~depth:0 trace +end + module NonNegativePolynomial = struct - (* Use Below for non-Top values and Above for Top values with their trace *) - type t = (NonNegativeNonTopPolynomial.t, TopTraces.t) below_above + (* Use Above for Top values, Below for Unreachable values with their trace, and Val for non-negative polynomials *) + type t = (UnreachableTraces.t, NonNegativeNonTopPolynomial.t, TopTraces.t) below_above type degree_with_term = - (Degree.t * NonNegativeNonTopPolynomial.t, TopTraces.t) AbstractDomain.Types.below_above + ( UnreachableTraces.t + , Degree.t * NonNegativeNonTopPolynomial.t + , TopTraces.t ) + AbstractDomain.Types.below_above let leq = - AbstractDomain.StackedUtils.leq ~leq_below:NonNegativeNonTopPolynomial.leq - ~leq_above:TopTraces.leq + AbstractDomain.StackedUtils.leq ~leq_below:UnreachableTraces.leq + ~leq:NonNegativeNonTopPolynomial.leq ~leq_above:TopTraces.leq let pp ~hum = + let pp_below f traces = + AbstractDomain.BottomLiftedUtils.pp_bottom f ; + if not hum then F.fprintf f ": %a" UnreachableTraces.pp traces + in let pp_above f traces = AbstractDomain.TopLiftedUtils.pp_top f ; if not hum then F.fprintf f ": %a" TopTraces.pp traces in - AbstractDomain.StackedUtils.pp ~pp_below:(NonNegativeNonTopPolynomial.pp ~hum) ~pp_above + AbstractDomain.StackedUtils.pp ~pp:(NonNegativeNonTopPolynomial.pp ~hum) ~pp_above ~pp_below let pp_hum = pp ~hum:true @@ -535,48 +590,69 @@ module NonNegativePolynomial = struct let top = Above TopTraces.bottom - let zero = Below NonNegativeNonTopPolynomial.zero + let zero = Val NonNegativeNonTopPolynomial.zero + + let one = Val NonNegativeNonTopPolynomial.one - let one = Below NonNegativeNonTopPolynomial.one + let of_unreachable node_loc = + Below (UnreachableTraces.singleton (UnreachableTrace.unreachable_node node_loc)) - let of_int_exn i = Below (NonNegativeNonTopPolynomial.of_int_exn i) + + let of_int_exn i = Val (NonNegativeNonTopPolynomial.of_int_exn i) let make_trace_set ~map_above = - AbstractDomain.StackedUtils.map ~f_below:Fn.id ~f_above:(fun above -> - TopTraces.singleton (map_above above) ) + AbstractDomain.StackedUtils.map + ~f_below:(fun _ -> assert false) + ~f:Fn.id + ~f_above:(fun above -> TopTraces.singleton (map_above above)) let of_non_negative_bound ?(degree_kind = DegreeKind.Linear) b = b |> NonNegativeBoundWithDegreeKind.make degree_kind |> NonNegativeBoundWithDegreeKind.classify |> NonNegativeNonTopPolynomial.of_valclass + (* Invariant: we always get a non-below bound from [of_valclass] *) |> make_trace_set ~map_above:TopTrace.unbounded_loop let is_symbolic = function - | Above _ -> + | Below _ | Above _ -> false - | Below p -> + | Val p -> NonNegativeNonTopPolynomial.is_symbolic p let is_top = function Above _ -> true | _ -> false - let is_zero = function Below p when NonNegativeNonTopPolynomial.is_zero p -> true | _ -> false + let is_unreachable = function Below _ -> true | _ -> false - let is_one = function Below p when NonNegativeNonTopPolynomial.is_one p -> true | _ -> false + let is_zero = function Val p when NonNegativeNonTopPolynomial.is_zero p -> true | _ -> false + + let is_one = function Val p when NonNegativeNonTopPolynomial.is_one p -> true | _ -> false let top_lifted_increasing ~f p1 p2 = - AbstractDomain.StackedUtils.combine ~dir:`Increasing p1 p2 ~f_below:f ~f_above:TopTraces.join + AbstractDomain.StackedUtils.combine ~f_below:UnreachableTraces.join ~dir:`Increasing p1 p2 ~f + ~f_above:TopTraces.join + + + let unreachable_lifted_increasing ~f p1 p2 = + match (p1, p2) with + | (Below _ as below), Val _ | Val _, (Below _ as below) -> + below + | _ -> + top_lifted_increasing ~f p1 p2 let plus = top_lifted_increasing ~f:NonNegativeNonTopPolynomial.plus + let mult_unreachable = unreachable_lifted_increasing ~f:NonNegativeNonTopPolynomial.mult + let mult = top_lifted_increasing ~f:NonNegativeNonTopPolynomial.mult let min_default_left p1 p2 = AbstractDomain.StackedUtils.combine ~dir:`Decreasing p1 p2 - ~f_below:NonNegativeNonTopPolynomial.min_default_left ~f_above:TopTraces.join + ~f:NonNegativeNonTopPolynomial.min_default_left ~f_above:TopTraces.join + ~f_below:UnreachableTraces.join let subst callee_pname location p eval_sym = @@ -586,37 +662,47 @@ module NonNegativePolynomial = struct (TopTraces.map (fun callee_trace -> TopTrace.call ~callee_pname ~location callee_trace) callee_traces) - | Below p -> + | Below callee_traces -> + Below + (UnreachableTraces.map + (fun callee_trace -> UnreachableTrace.call ~callee_pname ~location callee_trace) + callee_traces) + | Val p -> NonNegativeNonTopPolynomial.subst callee_pname location p eval_sym |> make_trace_set ~map_above:(fun (symbol, bound_trace) -> TopTrace.unbounded_symbol ~location ~symbol bound_trace ) let degree p = - match p with Above _ -> None | Below p -> Some (NonNegativeNonTopPolynomial.degree p) + match p with Above _ | Below _ -> None | Val p -> Some (NonNegativeNonTopPolynomial.degree p) let compare_by_degree = - let cmp_above _ _ = 0 (* All Top should be considered equal *) in - AbstractDomain.StackedUtils.compare ~cmp_above ~cmp_below:(fun p1 p2 -> + let cmp _ _ = 0 (* All pairs of Top/Unreachable should be considered equal *) in + AbstractDomain.StackedUtils.compare ~cmp_above:cmp + ~cmp:(fun p1 p2 -> Degree.compare (NonNegativeNonTopPolynomial.degree p1) (NonNegativeNonTopPolynomial.degree p2) ) + ~cmp_below:cmp let get_degree_with_term = - AbstractDomain.StackedUtils.map ~f_below:NonNegativeNonTopPolynomial.degree_with_term - ~f_above:Fn.id + AbstractDomain.StackedUtils.map ~f:NonNegativeNonTopPolynomial.degree_with_term ~f_above:Fn.id + ~f_below:Fn.id let get_symbols = - AbstractDomain.StackedUtils.map ~f_below:NonNegativeNonTopPolynomial.get_symbols ~f_above:Fn.id + AbstractDomain.StackedUtils.map ~f:NonNegativeNonTopPolynomial.get_symbols ~f_above:Fn.id + ~f_below:Fn.id let pp_degree ~only_bigO fmt = function | Above _ -> Format.pp_print_string fmt "Top" - | Below (degree, degree_term) -> + | Below _ -> + Format.pp_print_string fmt "Unreachable" + | Val (degree, degree_term) -> if only_bigO then Format.fprintf fmt "O(%a)" (NonNegativeNonTopPolynomial.pp ~hum:true) @@ -634,7 +720,9 @@ module NonNegativePolynomial = struct let polynomial_traces p = match get_symbols p with - | Below symbols -> + | Below trace -> + UnreachableTraces.make_err_trace trace + | Val symbols -> List.map symbols ~f:Bounds.NonNegativeBound.make_err_trace |> Errlog.concat_traces | Above trace -> TopTraces.make_err_trace trace diff --git a/infer/src/bufferoverrun/polynomials.mli b/infer/src/bufferoverrun/polynomials.mli index c4d92a588..89372612c 100644 --- a/infer/src/bufferoverrun/polynomials.mli +++ b/infer/src/bufferoverrun/polynomials.mli @@ -17,8 +17,6 @@ module Degree : sig val encode_to_int : t -> int (** Encodes the complex type [t] to an integer that can be used for comparison. *) - - val is_zero : t -> bool end module NonNegativeNonTopPolynomial : sig @@ -33,11 +31,20 @@ module TopTraces : sig val make_err_trace : t -> Errlog.loc_trace end +module UnreachableTraces : sig + type t + + val make_err_trace : t -> Errlog.loc_trace +end + module NonNegativePolynomial : sig include PrettyPrintable.PrintableType type degree_with_term = - (Degree.t * NonNegativeNonTopPolynomial.t, TopTraces.t) AbstractDomain.Types.below_above + ( UnreachableTraces.t + , Degree.t * NonNegativeNonTopPolynomial.t + , TopTraces.t ) + AbstractDomain.Types.below_above val pp_hum : Format.formatter -> t -> unit @@ -45,6 +52,8 @@ module NonNegativePolynomial : sig val top : t + val of_unreachable : Location.t -> t + val zero : t val one : t @@ -55,6 +64,8 @@ module NonNegativePolynomial : sig val is_top : t -> bool + val is_unreachable : t -> bool + val is_zero : t -> bool val is_one : t -> bool @@ -63,6 +74,9 @@ module NonNegativePolynomial : sig val plus : t -> t -> t + val mult_unreachable : t -> t -> t + (** if one of the operands is unreachable, the result is unreachable *) + val mult : t -> t -> t val min_default_left : t -> t -> t diff --git a/infer/src/cost/boundMap.ml b/infer/src/cost/boundMap.ml index 4b2b4599c..c9e8a30ef 100644 --- a/infer/src/cost/boundMap.ml +++ b/infer/src/cost/boundMap.ml @@ -56,11 +56,12 @@ let compute_upperbound_map node_cfg inferbo_invariant_map control_invariant_map let bound = match entry_mem with | Unreachable -> + let node_loc = NodeCFG.Node.loc node in L.debug Analysis Medium "@\n\ [COST ANALYSIS INTERNAL WARNING:] No 'env' found. This location is \ unreachable returning cost 0 \n" ; - BasicCost.zero + BasicCost.of_unreachable node_loc | ExcRaised -> BasicCost.one | Reachable mem -> @@ -68,8 +69,11 @@ let compute_upperbound_map node_cfg inferbo_invariant_map control_invariant_map BufferOverrunDomain.MemReach.range ~filter_loc:(filter_loc control_map) ~node_id mem in - (* The zero cost of node does not make sense especially when the abstract memory - is non-bottom. *) + (* The zero number of executions for a node + (corresponding to getting the range of bottom + values) does not make sense especially when the + abstract memory is non-bottom. This is a source + of unsoundness in the analysis. *) if BasicCost.is_zero cost then BasicCost.one else cost in L.(debug Analysis Medium) diff --git a/infer/src/cost/cost.ml b/infer/src/cost/cost.ml index 341085ae1..9e25583d3 100644 --- a/infer/src/cost/cost.ml +++ b/infer/src/cost/cost.ml @@ -123,11 +123,15 @@ module InstrBasicCost = struct assert false in let cost = get_instr_cost_record tenv extras instr_node instr in - if BasicCost.is_top (CostDomain.get_operation_cost cost) then - Logging.d_printfln_escaped "Statement cost became top at %a (%a)." InstrCFG.Node.pp_id - (InstrCFG.Node.id instr_node) + let operation_cost = CostDomain.get_operation_cost cost in + let log_msg top_or_bottom = + Logging.d_printfln_escaped "Statement cost became %s at %a (%a)." top_or_bottom + InstrCFG.Node.pp_id (InstrCFG.Node.id instr_node) (Sil.pp_instr ~print_types:false Pp.text) - instr ; + instr + in + if BasicCost.is_top operation_cost then log_msg "top" + else if BasicCost.is_unreachable operation_cost then log_msg "unreachable" ; cost end @@ -173,7 +177,7 @@ module WorstCaseCost = struct if BasicCost.is_top nb_exec then Logging.d_printfln_escaped "Node %a is analyzed to visit infinite (top) times." Node.pp_id node_id ; - CostDomain.mult_by_scalar instr_cost_record nb_exec + CostDomain.mult_by instr_cost_record ~nb_exec in let costs = CostDomain.plus costs node_cost in let reports = @@ -258,7 +262,7 @@ module Check = struct ~extras:(compute_errlog_extras cost) summary issue message in if BasicCost.is_top cost then report infinite_issue "cannot be computed" - else if BasicCost.is_zero cost then report zero_issue "is zero" + else if BasicCost.is_unreachable cost then report zero_issue "is zero(unreachable)" let check_and_report ~is_on_ui_thread WorstCaseCost.{costs; reports} proc_desc summary = diff --git a/infer/src/cost/costDomain.ml b/infer/src/cost/costDomain.ml index 2a616830f..44f0f6849 100644 --- a/infer/src/cost/costDomain.ml +++ b/infer/src/cost/costDomain.ml @@ -15,7 +15,7 @@ module BasicCost = struct (* NOTE: Increment the version number if you changed the [t] type. This is for avoiding demarshalling failure of cost analysis results in running infer-reportdiff. *) - let version = 4 + let version = 5 end (** @@ -54,7 +54,8 @@ let map ~f cost_record = VariantCostMap.map f cost_record let zero_record = VariantCostMap.empty -let mult_by_scalar cost_record scalar = map cost_record ~f:(BasicCost.mult scalar) +(** If nb_exec is unreachable, we map to unreachable, not 0 *) +let mult_by cost_record ~nb_exec = map cost_record ~f:(BasicCost.mult_unreachable nb_exec) let plus cost_record1 cost_record2 = VariantCostMap.union diff --git a/infer/src/cost/costDomain.mli b/infer/src/cost/costDomain.mli index a96058c3d..1e39dd7b0 100644 --- a/infer/src/cost/costDomain.mli +++ b/infer/src/cost/costDomain.mli @@ -38,8 +38,8 @@ val map : f:(BasicCost.t -> BasicCost.t) -> t -> t val zero_record : t (** Map representing cost record {OperationCost:0; AllocationCost:0; IOCost:0} *) -val mult_by_scalar : t -> BasicCost.t -> t -(** Map where each element is multiplied by a cost *) +val mult_by : t -> nb_exec:BasicCost.t -> t +(** Special map where each element is multiplied by the number of executions *) val plus : t -> t -> t (** Union of two maps where common costs are added together *) diff --git a/infer/tests/codetoanalyze/c/performance/issues.exp b/infer/tests/codetoanalyze/c/performance/issues.exp index d0a9cae17..1e967bea9 100644 --- a/infer/tests/codetoanalyze/c/performance/issues.exp +++ b/infer/tests/codetoanalyze/c/performance/issues.exp @@ -48,9 +48,9 @@ codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 10, INTEGER_OVERF codetoanalyze/c/performance/cost_test_deps.c, simulated_while, 12, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 215, O(1), degree = 0] codetoanalyze/c/performance/cost_test_deps.c, two_loops, 5, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([3, +oo] + 1):signed32] codetoanalyze/c/performance/cost_test_deps.c, two_loops, 7, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 546, O(1), degree = 0] -codetoanalyze/c/performance/exit.c, call_exit_unreachable_zero, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, [] -codetoanalyze/c/performance/exit.c, compute_exit_unreachable_zero, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, [] -codetoanalyze/c/performance/exit.c, exit_unreachable_zero, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, [] +codetoanalyze/c/performance/exit.c, call_exit_unreachable_zero, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, [Unreachable node] +codetoanalyze/c/performance/exit.c, compute_exit_unreachable_zero, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, [Unreachable node] +codetoanalyze/c/performance/exit.c, exit_unreachable_zero, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, [Unreachable node] codetoanalyze/c/performance/exit.c, inline_exit_unreachable_FP, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 3 ⋅ p + 2 ⋅ (1+max(0, p)), O(p), degree = 1,{1+max(0, p)},Loop at line 30, column 3,{p},Loop at line 30, column 3] codetoanalyze/c/performance/exit.c, linear, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 3 ⋅ p + 2 ⋅ (1+max(0, p)), O(p), degree = 1,{1+max(0, p)},Loop at line 18, column 3,{p},Loop at line 18, column 3] codetoanalyze/c/performance/instantiate.c, do_2K_times_Bad, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 14006, O(1), degree = 0] diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 2fe87cbe6..1ca3c64c0 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -220,4 +220,4 @@ codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.read_sum_ codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.throw_exception():int, 0, UNREACHABLE_CODE, no_bucket, ERROR, [Here] codetoanalyze/java/performance/UnknownCallsTest.java, UnknownCallsTest.unmodeled_impure_linear(java.util.ArrayList):void, 0, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 13 ⋅ list.length + 3 ⋅ (list.length + 1), O(list.length), degree = 1,{list.length + 1},Loop at line 61,{list.length},Loop at line 61] codetoanalyze/java/performance/Zero.java, Zero.infeasible_path_zero():void, 0, UNREACHABLE_CODE, no_bucket, ERROR, [Here] -codetoanalyze/java/performance/Zero.java, Zero.infeasible_path_zero():void, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, [] +codetoanalyze/java/performance/Zero.java, Zero.infeasible_path_zero():void, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, [Unreachable node]