Advertisement

A Formal Approach to Fixing Bugs

  • Sara Kalvala
  • Richard Warburton
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7021)

Abstract

Bugs within programs typically arise within well-known motifs, such as complex language features or misunderstood programming interfaces. Some software development tools often detect some of these situations, and some integrated development environments suggest automated fixes for some of the simple cases. However, it is usually difficult to hand-craft and integrate more complex bug-fixing into these environments. We present a language for specifying program transformations which is paired with a novel methodology for identifying and fixing bug patterns within Java source code. We propose a combination of source code and bytecode analyses: this allows for using the control flow in the bytecode to help identify the bugs while generating corrected source code. The specification language uses a combination of syntactic rewrite rules and dataflow analysis generated from temporal logic based conditions. We demonstrate the approach with a prototype implementation.

Keywords

Source Code Model Check Temporal Logic Java Program Side Condition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in to check access.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Pearson Education, London (2007)zbMATHGoogle Scholar
  2. 2.
    Bruneton, E., Lenglet, R., Coupaye, T.: ASM: a code manipulation tool to implement adaptable systems. In: Adaptable and Extensible Component Systems (2002)Google Scholar
  3. 3.
    Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems 8, 244–263 (1996)CrossRefzbMATHGoogle Scholar
  4. 4.
    Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, Workshop, pp. 52–71. Springer, London (1982)CrossRefGoogle Scholar
  5. 5.
    Eclipse Foundation. Eclipse website (2009), http://www.eclipse.org
  6. 6.
    Ernst, M.D.: Type Annotations Specification (JSR 308), http://types.cs.washington.edu/jsr308/ (October 5, 2009)
  7. 7.
    Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Science of Computer Programming 69(1-3), 35–45 (2007)CrossRefzbMATHGoogle Scholar
  8. 8.
    Hovemeyer, D., Pugh, W.: Finding bugs is easy. ACM SIGPLAN Notices 39(12), 92–106 (2004)CrossRefGoogle Scholar
  9. 9.
    Kalvala, S., Warburton, R., Lacey, D.: Program transformations using temporal logic side conditions. ACM Transactions on Programming Languages and Systems (TOPLAS) 31(4) (2009)Google Scholar
  10. 10.
    Kanade, A., Sanyal, A., Khedker, U.: A PVS based framework for validating compiler optimizations. In: SEFM 2006: Proceedings of the Fourth IEEE International Conference on Software Engineering and Formal Methods. IEEE Computer Society, Washington, DC (2006)Google Scholar
  11. 11.
    Lacey, D.: Program Transformation using Temporal Logic Specifications. PhD thesis, Oxford University Computing Laboratory (2003)Google Scholar
  12. 12.
    Lerner, S., Millstein, T., Chambers, C.: Automatically proving the correctness of compiler optimizations. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation. ACM Press, New York (2003)Google Scholar
  13. 13.
    Lerner, S., Millstein, T., Rice, E., Chambers, C.: Automated soundness proofs for dataflow analyses and transformations via local rules. In: POPL 2005: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 364–377. ACM Press, New York (2005)Google Scholar
  14. 14.
    Muchnick, S.: Advanced Compiler Design and Implementation. Morgan Kaufmann, San Francisco (1997)Google Scholar
  15. 15.
    Odersky, M., Spoon, L., Venners, B.: Programming in Scala, 2nd edn. Artima Press (2010)Google Scholar
  16. 16.
    Samanta, R., Deshmukh, J.V., Emerson, E.A.: Automatic generation of local repairs for boolean programs. In: FMCAD (2008)Google Scholar
  17. 17.
    Schmidt, D.A., Steffen, B.: Data-flow analysis as model checking of abstract interpretations. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  18. 18.
    Spieler, J.: UCDetector: the Unnecessary Code Detector website (2007), http://www.ucdetector.org
  19. 19.
    Steffen, B.: Generating data flow analysis algorithms from modal specifications. Science of Computer Programming 21, 115–139 (1993)CrossRefzbMATHGoogle Scholar
  20. 20.
    Warburton, R., Kalvala, S.: From specification to optimisation: An architecture for optimisation of Java bytecode. In: de Moor, O., Schwartzbach, M.I. (eds.) CC 2009. LNCS, vol. 5501, pp. 17–31. Springer, Heidelberg (2009)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Sara Kalvala
    • 1
  • Richard Warburton
    • 1
  1. 1.Department of Computer ScienceUniversity of WarwickUK

Personalised recommendations

Cite paper

Buy options