diff --git a/infer/src/backend/Summary.ml b/infer/src/backend/Summary.ml index ecd971ef6..f789ff647 100644 --- a/infer/src/backend/Summary.ml +++ b/infer/src/backend/Summary.ml @@ -119,21 +119,16 @@ let pp_errlog fmt err_log = F.fprintf fmt "WARNINGS: @[%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 "@\n" ; - pp_payload pe fmt summary.payload ; + pp_payload (Pp.html color) fmt summary.payload ; F.fprintf fmt "@\n" diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index f88e0d96a..e91627eac 100644 --- a/infer/src/backend/printer.ml +++ b/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 diff --git a/infer/src/biabduction/BiabductionSummary.ml b/infer/src/biabduction/BiabductionSummary.ml index 1e50a64db..d93ddfcc3 100644 --- a/infer/src/biabduction/BiabductionSummary.ml +++ b/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
@\n" (pp_spec pe (Some (!cnt, total))) spec ) - specs + List.iteri specs ~f:(fun cnt spec -> + F.fprintf fmt "%a
@\n" (pp_spec pe (Some (cnt + 1, total))) spec ) let string_of_phase = function FOOTPRINT -> "FOOTPRINT" | RE_EXECUTION -> "RE_EXECUTION" diff --git a/infer/src/biabduction/BiabductionSummary.mli b/infer/src/biabduction/BiabductionSummary.mli index 9520fa610..16f8571e7 100644 --- a/infer/src/biabduction/BiabductionSummary.mli +++ b/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 diff --git a/infer/src/biabduction/interproc.ml b/infer/src/biabduction/interproc.ml index f899763a6..6bd6fdccb 100644 --- a/infer/src/biabduction/interproc.ml +++ b/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''