Compactly Representing First-Order Structures for Static Analysis
A fundamental bottleneck in applying sophisticated static analyses to large programs is the space consumed by abstract program states. This is particularly true when analyzing programs that make extensive use of heap-allocated data. The TVLA Three-Valued Logic Analysis) program analysis and verification system models dynamic allocation precisely by representing program states as first-order structures. In such a representation, a finite collection of predicates is used to define states; the predicates range over a universe of individuals that may evolve—expand and contract—during analysis. Evolving first-order structures can be used to encode a wide variety of analyses, including most analyses whose abstract states are represented by directed graphs or maps. This paper addresses the problem of space consumption in such analyses by describing and evaluating two novel structure representation techniques. One technique uses ordered binary decision diagrams (OB-DDs); the other uses a variant of a functional map data structure. 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. In addition to TVLA, we believe that our results are applicable to many program analysis systems that represent states as graphs, maps, or other structures of similar complexity.
KeywordsBoolean Variable Abstract Interpretation Binary Decision Diagram Mutable Structure Program Point
Unable to display preview. Download preview PDF.
- 1.A. Appel and M. Ginsburg. Modern Compiler Implementation in C. Cambridge University Press, New York, Cambridge, 1998.Google Scholar
- 2.R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. A CM Computing Surveys, 24(3):293–318, Sept. 1992.Google Scholar
- 4.N. Dor, M. Rodeh, and M. Sagiv. Checking cleanness in linked lists. In Proc. Static Analysis Symp., pages 115–134, July 2000.Google Scholar
- 5.N. Klarlund, A. Moller, and M. I. Schwartzbach. MONA implementation secrets. In CIAA, pages 182–194, 2000.Google Scholar
- 8.L. Mauborgne. Abstract interpretation using typed decision graphs. Science of Computer Programming, 31(1):91–112, May 1998.Google Scholar
- 9.Microsoft Research. The SLAM project. http://research.microsoft.com/slam/, 2001.
- 10.F. Nielson, H. Nielson, and M. Sagiv. A Kleene analysis of mobile ambients. In G. Smolka, editor, Proc. of ESOP 2000, volume 1782 of LNCS, pages 305–319. Springer, 2000.Google Scholar
- 11.G. Ramalingam, A. Warshavsky, J. Field, D. Goyal, and M. Sagiv. Deriving specialized program analyses for certifying component-client conformance. In Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, pages 83–94, Berlin, June 2002.Google Scholar
- 12.T. Reps, M. Sagiv, and R. Wilhelm. Automatic verification of a simple mark and sweep garbabge collector. Presented in the 2001 University of Washington and Microsoft Research Summer Institute, Specifying and Checking Properties of Software, http://research.microsoft.com/specncheck/, 2001.
- 13.M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. In Proc. ACM Symp. on Principles of Programming Languages, pages 105–118, 1999.Google Scholar
- 14.S. Sagiv, N. Francez, M. Rodeh, and R. Wilhelm. A logic-based approach to data flow analysis problems. Acta Inf., 35(6):457–504, June 1998.Google Scholar
- 15.F. Somenzi. Colorado University Decision Diagram Package (CUDD). Department of Electrical and Computer Engineering, University of Colorado at Boulder, 1998. http://vlsi.colorado.edu/~fabio/CUDD/.
- 16.H. Veith. How to encode a logical structure by an OBDD. In IEEE Conference on Computational Complexity, pages 122–131, 1998.Google Scholar
- 17.E. Yahav. Verifying safety properties of concurrent Java programs using 3-valued logic. In Proc. ACM Symp. on Principles of Programming Languages, pages 27–40, 2001.Google Scholar
- 18.B. Yang, R. E. Bryant, D. R. O’Hallaron, A. Biere, O. Coudert, G. Janssen, R. K. Ranjan, and F. Somenzi. A performance study of BDD-based model checking. In Proceedings of the Formal Methods on Computer-Aided Design, pages 255–289, November 1998.Google Scholar
- 19.T. Yavuz-Kahveci, M. Tuncer, and T. Bultan. Composite symbolic library. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of Lecture Notes in Computer Science, pages 335–344. Springer-Verlag, April 2001.CrossRefGoogle Scholar