Cause clue clauses: error localization using maximum satisfiability

ABSTRACT

Much effort is spent by programmers everyday in trying to reduce long, failing execution traces to the cause of the error. We present an algorithm for error cause localization based on a reduction to the maximal satisfiability problem (MAX-SAT), which asks what is the maximum number of clauses of a Boolean formula that can be simultaneously satisfied by an assignment. At an intuitive level, our algorithm takes as input a program and a failing test, and comprises the following three steps. First, using bounded model checking, and a bound obtained from the execution of the test, we encode the semantics of a bounded unrolling of the program as a Boolean trace formula. Second, for a failing program execution (e.g., one that violates an assertion or a post-condition), we construct an unsatisfiable formula by taking the formula and additionally asserting that the input is the failing test and that the assertion condition does hold at the end. Third, using MAX-SAT, we find a maximal set of clauses in this formula that can be satisfied together, and output the complement set as a potential cause of the error.

We have implemented our algorithm in a tool called BugAssist that performs error localization for C programs. We demonstrate the effectiveness of BugAssist on a set of benchmark examples with injected faults, and show that in most cases, BugAssist can quickly and precisely isolate a few lines of code whose change eliminates the error. We also demonstrate how our algorithm can be modified to automatically suggest fixes for common classes of errors such as off-by-one.We have implemented our algorithm in a tool called BugAssist that performs error localization for C programs. We demonstrate the effectiveness of BugAssist on a set of benchmark examples with injected faults, and show that in most cases, BugAssist can quickly and precisely isolate a few lines of code whose change eliminates the error. We also demonstrate how our algorithm can be modified to automatically suggest fixes for common classes of errors such as off-by-one.

References

