diff --git a/infer/src/IR/Io_infer.ml b/infer/src/IR/Io_infer.ml index 0e4e5aeb7..ef6ba48b9 100644 --- a/infer/src/IR/Io_infer.ml +++ b/infer/src/IR/Io_infer.ml @@ -184,14 +184,16 @@ struct let pr_str = "" ^ text ^ "" in F.fprintf fmt " %s" pr_str - (** [pp_node_link path_to_root description isvisited isproof fmt id] - prints an html link to the given node. *) - let pp_node_link path_to_root description preds succs exn isvisited isproof fmt id = + (** File name for the node, given the procedure name and node id *) + let node_filename pname id = (Procname.to_filename pname) ^ "_node" ^ string_of_int id + + (** Print an html link to the given node. *) + let pp_node_link path_to_root pname ~description ~preds ~succs ~exn ~isvisited ~isproof fmt id = let display_name = (if description = "" then "N" else String.sub description 0 1) ^ "_" ^ (string_of_int id) in - let node_name = "node" ^ string_of_int id in + let node_fname = node_filename pname id in let style_class = if not isvisited then "dangling" @@ -213,7 +215,7 @@ struct pp_to_string pp () in if not isvisited then F.fprintf fmt " %s" node_text - else pp_link ~path: (path_to_root @ ["nodes"; node_name]) fmt node_text + else pp_link ~path: (path_to_root @ ["nodes"; node_fname]) fmt node_text (** Print an html link to the given proc *) let pp_proc_link path_to_root proc_name fmt text = diff --git a/infer/src/IR/Io_infer.mli b/infer/src/IR/Io_infer.mli index 95a150a10..747fa7ade 100644 --- a/infer/src/IR/Io_infer.mli +++ b/infer/src/IR/Io_infer.mli @@ -23,6 +23,9 @@ module Html : sig (** Return true if the html file was modified since the beginning of the analysis *) val modified_during_analysis : DB.source_file -> DB.Results_dir.path -> bool + (** File name for the node, given the procedure name and node id *) + val node_filename : Procname.t -> int -> string + (** Open an Html file to append data *) val open_out : DB.source_file -> DB.Results_dir.path -> Unix.file_descr * Format.formatter @@ -37,16 +40,14 @@ module Html : sig (** Print end color *) val pp_end_color : Format.formatter -> unit -> unit - (** [pp_node_link path_to_root description isvisited isproof fmt id] - prints an html link to the given node. + (** Print an html link to the given node. + Usage: [pp_node_link path_to_root ... fmt id]. [path_to_root] is the path to the dir for the procedure in the spec db. - [description] is a string description. - [is_visited] indicates whether the node should be active or greyed out. - [is_proof] indicates whether the node is part of a proof and should be green. [id] is the node identifier. *) val pp_node_link : - DB.Results_dir.path -> string -> int list -> int list -> int list -> - bool -> bool -> Format.formatter -> int -> unit + DB.Results_dir.path -> Procname.t -> + description:string -> preds:int list -> succs:int list -> exn:int list -> + isvisited:bool -> isproof:bool -> Format.formatter -> int -> unit (** Print an html link to the given proc *) val pp_proc_link : diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 593a0d2ae..1f635bcc8 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -102,14 +102,12 @@ module NodesHtml : sig val start_node : int -> Location.t -> Procname.t -> Cfg.node list -> Cfg.node list -> Cfg.node list -> DB.source_file -> bool - val finish_node : int -> DB.source_file -> unit + val finish_node : Procname.t -> int -> DB.source_file -> unit end = struct let log_files = Hashtbl.create 11 - let id_to_fname id = "node" ^ string_of_int id - let start_node nodeid loc proc_name preds succs exns source = - let node_fname = id_to_fname nodeid in + let node_fname = Io_infer.Html.node_filename proc_name nodeid in let modified = Io_infer.Html.modified_during_analysis source ["nodes"; node_fname] in let needs_initialization, (fd, fmt) = if modified then @@ -131,34 +129,49 @@ end = struct (Io_infer.Html.pp_line_link source [".."]) loc.Location.line; F.fprintf fmt "
PREDS:@\n"; IList.iter (fun node -> - Io_infer.Html.pp_node_link [".."] "" - (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list) - (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list) - (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list) - (is_visited proc_name node) false fmt (Cfg.Node.get_id node :> int)) preds; + Io_infer.Html.pp_node_link + [".."] + (Cfg.Node.get_proc_name node) + ~description:"" + ~preds:(IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list) + ~succs:(IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list) + ~exn:(IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list) + ~isvisited:(is_visited proc_name node) + ~isproof:false + fmt (Cfg.Node.get_id node :> int)) preds; F.fprintf fmt "
SUCCS: @\n"; IList.iter (fun node -> - Io_infer.Html.pp_node_link [".."] "" - (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list) - (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list) - (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list) - (is_visited proc_name node) false fmt (Cfg.Node.get_id node :> int)) succs; + Io_infer.Html.pp_node_link + [".."] + (Cfg.Node.get_proc_name node) + ~description:"" + ~preds:(IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list) + ~succs:(IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list) + ~exn:(IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list) + ~isvisited:(is_visited proc_name node) + ~isproof:false + fmt (Cfg.Node.get_id node :> int)) succs; F.fprintf fmt "
EXN: @\n"; IList.iter (fun node -> - Io_infer.Html.pp_node_link [".."] "" - (IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list) - (IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list) - (IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list) - (is_visited proc_name node) false fmt (Cfg.Node.get_id node :> int)) exns; + Io_infer.Html.pp_node_link + [".."] + (Cfg.Node.get_proc_name node) + ~description:"" + ~preds:(IList.map Cfg.Node.get_id (Cfg.Node.get_preds node) :> int list) + ~succs:(IList.map Cfg.Node.get_id (Cfg.Node.get_succs node) :> int list) + ~exn:(IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list) + ~isvisited:(is_visited proc_name node) + ~isproof:false + fmt (Cfg.Node.get_id node :> int)) exns; F.fprintf fmt "
@\n"; F.pp_print_flush fmt (); true ) else false - let finish_node nodeid source = - let fname = id_to_fname nodeid in - let fd = Hashtbl.find log_files (fname, source) in + let finish_node proc_name nodeid source = + let node_fname = Io_infer.Html.node_filename proc_name nodeid in + let fd = Hashtbl.find log_files (node_fname, source) in Unix.close fd; curr_html_formatter := F.std_formatter end @@ -393,7 +406,7 @@ let node_finish_session node source = if Config.write_html then begin F.fprintf !curr_html_formatter "%a" Io_infer.Html.pp_end_color (); - NodesHtml.finish_node (Cfg.Node.get_id node :> int) source + NodesHtml.finish_node (Cfg.Node.get_proc_name node) (Cfg.Node.get_id node :> int) source end (** Write html file for the procedure. @@ -415,12 +428,16 @@ let write_proc_html source whole_seconds pdesc = linenum; IList.iter (fun n -> - Io_infer.Html.pp_node_link [] - (Cfg.Node.get_description (pe_html Black) n) - (IList.map Cfg.Node.get_id (Cfg.Node.get_preds n) :> int list) - (IList.map Cfg.Node.get_id (Cfg.Node.get_succs n) :> int list) - (IList.map Cfg.Node.get_id (Cfg.Node.get_exn n) :> int list) - (is_visited pname n) false fmt (Cfg.Node.get_id n :> int)) + Io_infer.Html.pp_node_link + [] + (Cfg.Node.get_proc_name n) + ~description:(Cfg.Node.get_description (pe_html Black) n) + ~preds:(IList.map Cfg.Node.get_id (Cfg.Node.get_preds n) :> int list) + ~succs:(IList.map Cfg.Node.get_id (Cfg.Node.get_succs n) :> int list) + ~exn:(IList.map Cfg.Node.get_id (Cfg.Node.get_exn n) :> int list) + ~isvisited:(is_visited pname n) + ~isproof:false + fmt (Cfg.Node.get_id n :> int)) nodes; (match Specs.get_summary pname with | None -> @@ -525,14 +542,14 @@ let write_html_file linereader filename procs = Specs.Visitedset.mem (Cfg.Node.get_id n, []) !proof_cover in Io_infer.Html.pp_node_link [fname_encoding] - (Cfg.Node.get_description (pe_html Black) n) - (IList.map Cfg.Node.get_id (Cfg.Node.get_preds n) :> int list) - (IList.map Cfg.Node.get_id (Cfg.Node.get_succs n) :> int list) - (IList.map Cfg.Node.get_id (Cfg.Node.get_exn n) :> int list) - (is_visited (Cfg.Procdesc.get_proc_name pdesc) n) - isproof - fmt - (Cfg.Node.get_id n :> int)) + (Cfg.Node.get_proc_name n) + ~description:(Cfg.Node.get_description (pe_html Black) n) + ~preds:(IList.map Cfg.Node.get_id (Cfg.Node.get_preds n) :> int list) + ~succs:(IList.map Cfg.Node.get_id (Cfg.Node.get_succs n) :> int list) + ~exn:(IList.map Cfg.Node.get_id (Cfg.Node.get_exn n) :> int list) + ~isvisited:(is_visited (Cfg.Procdesc.get_proc_name pdesc) n) + ~isproof + fmt (Cfg.Node.get_id n :> int)) nodes_at_linenum; IList.iter (fun (n, _) ->