Skip to content

Instantly share code, notes, and snippets.

@paniq
Last active July 28, 2024 12:59
Show Gist options
  • Save paniq/859edcf05521aa6e4380c2bb2e95dacd to your computer and use it in GitHub Desktop.
Save paniq/859edcf05521aa6e4380c2bb2e95dacd to your computer and use it in GitHub Desktop.
Relation-Rule Based Callgraph Inference

Relation-Rule Based CFG Inference

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment