Explaining failures of program analyses

ABSTRACT

With programs getting larger and often more complex with each new release, programmers need all the help they can get in understanding and transforming programs. Fortunately, modern development environments, such as Eclipse, incorporate tools for understanding, navigating, and transforming programs. These tools typically use program analyses to extract relevant properties of programs.

These tools are often invaluable to developers; for example, many programmers use refactoring tools regularly. However, poor results by the underlying analyses can compromise a tool's usefulness. For example, a bug finding tool may produce too many false positives if the underlying analysis is overly conservative, and thus overwhelm the user with too many possible errors in the program. In such cases it would be invaluable for the tool to explain to the user why it believes that each bug exists. Armed with this knowledge, the user can decide which bugs are worth pursing and which are false positives.

The contributions of this paper are as follows: (i) We describe requirements on the structure of an analysis so that we can produce reasons when the analysis fails; the user of the analysis determines whether or not an analysis's results constitute failure. We also describe a simple language that enforces these requirements; (ii) We describe how to produce necessary and sufficient reasons for analysis failure; (iii) We evaluate our system with respect to a number of analyses and programs and find that most reasons are small (and thus usable) and that our system is fast enough for interactive use.

REFERENCES

• 1: Keith D. Cooper, Mary W. Hall, Robert T. Hood, Ken Kennedy, Kathryn S. McKinley, John M. Mellor-Crummey, Linda Torczon, and Scott K. Warren. The ParaScope parallel programming environment. Proceedings of the IEEE, 81(2):244--263, 1993.
• 2: Luiz De Rose , Kyle Gallivan , Efstratios Gallopoulos , Bret A. Marsolf , David A. Padua, FALCON: A MATLAB Interactive Restructuring Compiler, Proceedings of the 8th International Workshop on Languages and Compilers for Parallel Computing, p.269-288, August 10-12, 1995
• 3: Jan Friso Groote and Misa Keinänen. Solving disjunctive/conjunctive boolean equation systems with alternating fixed points, 2004.
• 4: Martin Hirzel , Daniel Von Dincklage , Amer Diwan , Michael Hind, Fast online pointer analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.2, p.11-es, April 2007 [doi>10.1145/1216374.1216379]
• 5: Sorin Lerner, Todd Millstein, and Craig Chambers. Automatically proving the correctness of compiler optimizations, 2003.
• 6: Shih-Wei Liao , Amer Diwan , Robert P. Bosch, Jr. , Anwar Ghuloum , Monica S. Lam, SUIF Explorer: an interactive and interprocedural parallelizer, Proceedings of the seventh ACM SIGPLAN symposium on Principles and practice of parallel programming, p.37-48, May 04-06, 1999, Atlanta, Georgia, United States
• 7: Angelika Mader. Verification of Modal Properties Using Infinite Boolean Equation Systems. PhD thesis.
• 8: David A. Schmidt, Data flow analysis is model checking of abstract interpretations, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.38-48, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268950]
• 9: David A. Schmidt , Bernhard Steffen, Program Analysis as Model Checking of Abstract Interpretations, Proceedings of the 5th International Symposium on Static Analysis, p.351-380, September 14-16, 1998
• 10: Sherry Shavor , Jim D'Anjou , Scott Fairbrother , Dan Kehn , John Kellerman , Pat McCarthy, The Java Developer's Guide to Eclipse, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2003
• 11: Standard performance evaluation corporation. SPECjbb2000 (java business benchmark). http://www.spec.org/jbb2000.
• 12: Standard performance evaluation corporation. SPECjvm98 benchmarks. http://www.spec.org/jvm98.
• 13: 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.3 PROGRAMMING LANGUAGES
      D.3.4 Processors

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

General Terms:
Documentation, Measurement, Reliability

Keywords:
analyses, reasons