Abstract
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.
Partially supported by the Israeli Academy of Science. Part of this work was done while visiting IBM’s T.J. Watson Research Center.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
A. Appel and M. Ginsburg. Modern Compiler Implementation in C. Cambridge University Press, New York, Cambridge, 1998.
R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. A CM Computing Surveys, 24(3):293–318, Sept. 1992.
L. Cardelli and A. Gordon. Mobile ambients. In M. Nivat, editor, Proc. of Foundations of Software Science and Computation Structures (FoSSaCS), volume 1378 of LNCS, pages 140–155. Springer-Verlag, Mar. 1998.
N. Dor, M. Rodeh, and M. Sagiv. Checking cleanness in linked lists. In Proc. Static Analysis Symp., pages 115–134, July 2000.
N. Klarlund, A. Moller, and M. I. Schwartzbach. MONA implementation secrets. In CIAA, pages 182–194, 2000.
T. Lev-Ami and M. Sagiv. TVLA: A framework for Kleene based static analysis. In J. Palsberg, editor, Proc. Static Analysis Symp., volume 1824 of Lecture Notes in Computer Science, pages 280–301. Springer-Verlag, 2000. http://www.cs.tau.ac.i1/~rumster/TVLA/.
F. Martin. PAG-an efficient program analyzer generator. International Journal on Software Tools for Technology Transfer, 2(1):46–67, 1998.
L. Mauborgne. Abstract interpretation using typed decision graphs. Science of Computer Programming, 31(1):91–112, May 1998.
Microsoft Research. The SLAM project. http://research.microsoft.com/slam/, 2001.
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.
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.
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.
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.
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.
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/.
H. Veith. How to encode a logical structure by an OBDD. In IEEE Conference on Computational Complexity, pages 122–131, 1998.
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.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Manevich, R., Ramalingam, G., Field, J., Goyal, D., Sagiv, M. (2002). Compactly Representing First-Order Structures for Static Analysis. In: Hermenegildo, M.V., Puebla, G. (eds) Static Analysis. SAS 2002. Lecture Notes in Computer Science, vol 2477. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45789-5_16
Download citation
DOI: https://doi.org/10.1007/3-540-45789-5_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44235-6
Online ISBN: 978-3-540-45789-3
eBook Packages: Springer Book Archive