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.
This work was supported by the EPSRC under grant EP/DO32466/1 “Verification of the optimising phase of a compiler”.
Chapter PDF
References
Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Pearson Education, London (2007)
Bruneton, E., Lenglet, R., Coupaye, T.: ASM: a code manipulation tool to implement adaptable systems. In: Adaptable and Extensible Component Systems (2002)
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)
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)
Eclipse Foundation. Eclipse website (2009), http://www.eclipse.org
Ernst, M.D.: Type Annotations Specification (JSR 308), http://types.cs.washington.edu/jsr308/ (October 5, 2009)
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)
Hovemeyer, D., Pugh, W.: Finding bugs is easy. ACM SIGPLAN Notices 39(12), 92–106 (2004)
Kalvala, S., Warburton, R., Lacey, D.: Program transformations using temporal logic side conditions. ACM Transactions on Programming Languages and Systems (TOPLAS) 31(4) (2009)
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)
Lacey, D.: Program Transformation using Temporal Logic Specifications. PhD thesis, Oxford University Computing Laboratory (2003)
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)
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)
Muchnick, S.: Advanced Compiler Design and Implementation. Morgan Kaufmann, San Francisco (1997)
Odersky, M., Spoon, L., Venners, B.: Programming in Scala, 2nd edn. Artima Press (2010)
Samanta, R., Deshmukh, J.V., Emerson, E.A.: Automatic generation of local repairs for boolean programs. In: FMCAD (2008)
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)
Spieler, J.: UCDetector: the Unnecessary Code Detector website (2007), http://www.ucdetector.org
Steffen, B.: Generating data flow analysis algorithms from modal specifications. Science of Computer Programming 21, 115–139 (1993)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kalvala, S., Warburton, R. (2011). A Formal Approach to Fixing Bugs. In: Simao, A., Morgan, C. (eds) Formal Methods, Foundations and Applications. SBMF 2011. Lecture Notes in Computer Science, vol 7021. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25032-3_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-25032-3_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25031-6
Online ISBN: 978-3-642-25032-3
eBook Packages: Computer ScienceComputer Science (R0)