A relational callgraph is described with unpredicated rules relating argument-free continuations, connecting a product of n
sources and m
conditions to a single sink (also called the goal). The format is as follows:
Y :- X[1], X[2], ..., X[n], c[1], c[2], ..., c[m].
means "when all continuations X[1]..X[n]
have been called, and all conditions c[1]..c[m]
have been met, then the goal Y
will be called". Because the right hand side is a product, the arguments are commutative and associative, so that the rule makes no demands as to in what order the sources are called, or the conditions are evaluated.
The resulting graph is a directed hypergraph of the B-graph class, with each rule constituting a B-arc.
We assume that the graph has been rewritten so that all edges sourcing the same continuation have exclusive conditions, so that the continuation's next goal is uniquely decidable.
The task is now to manifest the relational callgraph as a CFG (control flow graph) that satisfies all rules.
To achieve this, we define algebraic join (&
) and meet (|
) operators over two continuations. The join of two continuations a & b
is their immediate common dominator. The meet of two continuations a | b
is their immediate common post-dominator. Both operations are commutative, associative and satisfy absorption and idempotent identities.
Since A | B <-> A, B
, each B-arc can be collapsed to a single directed edge if the meet over all its sources is satisfiable.
Initially, only rules with singular sources can be collapsed, which solves all linear dependencies and allows to satisfy dependent rules. We iteratively collapse all satisfiable meets until a fixpoint is reached.
If any B-arcs remain, then it is because no common post-dominator for their sources exists, which requires the user to insert meet rules.
In addition, we require all conditions of the graph to be exclusive, so that each continuation with multiple out-edges will only take one path during evaluation.