Source file graphSig.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
(** A simple graph library to represent control-flow graphs.
We actually use an oriented hyper-graph structure: an edge connects
a set of (source) nodes to a set of (destination) nodes.
Equivalently, this can be seen as a bipartite graph where nodes and
edges correspond to the two node partitions.
Nodes model program locations, where an invariant can be stored.
Edges model transfer functions for basic blocks.
An edge can have several source nodes, to model control-flow joins
at the entry of basic blocks. It is also possible to model joins by
having several edges incoming into the same node.
An edge can have several destination nodes, to model conditionals with
several outputs from a basic block. Alternatively, several edges outgoing
from the same node can be used to model conditionals.
We use "ports" to distinguish and classify between the different
source and destination nodes of an edge. Ports carry tags.
It is possible to have a node connected to the same edge several times,
either on equal or different ports.
Nodes and edges have unique identifiers, ordered to serve as map keys.
Each node and edge has a mutable data field of polymorphic type.
However, data attached to nodes and edges can also be maintained
outside of the graph structure, using hash-tables or maps from identifiers
to the actual data.
Graphs are mutable to make it easier to construct them.
It is expected that, after creation in the front-end, graphs remain
unmodified (except maybe for the data fields).
*)
(** {2 Ordered, hashable data types} *)
(** Data-type that can be used both in sets, maps, and hash-tables. *)
module type ID_TYPE = sig
type t
val compare: t -> t -> int
val equal: t -> t -> bool
val hash: t -> int
end
(** {2 Nested lists} *)
(** Nested lists of nodes are used to represent herarchical decompositions
into strongly connected components.
*)
type 'a nested_list =
| Simple of 'a
| Composed of 'a nested_list list
(** {2 Parameter signature} *)
module type P = sig
module NodeId: ID_TYPE
(** Unique node identifiers, that can serve as keys in maps. *)
module EdgeId: ID_TYPE
(** Unique edge identifiers, that can serve as keys in maps. *)
module Port: ID_TYPE
(** Edges connect to nodes through tagged ports. *)
end
(** {2 Graph signature} *)
module type S = sig
(** {2 Types} *)
type ('node_data, 'edge_data) graph
(** Type of graphs.
Custom arbitrary data of type ['node_data] and ['edge_data] can be
stored, respectively, in nodes and edges.
*)
type ('node_data, 'edge_data) node
(** A node in the graph. *)
type ('node_data, 'edge_data) edge
(** An (hyper)-edge in the graph. *)
module P: P
type node_id = P.NodeId.t
type edge_id = P.EdgeId.t
type port = P.Port.t
(** Export back types from the functor parameter. *)
module NodeSet: SetExtSig.S with type elt = node_id
module EdgeSet: SetExtSig.S with type elt = edge_id
(** Sets constructed from ordered type parameters. *)
module NodeMap: MapExtSig.S with type key = node_id
module EdgeMap: MapExtSig.S with type key = edge_id
(** Maps constructed from ordered type parameters. *)
(** {2 Construction} *)
val create: unit -> ('n,'e) graph
(** Creates an empty graph. *)
val add_node: ('n,'e) graph -> node_id
-> ?inc:(port * ('n,'e) edge) list
-> ?out:(port * ('n,'e) edge) list
-> ?entry:port -> ?exit:port
-> 'n -> ('n,'e) node
(** Adds a node to the graph.
Optionally connects the node to incoming or outgoing edges.
Optionally sets as an entry or exit node on a port (defaults to None,
i.e., not entry nor exit).
The node identifier must be unique among the node in the graph;
raises [Invalid_argument] otherwise.
*)
val add_edge: ('n,'e) graph -> edge_id
-> ?src:(port * ('n,'e) node) list
-> ?dst:(port * ('n,'e) node) list
-> 'e -> ('n,'e) edge
(** Adds an edge to the graph.
Optionally connects the edge to source or destination nodes.
The edge identifier must be unique among the edges in the graph;
raises [Invalid_argument] otherwise.
*)
val remove_node: ('n,'e) graph -> ('n,'e) node -> unit
(** Removes a node if it exists in the graph; otherwise, do nothing.
All connections to incoming and outgoing edges are removed.
*)
val remove_edge: ('n,'e) graph -> ('n,'e) edge -> unit
(** Removes an edge if it exists in the graph; otherwise, do nothing.
All connections to source and destination nodes are removed.
*)
val node_set_entry: ('n,'e) graph -> ('n,'e) node -> port option -> unit
(** Sets whether a node is an entry node on some port, or not (None).
A given node can be entry for a single port at a time;
previous entry ports are removed.
*)
val node_set_exit: ('n,'e) graph -> ('n,'e) node -> port option -> unit
(** Sets whether a node is an exit node on some port, or not (None).
A given node can be exit on a single port at a time;
previous exit ports are removed.
*)
val node_add_in: ('n,'e) node -> port -> ('n,'e) edge -> unit
(** Adds an incoming edge to the node, on the given port.
A node can be connected to the same edge several times, on
different or equal ports.
Use the [_unique] version to ensure that a node is connected to
an given edge on a given port only once.
*)
val node_add_out: ('n,'e) node -> port -> ('n,'e) edge -> unit
(** Adds an outgoing edge to the node, on the given port. *)
val node_add_in_list: ('n,'e) node -> ((port * ('n,'e) edge) list) -> unit
(** Adds incoming edges to the node, on the given ports. *)
val node_add_out_list: ('n,'e) node -> ((port * ('n,'e) edge) list) -> unit
(** Adds outgoing edges to the node, on the given ports. *)
val edge_add_src: ('n,'e) edge -> port -> ('n,'e) node -> unit
(** Adds a source node to the edge, on the given port. *)
val edge_add_dst: ('n,'e) edge -> port -> ('n,'e) node -> unit
(** Adds a destination node to the edge, on the given port. *)
val edge_add_src_list: ('n,'e) edge -> ((port * ('n,'e) node) list) -> unit
(** Adds source nodes to the edge, on the given ports. *)
val edge_add_dst_list: ('n,'e) edge -> ((port * ('n,'e) node) list) -> unit
(** Adds destination nodes to the edge, on the given ports. *)
val node_add_in_unique: ('n,'e) node -> port -> ('n,'e) edge -> unit
(** Adds an incoming edge to the node, on the given port,
but only if not already present on this port.
Does not prevent the node to be connected to the edge on
other ports.
*)
val node_add_out_unique: ('n,'e) node -> port -> ('n,'e) edge -> unit
(** Adds an outgoing edge to the node, on the given port,
but only if not already present on this port.
*)
val node_add_in_list_unique: ('n,'e) node -> ((port * ('n,'e) edge) list) -> unit
(** Adds incoming edges to the node, on the given ports,
but only if not already present on this port.
*)
val node_add_out_list_unique: ('n,'e) node -> ((port * ('n,'e) edge) list) -> unit
(** Adds outgoing edges to the node, on the given ports,
but only if not already present on this port.
*)
val edge_add_src_unique: ('n,'e) edge -> port -> ('n,'e) node -> unit
(** Adds a source node to the edge, on the given port,
but only if not already present on this port.
*)
val edge_add_dst_unique: ('n,'e) edge -> port -> ('n,'e) node -> unit
(** Adds a destination node to the edge, on the given port,
but only if not already present on this port.
*)
val edge_add_src_list_unique: ('n,'e) edge -> ((port * ('n,'e) node) list) -> unit
(** Adds source nodes to the edge, on the given ports,
but only if not already present on this port.
*)
val edge_add_dst_list_unique: ('n,'e) edge -> ((port * ('n,'e) node) list) -> unit
(** Adds destination nodes to the edge, on the given ports,
but only if not already present on this port.
*)
val node_remove_in_port: ('n,'e) node -> port -> ('n,'e) edge -> unit
(** Removes all the connections to the node incoming from the edge
on the given port.
No edge nor node is deleted.
*)
val node_remove_out_port: ('n,'e) node -> port -> ('n,'e) edge -> unit
(** Removes all the connections from the node outgoing into the edge
on the given port.
No edge nor node is deleted.
*)
val node_remove_in: ('n,'e) node -> ('n,'e) edge -> unit
(** Removes all the connections to the node incoming into from the edge,
on all ports.
No edge nor node is deleted.
*)
val node_remove_out: ('n,'e) node -> ('n,'e) edge -> unit
(** Removes all the connections from the node incoming into the edge,
on all ports.
No edge nor node is deleted.
*)
val node_remove_all_in: ('n,'e) node -> unit
(** Removes all the connections incoming into the node,
for all edges and ports.
No edge nor node is deleted.
*)
val node_remove_all_out: ('n,'e) node -> unit
(** Removes all the connections outgoing from the node,
for all edges and ports.
No edge nor node is deleted.
*)
val edge_remove_src_port: ('n,'e) edge -> port -> ('n,'e) node -> unit
(** Removes all the connections to the edge from the node
on the given port.
No edge nor node is deleted.
*)
val edge_remove_dst_port: ('n,'e) edge -> port -> ('n,'e) node -> unit
(** Removes all the connections from the edge to the node
on the given port.
No edge nor node is deleted.
*)
val edge_remove_src: ('n,'e) edge -> ('n,'e) node -> unit
(** Removes all the connections to the edge from the node,
on all ports.
No edge nor node is deleted.
*)
val edge_remove_dst: ('n,'e) edge -> ('n,'e) node -> unit
(** Removes all the connections from the edge to the node
on all ports.
No edge nor node is deleted.
*)
val edge_remove_all_src: ('n,'e) edge -> unit
(** Removes all the connections at the source of the edge,
for all nodes and ports.
No edge nor node is deleted.
*)
val edge_remove_all_dst: ('n,'e) edge -> unit
(** Removes all the connections at the destination of the edge,
for all nodes and ports.
No edge nor node is deleted
*)
val node_set_in: ('n,'e) node -> ((port * ('n,'e) edge) list) -> unit
(** Sets the incoming edges to the node, on the given ports. *)
val node_set_out: ('n,'e) node -> ((port * ('n,'e) edge) list) -> unit
(** Sets the outgoing edges to the node, on the given ports. *)
val edge_set_src: ('n,'e) edge -> ((port * ('n,'e) node) list) -> unit
(** Sets the source nodes to the edge, on the given ports. *)
val edge_set_dst: ('n,'e) edge -> ((port * ('n,'e) node) list) -> unit
(** Sets destination nodes to the edge, on the given ports. *)
val node_set_in_unique: ('n,'e) node -> ((port * ('n,'e) edge) list) -> unit
(** Sets the incoming edges to the node, on the given ports. *)
val node_set_out_unique: ('n,'e) node -> ((port * ('n,'e) edge) list) -> unit
(** Sets the outgoing edges to the node, on the given ports. *)
val edge_set_src_unique: ('n,'e) edge -> ((port * ('n,'e) node) list) -> unit
(** Sets the source nodes to the edge, on the given ports. *)
val edge_set_dst_unique: ('n,'e) edge -> ((port * ('n,'e) node) list) -> unit
(** Sets destination nodes to the edge, on the given ports. *)
(** {2 Exploration} *)
val node_list: ('n,'e) graph -> ('n,'e) node list
(** The set of nodes in the graph as a list. *)
val edge_list: ('n,'e) graph -> ('n,'e) edge list
(** The set of edges in the graph as a list. *)
val node_set: ('n,'e) graph -> NodeSet.t
(** The set of nodes in the graph as a set of identifiers. *)
val edge_set: ('n,'e) graph -> EdgeSet.t
(** The set of edges in the graph as a set of identifiers. *)
val node_map: ('n,'e) graph -> ('n,'e) node NodeMap.t
(** The set of nodes in the graph as a map from identifiers to nodes. *)
val edge_map: ('n,'e) graph -> ('n,'e) edge EdgeMap.t
(** The set of edges in the graph as a map from identifiers to edges. *)
val has_node: ('n,'e) graph -> node_id -> bool
(** Whether the graph contains a node with this identifier. *)
val has_edge: ('n,'e) graph -> edge_id -> bool
(** Whether the graph contains an edge with this identifier. *)
val get_node: ('n,'e) graph -> node_id -> ('n,'e) node
(** The node corresponding to the identifier in the graph.
Raises [Not_found] if [has_node] is false.
*)
val get_edge: ('n,'e) graph -> edge_id -> ('n,'e) edge
(** The edge corresponding to the identifier in the graph.
Raises [Not_found] if [has_edge] is false.
*)
val entries: ('n,'e) graph -> (port * ('n,'e) node) list
(** List of entry nodes, with port. *)
val exits: ('n,'e) graph -> (port * ('n,'e) node) list
(** List of exist nodes, with port. *)
val edge_id: ('n,'e) edge -> edge_id
(** Edge identifier. *)
val edge_data: ('n,'e) edge -> 'e
(** Gets custom data associated to the edge. *)
val edge_set_data: ('n,'e) edge -> 'e -> unit
(** Sets custom data associated to the edge. *)
val edge_src: ('n,'e) edge -> (port * ('n,'e) node) list
(** List of edge source nodes. *)
val edge_dst: ('n,'e) edge -> (port * ('n,'e) node) list
(** List of edge destination nodes. *)
val edge_src_port: ('n,'e) edge -> port -> ('n,'e) node list
(** List of edge source nodes on the given port. *)
val edge_dst_port: ('n,'e) edge -> port -> ('n,'e) node list
(** List of edge destination nodes on the given port. *)
val edge_src_size: ('n,'e) edge -> int
(** Number of edge source nodes. *)
val edge_dst_size: ('n,'e) edge -> int
(** Number of edge destination nodes. *)
val edge_src_port_size: ('n,'e) edge -> port -> int
(** Number of edge source nodes on the given port. *)
val edge_dst_port_size: ('n,'e) edge -> port -> int
(** Number of edge destination nodes on the given port. *)
val node_id: ('n,'e) node -> node_id
(** Node identifier. *)
val node_data: ('n,'e) node -> 'n
(** Gets custom data associated to the node. *)
val node_set_data: ('n,'e) node -> 'n -> unit
(** Sets custom data associated to the node. *)
val node_in: ('n,'e) node -> (port * ('n,'e) edge) list
(** List of edges incoming into the node. *)
val node_out: ('n,'e) node -> (port * ('n,'e) edge) list
(** List of edges outgoing from the node. *)
val node_in_port: ('n,'e) node -> port -> ('n,'e) edge list
(** List of edges incoming into the node on the given port. *)
val node_out_port: ('n,'e) node -> port -> ('n,'e) edge list
(** List of edges outgoing from the node on the given port. *)
val node_in_size: ('n,'e) node -> int
(** Number of edges incoming into the node. *)
val node_out_size: ('n,'e) node -> int
(** Number of edges outgoing from the node. *)
val node_in_port_size: ('n,'e) node -> port -> int
(** Number of edges incoming into the node on the given port. *)
val node_out_port_size: ('n,'e) node -> port -> int
(** Number of edges outgoing from the node on the given port. *)
val node_entry_port: ('n,'e) graph -> ('n,'e) node -> port option
(** If the node is an entry node, returns its port, otherwise None. *)
val node_exit_port: ('n,'e) graph -> ('n,'e) node -> port option
(** If the node is an exit node, returns its port, otherwise None. *)
val node_has_out: ('n,'e) node -> ('n,'e) edge -> bool
(** Whether the given edge is outgoing from the node. *)
val node_has_out_port: ('n,'e) node -> port -> ('n,'e) edge -> bool
(** Whether the given edge is outgoing from the node on the given port. *)
val node_has_in: ('n,'e) node -> ('n,'e) edge -> bool
(** Whether the given edge is incoming into the node. *)
val node_has_in_port: ('n,'e) node -> port -> ('n,'e) edge -> bool
(** Whether the given edge is incoming into the node on the given port. *)
val edge_has_src: ('n,'e) edge -> ('n,'e) node -> bool
(** Whether the edge has the node as source. *)
val edge_has_src_port: ('n,'e) edge -> port -> ('n,'e) node -> bool
(** Whether the edge has the node as source on the given port. *)
val edge_has_dst: ('n,'e) edge -> ('n,'e) node -> bool
(** Whether the edge has the node as destination. *)
val edge_has_dst_port: ('n,'e) edge -> port -> ('n,'e) node -> bool
(** Whether the edge has the node as destination on the given port. *)
val node_out_nodes: ('n,'e) node
-> (port * ('n,'e) edge * port * ('n,'e) node) list
(** Successors nodes of a given node.
Each returned element [(port1,edge,port2,node)] gives the port [port1]
connecting the argument node to an edge [edge], the edge [edge],
the port [port2] connecting the edge [edge] to the successor node [node],
and finally the successor node [node].
*)
val node_in_nodes: ('n,'e) node
-> (('n,'e) node * port * ('n,'e) edge * port) list
(** Predecessor nodes of a given node.
Each returned element [(node,port1,edge,port2)] gives the predecessor
node [node], the port [port1] connecting it to an edge [edge],
the edge [edge], and finally the port [port2] connecting the edge
[edge] to the argument node.
*)
val node_out_nodes_port: ('n,'e) node -> port -> port
-> (('n,'e) edge * ('n,'e) node) list
(** Successor nodes of a given node connected through an edge
on the specified ports.
[node_out_nodes_port node port1 port2] returns a list of
[(edge,node')] elements, where [port1] connects the argument [node]
to an edge [edge] and [port2] connects the edge [edge] to a
successor node [node'].
*)
val node_in_nodes_port: ('n,'e) node -> port -> port
-> (('n,'e) node * ('n,'e) edge) list
(** Predecessor nodes of a given node connected through an edge
on the specified ports.
[node_in_nodes_port node port1 port2] returns a list of
[(node',edge)] elements, where [port1] connects the predecessor
[node'] to an edge [edge] and [port2] connects the edge [edge] to a
the argument node [node].
*)
val node_has_node_out: ('n,'e) node -> ('n,'e) node -> bool
(** Whether the first node has an outgoing edge into the second node. *)
val node_has_node_in: ('n,'e) node -> ('n,'e) node -> bool
(** Whether the first node has an incoming edge from the second node. *)
val node_has_node_out_port: ('n,'e) node -> port -> port -> ('n,'e) node -> bool
(** Whether the first node has an outgoing edge on the first port,
going into the second node on the second port.
*)
val node_has_node_in_port: ('n,'e) node -> port -> port -> ('n,'e) node -> bool
(** Whether the first node has an incoming edge on the first port,
coming from the second node on the second port.
*)
(** {2 Maps and folds} *)
val clone: ('n,'e) graph -> ('n,'e) graph
(** Creates a copy of the graph. *)
val clone_map: ('n1 -> 'n2) -> ('e1 -> 'e2) -> ('n1,'e1) graph
-> ('n2,'e2) graph
(** Creates a copy of the graph, applying a function to each
node data and each edge data.
*)
val transpose: ('n,'e) graph -> unit
(** Reverses the direction of all edges.
Also switches entry and exit nodes.
*)
val iter_nodes: (node_id -> ('n,'e) node -> unit) -> ('n,'e) graph -> unit
(** Iterates a function on all nodes.
The order in which the function is called is not specified.
*)
val iter_edges: (edge_id -> ('n,'e) edge -> unit) -> ('n,'e) graph -> unit
(** Iterates a function on all edges.
The order in which the function is called is not specified.
*)
val map_nodes: (node_id -> ('n,'e) node -> 'a) -> ('n,'e) graph
-> 'a NodeMap.t
(** Constructs a map from node identifiers, applying the given function.
The order in which the function is called is not specified.
*)
val map_edges: (edge_id -> ('n,'e) edge -> 'a) -> ('n,'e) graph
-> 'a EdgeMap.t
(** Constructs a map from edge identifiers, applying the given function.
The order in which the function is called is not specified.
*)
val fold_nodes: (node_id -> ('n,'e) node -> 'a -> 'a) -> ('n,'e) graph
-> 'a -> 'a
(** Accumulates a function on all nodes.
The order in which the function is called is not specified.
*)
val fold_edges: (edge_id -> ('n,'e) edge -> 'a -> 'a) -> ('n,'e) graph
-> 'a -> 'a
(** Accumulates a function on all edges.
The order in which the function is called is not specified.
*)
val iter_nodes_ordered: (node_id -> ('n,'e) node -> unit)
-> ('n,'e) graph -> unit
(** Iterates a function on all nodes.
The function is called in increasing identifier order.
*)
val iter_edges_ordered: (edge_id -> ('n,'e) edge -> unit)
-> ('n,'e) graph -> unit
(** Iterates a function on all edges.
The function is called in increasing identifier order.
*)
val map_nodes_ordered: (node_id -> ('n,'e) node -> 'a)
-> ('n,'e) graph -> 'a NodeMap.t
(** Constructs a map from node identifiers, applying the given function.
The function is called in increasing identifier order.
*)
val map_edges_ordered: (edge_id -> ('n,'e) edge -> 'a)
-> ('n,'e) graph -> 'a EdgeMap.t
(** Constructs a map from edge identifiers, applying the given function.
The function is called in increasing identifier order.
*)
val fold_nodes_ordered: (node_id -> ('n,'e) node -> 'a -> 'a)
-> ('n,'e) graph -> 'a -> 'a
(** Accumulates a function on all nodes.
The function is called in increasing identifier order.
*)
val fold_edges_ordered: (edge_id -> ('n,'e) edge -> 'a -> 'a)
-> ('n,'e) graph -> 'a -> 'a
(** Accumulates a function on all edges.
The function is called in increasing identifier order.
*)
(** {Simplification} *)
val remove_orphan: ('n,'e) graph -> unit
(** Removes orphan nodes and edges.
Orphan nodes have no incoming nor outgoing edges, and orphan
edges have no source nor destination nodes.
*)
(** {Topological ordering} *)
(**
Computes a weak topological ordering suitable to perform fixpoint
iterations with widening.
Implements Bourdoncle's algorithm [1].
[1] Francois Bourdoncle. Efficient Chaotic Iteration Strategies
With Widenings. In Proc. FMPA'93, 128-141, 1993. Springer.
*)
val weak_topological_order: ('n,'e) graph -> ('n,'e) node nested_list list
(** Returns an adminisible list of widening points.
Given a weak topological ordering, we compute the head of
every component.
*)
val widening_points: ('n,'e) node nested_list list -> ('n,'e) node list
(** {2 Printing} *)
(** Print in plain text. *)
type ('n,'e) printer = {
print_node: Format.formatter -> ('n,'e) node -> unit;
print_edge: Format.formatter -> ('n,'e) edge -> unit;
print_src: Format.formatter -> ('n,'e) node -> port -> ('n,'e) edge
-> unit;
print_dst: Format.formatter -> ('n,'e) edge -> port -> ('n,'e) node
-> unit;
print_entry: Format.formatter -> ('n,'e) node -> port -> unit;
print_exit: Format.formatter -> ('n,'e) node -> port -> unit;
}
val print: ('n,'e) printer -> Format.formatter -> ('n,'e) graph -> unit
(** Print in dot graph format. *)
type ('n,'e) dot_printer = {
dot_pp_node: Format.formatter -> ('n,'e) node -> unit;
dot_pp_edge: Format.formatter -> ('n,'e) edge -> unit;
dot_pp_port: Format.formatter -> port -> unit;
dot_filter_node: ('n,'e) node -> bool;
dot_filter_edge: ('n,'e) edge -> bool;
dot_filter_port: port -> bool;
}
val print_dot: ('n,'e) dot_printer -> string -> Format.formatter
-> ('n,'e) graph -> unit
(** [print_dot channel graph name printer].
outputs the graph in the specified channel in dot format.
In addition [name] gives the dot graph name.
The node, edge and port printer functions are user-specified.
*)
end