Variably interprocedural program analysis for runtime error detection

ABSTRACT

This paper describes an analysis approach based on a of static and dynamic techniques to ?nd run-time errors in Java code. It uses symbolic execution to ?nd constraints under which an error (e.g. a null pointer dereference, array out of bounds access, or assertion violation) may occur and then solves these constraints to ?nd test inputs that may expose the error. It only alerts the user to the possibility of a real error when it detects the expected exception during a program run.

The analysis is customizable in two important ways. First, we can adjust how deeply to follow calls from each top-level method. Second, we can adjust the path termination tion for the symbolic execution engine to be either a bound on the path condition length or a bound on the number of times each instruction can be revisited.

We evaluated the tool on a set of benchmarks from the literature as well as a number of real-world systems that range in size from a few thousand to 50,000 lines of code. The tool discovered all known errors in the benchmarks (as well as some not previously known) and reported on average 8 errors per 1000 lines of code for the industrial examples. In both cases the interprocedural call depth played little role in the error detection. That is, an intraprocedural analysis seems adequate for the class of errors we detect.

REFERENCES

• 1: C. BarrettandS. Berezin. CVCLite: A new implementation of the cooperating validity checker. In R. Alur and D. A. Peled, editors, Proceedings of the International Conference on Computer Aided Verification volume 3114 of Lecture Notes in Computer Science pages 515--518. Springer-Verlag, July 2004.
• 2: Robert S. Boyer , Bernard Elspas , Karl N. Levitt, SELECT—a formal system for testing and debugging programs by symbolic execution, ACM SIGPLAN Notices, v.10 n.6, p.234-245, June 1975
• 3: C. Cadar and D. Engler. Execution generated test cases: how to make systems code crash itself. In Proceedings of the International SPIN Workshop on Model Checking of Software 2005.
• 4: T. Copeland. PMD Applied Centennial Books, Nov. 2005.
• 5: P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Min, D. Monniaux, and X. Rival. The ASTRÉE analyser. In Proceedings of the European Symposium on Programming pages 21--30, 2005.
• 6: Coverity, Inc. http://www.coverity.com
• 7: Christoph Csallner , Yannis Smaragdakis, JCrasher: an automatic robustness tester for Java, Software—Practice & Experience, v.34 n.11, p.1025-1050, September 2004 [doi>10.1002/spe.602]
• 8: Christoph Csallner , Yannis Smaragdakis, Check 'n' crash: combining static checking and testing, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA [doi>10.1145/1062455.1062533]
• 9: Christoph Csallner , Yannis Smaragdakis, DSD-Crasher: a hybrid analysis tool for bug finding, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA [doi>10.1145/1146238.1146267]
• 10: Laura K. Dillon, Using symbolic execution for verification of Ada tasking programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.4, p.643-669, Oct. 1990 [doi>10.1145/88616.96551]
• 11: Michael D. Ernst , Adam Czeisler , William G. Griswold , David Notkin, Quickly detecting relevant program invariants, Proceedings of the 22nd international conference on Software engineering, p.449-458, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337240]
• 12: 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
• 13: M. R. Girgis, An experimental evaluation of a symbolic execution system, Software Engineering Journal, v.7 n.4, p.285-290, July 1992
• 14: 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
• 15: G. J. Holzmann. The Spin Model Checker Addison-Wesley, 2003.
• 16: 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]
• 17: S. C. Johnson. Lint, a C Program Checker BellLabs, 1978.
• 18: R. A. Kemmerer and S. T. Eckman. UNISEX: A UNIX-based symbolic executor for Pascal. Software - Practice and Experience 15(5):439--458, 1985.
• 19: S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems 2003.
• 20: 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]
• 21: Klocwork, Inc. http://www.klocwork.com
• 22: Bogdan Korel, Automated test data generation for programs with procedures, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.209-215, January 08-10, 1996, San Diego, California, United States
• 23: David Larochelle , David Evans, Statically detecting likely buffer overflow vulnerabilities, Proceedings of the 10th conference on USENIX Security Symposium, p.14-14, August 13-17, 2001, Washington, D.C.
• 24: National Institute of Standards and Technology. The economic impacts of inadequate infrastructure for software testing, May 2002.
• 25: Robby , Matthew B. Dwyer , John Hatcliff, Bogor: an extensible and highly-modular software model checking framework, Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering, September 01-05, 2003, Helsinki, Finland
• 26: T. Sakaguchi. UNISEX-C: a UNIx-based Symbolic EXecutor for standard C PhD thesis, University of California, Santa Barbara, 1997.
• 27: H. Schlenker and G. Ringwelski. POOC: A platform for object-oriented constraint programming, 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: R. Vallée-Rai, L. Hendren, V. Sundaresan, P. Lam, E. Gagnon, and P. Co. Soot -a Java optimization framework. In Proceedings of CASCON 1999 pages 125--135, 1999.
• 30: Willem Visser , Klaus Havelund , Guillaume Brat , Seungjoon Park , Flavio Lerda, Model Checking Programs, Automated Software Engineering, v.10 n.2, p.203-232, April 2003 [doi>10.1023/A:1022920129859]
• 31: T. Xie, D. Marinov, W. Schulte, and D. Notkin. Symstra: A framework for generating object-oriented unit tests using symbolic execution. Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems 3440:365--381, 2005.
• 32: Junfeng Yang , Can Sar , Paul Twohey , Cristian Cadar , Dawson Engler, Automatically Generating Malicious Disks using Symbolic Execution, Proceedings of the 2006 IEEE Symposium on Security and Privacy (S&P'06), p.243-257, May 21-24, 2006 [doi>10.1109/SP.2006.7]
• 33: Jian Zhang, Symbolic Execution of Program Paths Involving Pointer and Structure Variables, Proceedings of the Quality Software, Fourth International Conference on (QSIC'04), p.87-92, September 08-10, 2004 [doi>10.1109/QSIC.2004.32]

INDEX TERMS

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

General Terms:
Reliability, Verification

Keywords:
can-test, defect detection, generation, symbolic execution