Abstract
One of the continuing challenges in abstract interpretation is the creation of abstractions that yield analyses that are both tractable and precise enough to prove interesting properties about real-world programs. One source of difficulty is the need to handle programs with different behaviors along different execution paths. Disjunctive (powerset) abstractions capture such distinctions in a natural way. However, in general, powerset abstractions increase space and time costs by an exponential factor. Thus, powerset abstractions are generally perceived as very costly.
In this paper, we partially address this challenge by presenting and empirically evaluating a new heap abstraction. The new heap abstraction works by merging shape descriptors according to a partial isomorphism similarity criteria, resulting in a partially disjunctive abstraction.
We implemented this abstraction in TVLA – a generic system for implementing program analyses.We conducted an empirical evaluation of the new abstraction and compared it with the powerset heap abstraction. The experiments show that analyses based on the partially disjunctive heap abstraction are as precise as the ones based on the powerset heap abstraction. In terms of performance, analyses based on the partially disjunctive heap abstraction are often superior to analyses based on the powerset heap abstraction. The empirical results show considerable speedups, up to 2 orders of magnitude, enabling previously non-terminating analyses, such as verification of the Deutsch-Schorr-Waite scanning algorithm, to terminate with no negative effect on the overall precision. Indeed, experience indicates that the partially disjunctive shape abstraction improves performance across all TVLA analyses uniformly, and in many cases is essential for making precise shape analysis feasible.
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
Bagnara, R., Hill, P.M., Zaffanella, E.: Widening operators for powerset domains. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 135–148. Springer, Heidelberg (2004)
Chase, D., Wegman, M., Zadeck, F.: Analysis of pointers and structures. In: Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, pp. 296–310. ACM Press, New York (1990)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: Proc. ACM Symp. on Principles of Programming Languages, pp. 238–252. ACM Press, New York (1977)
Das, M., Lerner, S., Seigle, M.: Esp: Path-sensitive program verification in polynomial time. In: Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation (January 2002)
Deutsch, A.: Interprocedural alias analysis for pointers: Beyond k-limiting. In: Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, May 1994, pp. 230–241. ACM Press, New York (1994)
Giacobazzi, R., Ranzato, F.: Optimal domains for disjunctive abstract interpretation. Science of Computer Programming 32(1-3), 177–210 (1998)
Jones, N., Muchnick, S.: Flow analysis and optimization of Lisp-like structures. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Applications, ch. 4, pp. 102–131. Prentice-Hall, Englewood Cliffs (1981)
Larus, J.: Restructuring Symbolic Programs for Concurrent Execution on Multiprocessors. PhD thesis, Univ. of Calif., Berkeley, CA (May 1989)
Larus, J., Hilfinger, P.: Detecting conflicts between structure accesses. In: Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, pp. 21–34. ACM Press, New York (1988)
Lev-Ami, T., Sagiv, M.: TVLA: A framework for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 280–301. Springer, Heidelberg (2000), Available from http://www.cs.tau.ac.il/~tvla/
Lindstrom, G.: Scanning list structures without stacks or tag bits. Inf. Process. Lett. 2(2), 47–51 (1973)
Ramalingam, G., Warshavsky, A., Field, J., Goyal, D., Sagiv, M.: Deriving specialized program analyses for certifying component-client conformance. In: Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, June 2002, pp. 83–94. ACM Press, New York (2002)
Reps, T., Sagiv, M., Wilhelm, R.: 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 (2001), http://research.microsoft.com/specncheck/
Sagiv, M., Reps, T., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM Trans. Prog. Lang. Syst. 20(1), 1–50 (1998)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems 24(3), 217–298 (2002)
Stransky, J.: A lattice for abstract interpretation of dynamic (lisp-like) structures. Information and Computation 101(1), 70–102 (1992)
Yavuz-Kahveci, T., Bultan, T.: Automated verification of concurrent linked lists with counters. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 69–84. Springer, Heidelberg (2002)
Vallée-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E., Co, P.: Soot - a java optimization framework. In: Proceedings of CASCON 1999, pp. 125–135 (1999)
Yahav, E., Ramalingam, G.: Verifying safety properties using separation and heterogeneous abstraction. In: Proc. ACM SIGPLAN Conf. on Programming Language Design and Implementation, ACM Press, New York (2004) (to Appear)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Manevich, R., Sagiv, M., Ramalingam, G., Field, J. (2004). Partially Disjunctive Heap Abstraction. In: Giacobazzi, R. (eds) Static Analysis. SAS 2004. Lecture Notes in Computer Science, vol 3148. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27864-1_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-27864-1_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22791-5
Online ISBN: 978-3-540-27864-1
eBook Packages: Springer Book Archive