[debug] print full types in instructions on error

Summary:
Seems useful to know when we're printing one instruction only, but not when we
print lots of them for readability.

Reviewed By: mbouaziz

Differential Revision: D12823481

fbshipit-source-id: 2beb339f2

infer/src/IR/Cfg.ml

@@ -68,9 +68,13 @@ let store source_file cfg =
 let inline_synthetic_method ((ret_id, _) as ret) etl pdesc loc_call : Sil.instr option =
   let found instr instr' =
     L.(debug Analysis Verbose)
-      "XX inline_synthetic_method found instr: %a@." (Sil.pp_instr Pp.text) instr ;
+      "XX inline_synthetic_method found instr: %a@."
+      (Sil.pp_instr ~print_types:true Pp.text)
+      instr ;
     L.(debug Analysis Verbose)
-      "XX inline_synthetic_method instr': %a@." (Sil.pp_instr Pp.text) instr' ;
+      "XX inline_synthetic_method instr': %a@."
+      (Sil.pp_instr ~print_types:true Pp.text)
+      instr' ;
     Some instr'
   in
   let do_instr instr =

infer/src/IR/Exp.ml

@@ -252,9 +252,12 @@ and pp_captured_var pe pp_t f (exp, var, typ) =
       F.fprintf f "(%a %a:%a)" (pp_ pe pp_t) exp (Pvar.pp pe) var (Typ.pp pe) typ
 
 
-let pp_printenv pe pp_typ f e = pp_ pe (pp_typ pe) f e
+let pp_printenv ~print_types pe f e =
+  let pp_typ = if print_types then Typ.pp_full else Typ.pp in
+  pp_ pe (pp_typ pe) f e
 
-let pp f e = pp_printenv Pp.text Typ.pp f e
+
+let pp f e = pp_printenv ~print_types:false Pp.text f e
 
 let to_string e = F.asprintf "%a" pp e
 

infer/src/IR/Exp.mli

@@ -127,7 +127,7 @@ val program_vars : t -> Pvar.t Sequence.t
 val fold_captured : f:('a -> t -> 'a) -> t -> 'a -> 'a
 (** Fold over the expressions captured by this expression. *)
 
-val pp_printenv : Pp.env -> (Pp.env -> F.formatter -> Typ.t -> unit) -> F.formatter -> t -> unit
+val pp_printenv : print_types:bool -> Pp.env -> F.formatter -> t -> unit
 
 val pp : F.formatter -> t -> unit
 

infer/src/IR/Instrs.ml

@@ -145,4 +145,5 @@ let last (type r) (t : r t) =
 
 let find_map t ~f = Container.find_map ~iter t ~f
 
-let pp pe fmt t = iter t ~f:(fun instr -> F.fprintf fmt "%a;@\n" (Sil.pp_instr pe) instr)
+let pp pe fmt t =
+  iter t ~f:(fun instr -> F.fprintf fmt "%a;@\n" (Sil.pp_instr ~print_types:false pe) instr)

infer/src/IR/Sil.ml

@@ -257,7 +257,7 @@ let pp_seq_diff pp pe0 f =
 
 
 (** Pretty print an expression. *)
-let pp_exp_printenv pe0 f e0 =
+let pp_exp_printenv ?(print_types = false) pe0 f e0 =
   let pe, changed = color_pre_wrapper pe0 f e0 in
   let e =
     match pe.Pp.obj_sub with
@@ -268,7 +268,7 @@ let pp_exp_printenv pe0 f e0 =
   in
   if not (Exp.equal e0 e) then
     match e with Exp.Lvar pvar -> Pvar.pp_value f pvar | _ -> assert false
-  else Exp.pp_printenv pe Typ.pp f e ;
+  else Exp.pp_printenv ~print_types pe f e ;
   color_post_wrapper changed f
 
 
@@ -299,7 +299,7 @@ let pp_texp_full pe f = function
       F.fprintf f "%a%a%a%a" (Typ.pp_full pe) typ pp_size nbytes pp_len dynamic_length Subtype.pp
         subtype
   | e ->
-      Exp.pp_printenv pe Typ.pp_full f e
+      Exp.pp_printenv ~print_types:true pe f e
 
 
 (** Dump a type expression with all the details. *)
@@ -380,19 +380,22 @@ let if_kind_to_string = function
 
 
 (** Pretty print an instruction. *)
