Compilers and Translators:
Software Verification Tools
Lecture 19: Binary Decision Diagrams
November 8, 2007
- Pointer analysis
- Binary decision diagrams
- Interprocedural analysis
2. Pointer Analysis
- In C, pointer-alias analysis is complicated because C allows
arbitrary computations on pointers.
- In Java, virtual methods can cause method invocations to be
- Flow-insensitive analysis ignores control flow. Its advantage is
that it reduces the size of the representation of the results and
it converges faster than a flow-sensitive analysis. Its disadvantage
is that the points-to information can overestimate what
variables can point to. See Example 12.22, p. 936.
- For a simple example of a flow-insensitive pointer-alias analysis
formulated in Datalog see Section 12.4.4, pp. 937-940.
3. Binary Decision Diagrams
- A binary decision diagram (BDD) represents a boolean function f
by a rooted directed acyclic graph (DAG).
- Each interior node is labeled by a variable of the function.
- At the bottom of the DAG are two leaves, one labeled 0 the other 1.
- Each interior node v has two edges to children, one labeled "low"
(corresponding to the case where v = 0) the other labeled "high"
(corresponding to the case where v = 1).
- Given a truth assignment for the variables in f, we can determine the
value of f for that truth assignment by starting at the root of the
BDD and following the edge from each interior node corresponding
to the value of the variable representing by that node until we
are at a leaf. If it is the 0 leaf, then f has the value 0 for
that truth assignment; if it is the 1 leaf, then f has the value 1.
- An ordered BDD is one in which there is a linear order on the
variables represented by the interior nodes. Whenever there is an
edge from a parent node v to a child labeled w,
then v comes before
w in that linear order.
4. Transformations on BDDs
- Two transformations can be used to reduce the size of a BDD:
We can obtain a canonical BDD for a boolean formula f by applying
these two transformations until they cannot be applied any more.
Note that the canonical BDD is dependent on the linear ordering given
to the variables.
Finding a linear ordering that minimizes the canonical BDD is an
NP-complete problem. Various heuristics have been developed that
find small canonical forms for many BDDs arising in practice.
Given two BDDs a and b for boolean functions f
we can construct a BDD for the logical OR of f and g
by combining the two BDDs a and b.
See Algorithm 12.29, p. 956, for details.
- If an interior node v has both its high and low edges go to the
same node w, then we may shortcircuit v by having the edges entering
v go directly to w.
- If two nodes v and w have low edges that go to the same node
and high edges that go to the same node y, then we may merge
v and w.
Edges entering v and w now enter the merged node.