[Summary] Pp simplifications

Reviewed By: jeremydubreil

Differential Revision: D7974404

fbshipit-source-id: 15006cf

infer/src/backend/Summary.ml

@@ -119,21 +119,16 @@ let pp_errlog fmt err_log =
   F.fprintf fmt "WARNINGS: @[<h>%a@]" Errlog.pp_warnings err_log
 
 
-(** Return the signature of a procedure declaration as a string *)
-let get_signature summary =
-  let s = ref "" in
-  List.iter
-    ~f:(fun (p, typ) ->
-      let pp f = F.fprintf f "%a %a" (Typ.pp_full Pp.text) typ Mangled.pp p in
-      let decl = F.asprintf "%t" pp in
-      s := if String.equal !s "" then decl else !s ^ ", " ^ decl )
-    (get_formals summary) ;
-  F.asprintf "%a %a(%s)" (Typ.pp_full Pp.text) (get_ret_type summary) Typ.Procname.pp
-    (get_proc_name summary) !s
+let pp_signature fmt summary =
+  let pp_formal fmt (p, typ) = F.fprintf fmt "%a %a" (Typ.pp_full Pp.text) typ Mangled.pp p in
+  F.fprintf fmt "%a %a(%a)" (Typ.pp_full Pp.text) (get_ret_type summary) Typ.Procname.pp
+    (get_proc_name summary) (Pp.seq ~sep:", " pp_formal) (get_formals summary)
 
 
+let get_signature summary = F.asprintf "%a" pp_signature summary
+
 let pp_no_stats_specs fmt summary =
-  F.fprintf fmt "%s@\n" (get_signature summary) ;
+  F.fprintf fmt "%a@\n" pp_signature summary ;
   F.fprintf fmt "%a@\n" Status.pp summary.status
 
 
@@ -180,14 +175,12 @@ let pp_payload pe fmt
 
 
 let pp_text fmt summary =
-  let pe = Pp.text in
   pp_no_stats_specs fmt summary ;
-  F.fprintf fmt "%a@\n%a%a" pp_errlog (get_err_log summary) Stats.pp summary.stats (pp_payload pe)
-    summary.payload
+  F.fprintf fmt "%a@\n%a%a" pp_errlog (get_err_log summary) Stats.pp summary.stats
+    (pp_payload Pp.text) summary.payload
 
 
 let pp_html source color fmt summary =
-  let pe = Pp.html color in
   Io_infer.Html.pp_start_color fmt Black ;
   F.fprintf fmt "@\n%a" pp_no_stats_specs summary ;
   Io_infer.Html.pp_end_color fmt () ;
@@ -195,7 +188,7 @@ let pp_html source color fmt summary =
   Errlog.pp_html source [] fmt (get_err_log summary) ;
   Io_infer.Html.pp_hline fmt () ;
   F.fprintf fmt "<LISTING>@\n" ;
-  pp_payload pe fmt summary.payload ;
+  pp_payload (Pp.html color) fmt summary.payload ;
   F.fprintf fmt "</LISTING>@\n"
 
 

infer/src/backend/printer.ml

@@ -208,7 +208,7 @@ let force_delayed_print fmt =
         let (shallow: bool), (jpl: Prop.normal BiabductionSummary.Jprop.t list) =
           Obj.obj shallow_jpl
         in
-        BiabductionSummary.Jprop.pp_list pe_default shallow fmt jpl
+        BiabductionSummary.Jprop.pp_list pe_default ~shallow fmt jpl
     | L.PTjprop_short, jp ->
         let jp : Prop.normal BiabductionSummary.Jprop.t = Obj.obj jp in
         BiabductionSummary.Jprop.pp_short pe_default fmt jp

infer/src/biabduction/BiabductionSummary.ml

@@ -68,7 +68,7 @@ module Jprop = struct
   let get_id = function Prop (n, _) -> n | Joined (n, _, _, _) -> n
 
   (** Print a list of joined props, the boolean indicates whether to print subcomponents of joined props *)
