From a2230bca9d0778651c8cdb75f2be0a617b453cbe Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Tue, 16 Oct 2018 07:41:17 -0700 Subject: [PATCH] [debug] Print nodes using weak topological order Reviewed By: jberdine Differential Revision: D10376606 fbshipit-source-id: 81d89c310 --- infer/src/IR/Procdesc.ml | 10 +++ infer/src/IR/Procdesc.mli | 2 + infer/src/IR/WeakTopologicalOrder.ml | 13 ++++ infer/src/IR/WeakTopologicalOrder.mli | 2 + infer/src/backend/printer.ml | 94 +++++++++++++++------------ 5 files changed, 79 insertions(+), 42 deletions(-) diff --git a/infer/src/IR/Procdesc.ml b/infer/src/IR/Procdesc.ml index 5a4a2e1eb..4c04cbea4 100644 --- a/infer/src/IR/Procdesc.ml +++ b/infer/src/IR/Procdesc.ml @@ -88,6 +88,7 @@ module Node = struct type t = { id: id (** unique id of the node *) ; mutable dist_exit: int option (** distance to the exit node *) + ; mutable wto_index: int ; mutable exn: t list (** exception nodes in the cfg *) ; mutable instrs: Instrs.not_reversed_t (** instructions for symbolic execution *) ; kind: nodekind (** kind of node *) @@ -105,6 +106,7 @@ module Node = struct let dummy pname = { id= 0 ; dist_exit= None + ; wto_index= Int.max_value ; instrs= Instrs.empty ; kind= Skip_node "dummy" ; loc= Location.dummy @@ -199,6 +201,8 @@ module Node = struct let get_distance_to_exit node = node.dist_exit + let get_wto_index node = node.wto_index + (** Append the instructions to the list of instructions to execute *) let append_instrs node instrs = if instrs <> [] then node.instrs <- Instrs.append_list node.instrs instrs @@ -544,6 +548,7 @@ let create_node_from_not_reversed pdesc loc kind instrs = let node = { Node.id= node_id ; dist_exit= None + ; wto_index= Int.max_value ; instrs ; kind ; loc @@ -600,6 +605,11 @@ let get_wto pdesc = wto | None -> let wto = WTO.make pdesc in + let _ : int = + WeakTopologicalOrder.Partition.fold_nodes wto ~init:0 ~f:(fun idx node -> + node.Node.wto_index <- idx ; + idx + 1 ) + in pdesc.wto <- Some wto ; wto diff --git a/infer/src/IR/Procdesc.mli b/infer/src/IR/Procdesc.mli index 8cda7cd23..4c8d9ca7b 100644 --- a/infer/src/IR/Procdesc.mli +++ b/infer/src/IR/Procdesc.mli @@ -141,6 +141,8 @@ module Node : sig val get_succs : t -> t list (** Get the successor nodes of the current node *) + val get_wto_index : t -> int + val hash : t -> int (** Hash function for nodes *) diff --git a/infer/src/IR/WeakTopologicalOrder.ml b/infer/src/IR/WeakTopologicalOrder.ml index 60eb6608c..92367d7ae 100644 --- a/infer/src/IR/WeakTopologicalOrder.ml +++ b/infer/src/IR/WeakTopologicalOrder.ml @@ -22,6 +22,19 @@ module Partition = struct let add_component head rest next = Component {head; rest; next} + let rec fold_nodes partition ~init ~f = + match partition with + | Empty -> + init + | Node {node; next} -> + let init = f init node in + (fold_nodes [@tailcall]) next ~init ~f + | Component {head; rest; next} -> + let init = f init head in + let init = fold_nodes rest ~init ~f in + (fold_nodes [@tailcall]) next ~init ~f + + let rec fold_heads partition ~init ~f = match partition with | Empty -> diff --git a/infer/src/IR/WeakTopologicalOrder.mli b/infer/src/IR/WeakTopologicalOrder.mli index 3ac06e712..ea0b037f8 100644 --- a/infer/src/IR/WeakTopologicalOrder.mli +++ b/infer/src/IR/WeakTopologicalOrder.mli @@ -26,6 +26,8 @@ module Partition : sig | Node of {node: 'node; next: 'node t} | Component of {head: 'node; rest: 'node t; next: 'node t} + val fold_nodes : ('node t, 'node, _) Container.fold + val fold_heads : ('node t, 'node, _) Container.fold val expand : fold_right:('a, 'b, 'b t) Container.fold -> 'a t -> 'b t diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 87f2eb5b5..0530bd4ce 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -78,18 +78,26 @@ let is_visited node = Summary.Stats.is_visited stats node_id -let pp_node_link path_to_root ~description fmt node = - let description = - if description then Procdesc.Node.get_description (Pp.html Black) node else "" +let compare_node = + let key node = (Procdesc.Node.get_wto_index node, Procdesc.Node.get_id node) in + fun node1 node2 -> [%compare: int * Procdesc.Node.id] (key node1) (key node2) + + +let pp_node_link_seq path_to_root ~description fmt nodes = + let nodes = List.sort nodes ~compare:compare_node in + let pp_one fmt node = + let description = + if description then Procdesc.Node.get_description (Pp.html Black) node else "" + in + let pname = Procdesc.Node.get_proc_name node in + Io_infer.Html.pp_node_link path_to_root pname ~description + ~preds:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_preds node) :> int list) + ~succs:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_succs node) :> int list) + ~exn:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_exn node) :> int list) + ~isvisited:(is_visited node) fmt + (Procdesc.Node.get_id node :> int) in - Io_infer.Html.pp_node_link path_to_root - (Procdesc.Node.get_proc_name node) - ~description - ~preds:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_preds node) :> int list) - ~succs:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_succs node) :> int list) - ~exn:(List.map ~f:Procdesc.Node.get_id (Procdesc.Node.get_exn node) :> int list) - ~isvisited:(is_visited node) fmt - (Procdesc.Node.get_id node :> int) + Pp.seq pp_one fmt nodes (* =============== START of module NodesHtml =============== *) @@ -111,7 +119,7 @@ module NodesHtml : sig end = struct let log_files = Hashtbl.create 11 - let pp_node_link fmt node = pp_node_link [".."] ~description:false fmt node + let pp_node_link_seq fmt node = pp_node_link_seq [".."] ~description:false fmt node let start_node nodeid loc proc_name preds succs exns source = let node_fname = Io_infer.Html.node_filename proc_name nodeid in @@ -132,11 +140,11 @@ end = struct (Io_infer.Html.pp_line_link source [".."]) loc.Location.line ; F.fprintf fmt "
PREDS:@\n" ; - Pp.seq pp_node_link fmt preds ; + pp_node_link_seq fmt preds ; F.fprintf fmt "
SUCCS: @\n" ; - Pp.seq pp_node_link fmt succs ; + pp_node_link_seq fmt succs ; F.fprintf fmt "
EXN: @\n" ; - Pp.seq pp_node_link fmt exns ; + pp_node_link_seq fmt exns ; F.fprintf fmt "
@\n" ; F.pp_print_flush fmt () ; true ) @@ -217,7 +225,7 @@ let write_proc_html pdesc = ~text:(Some (Escape.escape_xml (Typ.Procname.to_string pname))) []) linenum ; - Pp.seq (pp_node_link [] ~description:true) fmt nodes ; + pp_node_link_seq [] ~description:true fmt nodes ; ( match Summary.get pname with | None -> () @@ -251,6 +259,7 @@ let pp_err_message fmt err_string = let write_html_proc source table_nodes_at_linenum global_err_log proc_desc = let proc_name = Procdesc.get_proc_name proc_desc in + let _ = (* Initializes wto_indexes *) Procdesc.get_wto proc_desc in let process_node n = let lnum = (Procdesc.Node.get_loc n).Location.line in let curr_nodes = try Hashtbl.find table_nodes_at_linenum lnum with Caml.Not_found -> [] in @@ -294,9 +303,6 @@ let write_html_file linereader filename procs = | None -> raise End_of_file in - let nodes_at_linenum = - try Hashtbl.find table_nodes_at_linenum line_number with Caml.Not_found -> [] - in let errors_at_linenum = try let errset = Hashtbl.find table_err_per_line line_number in @@ -305,29 +311,33 @@ let write_html_file linereader filename procs = in F.fprintf fmt "%d%s " line_number line_number line_html ; - Pp.seq (pp_node_link [fname_encoding] ~description:true) fmt nodes_at_linenum ; - List.iter - ~f:(fun n -> - match Procdesc.Node.get_kind n with - | Procdesc.Node.Start_node -> - let proc_name = Procdesc.Node.get_proc_name n in - let num_specs = - match Summary.get proc_name with - | None -> - 0 - | Some summary -> - List.length (Tabulation.get_specs_from_payload summary) - in - let label = - F.sprintf "%s: %d specs" - (Escape.escape_xml (Typ.Procname.to_string proc_name)) - num_specs - in - F.pp_print_char fmt ' ' ; - Io_infer.Html.pp_proc_link [fname_encoding] proc_name fmt label - | _ -> - () ) - nodes_at_linenum ; + ( match Hashtbl.find table_nodes_at_linenum line_number with + | nodes_at_linenum -> + pp_node_link_seq [fname_encoding] ~description:true fmt nodes_at_linenum ; + List.iter + ~f:(fun n -> + match Procdesc.Node.get_kind n with + | Procdesc.Node.Start_node -> + let proc_name = Procdesc.Node.get_proc_name n in + let num_specs = + match Summary.get proc_name with + | None -> + 0 + | Some summary -> + List.length (Tabulation.get_specs_from_payload summary) + in + let label = + F.sprintf "%s: %d specs" + (Escape.escape_xml (Typ.Procname.to_string proc_name)) + num_specs + in + F.pp_print_char fmt ' ' ; + Io_infer.Html.pp_proc_link [fname_encoding] proc_name fmt label + | _ -> + () ) + nodes_at_linenum + | exception Caml.Not_found -> + () ) ; List.iter ~f:(pp_err_message fmt) errors_at_linenum ; F.fprintf fmt "@\n" in