[Javabdd-devel] bug in buddy library: reordering

[John W. <jw...@st...>]

I have tracked down a tricky bug involving garbage collection and variable
reordering.  When calling setvarorder(), some BDDs are not getting
reordered, leading to invalid BDDs because the levels are no longer
monotonically increasing.  This bug affects all BDD reordering (swapvar,
dynamic reordering, etc.)

This is a serious bug because it will cause the library to silently give
incorrect results to BDD operations.

The problem seems to be in the construction of the dependency imatrix.
mark_roots() is supposed to mark the externally-accessible BDD references
and mark which variables depend on each other in the imatrix.

mark_roots() calls addref_rec(), which is supposed to recurse down the BDD,
adding variable dependencies.  mark_roots() uses "REF(r) == 0" to test
whether or not it has already visited and therefore computed the
dependencies for a BDD node.

Herein lies the problem. If an internal BDD node has an external reference,
its refcount will not be zero, and mark_roots() will assume it has computed
the imatrix dependencies when it has not.

The whole mark_roots() process seems to assume that it can use the refcount
field as a marker for BDD nodes.  This is wrong and we should think about
the right way to do this. We may need to use an external table instead.

Coming up with a test case that exhibits the bug is nontrivial because the
BDDs must be allocated in a non-sequential order.  For this to happen, there
must have been a garbage collection in the past where nodes were reclaimed
and new nodes were given numbers before old nodes.  Thus, all of the test
cases that exhibit the bug are rather large.

-John