Effective typestate verification in the presence of aliasing

ABSTRACT

This paper addresses the challenge of sound typestate verification, with acceptable precision, for real-world Java programs. We present a novel framework for verification of typestate properties, including several new techniques to precisely treat aliases without undue performance costs. In particular, we present a flowsensitive, context-sensitive, integrated verifier that utilizes a parametric abstract domain combining typestate and aliasing information.To scale to real programs without compromising precision, we present a staged verification system in which faster verifiers run as early stages which reduce the workload for later, more precise, stages.We have evaluated our framework on a number of real Java programs, checking correct API usage for various Java standard libraries. The results show that our approach scales to hundreds of thousands of lines of code, and verifies correctness for 93% of the potential points of failure.

REFERENCES

• 1: Alex Aiken , Jeffrey S. Foster , John Kodumal , Tachio Terauchi, Checking and inferring local non-aliasing, ACM SIGPLAN Notices, v.38 n.5, May 2003
• 2: Rajeev Alur , Pavol Černý , P. Madhusudan , Wonhong Nam, Synthesis of interface specifications for Java classes, ACM SIGPLAN Notices, v.40 n.1, p.98-109, January 2005
• 3: L. O. Andersen. Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, Univ. of Copenhagen, May 1994. (DIKU report 94/19).
• 4: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 5: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, ACM SIGPLAN Notices, v.37 n.1, p.1-3, Jan. 2002
• 6: David R. Chase , Mark Wegman , F. Kenneth Zadeck, Analysis of pointers and structures, ACM SIGPLAN Notices, v.25 n.6, p.296-310, Jun. 1990
• 7: Jong-Deok Choi , Michael Burke , Paul Carini, Efficient flow-sensitive interprocedural computation of pointer-induced aliases and side effects, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.232-245, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158639]
• 8: James C. Corbett , Matthew B. Dwyer , John Hatcliff , Shawn Laubach , Corina S. Păsăreanu , Robby , Hongjun Zheng, Bandera: extracting finite-state models from Java source code, Proceedings of the 22nd international conference on Software engineering, p.439-448, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337234]
• 9: 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]
• 10: Manuvir Das, Unification-based pointer analysis with directional assignments, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.35-46, June 18-21, 2000, Vancouver, British Columbia, Canada
• 11: 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
• 12: R. DeLine and M. Fähndrich. Typestates for objects. In 18th European Conference on Object-Oriented Programming (ECOOP), volume 3086 of LNCS, June 2004.
• 13: 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
• 14: Maryam Emami , Rakesh Ghiya , Laurie J. Hendren, Context-sensitive interprocedural points-to analysis in the presence of function pointers, Proceedings of the ACM SIGPLAN 1994 conference on Programming language design and implementation, p.242-256, June 20-24, 1994, Orlando, Florida, United States
• 15: Manuel Fahndrich , Robert DeLine, Adoption and focus: practical linear types for imperative programming, ACM SIGPLAN Notices, v.37 n.5, May 2002
• 16: J. Field, D. Goyal, G. Ramalingam, and E. Yahav. Typestate verification: Abstraction techniques and complexity results. In Proc. of Static Analysis Symposium (SAS'03), volume 2694 of LNCS, pages 439--462. Springer, June 2003.
• 17: S. Fink, J. Dolby, and L. Colby. Semi-automatic J2EE transaction configuration. Technical Report RC23326, IBM, 2004.
• 18: Rajiv Gupta, Optimizing array bound checks using flow analysis, ACM Letters on Programming Languages and Systems (LOPLAS), v.2 n.1-4, p.135-150, March–Dec. 1993 [doi>10.1145/176454.176507]
• 19: S. Guyer and C. Lin. Client-driven pointer analysis. In Proc. of SAS'03, volume 2694 of LNCS, pages 214--236, June 2003.
• 20: Rebecca Hasti , Susan Horwitz, Using static single assignment form to improve flow-insensitive pointer analysis, ACM SIGPLAN Notices, v.33 n.5, p.97-105, May 1998
• 21: Nevin Heintze , Olivier Tardieu, Ultra-fast aliasing analysis using CLA: a million lines of C code in a second, ACM SIGPLAN Notices, v.36 n.5, p.254-263, May 2001
• 22: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 23: William Landi , Barbara G. Ryder, A safe approximate algorithm for interprocedural aliasing, ACM SIGPLAN Notices, v.27 n.7, p.235-248, July 1992
• 24: O. Lhoták and L. Hendren. Scaling Java points-to analysis using SPARK. In 12th International Conference on Compiler Construction (CC), volume 2622 of LNCS, pages 153--169, Apr. 2003.
• 25: B. Livshits, J. Whaley, and M. S. Lam. Reflection analysis for java. In Proceedings of Programming Languages and Systems: Third Asian Symposium, APLAS 2005, November 2005.
• 26: Ana Milanova , Atanas Rountev , Barbara G. Ryder, Parameterized object sensitivity for points-to analysis for Java, ACM Transactions on Software Engineering and Methodology (TOSEM), v.14 n.1, p.1-41, January 2005 [doi>10.1145/1044834.1044835]
• 27: John Plevyak , Andrew A. Chien, Precise concrete type inference for object-oriented languages, ACM SIGPLAN Notices, v.29 n.10, p.324-340, Oct. 1994
• 28: G. Ramalingam, On sparse evaluation representations, Theoretical Computer Science, v.277 n.1-2, p.119-147, April 28, 2002 [doi>10.1016/S0304-3975(00)00315-7]
• 29: 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]
• 30: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.105-118, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292552]
• 31: Mooly Sagiv , Thomas Reps , Reinhard Wilhelm, Parametric shape analysis via 3-valued logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.24 n.3, p.217-298, May 2002 [doi>10.1145/514188.514190]
• 32: 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
• 33: John Whaley , Michael C. Martin , Monica S. Lam, Automatic extraction of object-oriented component interfaces, Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis, July 22-24, 2002, Roma, Italy
• 34: Robert P. Wilson , Monica S. Lam, Efficient context-sensitive pointer analysis for C programs, ACM SIGPLAN Notices, v.30 n.6, p.1-12, June 1995
• 35: Eran Yahav , G. Ramalingam, Verifying safety properties using separation and heterogeneous abstractions, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA

INDEX TERMS

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

General Terms:
Algorithms, Verification

Keywords:
alias analysis, program verification, typestate