-  let pp_list pe shallow f jplist =
+  let pp_list pe ~shallow f jplist =
     let rec pp_seq_newline f = function
       | [] ->
           ()
@@ -86,7 +86,7 @@ module Jprop = struct
 
 
   (** dump a joined prop list, the boolean indicates whether to print toplevel props only *)
-  let d_list (shallow: bool) (jplist: Prop.normal t list) =
+  let d_list ~(shallow: bool) (jplist: Prop.normal t list) =
     L.add_print_action (L.PTjprop_list, Obj.repr (shallow, jplist))
 
 
@@ -143,28 +143,18 @@ end
 
 (***** End of module Jprop *****)
 
-module Visitedset = Caml.Set.Make (struct
-  type t = Procdesc.Node.id * int list
-
-  let compare (node_id1, _) (node_id2, _) = Procdesc.Node.compare_id node_id1 node_id2
-end)
-
-let visited_str vis =
-  let s = ref "" in
-  let lines = ref Int.Set.empty in
-  let do_one (_, ns) =
-    (* if List.length ns > 1 then
-       begin
-       let ss = ref "" in
-       List.iter ~f:(fun n -> ss := !ss ^ " " ^ string_of_int n) ns;
-       L.out "Node %d has lines %s@." node !ss
-       end; *)
-    List.iter ~f:(fun n -> lines := Int.Set.add !lines n) ns
-  in
-  Visitedset.iter do_one vis ;
-  Int.Set.iter ~f:(fun n -> s := !s ^ " " ^ string_of_int n) !lines ;
-  !s
+module Visitedset = struct
+  include Caml.Set.Make (struct
+    type t = Procdesc.Node.id * int list
+
+    let compare (node_id1, _) (node_id2, _) = Procdesc.Node.compare_id node_id1 node_id2
+  end)
 
