Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
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.