Snugglebug: a powerful approach to weakest preconditions

ABSTRACT

Symbolic analysis shows promise as a foundation for bug-finding, specification inference, verification, and test generation. This paper addresses demand-driven symbolic analysis for object-oriented programs and frameworks. Many such codes comprise large, partial programs with highly dynamic behaviors--polymorphism, reflection, and so on--posing significant scalability challenges for any static analysis.

We present an approach based on interprocedural backwards propagation of weakest preconditions. We present several novel techniques to improve the efficiency of such analysis. First, we present directed call graph construction, where call graph construction and symbolic analysis are interleaved. With this technique, call graph construction is guided by constraints discovered during symbolic analysis, obviating the need for exhaustively exploring a large, conservative call graph. Second, we describe generalization, a technique that greatly increases the reusability of procedure summaries computed during interprocedural analysis. Instead of tabulating how a procedure transforms a symbolic state in its entirety, our technique tabulates how the procedure transforms only the pertinent portion of the symbolic state. Additionally, we show how integrating an inexpensive, custom logic simplifier with weakest precondition computation dramatically improves performance.

We have implemented the analysis in a tool called Snugglebug and evaluated it as a bug-report feasibility checker. Our results show that the algorithmic techniques were critical for successfully analyzing large Java applications.

REFERENCES

• 1: S. Anand, P. Godefroid, and N. Tillmann. Demand-driven compositional symbolic execution. In TACAS, 2008.
• 2: L. O. Andersen. Program Analysis and Specialization for the C Programming Language. PhD thesis, University of Copenhagen, DIKU, 1994.
• 3: Domagoj Babic , Alan J. Hu, Calysto: scalable and precise extended static checking, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany [doi>10.1145/1368088.1368118]
• 4: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 5: M. Barnett, B. E. Chang, R. Deline, B. Jacobs, and K. R. Leino. Boogie: A modular reusable verifier for object-oriented programs. In FMCO, 2005.
• 6: C. Barrett and C. Tinelli. CVC3. In CAV, 2007.
• 7: Nels E. Beckman , Aditya V. Nori , Sriram K. Rajamani , Robert J. Simmons, Proofs from tests, Proceedings of the 2008 international symposium on Software testing and analysis, July 20-24, 2008, Seattle, WA, USA [doi>10.1145/1390630.1390634]
• 8: William R. Bush , Jonathan D. Pincus , David J. Sielaff, A static analyzer for finding dynamic programming errors, Software—Practice & Experience, v.30 n.7, p.775-802, June 2000 [doi>10.1002/(SICI)1097-024X(200006)30:7<775::AID-SPE309>3.0.CO;2-H]
• 9: C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, 2008.
• 10: Patrick Cousot , Radhia Cousot, Modular Static Program Analysis, Proceedings of the 11th International Conference on Compiler Construction, p.159-178, April 08-12, 2002
• 11: Christoph Csallner , Yannis Smaragdakis , Tao Xie, DSD-Crasher: A hybrid analysis tool for bug finding, ACM Transactions on Software Engineering and Methodology (TOSEM), v.17 n.2, p.1-37, April 2008 [doi>10.1145/1348250.1348254]
• 12: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 13: Julian Dolby , Mandana Vaziri , Frank Tip, Finding bugs efficiently with a SAT solver, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia [doi>10.1145/1287624.1287653]
• 14: Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
• 15: Cormac Flanagan , K. Rustan M. Leino , Mark Lillibridge , Greg Nelson , James B. Saxe , Raymie Stata, Extended static checking for Java, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 16: Patrice Godefroid, Compositional dynamic test generation, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 17: Patrice Godefroid , Nils Klarlund , Koushik Sen, DART: directed automated random testing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 18: David Grove , Craig Chambers, A framework for call graph construction algorithms, ACM Transactions on Programming Languages and Systems (TOPLAS), v.23 n.6, p.685-746, November 2001 [doi>10.1145/506315.506316]
• 19: Bhargav S. Gulavani , Thomas A. Henzinger , Yamini Kannan , Aditya V. Nori , Sriram K. Rajamani, SYNERGY: a new algorithm for property checking, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA [doi>10.1145/1181775.1181790]
• 20: 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
• 21: David Hovemeyer , William Pugh, Finding bugs is easy, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA [doi>10.1145/1028664.1028717]
• 22: Daniel Jackson , Mandana Vaziri, Finding bugs with a constraint solver, Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, p.14-25, August 21-24, 2000, Portland, Oregon, United States
• 23: James C. King, Symbolic execution and program testing, Communications of the ACM, v.19 n.7, p.385-394, July 1976 [doi>10.1145/360248.360252]
• 24: Roman Manevich , Manu Sridharan , Stephen Adams , Manuvir Das , Zhe Yang, PSE: explaining program failures via postmortem static analysis, Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, October 31-November 06, 2004, Newport Beach, CA, USA
• 25: John McCarthy, A Basis for a Mathematical Theory of Computation, Massachusetts Institute of Technology, Cambridge, MA, 1962
• 26: 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]
• 27: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 28: Koushik Sen , Darko Marinov , Gul Agha, CUTE: a concolic unit testing engine for C, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 29: M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis, chapter 7, pages 189--233. Prentice-Hall, 1981.
• 30: Mana Taghdiri, Inferring Specifications to Detect Errors in Code, Proceedings of the 19th IEEE international conference on Automated software engineering, p.144-153, September 20-24, 2004 [doi>10.1109/ASE.2004.42]
• 31: Willem Visser , Corina S. Pǎsǎreanu , Sarfraz Khurshid, Test input generation with java PathFinder, Proceedings of the 2004 ACM SIGSOFT international symposium on Software testing and analysis, July 11-14, 2004, Boston, Massachusetts, USA
• 32: T.J. Watson Libraries for Analysis (WALA). http://wala.sf.net.
• 33: Yichen Xie , Alex Aiken, Saturn: A scalable framework for error detection using Boolean satisfiability, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.3, p.16-es, May 2007 [doi>10.1145/1232420.1232423]

INDEX TERMS

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

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Symbolic execution

General Terms:
Algorithms, Languages, Verification

Keywords:
interprocedural analysis, symbolic analysis, weakest preconditions