×

zbMATH — the first resource for mathematics

Precise interprocedural analysis in the presence of pointers to the stack. (English) Zbl 1326.68107
Barthe, Gilles (ed.), Programming languages and systems. 20th European symposium on programming, ESOP 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19717-8/pbk). Lecture Notes in Computer Science 6602, 459-479 (2011).
Summary: In a language with procedures calls and pointers as parameters, an instruction can modify memory locations anywhere in the call-stack. The presence of such side effects breaks most generic interprocedural analysis methods, which assume that only the top of the stack may be modified. We present a method that addresses this issue, based on the definition of an equivalent local semantics in which writing through pointers has a local effect on the stack. Our second contribution in this context is an adequate representation of summary functions that models the effect of a procedure, not only on the values of its scalar and pointer variables, but also on the values contained in pointed memory locations. Our implementation in the interprocedural analyser PInterproc results in a verification tool that infers relational properties on the value of Boolean, numerical and pointer variables.
For the entire collection see [Zbl 1213.68027].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N15 Theory of programming languages
Software:
Apron; CUDD
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Andersen, L.: Program Analysis and Specialization for the C Programming Language. Ph.D. thesis (1994), http://ftp.diku.dk/pub/diku/semantics/papers/D-203.dvi.Z
[2] Bourdoncle, F.: Interprocedural Abstract Interpretation of Block Structured Languages with Nested Procedures, Aliasing and Recursivity. In: Deransart, P., Małuszyński, J. (eds.) PLILP 1990. LNCS, vol. 456, Springer, Heidelberg (1990) · doi:10.1007/BFb0024192
[3] Bravenboer, M., Smaragdakis, Y.: Strictly declarative specification of sophisticated points-to analyses. In: Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2009 (2009) · doi:10.1145/1640089.1640108
[4] Chase, D.R., Wegman, M., Zadeck, F.K.: Analysis of pointers and structures. In: Prog. Lang. Design and Implementation, PLDI 1990 (1990) · doi:10.1145/93542.93585
[5] Chatterjee, R., Ryder, B.G., Landi, W.: Relevant context inference. In: Principles of Prog. Languages, POPL 1999 (1999) · doi:10.1145/292540.292554
[6] Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Prog. Languages, POPL 1977 (1977) · Zbl 1149.68389 · doi:10.1145/512950.512973
[7] Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: IFIP Conf. on Formal Description of Programming Concepts (1977) · Zbl 0393.68080
[8] Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Rival, X.: Why does astrée scale up? Formal Methods in System Design 35(3) (2009) · Zbl 1185.68241 · doi:10.1007/s10703-009-0089-6
[9] Delmas, D., Goubault, E., Putot, S., Souyris, J., Tekkal, K., Védrine, F.: Towards an industrial use of fluctuat on safety-critical avionics softwar. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 53–69. Springer, Heidelberg (2009) · Zbl 05625581 · doi:10.1007/978-3-642-04570-7_6
[10] Filliâtre, J.C., Marché, C.: Multi-prover verification of C programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 15–29. Springer, Heidelberg (2004) · doi:10.1007/978-3-540-30482-1_10
[11] Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. In: Prog. Lang. Design and Implementation, PLDI 2008. ACM, New York (2008)
[12] Heintze, N., Tardieu, O.: Demand-driven pointer analysis. In: Prog. Lang. Design and Implementation, PLDI 2001 (2001) · doi:10.1145/378795.378802
[13] Hind, M.: Pointer analysis: haven’t we solved this problem yet? In: Prog. Analysis For Software Tools and Engineering, PASTE 2001 (2001) · doi:10.1145/379605.379665
[14] Jeannet, B.: The BDDAPRON logico-numerical abstract domains library, http://www.inrialpes.fr/pop-art/people/bjeannet/bjeannet-forge/bddapron/
[15] Jeannet, B.: Relational interprocedural verification of concurrent programs. In: Software Engineering and Formal Methods, SEFM 2009. IEEE, Los Alamitos (2009)
[16] Jeannet, B., Argoud, M., Lalire, G.: The Interproc interprocedural analyzer, http://pop-art.inrialpes.fr/interproc/interprocweb.cgi
[17] Jeannet, B., Loginov, A., Reps, T., Sagiv, M.: A relational approach to interprocedural shape analysis. ACM Trans. On Programming Languages and Systems (TOPLAS) 32(2) (2010) · Zbl 1104.68416 · doi:10.1145/1667048.1667050
[18] Jeannet, B., Miné, A.: APRON: A library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009), http://apron.cri.ensmp.fr/library/ · Zbl 05571933 · doi:10.1007/978-3-642-02658-4_52
[19] Jeannet, B., Serwe, W.: Abstracting call-stacks for interprocedural verification of imperative programs. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 258–273. Springer, Heidelberg (2004) · Zbl 1108.68392 · doi:10.1007/978-3-540-27815-3_22
[20] Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Pfahler, P., Kastens, U. (eds.) CC 1992. LNCS, vol. 641, Springer, Heidelberg (1992) · doi:10.1007/3-540-55984-1_13
[21] Landi, W., Ryder, B.G.: A safe approximate algorithm for interprocedural pointer aliasing. In: PLDI (1992)
[22] Midtgaard, J.: Control-flow analysis of functional programs. ACM Computing Surveys (2011); preliminary version available as BRICS technical report RS-07-18
[23] Miné, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Languages, Compilers and Tools for Embedded Systems, LCTES 2006 (2006) · doi:10.1145/1134650.1134659
[24] Polyspace, http://www.mathworks.com/products/polyspace/
[25] 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
[26] Sharir, M., Pnueli, A.: Semantic foundations of program analysis. In: Muchnick, S., Jones, N. (eds.) Program Flow Analysis: Theory and Applications, ch. 7. Prentice-Hall, Englewood Cliffs (1981)
[27] Somenzi, F.:Cudd: Colorado University Decision Diagram Package, ftp://vlsi.colorado.edu/pub
[28] Sotin, P., Jeannet, B.: Precise interprocedural analysis in the presence of pointers to the stack (January 2011), http://hal.archives-ouvertes.fr/inria-00547888/fr/ · Zbl 1326.68107
[29] Steensgaard, B.: Points-to Analysis in Almost Linear Time. In: Principles of Prog. Languages, POPL 1996 (1996) · doi:10.1145/237721.237727
[30] Whaley, J., Lam, M.S.: Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In: Prog. Lang. Design and Implementation, PLDI 2004 (2004) · doi:10.1145/996841.996859
[31] Wilson, R.P., Lam, M.S.: Efficient context-sensitive pointer analysis for c programs. In: Prog. Lang. Design and Implementation, PLDI 1995 (1995) · doi:10.1145/207110.207111
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.