[Cost] Do not print Top trace in trace step

Reviewed By: ezgicicek

Differential Revision: D14341689

fbshipit-source-id: 9d65cd41b

infer/src/backend/Differential.ml

@@ -146,7 +146,7 @@ let issue_of_cost cost_info ~delta ~prev_cost ~curr_cost =
   in
   let curr_degree_with_term = CostDomain.BasicCost.get_degree_with_term curr_cost in
   let curr_cost_msg fmt () =
-    Format.fprintf fmt "Cost is %a (degree is %a)" CostDomain.BasicCost.pp curr_cost
+    Format.fprintf fmt "Cost is %a (degree is %a)" CostDomain.BasicCost.pp_hum curr_cost
       (CostDomain.BasicCost.pp_degree ~only_bigO:false)
       curr_degree_with_term
   in

infer/src/backend/InferPrint.ml

@@ -347,7 +347,7 @@ module JsonCostsPrinter = MakeJsonListPrinter (struct
         let degree_with_term = CostDomain.BasicCost.get_degree_with_term basic_operation_cost in
         let hum =
           { Jsonbug_t.hum_polynomial=
-              Format.asprintf "%a" CostDomain.BasicCost.pp basic_operation_cost
+              Format.asprintf "%a" CostDomain.BasicCost.pp_hum basic_operation_cost
           ; hum_degree=
               Format.asprintf "%a"
                 (CostDomain.BasicCost.pp_degree ~only_bigO:false)

infer/src/bufferoverrun/bounds.ml

@@ -1063,7 +1063,10 @@ module NonNegativeBound = struct
     (b, BoundTrace.make_err_trace t)
 
 
-  let pp fmt (bound, _) = Bound.pp fmt bound
+  let pp ~hum fmt (bound, t) =
+    Bound.pp fmt bound ;
+    if not hum then F.fprintf fmt ": %a" BoundTrace.pp t
+
 
   let zero loop_head_loc = (Bound.zero, BoundTrace.Loop loop_head_loc)
 

infer/src/bufferoverrun/bounds.mli

@@ -131,7 +131,7 @@ module NonNegativeBound : sig
 
   val of_modeled_function : string -> Location.t -> Bound.t -> t
 
-  val pp : Format.formatter -> t -> unit
+  val pp : hum:bool -> Format.formatter -> t -> unit
 
   val make_err_trace : t -> string * Errlog.loc_trace
 

infer/src/bufferoverrun/polynomials.ml

@@ -70,7 +70,7 @@ module type NonNegativeSymbol = sig
     -> Bound.eval_sym
     -> (NonNegativeInt.t, t, TopTrace.t) Bounds.valclass
 
-  val pp : F.formatter -> t -> unit
+  val pp : hum:bool -> F.formatter -> t -> unit
 end
 
 module type NonNegativeSymbolWithDegreeKind = sig
@@ -119,7 +119,7 @@ module MakeSymbolWithDegreeKind (S : NonNegativeSymbol) :
         Bounds.ValTop trace
 
 
-  let pp f {degree_kind; symbol} = DegreeKind.pp_hole S.pp f degree_kind symbol
+  let pp ~hum f {degree_kind; symbol} = DegreeKind.pp_hole (S.pp ~hum) f degree_kind symbol
 
   let degree_kind {degree_kind} = degree_kind
 
@@ -355,7 +355,7 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
 
   let multiplication_sep = F.sprintf " %s " SpecialChars.multiplication_sign
 
-  let pp : F.formatter -> t -> unit =
+  let pp : hum:bool -> F.formatter -> t -> unit =
     let add_symb s (((last_s, last_occ) as last), others) =
       if Int.equal 0 (S.compare s last_s) then ((last_s, PositiveInt.succ last_occ), others)
       else ((s, PositiveInt.one), last :: others)
@@ -371,33 +371,33 @@ module MakePolynomial (S : NonNegativeSymbolWithDegreeKind) = struct
       let s = F.asprintf "%a" pp x in
       if String.contains s ' ' then F.fprintf fmt "(%s)" s else F.pp_print_string fmt s
     in
-    let pp_symb fmt symb = pp_magic_parentheses S.pp fmt symb in
-    let pp_symb_exp fmt (symb, exp) = F.fprintf fmt "%a%a" pp_symb symb pp_exp exp in
-    let pp_symbs fmt (last, others) =
-      List.rev_append others [last] |> Pp.seq ~sep:multiplication_sep pp_symb_exp fmt
+    let pp_symb ~hum fmt symb = pp_magic_parentheses (S.pp ~hum) fmt symb in
+    let pp_symb_exp ~hum fmt (symb, exp) = F.fprintf fmt "%a%a" (pp_symb ~hum) symb pp_exp exp in
+    let pp_symbs ~hum fmt (last, others) =
+      List.rev_append others [last] |> Pp.seq ~sep:multiplication_sep (pp_symb_exp ~hum) fmt
     in
-    let rec pp_sub ~print_plus symbs fmt {const; terms} =
+    let rec pp_sub ~hum ~print_plus symbs fmt {const; terms} =
       let print_plus =
         if not (NonNegativeInt.is_zero const) then (
           if print_plus then F.pp_print_string fmt " + " ;
-          F.fprintf fmt "%a%a" pp_coeff const pp_symbs symbs ;
+          F.fprintf fmt "%a%a" pp_coeff const (pp_symbs ~hum) symbs ;
           true )
         else print_plus
       in
       ( M.fold
           (fun s p print_plus ->
-            pp_sub ~print_plus (add_symb s symbs) fmt p ;
+            pp_sub ~hum ~print_plus (add_symb s symbs) fmt p ;
             true )
           terms print_plus
         : bool )
       |> ignore
     in
-    fun fmt {const; terms} ->
+    fun ~hum fmt {const; terms} ->
       let const_not_zero = not (NonNegativeInt.is_zero const) in
       if const_not_zero || M.is_empty terms then NonNegativeInt.pp fmt const ;
       ( M.fold
           (fun s p print_plus ->
-            pp_sub ~print_plus ((s, PositiveInt.one), []) fmt p ;
+            pp_sub ~hum ~print_plus ((s, PositiveInt.one), []) fmt p ;
             true )
           terms const_not_zero
         : bool )
@@ -433,13 +433,18 @@ module NonNegativePolynomial = struct
       ~le_above:TopTraces.( <= )
 
 
-  let pp =
+  let pp ~hum =
     let pp_above f traces =
-      F.fprintf f "%t: %a" AbstractDomain.TopLiftedUtils.pp_top TopTraces.pp 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 ~pp_above
+    AbstractDomain.StackedUtils.pp ~pp_below:(NonNegativeNonTopPolynomial.pp ~hum) ~pp_above
 
 
+  let pp_hum = pp ~hum:true
+
+  let pp = pp ~hum:false
+
   let top = Above TopTraces.bottom
 
   let zero = Below NonNegativeNonTopPolynomial.zero
@@ -518,7 +523,8 @@ module NonNegativePolynomial = struct
     | Above _ ->
         Format.pp_print_string fmt "Top"
     | Below (degree, degree_term) ->
-        if only_bigO then Format.fprintf fmt "O(%a)" NonNegativeNonTopPolynomial.pp degree_term
+        if only_bigO then
+          Format.fprintf fmt "O(%a)" (NonNegativeNonTopPolynomial.pp ~hum:true) degree_term
         else Degree.pp fmt degree
 
 

infer/src/bufferoverrun/polynomials.mli

@@ -41,6 +41,8 @@ module NonNegativePolynomial : sig
   type degree_with_term =
     (Degree.t * NonNegativeNonTopPolynomial.t, TopTraces.t) AbstractDomain.Types.below_above
 
+  val pp_hum : Format.formatter -> t -> unit
+
   val ( <= ) : lhs:t -> rhs:t -> bool
 
   val top : t

infer/src/checkers/cost.ml

@@ -616,7 +616,7 @@ module InstrBasicCost = struct
 end
 
 let compute_errlog_extras cost =
-  { Jsonbug_t.cost_polynomial= Some (Format.asprintf "%a" BasicCost.pp cost)
+  { Jsonbug_t.cost_polynomial= Some (Format.asprintf "%a" BasicCost.pp_hum cost)
   ; cost_degree= BasicCost.degree cost |> Option.map ~f:Polynomials.Degree.encode_to_int }
 
 
@@ -719,10 +719,10 @@ module Check = struct
       F.asprintf
         "%s from the beginning of the function up to this program point is likely above the \
          acceptable threshold of %d (estimated cost %a%s)"
-        name threshold BasicCost.pp cost degree_str
+        name threshold BasicCost.pp_hum cost degree_str
     in
     let cost_trace =
-      let cost_desc = F.asprintf "with estimated cost %a%s" BasicCost.pp cost degree_str in
+      let cost_desc = F.asprintf "with estimated cost %a%s" BasicCost.pp_hum cost degree_str in
       Errlog.make_trace_element 0 location cost_desc []
     in
     Reporting.log_error summary ~loc:location