-let pp_instr pe0 f instr =
+let pp_instr ~print_types pe0 f instr =
+  let pp_typ = if print_types then Typ.pp_full else Typ.pp in
   let pe, changed = color_pre_wrapper pe0 f instr in
   ( match instr with
   | Load (id, e, t, loc) ->
-      F.fprintf f "%a=*%a:%a [%a]" Ident.pp id (pp_exp_printenv pe) e (Typ.pp pe) t Location.pp loc
+      F.fprintf f "%a=*%a:%a [%a]" Ident.pp id (pp_exp_printenv ~print_types pe) e (pp_typ pe0) t
-  | Store (e1, t, e2, loc) ->
-      F.fprintf f "*%a:%a=%a [%a]" (pp_exp_printenv pe) e1 (Typ.pp pe) t (pp_exp_printenv pe) e2
         Location.pp loc
+  | Store (e1, t, e2, loc) ->
+      F.fprintf f "*%a:%a=%a [%a]" (pp_exp_printenv ~print_types pe) e1 (pp_typ pe0) t
+        (pp_exp_printenv ~print_types pe) e2 Location.pp loc
   | Prune (cond, loc, true_branch, _) ->
-      F.fprintf f "PRUNE(%a, %b); [%a]" (pp_exp_printenv pe) cond true_branch Location.pp loc
+      F.fprintf f "PRUNE(%a, %b); [%a]" (pp_exp_printenv ~print_types pe) cond true_branch
+        Location.pp loc
   | Call ((id, _), e, arg_ts, loc, cf) ->
       F.fprintf f "%a=" Ident.pp id ;
-      F.fprintf f "%a(%a)%a [%a]" (pp_exp_printenv pe) e
+      F.fprintf f "%a(%a)%a [%a]" (pp_exp_printenv ~print_types pe) e
         (Pp.comma_seq (pp_exp_typ pe))
         arg_ts CallFlags.pp cf Location.pp loc
   | Nullify (pvar, loc) ->
@@ -423,7 +426,7 @@ let add_with_block_parameters_flag instr =
 let is_block_pvar pvar = Typ.has_block_prefix (Mangled.to_string (Pvar.get_name pvar))
 
 (** Dump an instruction. *)
-let d_instr (i : instr) = L.add_print_with_pe ~color:Pp.Green pp_instr i
+let d_instr (i : instr) = L.add_print_with_pe ~color:Pp.Green (pp_instr ~print_types:true) i
 
 let pp_atom pe0 f a =
   let pe, changed = color_pre_wrapper pe0 f a in

infer/src/IR/Sil.mli

@@ -255,7 +255,7 @@ val color_pre_wrapper : Pp.env -> F.formatter -> 'a -> Pp.env * bool
 val color_post_wrapper : bool -> F.formatter -> unit
 (** Close color annotation if changed *)
 
-val pp_exp_printenv : Pp.env -> F.formatter -> Exp.t -> unit
+val pp_exp_printenv : ?print_types:bool -> Pp.env -> F.formatter -> Exp.t -> unit
 (** Pretty print an expression. *)
 
 val d_exp : Exp.t -> unit
@@ -288,7 +288,7 @@ val instr_get_exps : instr -> Exp.t list
 val if_kind_to_string : if_kind -> string
 (** Pretty print an if_kind *)
 
-val pp_instr : Pp.env -> F.formatter -> instr -> unit
+val pp_instr : print_types:bool -> Pp.env -> F.formatter -> instr -> unit
 (** Pretty print an instruction. *)
 
 val d_instr : instr -> unit

infer/src/absint/AbstractInterpreter.ml

@@ -151,7 +151,9 @@ module AbstractInterpreterCommon (TransferFunctions : TransferFunctions.SIL) = s
           | exn ->
               IExn.reraise_after exn ~f:(fun () ->
                   if not !logged_error then (
-                    L.internal_error "In instruction %a@\n" (Sil.pp_instr Pp.text) instr ;
+                    L.internal_error "In instruction %a@\n"
+                      (Sil.pp_instr ~print_types:true Pp.text)
+                      instr ;
                     logged_error := true ) )
         in
         Instrs.fold ~f:compute_post ~init:pre instrs

infer/src/backend/dotty.ml

@@ -1112,7 +1112,7 @@ let pp_cfgnodelabel pdesc fmt (n : Procdesc.Node.t) =
         Format.fprintf fmt "Skip %s" s
   in
   let instr_string i =
-    let pp f = Sil.pp_instr Pp.text f i in
+    let pp f = Sil.pp_instr ~print_types:false Pp.text f i in
     let str = F.asprintf "%t" pp in
     Escape.escape_dotty str
   in

infer/src/biabduction/SymExecBlocks.ml

@@ -84,7 +84,9 @@ let resolve_method_with_block_args_and_analyze ~caller_pdesc pname act_params =
       in
       Logging.(debug Analysis Verbose) "Instructions of specialized method:@." ;
       Procdesc.iter_instrs
-        (fun _ instr -> Logging.(debug Analysis Verbose) "%a@." (Sil.pp_instr Pp.text) instr)
+        (fun _ instr ->
+          Logging.(debug Analysis Verbose) "%a@." (Sil.pp_instr ~print_types:false Pp.text) instr
+          )
         specialized_pdesc ;
       Logging.(debug Analysis Verbose) "End of instructions@." ;
       match Ondemand.analyze_proc_desc ~caller_pdesc specialized_pdesc with

infer/src/bufferoverrun/bufferOverrunChecker.ml

@@ -143,7 +143,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
    fun instr pre post ->
     L.(debug BufferOverrun Verbose) "@\n@\n================================@\n" ;
     L.(debug BufferOverrun Verbose) "@[<v 2>Pre-state : @,%a" Dom.Mem.pp pre ;
-    L.(debug BufferOverrun Verbose) "@]@\n@\n%a" (Sil.pp_instr Pp.text) instr ;
+    L.(debug BufferOverrun Verbose) "@]@\n@\n%a" (Sil.pp_instr ~print_types:true Pp.text) instr ;
     L.(debug BufferOverrun Verbose) "@\n@\n" ;
     L.(debug BufferOverrun Verbose) "@[<v 2>Post-state : @,%a" Dom.Mem.pp post ;
     L.(debug BufferOverrun Verbose) "@]@\n" ;
@@ -661,7 +661,7 @@ module Report = struct
    fun instr pre cond_set ->
     L.(debug BufferOverrun Verbose) "@\n@\n================================@\n" ;
     L.(debug BufferOverrun Verbose) "@[<v 2>Pre-state : @,%a" Dom.Mem.pp pre ;
-    L.(debug BufferOverrun Verbose) "@]@\n@\n%a" (Sil.pp_instr Pp.text) instr ;
+    L.(debug BufferOverrun Verbose) "@]@\n@\n%a" (Sil.pp_instr ~print_types:true Pp.text) instr ;
     L.(debug BufferOverrun Verbose) "@[<v 2>@\n@\n%a" PO.ConditionSet.pp cond_set ;
     L.(debug BufferOverrun Verbose) "@]@\n" ;
     L.(debug BufferOverrun Verbose) "================================@\n@."

infer/src/checkers/cost.ml

@@ -89,8 +89,9 @@ module TransferFunctionsNodesBasicCost = struct
           astate
     in
     L.(debug Analysis Medium)
-      "@\n>>>Instr: %a   Cost: %a@\n" (Sil.pp_instr Pp.text) instr
+      "@\n>>>Instr: %a   Cost: %a@\n"
-      CostDomain.NodeInstructionToCostMap.pp astate' ;
+      (Sil.pp_instr ~print_types:false Pp.text)
+      instr CostDomain.NodeInstructionToCostMap.pp astate' ;
     astate'
 
 
@@ -690,8 +691,9 @@ module TransferFunctionsWCET = struct
           assert false
     in
     L.(debug Analysis Medium)
-      "@\n[>>>AnalyzerWCET] Instr: %a   Cost: %a@\n" (Sil.pp_instr Pp.text) instr BasicCost.pp
+      "@\n[>>>AnalyzerWCET] Instr: %a   Cost: %a@\n"
-      cost_node ;
+      (Sil.pp_instr ~print_types:false Pp.text)
+      instr BasicCost.pp cost_node ;
     let astate' =
       let und_node = CFG.Node.underlying_node node in
       let preds = Procdesc.Node.get_preds und_node in

infer/src/unit/analyzerTester.ml

@@ -28,7 +28,7 @@ module StructuredSil = struct
 
   let rec pp_structured_instr fmt = function
     | Cmd instr ->
-        Sil.pp_instr Pp.text fmt instr
+        Sil.pp_instr ~print_types:false Pp.text fmt instr
     | If (exp, then_instrs, else_instrs) ->
         (* TODO (t10287763): indent bodies of if/while *)
         F.fprintf fmt "if (%a) {@.%a@.} else {@.%a@.}" Exp.pp exp pp_structured_instr_list