pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[debug][html] Distinguish debug html files for same node in different procedures

Browse Source 
Reviewed By: jvillard

Differential Revision: D4110463

fbshipit-source-id: b60f397
master
Cristiano Calcagno 8 years ago committed by Facebook Github Bot
parent aa3ebf117c
commit d1f8894a9a
3 changed files with 69 additions and 49 deletions
Show Stats Download Patch File Download Diff File

12
infer/src/IR/Io_infer.ml
Unescape View File

@ -184,14 +184,16 @@ struct
let pr_str = "<a " ^ name_str ^ "href=\"" ^ link_str ^ "\">" ^ text ^ "</a>" in let pr_str = "<a " ^ name_str ^ "href=\"" ^ link_str ^ "\">" ^ text ^ "</a>" in
F.fprintf fmt " %s" pr_str F.fprintf fmt " %s" pr_str
(** [pp_node_link path_to_root description isvisited isproof fmt id] (** File name for the node, given the procedure name and node id *)
prints an html link to the given node. *) let node_filename pname id = (Procname.to_filename pname) ^ "_node" ^ string_of_int id
let pp_node_link path_to_root description preds succs exn isvisited isproof fmt 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 = let display_name =
(if description = "" then "N" else String.sub description 0 1) (if description = "" then "N" else String.sub description 0 1)
^ "_" ^ "_"
^ (string_of_int id) in ^ (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 = let style_class =
if not isvisited if not isvisited
then "dangling" then "dangling"
@ -213,7 +215,7 @@ struct
pp_to_string pp () in pp_to_string pp () in
if not isvisited if not isvisited
then F.fprintf fmt " %s" node_text 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 *) (** Print an html link to the given proc *)
let pp_proc_link path_to_root proc_name fmt text = let pp_proc_link path_to_root proc_name fmt text =

15
infer/src/IR/Io_infer.mli
Unescape View File

@ -23,6 +23,9 @@ module Html : sig
(** Return true if the html file was modified since the beginning of the analysis *) (** 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 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 *) (** Open an Html file to append data *)
val open_out : DB.source_file -> DB.Results_dir.path -> Unix.file_descr * Format.formatter 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 *) (** Print end color *)
val pp_end_color : Format.formatter -> unit -> unit val pp_end_color : Format.formatter -> unit -> unit
(** [pp_node_link path_to_root description isvisited isproof fmt id] (** Print an html link to the given node.
prints 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. [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. *) [id] is the node identifier. *)
val pp_node_link : val pp_node_link :
DB.Results_dir.path -> string -> int list -> int list -> int list -> DB.Results_dir.path -> Procname.t ->
bool -> bool -> Format.formatter -> int -> unit 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 *) (** Print an html link to the given proc *)
val pp_proc_link : val pp_proc_link :

91
infer/src/backend/printer.ml
Unescape View File

