Abstract
We present a framework for interprocedural shape analysis, which is context- and flow-sensitive with the ability to perform destructive pointer updates. We limit our attention to cutpoint-free programs—programs in which reasoning on a procedure call only requires consideration of context reachable from the actual parameters. For such programs, we show that our framework is able to perform an efficient modular analysis. Technically, our analysis computes procedure summaries as transformers from inputs to outputs while ignoring parts of the heap not relevant to the procedure. This makes the analysis modular in the heap and thus allows reusing the effect of a procedure at different call-sites and even between different contexts occurring at the same call-site. We have implemented a prototype of our framework and used it to verify interesting properties of cutpoint-free programs, including partial correctness of a recursive quicksort implementation.
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.
References
Almeida, P.S.: Balloon types: Controlling sharing of state in data types. In: European Conference on Object-Oriented Programming, ESOP (1997)
Ball, T., Rajamani, S.K.: Bebop: A path-sensitive interprocedural dataflow engine. In: Workshop on Program Analysis for Software Tools and Engineering, PASTE (2001)
Banerjee, A., Naumann, D.A.: Representation independence, confinement, and access control. In: Symp. on Princ. of Prog. Lang. POPL (2002)
Bokowski, B., Vitek, J.: Confined types. In: Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA (1999)
Boyapati, C., Liskov, B., Shrira, L.: Ownership types for object encapsulation. In: Symp. on Princ. of Prog. Lang. POPL (2003)
Chase, D.R., Wegman, M., Zadeck, F.: Analysis of pointers and structures. In: Conf. on Prog. Lang. Design and Impl. PLDI (1990)
Chong, S., Rugina, R.: Static analysis of accessed regions in recursive data structures. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, p. 1075. Springer, Heidelberg (2003)
Clarke, D., Noble, J., Potter, J.: Simple ownership types for object containment. In: European Conference on Object-Oriented Programming, ESOP (2001)
Clarke, D.G., Potter, J.M., Noble, J.: Ownership types for flexible alias protection. In: Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA (1998)
Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: Neuhold, E.J. (ed.) Formal Descriptions of Programming Concepts, IFIP WG 2.2, St. Andrews, Canada, August 1977, pp. 237–277. North-Holland, Amsterdam (1978)
Das, M., Lerner, S., Seigle, M.: ESP: path-sensitive program verification in polynomial time. In: Conf. on Prog. Lang. Design and Impl., PLDI (2002)
Deutsch, A.: Interprocedural may-alias analysis for pointers: Beyond k-limiting. In: Conf. on Prog. Lang. Design and Impl., PLDI (1994)
Dor, N., Rodeh, M., Sagiv, M.: Checking cleanness in linked lists. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 115–135. Springer, Heidelberg (2000)
Grothoff, C., Palsberg, J., Vitek, J.: Encapsulating objects with confined types. In: Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA (2001)
Hackett, B., Rugina, R.: Region-based shape analysis with tracked locations. In: Symp. on Princ. of Prog. Lang, POPL (2005)
Hoare, C.A.R.: Algorithm 64: Quicksort. Comm. of the ACM (CACM) 4(7), 321 (1961)
Hogg, J.: Islands: Aliasing protection in object-oriented languages. In: Conference on Object-Oriented Programming Systems, Languages, and Applications, OOPSLA (1991)
Ishtiaq, S.S., O’Hearn, P.W.: BI as an assertion language for mutable data structures. In: Symp. on Princ. of Prog. Lang, POPL (2001)
Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A relational approach to interprocedural shape analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 246–264. Springer, Heidelberg (2004)
Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Pfahler, P., Kastens, U. (eds.) CC 1992. LNCS, vol. 641, pp. 125–140. Springer, Heidelberg (1992)
Leino, K.R.M., Poetzsch-Heffter, A., Zhou, Y.: Using data groups to specify and check side effects. In: Conf. on Prog. Lang. Design and Impl, PLDI (2002)
Lev-Ami, T., Reps, T., Sagiv, M., Wilhelm, R.: Putting static analysis to work for verification: A case study. In: Int. Symp. on Software Testing and Analysis, ISSTA (2000)
Lev-Ami, T., Sagiv, M.: TVLA: A framework for Kleene based static analysis. In: Palsberg, J. (ed.) SAS, LNCS, vol. 1824, pp. 280–302. Springer, Heidelberg (2000), Available at, http://www.math.tau.ac.il/~tvla
Manevich, R., Sagiv, M., Ramalingam, G., Field, J.: Partially disjunctive heap abstraction. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 265–279. Springer, Heidelberg (2004)
Müller, P., Poetzsch-Heffter, A.: Universes: A type system for alias and dependency control. Technical Report 279, Fernuniversität Hagen (2001)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999)
Noble, J., Biddle, R., Tempero, E., Potanin, A., Clarke, D.: Towards a model of encapsulation. In: The First International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming, IWACO (2003)
Noble, J., Vitek, J., Potter, J.: Flexible alias protection. In: European Conference on Object-Oriented Programming, ESOP (1998)
Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Symp. on Princ. of Prog. Lang, POPL (1995)
Reps, T., Sagiv, M., Loginov, A.: Finite differencing of logical formulas for static analysis. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 380–398. Springer, Heidelberg (2003)
Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Symp. on Logic in Computer Science, LICS (2002)
Rinetzky, N., Bauer, J., Reps, T., Sagiv, M., Wilhelm, R.: A semantics for procedure local heaps and its abstractions. Tech. Rep. 1, AVACS, (September 2004), Available at, http://www.avacs.org
Rinetzky, N., Bauer, J., Reps, T., Sagiv, M., Wilhelm, R.: A semantics for procedure local heaps and its abstractions. In: Symp. on Princ. of Prog. Lang., POPL (2005)
Rinetzky, N., Sagiv, M.: Interprocedural shape analysis for recursive programs. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol. 2027, p. 133. Springer, Heidelberg (2001)
Rinetzky, N., Sagiv, M., Yahav, E.: Interprocedural shape analysis for cutpoint-free programs. Tech. Rep. 104/05, Tel Aviv Uni. (April 2005), Available at, http://www.math.tau.ac.il/~maon
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. Trans. on Prog. Lang. and Syst (TOPLAS) 24(3), 217–298 (2002)
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. 264–289. Springer, Heidelberg (2003)
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)
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
Rinetzky, N., Sagiv, M., Yahav, E. (2005). Interprocedural Shape Analysis for Cutpoint-Free Programs. In: Hankin, C., Siveroni, I. (eds) Static Analysis. SAS 2005. Lecture Notes in Computer Science, vol 3672. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11547662_20
Download citation
DOI: https://doi.org/10.1007/11547662_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28584-7
Online ISBN: 978-3-540-31971-9
eBook Packages: Computer ScienceComputer Science (R0)