1 | .once
|
2 |
|
3 | // Components
|
4 | // ==========
|
5 |
|
6 | // A simple DAG
|
7 | .comp DiGraph {
|
8 | .decl node(f:Function, s:Statement)
|
9 | .decl edge(f:Function, u:Statement, g:Function, v:Statement)
|
10 | .decl reachable(f: Function, u:Statement, g:Function, v:Statement)
|
11 |
|
12 | node(f, s) :- edge(f, s, _, _).
|
13 | node(f, s) :- edge(_, _, f, s).
|
14 |
|
15 | reachable(f, s1, g, s2) :- edge(f, s1, g, s2).
|
16 | reachable(f, s1, f, s3) :- reachable(f, s1, f, s2), edge(f, s2, f, s3).
|
17 | // XXX: add inter-procedural reachaibility rule
|
18 | }
|
19 |
|
20 | // Facts and Relations (Inputs)
|
21 | // ============================
|
22 |
|
23 | .type Function <: symbol
|
24 | .type Statement <: number
|
25 |
|
26 | // True if there is an edge from s1 to s2 in the control flow graph of f.
|
27 | .decl cf_edge(f:Function, s1:Statement, s2:Statement)
|
28 | .input cf_edge
|
29 |
|
30 | // Rules and Outputs
|
31 | // =================
|
32 |
|
33 | .init CFGraph = DiGraph
|
34 | CFGraph.edge(f, s1, f, s2) :- cf_edge(f, s1, s2).
|