| 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).
|