skip to main content
research-article
Open access

A relational approach to interprocedural shape analysis

Published: 08 February 2010 Publication History

Abstract

This article addresses the verification of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued fields, that is, interprocedural shape analysis. The article makes three contributions.
— It introduces a new method for abstracting relations over memory configurations for use in abstract interpretation.
— It shows how this method furnishes the elements needed for a compositional approach to shape analysis. In particular, abstracted relations are used to represent the shape transformation performed by a sequence of operations, and an overapproximation to relational composition can be performed using the meet operation of the domain of abstracted relations.
— It applies these ideas in a new algorithm for context-sensitive interprocedural shape analysis. The algorithm creates procedure summaries using abstracted relations over memory configurations, and the meet-based composition operation provides a way to apply the summary transformer for a procedure P at each call site from which P is called.
The algorithm has been applied successfully to establish properties of both (i) recursive programs that manipulate lists and (ii) recursive programs that manipulate binary trees.

References

[1]
Arnold, G. 2006. Specialized 3-valued logic shape analysis using structure-based refinement and loose embedding. In Proceedings of the Static Analysis Symposium (SAS'06). Lecture Notes in Computer Science, vol. 4134, Springer.
[2]
Arnold, G., Manevich, R., Sagiv, M., and Shaham, R. 2006. Combining shape analyses by intersecting abstractions. In Proceedings of the International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'06). Lecture Notes in Computer Science, vol. 3855, Springer.
[3]
Ball, T. and Rajamani, S. 2001. Bebop: A path-sensitive interprocedural dataflow engine. Prog. Anal. Softw. Tools Engin, 97--103.
[4]
Berdine, J., Calcagno, C., and O'Hearn, P. W. 2005. Smallfoot: Modular automatic assertion checking with separation logic. In Proceedings of the Symposium on Formal Methods for Components and Objects (FMCO'05). Lecture Notes in Computer Science, vol. 4111, Springer, 115--137.
[5]
Bogudlov, I., Lev-Ami, T., Reps, T., and Sagiv, M. 2007a. Revamping TVLA: Making parametric shape analysis competitive. Tech. rep. TR-2007--01-01, Tel-Aviv University, Tel-Aviv, Israel.
[6]
Bogudlov, I., Lev-Ami, T., Reps, T., and Sagiv, M. 2007b. Revamping TVLA: Making parametric shape analysis competitive (tool paper). In Proceedings of the International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 4590, Springer.
[7]
Bouajjani, A., Esparza, J., and Maler, O. 1997. Reachability analysis of pushdown automata: Application to model checking. In Proceedings of the International Conference on Concurrency Theory (CONCUR'97). Lecture Notes in Computer Science, vol. 1243, Springer, 135--150.
[8]
Bouajjani, A., Esparza, J., and Touili, T. 2003. A generic approach to the static analysis of concurrent programs with procedures. In Principles of Programming Languange, ACM Press, New York, 62--73.
[9]
Clarke, Jr., E., Grumberg, O., and Peled, D. 1999. Model Checking. The MIT Press.
[10]
Cousot, P. and Cousot, R. 1977. Static determination of dynamic properties of recursive procedures. In Formal Descriptions of Programming Concepts, E. Neuhold, Ed. North-Holland, 237--277.
[11]
Cousot, P. and Halbwachs, N. 1978. Automatic discovery of linear constraints among variables of a program. In Principles of Programming Language, ACM Press, New York, 84--96.
[12]
Finkel, A., B. Willems, and Wolper, P. 1997. A direct symbolic approach to model checking pushdown systems. Electron. Notes Theor. Comput. Sci. 9.
[13]
Gopan, D., DiMaio, F., N.Dor, Reps, T., and Sagiv, M. 2004. Numeric domains with summarized dimensions. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2988, Springer, 512--529.
[14]
Gotsman, A., Berdine, J., and Cook, B. 2006. Interprocedural shape analysis with separated heap abstractions. In Proceedings of the Static Analysis Symposium (SAS'06). Lecture Notes in Computer Science, vol. 4134, Springer, 240--260.
[15]
Gries, D. 1981. The Science of Programming. Springer.
[16]
Jeannet, B., Loginov, A., Reps, T., and Sagiv, M. 2004. A relational approach to interprocedural shape analysis. In Proceedings of the Static Analysis Symposium (SAS'04). Lecture Notes in Computer Science, vol. 3148, Springer.
[17]
Jeannet, B. and Serwe, W. 2004. Abstracting call-stacks for interprocedural verification of imperative programs. In Proceedings of the Workshop on Algebraic Methodology and Software Technology (AMAST'04). Lecture Notes in Computer Science, vol. 3116, Springer.
[18]
Knoop, J. and Steffen, B. 1992. The interprocedural coincidence theorem. In Computing Construction. Lecture Notes in Computer Science, vol. 641, Springer, 125--140.
[19]
Lahiri, S. K. and Qadeer, S. 2008. Back to the future: Revisiting precise program verification using smt solvers. In Principles of Programming Language. ACM Press, New York.
[20]
Lev-Ami, T., Reps, T., Sagiv, M., and Wilhelm, R. 2000. Putting static analysis to work for verification: A case study. In Proceedings of the International Symposium on Software Testing and Analysis. 26--38.
[21]
Lev-Ami, T. and Sagiv, M. 2000. TVLA: A system for implementing static analyses. In Proceedings of the Static Analysis Symposium (SAS'00). Lecture Notes in Computer Science, vol. 1824, Springer, 280--301.
[22]
Loginov, A. 2006. Refinement-based program verification via three-valued-logic analysis. Ph.D. thesis, Tech. rep. 1574. Computer Science Department, University of Wisconsin, Madison, WI.
[23]
Loginov, A., Reps, T., and Sagiv, M. 2005. Abstraction refinement via inductive learning. In Proceedings of the International Conference on Computer Aided Verification. Lecture Notes in Computer Science, vol. 3576, Springer.
[24]
Manna, Z. and Pnueli, A. 1995. Temporal Verification of Reactive Systems: Safety, Springer.
[25]
Marron, M., Hermenegildo, M. V., Kapur, D., and Stefanovic, D. 2008. Efficient context-sensitive shape analysis with graph based heap models. In Computer Construction. Lecture Notes in Computer Science, vol. 4959, Springer, 245--259.
[26]
Miné, A. 2006. The octagon abstract domain. Higher-Order Symb. Comput. 19, 1, 31--100.
[27]
Møller, A. and Schwartzbach, M. I. 2001. The pointer assertion logic engine. In Programming Language Design and Implementation. 221--231.
[28]
Reps, T., Horwitz, S., and Sagiv, M. 1995. Precise interprocedural dataflow analysis via graph reachability. In Principles of Programming Language. ACM Press, New York, 49--61.
[29]
Reps, T., Sagiv, M., and Loginov, A. 2003. Finite differencing of logical formulas for static analysis. In Proceedings of the European Symposium on Programming. Lecture Notes in Computer Science, vol. 2618, 380--398.
[30]
Reps, T., Schwoon, S., Jha, S., and Melski, D. 2005. Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program. 58, 1--2, 206--263.
[31]
Rinetzky, N., Bauer, J., Reps, T., Sagiv, M., and Wilhelm, R. 2005a. A semantics for procedure local heaps and its abstraction. In Proceedings of the 32nd ACM SIGPLAN -- SIGACT Symposium on Principles of Programming Languages (POPL'05).
[32]
Rinetzky, N. and Sagiv, M. 2001. Interprocedural shape analysis for recursive programs. In Computer Construction. Lecture Notes in Computer Science, vol. 2027, Springer, 133--149.
[33]
Rinetzky, N., Sagiv, M., and Yahav, E. 2005b. Interprocedural shape analysis for cutpoint-free programs. In Proceedings of the Static Analysis Symposium (SAS'05). Lecture Notes in Computer Science, vol. 3672, Springer.
[34]
Sagiv, M., Reps, T., and Horwitz, S. 1996. Precise interprocedural dataflow analysis with applications to constant propagation. Theor. Comput. Sci. 167, 131--170.
[35]
Sagiv, M., Reps, T., and Wilhelm, R. 2002. Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24, 3, 217--298.
[36]
Schwoon, S. 2002. Model-checking pushdown systems. Ph.D. thesis, Technical University of Munich, Munich, Germany.
[37]
Sharir, M. and Pnueli, A. 1981. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, S. Muchnick and N. Jones, Eds. Prentice-Hall, Englewood Cliffs, NJ. Chapter 7, 189--234.
[38]
Yorsh, G., Reps, T., and Sagiv, M. 2004. Symbolically computing most-precise abstract operations for shape analysis. In Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 2988, Springer, 530--545.

Cited By

View all
  • (2024)DAInfer: Inferring API Aliasing Specifications from Library Documentation via Neurosymbolic OptimizationProceedings of the ACM on Software Engineering10.1145/36608161:FSE(2469-2492)Online publication date: 12-Jul-2024
  • (2024)Interactive Abstract Interpretation with Demanded SummarizationACM Transactions on Programming Languages and Systems10.1145/364844146:1(1-40)Online publication date: 15-Feb-2024
  • (2023) Anchor: Fast and Precise Value-flow Analysis for Containers via Memory OrientationACM Transactions on Software Engineering and Methodology10.1145/356580032:3(1-39)Online publication date: 26-Apr-2023
  • Show More Cited By

Index Terms

  1. A relational approach to interprocedural shape analysis

                              Recommendations

                              Comments

                              Information & Contributors

                              Information

                              Published In

                              cover image ACM Transactions on Programming Languages and Systems
                              ACM Transactions on Programming Languages and Systems  Volume 32, Issue 2
                              January 2010
                              123 pages
                              ISSN:0164-0925
                              EISSN:1558-4593
                              DOI:10.1145/1667048
                              Issue’s Table of Contents
                              Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

                              Publisher

                              Association for Computing Machinery

                              New York, NY, United States

                              Publication History

                              Published: 08 February 2010
                              Accepted: 01 May 2009
                              Revised: 01 December 2008
                              Received: 01 May 2008
                              Published in TOPLAS Volume 32, Issue 2

                              Permissions

                              Request permissions for this article.

                              Check for updates

                              Author Tags

                              1. 3-valued logic
                              2. Abstract interpretation
                              3. context-sensitive analysis
                              4. destructive updating
                              5. interprocedural dataflow analysis
                              6. pointer analysis
                              7. shape analysis
                              8. static analysis

                              Qualifiers

                              • Research-article
                              • Research
                              • Refereed

                              Funding Sources

                              Contributors

                              Other Metrics

                              Bibliometrics & Citations

                              Bibliometrics

                              Article Metrics

                              • Downloads (Last 12 months)80
                              • Downloads (Last 6 weeks)18
                              Reflects downloads up to 14 Feb 2025

                              Other Metrics

                              Citations

                              Cited By

                              View all
                              • (2024)DAInfer: Inferring API Aliasing Specifications from Library Documentation via Neurosymbolic OptimizationProceedings of the ACM on Software Engineering10.1145/36608161:FSE(2469-2492)Online publication date: 12-Jul-2024
                              • (2024)Interactive Abstract Interpretation with Demanded SummarizationACM Transactions on Programming Languages and Systems10.1145/364844146:1(1-40)Online publication date: 15-Feb-2024
                              • (2023) Anchor: Fast and Precise Value-flow Analysis for Containers via Memory OrientationACM Transactions on Software Engineering and Methodology10.1145/356580032:3(1-39)Online publication date: 26-Apr-2023
                              • (2021)A relational shape abstract domainFormal Methods in System Design10.1007/s10703-021-00366-457:3(343-400)Online publication date: 24-Apr-2021
                              • (2020)Interprocedural Shape Analysis Using Separation Logic-Based Transformer SummariesStatic Analysis10.1007/978-3-030-65474-0_12(248-273)Online publication date: 18-Nov-2020
                              • (2019)Mergeable replicated data typesProceedings of the ACM on Programming Languages10.1145/33605803:OOPSLA(1-29)Online publication date: 10-Oct-2019
                              • (2018)TwASProceedings of the 33rd Annual ACM Symposium on Applied Computing10.1145/3167132.3167330(1857-1864)Online publication date: 9-Apr-2018
                              • (2017)A Relational Shape Abstract DomainNASA Formal Methods10.1007/978-3-319-57288-8_15(212-229)Online publication date: 9-Apr-2017
                              • (2016)Automatically learning shape specificationsACM SIGPLAN Notices10.1145/2980983.290812551:6(491-507)Online publication date: 2-Jun-2016
                              • (2016)Automatically learning shape specificationsProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2908080.2908125(491-507)Online publication date: 2-Jun-2016
                              • Show More Cited By

                              View Options

                              View options

                              PDF

                              View or Download as a PDF file.

                              PDF

                              eReader

                              View online with eReader.

                              eReader

                              Login options

                              Full Access

                              Figures

                              Tables

                              Media

                              Share

                              Share

                              Share this Publication link

                              Share on social media