Generating precise and concise procedure summaries

ABSTRACT

We present a framework for generating procedure summaries that are (a) precise - applying the summary in a given context yields the same result as re-analyzing the procedure in that context, and(b) concise - the summary exploits the commonalitiesin the ways the procedure manipulates abstract values, and does not contain superfluous context information.

The use of a precise and concise procedure summary inmodular analyses provides a way to capture infinitely many possible contexts in a finite way; in interprocedural analyses, it provides a compact representation of an explicit input-output summary table without loss of precision.

We define a class of abstract domains and transformers for which precise and concise summaries can be efficiently generated using our framework. Our framework is rich enough to encode a wide range of problems, including all IFDS and IDE problems. In addition, we show how the framework is instantiated to provide novel solutions to two hard problems: modular linear constant propagation and modular typestate verification, both in the presence of aliasing. We implemented a prototype of our framework that computes summaries for the typestate domain, and report on preliminary experimental results.

REFERENCES

• 1: Thomas Ball , Todd Millstein , Sriram K. Rajamani, Polymorphic predicate abstraction, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.2, p.314-343, March 2005 [doi>10.1145/1057387.1057391]
• 2: Ramkrishna Chatterjee , Barbara G. Ryder , William A. Landi, Relevant context inference, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.133-146, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292554]
• 3: Ben-Chung Cheng , Wen-Mei W. Hwu, Modular interprocedural pointer analysis using access paths: design, implementation, and evaluation, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.57-69, June 18-21, 2000, Vancouver, British Columbia, Canada
• 4: Patrick Cousot , Radhia Cousot, Modular Static Program Analysis, Proceedings of the 11th International Conference on Compiler Construction, p.159-178, April 08-12, 2002
• 5: Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 6: P. Cousot and R. Cousot. Static determination of dynamic properties of recursive procedures. In E.J. Neuhold, editor, Formal Descriptions of Programming Concepts, (IFIP WG 2.2, St. Andrews, Canada, August 1977), pages 237--277. North-Holland, 1978.
• 7: Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
• 8: Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
• 9: Manuvir Das , Sorin Lerner , Mark Seigle, ESP: path-sensitive program verification in polynomial time, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 10: R. DeLine and M. Fähndrich. Adoption and focus: Practical linear types for imperative programming. In PDLI, pages 13--24, June 2002.
• 11: R. DeLine and M. Fähndrich. Typestates for objects. In ECOOP, pages 465--490, 2004.
• 12: Nurit Dor , Stephen Adams , Manuvir Das , Zhe Yang, Software validation via scalable path-sensitive value flow analysis, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 13: J. Field, D. Goyal, G. Ramalingam, and E. Yahav. Typestate verification: Abstraction techniques and complexity results. In SAS, pages 439--462, 2003.
• 14: Stephen Fink , Eran Yahav , Nurit Dor , G. Ramalingam , Emmanuel Geay, Effective typestate verification in the presence of aliasing, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146254]
• 15: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 16: Ganymed SSH-2 for java. http://www.ganymed.ethz.ch/ssh2/.
• 17: S. Gulwani and A. Tiwari. Computing procedure summaries for interprocedural analysis. In ESOP, pages 253--267, 2007.
• 18: Ranjit Jhala , Rupak Majumdar, Interprocedural analysis of asynchronous programs, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 19: Markus Müller-Olm , Helmut Seidl, Precise interprocedural analysis through linear algebra, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.330-341, January 14-16, 2004, Venice, Italy
• 20: Greg Nelson , Derek C. Oppen, Fast Decision Procedures Based on Congruence Closure, Journal of the ACM (JACM), v.27 n.2, p.356-364, April 1980 [doi>10.1145/322186.322198]
• 21: Shaz Qadeer , Dinghao Wu, KISS: keep it simple and sequential, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 22: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 23: Thomas Reps , Stefan Schwoon , Somesh Jha , David Melski, Weighted pushdown systems and their application to interprocedural dataflow analysis, Science of Computer Programming, v.58 n.1-2, p.206-263, October 2005 [doi>10.1016/j.scico.2005.02.009]
• 24: N. Rinetzky, M. Sagiv, and E. Yahav. Interprocedural shape analysis for cutpoint-free programs. In Proc. Static Analysis Symp., 2005.
• 25: Mooly Sagiv , Thomas Reps , Susan Horwitz, Precise interprocedural dataflow analysis with applications to constant propagation, Theoretical Computer Science, v.167 n.1-2, p.131-170, Oct. 30, 1996
• 26: Mooly Sagiv , Thomas Reps , Susan Horwitz, Precise interprocedural dataflow analysis with applications to constant propagation, Theoretical Computer Science, v.167 n.1-2, p.131-170, Oct. 30, 1996
• 27: Alexandru D. Salcianu , Martin C. Rinard, Pointer analysis for java programs: novel techniques and applications, Massachusetts Institute of Technology, Cambridge, MA, 2006
• 28: M. Sharir and A. Pnueli. Two approaches to interprocedural data ow analysis. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 7, pages 189--234. Prentice-Hall, Englewood Cliffs, NJ, 1981.
• 29: R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
• 30: The Ashes suite. The ashes suite. http://www.sable.mcgill.ca/ashes/.
• 31: John Whaley , Martin Rinard, Compositional pointer and escape analysis for Java programs, Proceedings of the 14th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.187-206, November 01-05, 1999, Denver, Colorado, United States
• 32: Yichen Xie , Alex Aiken, Scalable error detection using boolean satisfiability, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.351-363, January 12-14, 2005, Long Beach, California, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Assertion checkers; Reliability

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Pre- and post-conditions; Assertions; Specification techniques

General Terms:
Algorithms, Languages, Reliability, Verification

Keywords:
aliasing, composition, dataflow analysis, micro-transformers, relational analysis, summarization, symbolic summary, typestate verification