PSE: explaining program failures via postmortem static analysis

ABSTRACT

In this paper, we describe PSE (Postmortem Symbolic Evaluation), a static analysis algorithm that can be used by programmers to diagnose software failures. The algorithm requires minimal information about a failure, namely its kind (e.g. NULL dereference), and its location in the program's source code. It produces a set of execution traces along which the program can be driven to the given failure.

PSE tracks the flow of a single value of interest from the point in the program where the failure occurred back to the points in the program where the value may have originated. The algorithm combines a novel dataflow analysis and memory alias analysis in a manner that allows for precise exploration of the program's behavior in polynomial time.

We have applied PSE to the problem of diagnosing potential NULL-dereference errors in a suite of C programs, including several SPEC benchmarks and a large commercial operating system. In most cases, the analysis is able to either validate a pointer dereference, or find precise error traces demonstrating a NULL value for the pointer, in less than a second.

REFERENCES

• 1: Hiralal Agrawal , Joseph R. Horgan, Dynamic program slicing, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.246-256, June 1990, White Plains, New York, United States
• 2: Hiraral Agrawal, Joseph R. Horgan, Saul London, and W. Eric Wong. Fault Localization using Execution Slices and Dataflow Tests. In Proceedings of the IEEE International Symposium on Software Reliability Engineering, October 1995.
• 3: Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
• 4: Thomas Ball , Mayur Naik , Sriram K. Rajamani, From symptom to cause: localizing errors in counterexample traces, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.97-105, January 15-17, 2003, New Orleans, Louisiana, USA
• 5: Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
• 6: Peter Bunus and Peter Fritzson. Semi-Automatic Fault Localization and Behavior Verification for Physical System Simulation Models. In Proceedings of the IEEE International Conference on Automated Software Engineering, October 2003.
• 7: 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 ]
• 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: Microsoft Corporation. Microsoft Online Crash Analysis. http://oca.microsoft.com/en/dcp20.asp.
• 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: Manuvir Das , Ben Liblit , Manuel Fähndrich , Jakob Rehof, Estimating the Impact of Scalable Pointer Analysis on Optimization, Proceedings of the 8th International Symposium on Static Analysis, p.260-278, July 16-18, 2001
• 13: Richard A. DeMillo , Hsin Pan , Eugene H. Spafford, Critical slicing for software fault localization, Proceedings of the 1996 ACM SIGSOFT international symposium on Software testing and analysis, p.121-134, January 08-10, 1996, San Diego, California, United States
• 14: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 15: 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
• 16: Margaret Francel , Spencer Rugaber, Fault localization using execution traces, Proceedings of the 30th annual Southeast regional conference, April 08-10, 1992, Raleigh, North Carolina [doi>10.1145/503720.503747]
• 17: Seth Hallem , Benjamin Chelf , Yichen Xie , Dawson Engler, A system and language for building system-specific, static analyses, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 18: Ben Liblit , Alex Aiken, Building a Better Backtrace: Techniques for Postmortem Program Analysis, University of California at Berkeley, Berkeley, CA, 2002
• 19: Hsin Pan and Eugene H. Spafford. Toward Automatic Localization of Software Faults. In Proceedings of the Pacific Northwest Software Quality Conference, October 1992.
• 20: Brock Pytlik, Manos Renieris, Shriram Krishnamurthi, and Steven P. Reiss. Automated Fault Localization Using Potential Invariants. In Proceedings of the International Workshop on Automated and Algorithmic Debugging, September 2003.
• 21: 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]
• 22: 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
• 23: R. E. Strom , D. M. Yellin, Extending Typestate Checking Using Conditional Liveness Analysis, IEEE Transactions on Software Engineering, v.19 n.5, p.478-485, May 1993 [doi>10.1109/32.232013 ]
• 24: Frank Tip. A survey of program slicing techniques. Journal of programming languages, 3:121--189, 1995.
• 25: Mark Weiser, Program slicing, Proceedings of the 5th international conference on Software engineering, p.439-449, March 09-12, 1981, San Diego, California, United States

INDEX TERMS

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

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

General Terms:
Algorithms, Reliability, Security, Verification

Keywords:
alias analysis, postmortem analysis, typestate, value flow