[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

@@ -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

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

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

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

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

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)

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 =

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

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 *)

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, [<LHS trace>,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]

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]