Modular and verified automatic program repair

ABSTRACT

We study the problem of suggesting code repairs at design time, based on the warnings issued by modular program verifiers. We introduce the concept of a verified repair, a change to a program's source that removes bad execution traces while increasing the number of good traces, where the bad/good traces form a partition of all the traces of a program. Repairs are property-specific. We demonstrate our framework in the context of warnings produced by the modular cccheck (a.k.a. Clousot) abstract interpreter, and generate repairs for missing contracts, incorrect locals and objects initialization, wrong conditionals, buffer overruns, arithmetic overflow and incorrect floating point comparisons. We report our experience with automatically generating repairs for the .NET framework libraries, generating verified repairs for over 80% of the warnings generated by cccheck.

References

1. S. Chandra, E. Torlak, S. Barman, and R. Bodık. Angelic debugging. In ICSE, 2011.
2. E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV, 2000.
3. P. Cousot. Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theor. Comput. Sci., 277(1--2), 2002.
4. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In ACM POPL, 1977.
5. P. Cousot, R. Cousot, and F. Logozzo. A parametric segmentation functor for fully automatic and scalable array content analysis. In POPL, 2011.
6. P. Cousot, R. Cousot, and F. Logozzo. Precondition inference from intermittent assertions and application to contracts on collections. In VMCAI, 2011.
7. P. Cousot, R. Cousot, F. Logozzo, and M. Barnett. An abstract interpretation framework for refactoring with application to extract methods with contracts. In OOPSLA, 2012.
8. I. Dillig, T. Dillig, and A. Aiken. Automated error diagnosis using abductive inference. In PLDI, 2012.
9. B. Elkarablieh, S. Khurshid, D. Vu, and K. S. McKinley. Starc: static analysis for efficient repair of complex data. In OOPSLA, 2007.
10. M. Fahndrich. Static verification for Code Contracts. In SAS, 2010.
11. M. Fahndrich and K. R. M. Leino. Declaring and checking non-null types in an object-oriented language. In ACM OOPSLA, 2003.
12. M. Fahndrich and F. Logozzo. Static contract checking with abstract interpretation. In FoVeOOS, 2010.
13. Eclipse Foundation. Eclipse.texttthttp://eclipse.org, 2011.
14. A. Griesmayer, R. Bloem, and B. Cook. Repair of boolean programs with an application to c. In CAV, 2006.
15. C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10), 1969.
16. B. Jobstmann, A. Griesmayer, and R. Bloem. Program repair as a game. In CAV, 2005.
17. M. Jose and R. Majumdar. Cause clue clauses: error localization using maximum satisfiability. In PLDI, 2011.
18. V. Laviron and F. Logozzo. Subpolyhedra: A (more) scalable approach to infer linear inequalities. In VMCAI, 2009.
19. C. Le Goues, M. Dewey-Vogt, S. Forrest, and W. Weimer. A systematic study of automated program repair: Fixing 55 out of 105 bugs for$8 each. In ICSE, 2012.
20. B. Liskov and J. M. Wing. A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst., 16(6), 1994.
21. F. Logozzo, M. Barnett, P. Cousot, R. Cousot, and M. F\"ahndrich. A semantic integrated development environment. In OOPSLA Companion, 2012.
22. F. Logozzo and M. Fahndrich. Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. In SAC, 2008.
23. F. Logozzo and M. Fahndrich. Checking compatibility of bit sizes in floating point comparison operations. In 3rd workshop on Numerical and Symbolic Abstract Domains, ENTCS, 2011.
24. M. Martel. Program transformation for numerical precision. In PEPM, 2009.
25. B. Meyer. Applying "Design by Contract". IEEE Computer, 25(10):40--51, 1992.
26. Microsoft. Roslyn CTP. http://msdn.microsoft.com/en-us/roslyn, 2011.
27. J. H. Perkins, S. Kim, S. Larsen, S. P. Amarasinghe, J. Bachrach, M. Carbin, C. Pacheco, F. Sherwood, S. Sidiroglou, G. Sullivan, W.-F. Wong, Y. Zibin, M. D. Ernst, and M. Rinard. Automatically patching errors in deployed software. In ACM SOSP, 2009.
28. M. Pezzè, M. C. Rinard, W. Weimer, and A. Zeller. Self-repairing programs (Dagstuhl seminar 11062). Dagstuhl Reports, 1(2):16--29, 2011.
29. X. Rival. Understanding the origin of alarms in astrée. In SAS, 2005.
30. R. Samanta, J. V. Deshmukh, and E. A. Emerson. Automatic generation of local repairs for boolean programs. In FMCAD, 2008.
31. H. Samimi, M. Sch\"afer, S. Artzi, T. D. Millstein, F. Tip, and L. J. Hendren. Automated repair of html generation errors in php applications using string constraint solving. In ICSE, 2012.
32. N. Tillmann and J. de Halleux. Pex-white box test generation for .net. In TAP, 2008.
33. M. T. Vechev, E. Yahav, and G. Yorsh. Abstraction-guided synthesis of synchronization. In POPL, 2010.
34. Y. Wei, Y. Pei, C. A. Furia, L. S. Silva, S. Buchholz, B. Meyer, and A. Zeller. Automated fixing of programs with contracts. In ISSTA, pages 61--72, 2010.
35. W. Weimer, T. Nguyen, C. Le Goues, and S. Forrest. Automatically finding patches using genetic programming. In ICSE, 2009.
36. M. W. Whalen, P. Godefroid, L. Mariani, A. Polini, N. Tillmann, and W. Visser. Fite: future integrated testing environment. In FoSER, 2010.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification