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 event graph is described with unpredicated rules relating events, 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 events X[1]..X[n] have happened, and all conditions c[1]..c[m] have been met, then the goal Y will happen". 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.

The task is now to manifest the relational event graph as a CFG (control flow graph) that satisfies all rules.

To achieve this, we define algebraic join and meet operators future and past over two events. The soonest shared future of two events future(a, b) is their immediate common post-dominator, and constitutes the join operation (or supremum). The latest common past of two events past(a, b) is their immediate common dominator, and forms the meet operation (or infimum). For the rule B :- A., future(A,B) == B and past(A,B) == A. Both operations are commutative, associative and satisfy absorption and idempotent identities.

Since A, B <-> future(A, B), each B-arc can be collapsed to a single directed edge if the future 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 futures until a fixpoint is reached.

Within the iterations, graph rules must be rewritten so all edges sourcing the same event have exclusive conditions, and therefore the event's next goal is linearly decidable.

If any B-arcs remain, then it is because no common post-dominator for their sources exists, which requires the user to insert a rule for every source with the same goal.

A rule may have a data dependency on a source X[i] that does not dominate the future G (i.e. function call pattern). If X[i] is an immediate predecessor of G = future(X[1],...,X[n]), then a phi node can be used. However, if the edge distance between X[i] and G is greater than one, then X[i]'s data d must be implicitly forwarded as an option type, and the rule must add a "is option d set" condition.

If this implicit solution is undesired (for the sake of intuitive reasoning, or simplification of the compiler), then an additional constraint can be imposed which requires any source X[i] to be a dominator of G (that is, past(X[i],G) == X[i]).

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