×

Interprocedural shape analysis for effectively cutpoint-free programs. (English) Zbl 1383.68025

Voronkov, Andrei (ed.) et al., Programming logics. Essays in memory of Harald Ganzinger. Berlin: Springer (ISBN 978-3-642-37650-4/pbk). Lecture Notes in Computer Science 7797, 414-445 (2013).
Summary: We present a framework for local interprocedural shape analysis that computes procedure summaries as transformers of procedure-local heaps (the parts of the heap that the procedure may reach). A main challenge in procedure-local shape analysis is the handling of cutpoints, objects that separate the input heap of an invoked procedure from the rest of the heap, which – from the viewpoint of that invocation – is non-accessible and immutable.
In this paper, we limit our attention to effectively cutpoint-free programs – programs in which the only objects that separate the callee’s heap from the rest of the heap, when considering live reference fields, are the ones pointed to by the actual parameters of the invocation. This limitation (and certain variations of it, which we also describe) simplifies the local-reasoning about procedure calls because the analysis needs not track cutpoints. Furthermore, our analysis (conservatively) verifies that a program is effectively cutpoint-free
For the entire collection see [Zbl 1259.03008].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
68Q55 Semantics in the theory of computing
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Arnold, G., Manevich, R., Sagiv, M., Shaham, R.: Combining Shape Analyses by Intersecting Abstractions. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 33–48. Springer, Heidelberg (2006) · Zbl 1176.68111 · doi:10.1007/11609773_3
[2] Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Symp. on Princ. of Prog. Lang. (POPL), pp. 289–300. ACM (2009) · Zbl 1315.68085 · doi:10.1145/1594834.1480917
[3] Chase, D.R., Wegman, M., Zadeck, F.: Analysis of pointers and structures. In: Conf. on Prog. Lang. Design and Impl., PLDI (1990) · doi:10.1145/93542.93585
[4] Chong, S., Rugina, R.: Static analysis of accessed regions in recursive data structures. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 463–482. Springer, Heidelberg (2003) · Zbl 1067.68556 · doi:10.1007/3-540-44898-5_26
[5] 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. (POPL), pp. 238–252. ACM Press, New York (1977)
[6] 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), pp. 237–277. North-Holland (August 1977) · Zbl 0393.68080
[7] Deutsch, A.: Interprocedural alias analysis for pointers: Beyond k-limiting. In: Conf. on Prog. Lang. Design and Impl. (PLDI) (1994)
[8] Gotsman, A., Berdine, J., Cook, B.: Interprocedural Shape Analysis with Separated Heap Abstractions. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 240–260. Springer, Heidelberg (2006) · Zbl 1225.68072 · doi:10.1007/11823230_16
[9] Hackett, B., Rugina, R.: Region-based shape analysis with tracked locations. In: Symp. on Princ. of Prog. Lang. (POPL) (2005) · Zbl 1369.68140 · doi:10.1145/1040305.1040331
[10] 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) · Zbl 1323.68077 · doi:10.1145/360204.375719
[11] 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) · Zbl 1104.68416 · doi:10.1007/978-3-540-27864-1_19
[12] Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Int. Conf. on Comp. Construct. (CC) (1992) · doi:10.1007/3-540-55984-1_13
[13] Lev-Ami, T., Sagiv, M.: . TVLA: A framework for Kleene based static analysis. In: International Static Analysis Symposium (SAS) (2000), http://www.math.tau.ac.il/ tvla · Zbl 0966.68580
[14] Marron, M., Hermenegildo, M., Kapur, D., Stefanovic, D.: Efficient context-sensitive shape analysis with graph based heap models. In: Int. Conf. on Comp. Construct. (CC), pp. 245–259 (2008) · Zbl 05263844 · doi:10.1007/978-3-540-78791-4_17
[15] 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)
[16] Plotkin, G.D.: A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, University of Aarhus (1981)
[17] Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: Symp. on Princ. of Prog. Lang. (POPL) (1995) · Zbl 0874.68133 · doi:10.1145/199448.199462
[18] Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: Symp. on Logic in Computer Science (LICS) (2002) · doi:10.1109/LICS.2002.1029817
[19] Rinetzky, N.: Interprocedural and Modular Local Heap Shape Analysis. PhD thesis, Tel Aviv University (June 2008)
[20] 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) · Zbl 1369.68154 · doi:10.1145/1040305.1040330
[21] Rinetzky, N., Poetzsch-Heffter, A., Ramalingam, G., Sagiv, M., Yahav, E.: Modular Shape Analysis for Dynamically Encapsulated Programs. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 220–236. Springer, Heidelberg (2007) · Zbl 05187158 · doi:10.1007/978-3-540-71316-6_16
[22] Rinetzky, N., Sagiv, M.: Interprocedural shape analysis for recursive programs. In: Int. Conf. on Comp. Construct. (CC) (2001) · Zbl 0977.68688 · doi:10.1007/3-540-45306-7_10
[23] Rinetzky, N., Sagiv, M., Yahav, E.: Interprocedural Shape Analysis for Cutpoint-Free Programs. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 284–302. Springer, Heidelberg (2005) · Zbl 1141.68375 · doi:10.1007/11547662_20
[24] Rubinstein, S.: On the utility of cutpoints for monitoring program execution. Master’s thesis, Tel Aviv University, Tel Aviv, Israel (2006)
[25] 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) · Zbl 05459332 · doi:10.1145/514188.514190
[26] 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) · Zbl 1067.68550 · doi:10.1007/3-540-44898-5_27
[27] 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, NJ (1981)
[28] Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W.: Scalable Shape Analysis for Systems Code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 385–398. Springer, Heidelberg (2008) · Zbl 1155.68359 · doi:10.1007/978-3-540-70545-1_36
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.