+  let pp fmt visitedset =
+    let collect_lines (_, ns) acc = List.fold ns ~f:Int.Set.add ~init:acc in
+    let lines = fold collect_lines visitedset Int.Set.empty in
+    Pp.seq F.pp_print_int fmt (Int.Set.elements lines)
+end
 
 (** A spec consists of:
     pre: a joined prop
@@ -245,28 +235,29 @@ let equal_phase = [%compare.equal : phase]
 
 (** Print the spec *)
 let pp_spec pe num_opt fmt spec =
-  let num_str =
-    match num_opt with
+  let pp_num_opt fmt = function
     | None ->
-        "----------"
+        F.pp_print_string fmt "----------"
     | Some (n, tot) ->
-        Format.sprintf "%d of %d [nvisited:%s]" n tot (visited_str spec.visited)
+        F.fprintf fmt "%d of %d [nvisited:%a]" n tot Visitedset.pp spec.visited
   in
   let pre = Jprop.to_prop spec.pre in
   let pe_post = Prop.prop_update_obj_sub pe pre in
   let post_list = List.map ~f:fst spec.posts in
   match pe.Pp.kind with
   | TEXT ->
-      F.fprintf fmt "--------------------------- %s ---------------------------@\n" num_str ;
+      F.fprintf fmt "--------------------------- %a ---------------------------@\n" pp_num_opt
+        num_opt ;
       F.fprintf fmt "PRE:@\n%a@\n" (Prop.pp_prop Pp.text) pre ;
       F.fprintf fmt "%a@\n" (Propgraph.pp_proplist pe_post "POST" (pre, true)) post_list ;
       F.pp_print_string fmt "----------------------------------------------------------------"
   | HTML ->
-      F.fprintf fmt "--------------------------- %s ---------------------------@\n" num_str ;
+      F.fprintf fmt "--------------------------- %a ---------------------------@\n" pp_num_opt
+        num_opt ;
       F.fprintf fmt "PRE:@\n%a%a%a@\n" Io_infer.Html.pp_start_color Pp.Blue
         (Prop.pp_prop (Pp.html Blue))
         pre Io_infer.Html.pp_end_color () ;
-      (Propgraph.pp_proplist pe_post "POST" (pre, true)) fmt post_list ;
+      Propgraph.pp_proplist pe_post "POST" (pre, true) fmt post_list ;
       F.pp_print_string fmt "----------------------------------------------------------------"
 
 
@@ -275,20 +266,12 @@ let d_spec (spec: 'a spec) = L.add_print_action (L.PTspec, Obj.repr spec)
 
 let pp_specs pe fmt specs =
   let total = List.length specs in
-  let cnt = ref 0 in
   match pe.Pp.kind with
   | TEXT ->
-      List.iter
-        ~f:(fun spec ->
-          incr cnt ;
-          (pp_spec pe (Some (!cnt, total))) fmt spec )
-        specs
+      List.iteri specs ~f:(fun cnt spec -> pp_spec pe (Some (cnt + 1, total)) fmt spec)
   | HTML ->
-      List.iter
-        ~f:(fun spec ->
-          incr cnt ;
-          F.fprintf fmt "%a<br>@\n" (pp_spec pe (Some (!cnt, total))) spec )
-        specs
+      List.iteri specs ~f:(fun cnt spec ->
+          F.fprintf fmt "%a<br>@\n" (pp_spec pe (Some (cnt + 1, total))) spec )
 
 
 let string_of_phase = function FOOTPRINT -> "FOOTPRINT" | RE_EXECUTION -> "RE_EXECUTION"

infer/src/biabduction/BiabductionSummary.mli

@@ -23,7 +23,7 @@ module Jprop : sig
   val d_shallow : Prop.normal t -> unit
   (** Dump the toplevel prop *)
 
-  val d_list : bool -> Prop.normal t list -> unit
+  val d_list : shallow:bool -> Prop.normal t list -> unit
   (** dump a joined prop list, the boolean indicates whether to print toplevel props only *)
 
   val free_vars : Prop.normal t -> Ident.t Sequence.t
@@ -39,7 +39,7 @@ module Jprop : sig
   val map : ('a Prop.t -> 'b Prop.t) -> 'a t -> 'b t
   (** map the function to each prop in the jprop, pointwise *)
 
-  val pp_list : Pp.env -> bool -> Format.formatter -> Prop.normal t list -> unit
+  val pp_list : Pp.env -> shallow:bool -> Format.formatter -> Prop.normal t list -> unit
   (** Print a list of joined props, the boolean indicates whether to print subcomponents of joined props *)
 
   val pp_short : Pp.env -> Format.formatter -> Prop.normal t -> unit

infer/src/biabduction/interproc.ml

@@ -235,7 +235,7 @@ let collect_preconditions tenv summary : Prop.normal BiabductionSummary.Jprop.t
   L.d_ln () ;
   L.d_strln ("#### Footprint of " ^ Typ.Procname.to_string proc_name ^ " after Join  ####") ;
   L.d_increase_indent 1 ;
-  BiabductionSummary.Jprop.d_list false jplist ;
+  BiabductionSummary.Jprop.d_list ~shallow:false jplist ;
   L.d_decrease_indent 1 ;
   L.d_ln () ;
   let jplist' =
@@ -243,7 +243,7 @@ let collect_preconditions tenv summary : Prop.normal BiabductionSummary.Jprop.t
   in
   L.d_strln ("#### Renamed footprint of " ^ Typ.Procname.to_string proc_name ^ ":  ####") ;
   L.d_increase_indent 1 ;
-  BiabductionSummary.Jprop.d_list false jplist' ;
+  BiabductionSummary.Jprop.d_list ~shallow:false jplist' ;
   L.d_decrease_indent 1 ;
   L.d_ln () ;
   let jplist'' =
@@ -254,7 +254,7 @@ let collect_preconditions tenv summary : Prop.normal BiabductionSummary.Jprop.t
   in
   L.d_strln ("#### Abstracted footprint of " ^ Typ.Procname.to_string proc_name ^ ":  ####") ;
   L.d_increase_indent 1 ;
-  BiabductionSummary.Jprop.d_list false jplist'' ;
+  BiabductionSummary.Jprop.d_list ~shallow:false jplist'' ;
   L.d_decrease_indent 1 ;
   L.d_ln () ;
   jplist''