[cost] Print debug information when top value is generated

Summary: It prints debug information when top values is generated.

Reviewed By: ngorogiannis

Differential Revision: D17285448

fbshipit-source-id: 0621fd36d

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -618,8 +618,11 @@ module MemPure = struct
   let bot = empty
 
   let range :
-      filter_loc:(Loc.t -> LoopHeadLoc.t option) -> t -> Polynomials.NonNegativePolynomial.t =
+         filter_loc:(Loc.t -> LoopHeadLoc.t option)
-   fun ~filter_loc mem ->
+      -> node_id:ProcCfg.Normal.Node.id
+      -> t
+      -> Polynomials.NonNegativePolynomial.t =
+   fun ~filter_loc ~node_id mem ->
     fold
       (fun loc (_, v) acc ->
         match filter_loc loc with
@@ -627,8 +630,19 @@ module MemPure = struct
             let itv = Val.get_itv v in
             if Itv.has_only_non_int_symbols itv then acc
             else
-              Itv.range loop_head_loc itv |> Itv.ItvRange.to_top_lifted_polynomial
+              let range1 = Itv.range loop_head_loc itv |> Itv.ItvRange.to_top_lifted_polynomial in
-              |> Polynomials.NonNegativePolynomial.mult acc
+              if Polynomials.NonNegativePolynomial.is_top range1 then
+                L.d_printfln_escaped "Range of %a (loc:%a) became top at %a." Itv.pp itv Loc.pp loc
+                  ProcCfg.Normal.Node.pp_id node_id ;
+              let range = Polynomials.NonNegativePolynomial.mult acc range1 in
+              if
+                (not (Polynomials.NonNegativePolynomial.is_top acc))
+                && Polynomials.NonNegativePolynomial.is_top range
+              then
+                L.d_printfln_escaped "Multiplication of %a and %a (loc:%a) became top at %a."
+                  Polynomials.NonNegativePolynomial.pp acc Polynomials.NonNegativePolynomial.pp
+                  range1 Loc.pp loc ProcCfg.Normal.Node.pp_id node_id ;
+              range
         | None ->
             acc )
       mem Polynomials.NonNegativePolynomial.one
@@ -1609,8 +1623,11 @@ module MemReach = struct
 
 
   let range :
-      filter_loc:(Loc.t -> LoopHeadLoc.t option) -> t -> Polynomials.NonNegativePolynomial.t =
+         filter_loc:(Loc.t -> LoopHeadLoc.t option)
-   fun ~filter_loc {mem_pure} -> MemPure.range ~filter_loc mem_pure
+      -> node_id:ProcCfg.Normal.Node.id
+      -> t
+      -> Polynomials.NonNegativePolynomial.t =
+   fun ~filter_loc ~node_id {mem_pure} -> MemPure.range ~filter_loc ~node_id mem_pure
 
 
   let get_relation : t -> Relation.t = fun m -> m.relation

infer/src/bufferoverrun/polynomials.ml

@@ -121,6 +121,7 @@ module MakeSymbolWithDegreeKind (S : NonNegativeSymbol) :
     | Symbolic symbol ->
         Bounds.Symbolic {degree_kind; symbol}
     | ValTop trace ->
+        Logging.d_printfln_escaped "subst(%a) became top." (S.pp ~hum:false) symbol ;
         Bounds.ValTop trace
 
 

infer/src/checkers/cost.ml

@@ -82,7 +82,8 @@ module BoundMap = struct
                        unreachable returning cost 0 \n" ;
                     BasicCost.zero
                 | NonBottom mem ->
-                    BufferOverrunDomain.MemReach.range ~filter_loc:(filter_loc control_map) mem
+                    BufferOverrunDomain.MemReach.range ~filter_loc:(filter_loc control_map)
+                      ~node_id mem
               in
               L.(debug Analysis Medium)
                 "@\n>>>Setting bound for node = %a  to %a@\n\n" Node.pp_id node_id BasicCost.pp
@@ -604,7 +605,13 @@ module InstrBasicCost = struct
       | More ->
           assert false
     in
-    get_instr_cost_record tenv extras instr_node instr
+    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)
+        (Sil.pp_instr ~print_types:false Pp.text)
+        instr ;
+    cost
 end
 
 let compute_errlog_extras cost =
@@ -653,6 +660,9 @@ module WorstCaseCost = struct
       let instr_cost_record = InstrBasicCost.get_instr_node_cost_record tenv extras instr_node in
       let node_id = InstrCFG.Node.underlying_node instr_node |> Node.id in
       let nb_exec = get_node_nb_exec node_id in
+      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
     in
     let costs = CostDomain.plus costs node_cost in