Abstract
We consider the problem of computing the intersection (meet) of heap abstractions. This problem is useful, among other applications, to relate abstract memory states computed by forward analysis with abstract memory states computed by backward analysis. Since dynamically allocated heap objects have no static names, relating objects computed by different analyses cannot be done directly. We show that the problem of computing meet is computationally hard. We describe a constructive formulation of meet based on certain relations between abstract heap objects. The problem of enumerating those relations is reduced to finding constrained matchings in graphs. We implemented the algorithm in the TVLA system and used it to prove temporal heap properties of several small Java programs, and obtained empirical evidence showing the effectiveness of the meet algorithm.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Arnold, G., Manevich, R., Sagiv, M., Shaham, R.: Intersecting heap abstractions with applications to compile-time memory management. Technical Report TR-2005-04-135520, Tel Aviv University (April 2005), Available at, http://www.cs.tau.ac.il/rumster/TR-2005-04-135520.pdf
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximation of fixed points. In: Symp. on Princ. of Prog. Lang., pp. 238–252. ACM Press, New York (1977)
Jeannet, B., Alexey, L., Reps, T., Sagiv., M.: A relational approach to interprocedural shape analysis. In: Proc. Static Analysis Symp. Springer, Heidelberg (2004)
Kuncak, V., Rinard, M.: Boolean algebra of shape analysis constraints. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 59–72. Springer, Heidelberg (2004)
Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Proc. Static Analysis Symp, pp. 280–301 (2000)
Manna, Z., Pnueli, A.: A hierarchy of temporal properties (invited paper). In: Proceedings of the ninth annual ACM symposium on Principles of distributed computing, pp. 377–410 (1989)
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)
Shaham, R., Kolodner, E.K., Sagiv, M.: Heap profiling for space-efficient Java. In: SIGPLAN Conf. on Prog. Lang. Design and Impl., June 2001, pp. 104–113. ACM Press, New York (2001)
Shaham, R., Yahav, E., Kolodner, E.K., Sagiv, M.: Establishing local temporal heap safety properties with applications to compile-time memory management. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 483–503. Springer, Heidelberg (2003)
Yorsh, G.: Logical characterizations of heap abstractions. Master’s thesis, Tel-Aviv University, Tel-Aviv, Israel (2003), http://www.cs.tau.ac.il/~gretay/
Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 530–545. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Arnold, G., Manevich, R., Sagiv, M., Shaham, R. (2005). Combining Shape Analyses by Intersecting Abstractions. In: Emerson, E.A., Namjoshi, K.S. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2006. Lecture Notes in Computer Science, vol 3855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11609773_3
Download citation
DOI: https://doi.org/10.1007/11609773_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31139-3
Online ISBN: 978-3-540-31622-0
eBook Packages: Computer ScienceComputer Science (R0)