1. Thomas Ball, Mayur Naik, and Sriram K. Rajamani. From symptom to cause: localizing errors in counterexample traces. In POPL '03: Principles of Programming Languages, pages 97--105, 2003. ACM.
2. A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu. Symbolic model checking using sat procedures instead of bdds. In DAC '09: Design Automation Conference, pages 317--320, 1999. ACM.
3. Cristian Cadar, Daniel Dunbar, and Dawson Engler. Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI '08: Operating Systems Design and Implementation, pages 209--224, 2008. USENIX Association.
4. Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, and Dawson R. Engler. Exe: automatically generating inputs of death. In CCS '06: Computer and Communications security, pages 322--335, 2006. ACM.
5. Yibin Chen, Sean Safarpour, Andreas Veneris, and Joao Marques-Silva. Spatial and temporal design debug using partial maxsat. In GLSVLSI '09: Great Lakes Symposium on VLSI, pages 345--350, 2009. ACM.
6. Edmund Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ANSI-C programs. In TACAS '04: Tools and Algorithms for the Construction and Analysis of Systems, volume 2988 of Lecture Notes in Computer Science, pages 168--176, 2004. Springer.
7. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. ACM, 7:201--215, July 1960.
8. Hyunsook Do, Sebastian Elbaum, and Gregg Rothermel. Supporting controlled experimentation with testing techniques: An infrastructure and its potential impact. Empirical Softw. Engg., 10(4):405--435, 2005.
9. Niklas Eén and Niklas Sörensson. Minisat v2.0 (beta). In SAT-Race, 2006. http://fmv.jku.at/sat-race-2006/.
10. Zhaohui Fu and Sharad Malik. On solving the partial MAX-SAT problem. In SAT '06: Theory and Applications of Satisfiability Testing, volume 4121 of Lecture Notes in Computer Science, pages 252--265, 2006. Springer.
11. Patrice Godefroid, Nils Klarlund, and Koushik Sen. Dart: directed automated random testing. In PLDI '05: Programming Language Design and Implementation, pages 213--223, 2005. ACM.
12. Andreas Griesmayer, Stefan Staber, and Roderick Bloem. Automated fault localization for C programs. ENTCS, 174:95--111, 2007.
13. Alex Groce, Sagar Chaki, Daniel Kroening, and Ofer Strichman. Error explanation with distance metrics. Int. J. Softw. Tools Technol. Transf., 8:229--247, 2006.
14. Monica Hutchins, Herb Foster, Tarak Goradia, and Thomas Ostrand. Experiments of the effectiveness of dataflow- and controlflow-based test adequacy criteria. In ICSE '94: International Conference on Software Engineering, pages 191--200, 1994. IEEE Computer Society.
15. James C. King. Symbolic execution and program testing. Commun. ACM, 19:385--394, July 1976.
16. Chu Min Li and Felip Manyà. MaxSAT, hard and soft constraints. In Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, chapter 19, pages 613--631. IOS Press, 2009.
17. Chu Min Li, Felip Manyà, and Jordi Planes. New inference rules for MAX-SAT. J. Artif. Int. Res., 30:321--359, October 2007.
18. Mark H. Liffiton and Karem A. Sakallah. On finding all minimally unsatisfiable subformulas. In SAT '05: Theory and Applications of Satisfiability Testing, volume 3569 of Lecture Notes in Computer Science, pages 173--186, 2005. Springer.
19. Joao Marques-Silva. Minimal unsatisfiability: Models, algorithms and applications (invited paper). In ISMVL '10: International Symposium on Multiple-Valued Logic, pages 9--14, 2010. IEEE Computer Society.
20. Joao Marques-Silva and Jordi Planes. Algorithms for maximum satisfiability using unsatisfiable cores. In DATE '08: Design, Automation and Test in Europe, pages 408--413, 2008. ACM.
21. Todd C. Miller and Theo de Raadt. strlcpy and strlcat: consistent, safe, string copy and concatenation. In USENIX Annual Technical Conference, pages 175--178, 1999. USENIX Association.
22. Dawei Qi, Abhik Roychoudhury, Zhenkai Liang, and Kapil Vaswani. Darwin: an approach for debugging evolving programs. In ESEC/FSE '09: European Software Engineering Conference and Foundations of Software Engineering, pages 33--42, 2009. ACM.
23. Manos Renieres and Steven P. Reiss. Fault localization with nearest neighbor queries. In ASE '03: Automated Software Engineering, pages 30--39, 2003. IEEE Computer Society.
24. Sean Safarpour, Hratch Mangassarian, Andreas Veneris, Mark H. Liffiton, and Karem A. Sakallah. Improved design debugging using maximum satisfiability. In FMCAD '07: Formal Methods in Computer-Aided Design, pages 13--19, 2007. IEEE Computer Society.
25. Koushik Sen, Darko Marinov, and Gul Agha. CUTE: a concolic unit testing engine for C. In ESEC/FSE '05: European Software Engineering Conference and Foundations of Software Engineering, pages 263--272, 2005. ACM.
26. Ilya Shlyakhter, Robert Seater, Daniel Jackson, Manu Sridharan, and Mana Taghdiri. Debugging overconstrained declarative models using unsatisfiable cores. ASE '03: Automated Software Engineering, pages 94--105, 2003. IEEE Computer Society.
27. Armando Solar-Lezama, Rodric Rabbah, Rastislav Bodík, and Kemal Ebcioğlu. Programming by sketching for bit-streaming programs. PLDI '05: Programming Languages Design and Implementation, pages 281--294, 2005.ACM.
28. Armando Solar-Lezama, Liviu Tancau, Rastislav Bodík, Sanjit A. Seshia, and Vijay A. Saraswat. Combinatorial sketching for finite programs. In ASPLOS '06: Architectural Support for Programming Languages and Operating Systems, pages 404--415, 2006. ACM.
29. Saurabh Srivastava, Sumit Gulwani, and Jeffrey S. Foster. VS3: SMT solvers for program verification. In CAV '09: Computer-Aided Verification, volume 5643 of Lecture Notes in Computer Science,pages 702--708, 2009.Springer.
30. F. Tip. A survey of program slicing techniques. Journal of Programming Languages, 3:121--189, 1995.
31. Wikipedia. Off-by-one error, the free encyclopedia, 2004. {Online; accessed 28-March-2010}.
32. Yichen Xie and Alex Aiken. Scalable error detection using boolean satisfiability. In POPL '05: Principles of Programming Languages, pages 351--363, 2005. ACM.
33. Andreas Zeller. Isolating cause-effect chains from computer programs. In FSE '10: Foundations of Software Engineering, pages 1--10, 2002. ACM.
34. Andreas Zeller and Ralf Hildebrandt. Simplifying and isolating failure-inducing input. IEEE Trans. Softw. Eng., 28:183--200, 2002.

Index Terms

• Software and its engineering

  • Software creation and management

    • Software verification and validation

      • Software defect analysis

        • Software testing and debugging

• Theory of computation

  • Logic

    • Logic and verification

  • Semantics and reasoning

    • Program reasoning

      • Program analysis

    • Program semantics