A fundamental bottleneck in applying sophisticated static analyses to
large programs is space. This is particularly true for modern programs
where interesting and relevant information is increasingly found in the
heap (i.e., in dynamically allocated data structures), instead of being
stored in a fixed set of variables. An abstraction of the potentially unbounded
heap that is precise enough for an intended application may often have
prohibitive space requirements.
The TVLA (Three-Valued Logic Analysis) program analysis and verification
system is designed to model dynamic allocation precisely by representing
program states as first-order structures.
A first-order representation uses a finite collection of predicates
to define states; the predicates range over a universe of individuals
that may evolve---expand and contract---during analysis. While TVLA has
been used to verify a variety of nontrivial properties of programs that
perform dynamic allocation, the space required by the current version
of TVLA for analysis of programs exceeding more than a few thousand
lines is often prohibitive. This paper addresses the problem of space
consumption in first-order state representations by describing and
evaluating two new structure representation techniques. One technique
uses ordered binary decision diagrams (OBDDs); the other uses a
variant of a functional map data structure.
While both of these core data structures are well-known, there have
been only a few prior efforts at applying such data structures in the
context of static analysis.
In particular, we are not aware of any prior work on encoding evolving
first-order structures using these data structures.
Using a suite of benchmark analysis problems,
we systematically compare the new representations with TVLA's existing
state representation. The results show that both the OBDD and
functional implementations reduce space consumption in TVLA by a
factor of 4 to 10 relative to the current TVLA state representation,
without compromising analysis time. We believe that our techniques
should also be applicable to other program analysis
systems that represent program states as maps or directed graphs.