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 Callgraph 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 callgraph (as precursor of a control flow graph) that satisfies all rules.

We recognize the callgraph as a transitive reduction of the hypergraph, which means all source edges of a rule are reducible to one (and only one) edge that, in the strict interpretation, is dominated by all sources reachable through existing callgraph edges.

Because the callgraph is initially incomplete, we must start from trivially reducible rules with single sources. This adds more edges to the callgraph, which allows us to reduce more complex rules, until a fixpoint is reached because no more rules can be reduced. See this example (conditions omitted for clarity):

(1) A.
(2) B :- A.
(3) B :- A, B, C.
(4) C :- A, B.
(5) D :- A, B.
// iteration 1: trivially reducible rules
(1) A.
(2) B :- A.
// iteration 2
(4) C :- B. // :- A
(5) D :- B. // :- A
// iteration 3
(3) B :- C. // :- B :- A

If a rule reduction leads to more than one possible callgraph edge, there exists an ambiguity in the program that the user must resolve by adding more edges.

If one or more rules remain undecidable after the fixpoint, the user should be warned as the rules would never be applied.

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