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

[debug] Print nodes using weak topological order

Browse Source 
Reviewed By: jberdine

Differential Revision: D10376606

fbshipit-source-id: 81d89c310
master
Mehdi Bouaziz 6 years ago committed by Facebook Github Bot
parent 8ef9bf7641
commit a2230bca9d
5 changed files with 79 additions and 42 deletions
Show Stats Download Patch File Download Diff File

10
infer/src/IR/Procdesc.ml
Unescape View File

@ -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

2
infer/src/IR/Procdesc.mli
Unescape View File

@ -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 *)

13
infer/src/IR/WeakTopologicalOrder.ml
Unescape View File

@ -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 ->

2
infer/src/IR/WeakTopologicalOrder.mli
Unescape View File

@ -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

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

@ -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 "<br>PREDS:@\n" ;
Pp.seq pp_node_link fmt preds ;
pp_node_link_seq fmt preds ;
F.fprintf fmt "<br>SUCCS: @\n" ;
Pp.seq pp_node_link fmt succs ;
pp_node_link_seq fmt succs ;
F.fprintf fmt "<br>EXN: @\n" ;
Pp.seq pp_node_link fmt exns ;
pp_node_link_seq fmt exns ;
F.fprintf fmt "<br>@\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 "<tr><td class=\"num\" id=\"LINE%d\">%d</td><td class=\"line\">%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 "</td></tr>@\n"
in

Write Preview
Loading…
Cancel
Save