@ -102,14 +102,12 @@ module NodesHtml : sig
val start_node : val start_node :
int -> Location.t -> Procname.t -> Cfg.node list -> Cfg.node list -> Cfg.node list -> int -> Location.t -> Procname.t -> Cfg.node list -> Cfg.node list -> Cfg.node list ->
DB.source_file -> bool DB.source_file -> bool
val finish_node : int -> DB.source_file -> unit val finish_node : Procname.t -> int -> DB.source_file -> unit
end = struct end = struct
let log_files = Hashtbl.create 11 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 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 modified = Io_infer.Html.modified_during_analysis source ["nodes"; node_fname] in
let needs_initialization, (fd, fmt) = let needs_initialization, (fd, fmt) =
if modified then if modified then
@ -131,34 +129,49 @@ end = struct
(Io_infer.Html.pp_line_link source [".."]) loc.Location.line; (Io_infer.Html.pp_line_link source [".."]) loc.Location.line;
F.fprintf fmt "<br>PREDS:@\n"; F.fprintf fmt "<br>PREDS:@\n";
IList.iter (fun node -> IList.iter (fun node ->
Io_infer.Html.pp_node_link [".."] "" 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) (Cfg.Node.get_proc_name node)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list) ~description:""
(is_visited proc_name node) false fmt (Cfg.Node.get_id node :> int)) preds; ~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 "<br>SUCCS: @\n"; F.fprintf fmt "<br>SUCCS: @\n";
IList.iter (fun node -> IList.iter (fun node ->
Io_infer.Html.pp_node_link [".."] "" 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) (Cfg.Node.get_proc_name node)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list) ~description:""
(is_visited proc_name node) false fmt (Cfg.Node.get_id node :> int)) succs; ~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 "<br>EXN: @\n"; F.fprintf fmt "<br>EXN: @\n";
IList.iter (fun node -> IList.iter (fun node ->
Io_infer.Html.pp_node_link [".."] "" 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) (Cfg.Node.get_proc_name node)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn node) :> int list) ~description:""
(is_visited proc_name node) false fmt (Cfg.Node.get_id node :> int)) exns; ~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 "<br>@\n"; F.fprintf fmt "<br>@\n";
F.pp_print_flush fmt (); F.pp_print_flush fmt ();
true true
) )
else false else false
let finish_node nodeid source = let finish_node proc_name nodeid source =
let fname = id_to_fname nodeid in let node_fname = Io_infer.Html.node_filename proc_name nodeid in
let fd = Hashtbl.find log_files (fname, source) in let fd = Hashtbl.find log_files (node_fname, source) in
Unix.close fd; Unix.close fd;
curr_html_formatter := F.std_formatter curr_html_formatter := F.std_formatter
end end
@ -393,7 +406,7 @@ let node_finish_session node source =
if Config.write_html then begin if Config.write_html then begin
F.fprintf !curr_html_formatter "</LISTING>%a" F.fprintf !curr_html_formatter "</LISTING>%a"
Io_infer.Html.pp_end_color (); 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 end
(** Write html file for the procedure. (** Write html file for the procedure.
@ -415,12 +428,16 @@ let write_proc_html source whole_seconds pdesc =
linenum; linenum;
IList.iter IList.iter
(fun n -> (fun n ->
Io_infer.Html.pp_node_link [] 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) (Cfg.Node.get_proc_name n)
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs n) :> int list) ~description:(Cfg.Node.get_description (pe_html Black) n)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn n) :> int list) ~preds:(IList.map Cfg.Node.get_id (Cfg.Node.get_preds n) :> int list)
(is_visited pname n) false fmt (Cfg.Node.get_id n :> int)) ~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; nodes;
(match Specs.get_summary pname with (match Specs.get_summary pname with
| None -> | None ->
@ -525,14 +542,14 @@ let write_html_file linereader filename procs =
Specs.Visitedset.mem (Cfg.Node.get_id n, []) !proof_cover in Specs.Visitedset.mem (Cfg.Node.get_id n, []) !proof_cover in
Io_infer.Html.pp_node_link Io_infer.Html.pp_node_link
[fname_encoding] [fname_encoding]
(Cfg.Node.get_description (pe_html Black) n) (Cfg.Node.get_proc_name n)
(IList.map Cfg.Node.get_id (Cfg.Node.get_preds n) :> int list) ~description:(Cfg.Node.get_description (pe_html Black) n)
(IList.map Cfg.Node.get_id (Cfg.Node.get_succs n) :> int list) ~preds:(IList.map Cfg.Node.get_id (Cfg.Node.get_preds n) :> int list)
(IList.map Cfg.Node.get_id (Cfg.Node.get_exn n) :> int list) ~succs:(IList.map Cfg.Node.get_id (Cfg.Node.get_succs n) :> int list)
(is_visited (Cfg.Procdesc.get_proc_name pdesc) n) ~exn:(IList.map Cfg.Node.get_id (Cfg.Node.get_exn n) :> int list)
isproof ~isvisited:(is_visited (Cfg.Procdesc.get_proc_name pdesc) n)
fmt ~isproof
(Cfg.Node.get_id n :> int)) fmt (Cfg.Node.get_id n :> int))
nodes_at_linenum; nodes_at_linenum;
IList.iter IList.iter
(fun (n, _) -> (fun (n, _) ->

Write Preview
Loading…
Cancel
Save