Abstract
Shape analysis concerns the problem of determining “shape invariants” for programs that perform destructive updating on dynamically allocated storage. This paper presents a new algorithm that takes as input an abstract value (a 3-valued logical structure describing some set of concrete stores X) and a precondition p, and computes the most-precise abstract value for the stores in X that satisfy p. This algorithm solves several open problems in shape analysis: (i) computing the most-precise abstract value of a set of concrete stores specified by a logical formula; (ii) computing best transformers for atomic program statements and conditions; (iii) computing best transformers for loop-free code fragments (i.e., blocks of atomic program statements and conditions); (iv) performing interprocedural shape analysis using procedure specifications and assume-guarantee reasoning; and (v) computing the most-precise overapproximation of the meet of two abstract values.
The algorithm employs a decision procedure for the logic used to express properties of data structures. A decidable logic for expressing such properties is described in [5]. The algorithm can also be used with an undecidable logic and a theorem prover; termination can be assured by using standard techniques (e.g., having the theorem prover return a safe answer if a time-out threshold is exceeded) at the cost of losing the ability to guarantee that a most-precise result is obtained. A prototype has been implemented in TVLA, using the SPASS theorem prover.
Supported by ONR contract N00014-01-1-0796.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 260–264. Springer, Heidelberg (2001)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Symp. on Princ. of Prog. Lang., pp. 269–282. ACM Press, New York (1979)
Henriksen, J.G., Jensen, J., Jørgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, Springer, Heidelberg (1995)
Immerman, N.: Descriptive Complexity. Springer, Heidelberg (1999)
Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., Yorsh, G.: Decidable logics for expressing heap connectivity (2003) (in preparation)
Jones, N.D., Muchnick, S.S.: Flow analysis and optimization of Lisp-like structures. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications. ch. 4, pp. 102–131. Prentice-Hall, Englewood Cliffs (1981)
Klarlund, N., Schwartzbach, M.: Graph types. In: Symp. on Princ. of Prog. Lang., January 1993, ACM Press, New York (1993)
Lev-Ami, T., Sagiv, M.: TVLA: A system for implementing static analyses. In: Static Analysis Symp., pp. 280–301 (2000)
Reps, T., Sagiv, M., Yorsh, G.: Symbolic implementation of the best transformer. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 252–266. Springer, Heidelberg (2004) (to appear)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: Symp. on Princ. of Prog. Lang., January 1999, pp. 105–118. ACM Press, New York (1999)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. Trans. on Prog. Lang. and Syst. (2002)
Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications. ch. 7, pp. 189–234. Prentice-Hall, Englewood Cliffs (1981)
Wang, E.Y.-B.: Analysis of Recursive Types in an Imperative Language. PhD thesis, Univ. of Calif., Berkeley, CA (1994)
Weidenbach, C.: SPASS: An automated theorem prover for first-order logic with equality, Available at http://spass.mpi-sb.mpg.de/index.html
Yorsh, G.: Logical characterizations of heap abstractions. Master’s thesis, Tel-Aviv University, Tel-Aviv, Israel (2003), Available at http://www.math.tau.ac.il/~gretay
Yorsh, G., Reps, T., Sagiv, M.: Symbolically computing most-precise abstract operations for shape analysis. Technical report, TAU (2003), Available at http://www.cs.tau.ac.il/~gretay
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
Yorsh, G., Reps, T., Sagiv, M. (2004). Symbolically Computing Most-Precise Abstract Operations for Shape Analysis. In: Jensen, K., Podelski, A. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2004. Lecture Notes in Computer Science, vol 2988. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24730-2_39
Download citation
DOI: https://doi.org/10.1007/978-3-540-24730-2_39
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21299-7
Online ISBN: 978-3-540-24730-2
eBook Packages: Springer Book Archive