Abstract
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.
Chapter PDF
References
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
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)
Bravenboer, M., Smaragdakis, Y.: Strictly declarative specification of sophisticated points-to analyses. In: Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2009 (2009)
Chase, D.R., Wegman, M., Zadeck, F.K.: Analysis of pointers and structures. In: Prog. Lang. Design and Implementation, PLDI 1990 (1990)
Chatterjee, R., Ryder, B.G., Landi, W.: Relevant context inference. In: Principles of Prog. Languages, POPL 1999 (1999)
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)
Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: IFIP Conf. on Formal Description of Programming Concepts (1977)
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)
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)
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)
Halbwachs, N., Péron, M.: Discovering properties about arrays in simple programs. In: Prog. Lang. Design and Implementation, PLDI 2008. ACM, New York (2008)
Heintze, N., Tardieu, O.: Demand-driven pointer analysis. In: Prog. Lang. Design and Implementation, PLDI 2001 (2001)
Hind, M.: Pointer analysis: haven’t we solved this problem yet? In: Prog. Analysis For Software Tools and Engineering, PASTE 2001 (2001)
Jeannet, B.: The BDDAPRON logico-numerical abstract domains library, http://www.inrialpes.fr/pop-art/people/bjeannet/bjeannet-forge/bddapron/
Jeannet, B.: Relational interprocedural verification of concurrent programs. In: Software Engineering and Formal Methods, SEFM 2009. IEEE, Los Alamitos (2009)
Jeannet, B., Argoud, M., Lalire, G.: The Interproc interprocedural analyzer, http://pop-art.inrialpes.fr/interproc/interprocweb.cgi
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)
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/
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)
Knoop, J., Steffen, B.: The interprocedural coincidence theorem. In: Pfahler, P., Kastens, U. (eds.) CC 1992. LNCS, vol. 641, Springer, Heidelberg (1992)
Landi, W., Ryder, B.G.: A safe approximate algorithm for interprocedural pointer aliasing. In: PLDI (1992)
Midtgaard, J.: Control-flow analysis of functional programs. ACM Computing Surveys (2011); preliminary version available as BRICS technical report RS-07-18
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)
Polyspace, http://www.mathworks.com/products/polyspace/
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)
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)
Somenzi, F.:Cudd: Colorado University Decision Diagram Package, ftp://vlsi.colorado.edu/pub
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/
Steensgaard, B.: Points-to Analysis in Almost Linear Time. In: Principles of Prog. Languages, POPL 1996 (1996)
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)
Wilson, R.P., Lam, M.S.: Efficient context-sensitive pointer analysis for c programs. In: Prog. Lang. Design and Implementation, PLDI 1995 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sotin, P., Jeannet, B. (2011). Precise Interprocedural Analysis in the Presence of Pointers to the Stack. In: Barthe, G. (eds) Programming Languages and Systems. ESOP 2011. Lecture Notes in Computer Science, vol 6602. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19718-5_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-19718-5_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19717-8
Online ISBN: 978-3-642-19718-5
eBook Packages: Computer ScienceComputer Science (R0)