A non-null annotation inferencer for Java bytecode

ABSTRACT

We present a non-null annotations inferencer for the Java bytecode language. We previously proposed an analysis to infer non-null annotations and proved it soundness and completeness with respect to a state of the art type system. This paper proposes extensions to our former analysis in order to deal with the Java bytecode language. We have implemented both analyses and compared their behaviour on several benchmarks. The results show a substantial improvement in the precision and, despite being a whole-program analysis, production applications can be analyzed within minutes.

REFERENCES

• 1: Artho, C., and Havelund, K. Applying Jlint to space exploration software. In Proc. of the 5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2004) (2004), vol. 2937 of LNCS, Springer, pp. 297--308.
• 2: Cannasse, N., Turpin, T., Hubert, L., Besson, F., and André, E. JavaLib. Inria, March 2007. javalib.gforge.inria.fr.
• 3: Chalin, P., and James, P. R. Non-null references by default in Java: Alleviating the nullity annotation burden. In Proc. of European Conference on Object-Oriented Programming (ECOOP'07) (2007), vol. 4609 of LNCS, Springer, pp. 227--247.
• 4: David R. Chase , Mark Wegman , F. Kenneth Zadeck, Analysis of pointers and structures, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.296-310, June 1990, White Plains, New York, United States
• 5: Maciej Cielecki , Jȩdrzej Fulara , Krzysztof Jakubczyk , Łukasz Jancewicz, Propagation of JML non-null annotations in Java programs, Proceedings of the 4th international symposium on Principles and practice of programming in Java, August 30-September 01, 2006, Mannheim, Germany [doi>10.1145/1168054.1168073]
• 6: Cok, D. R., and Kiniry, J. R. Esc/java2.
• 7: Eclipse 3.3 (europa). www.eclipse.org.
• 8: Ekman, T. Extensible Compiler Construction. PhD thesis, Lund University, June 2006.
• 9: Ekman, T., and Hedin, G. Pluggable checking and inferencing of non-null types for Java. Journal of Object Technology 6, 9 (October 2007), 455--475. Special Issue: TOOLS EUROPE 2007.
• 10: Fähndrich, M., and Leino, K. R. M. Declaring and checking non-null types in an object-oriented language. In Proc. of the Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA'03) (2003), vol. 2021 of LNCS, Springer-Verlag, pp. 302--312.
• 11: Manuel Fahndrich , Songtao Xia, Establishing object invariants with delayed types, Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications, October 21-25, 2007, Montreal, Quebec, Canada
• 12: Cormac Flanagan , K. Rustan M. Leino, Houdini, an Annotation Assistant for ESC/Java, Proceedings of the International Symposium of Formal Methods Europe on Formal Methods for Increasing Software Productivity, p.500-517, March 12-16, 2001
• 13: The gnu compiler for the java programming language, 2007. gcc.gnu.org/java.
• 14: David Hovemeyer , William Pugh, Finding more null pointer bugs, but not too many, Proceedings of the 7th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.9-14, June 13-14, 2007, San Diego, California, USA [doi>10.1145/1251535.1251537]
• 15: David Hovemeyer , Jaime Spacco , William Pugh, Evaluating and tuning a static analysis to find null pointer bugs, ACM SIGSOFT Software Engineering Notes, v.31 n.1, January 2006
• 16: Laurent Hubert , Thomas Jensen , David Pichardie, Semantic Foundations and Inference of Non-null Annotations, Proceedings of the 10th IFIP WG 6.1 international conference on Formal Methods for Open Object-Based Distributed Systems, June 04-06, 2008, Oslo, Norway [doi>10.1007/978-3-540-68863-1_9]
• 17: Javacc. javacc.dev.java.net.
• 18: Jess. herzberg.ca.sandia.gov.
• 19: Julia. profs.sci.univr.it/~spoto/julia/.
• 20: Leino, K. R. M., Saxe, J. B., and Stata, R. ESC/Java user's manual, technical note 2000--002 ed. Compaq Systems Research Center, October 2000.
• 21: Leroy, X., Doligez, D., Garrigue, J., Rémy, D., and Vouillon, J. The Objective Caml system. Inria, May 2007. caml.inria.fr/ocaml/.
• 22: Male, C., Pearce, D. J., Potanin, A., and Dymnikov, C. Java bytecode verification for @NonNull types. In Proc. of the Conference on Compiler Construction (CC'08) (2008), Springer-Verlag.
• 23: Jon Meyer , Troy Downing, Java virtual machine, O'Reilly & Associates, Inc., Sebastopol, CA, 1997
• 24: Matthew M. Papi , Mahmood Ali , Telmo Luis Correa, Jr. , Jeff H. Perkins , Michael D. Ernst, Practical pluggable types for java, Proceedings of the 2008 international symposium on Software testing and analysis, July 20-24, 2008, Seattle, WA, USA [doi>10.1145/1390630.1390656]
• 25: O. Shivers, Control flow analysis in scheme, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation, p.164-174, June 20-24, 1988, Atlanta, Georgia, United States
• 26: SPEC JVM98 benchmarks. www.spec.org/jvm98.
• 27: Fausto Spoto, Nullness Analysis in Boolean Form, Proceedings of the 2008 Sixth IEEE International Conference on Software Engineering and Formal Methods, p.21-30, November 10-14, 2008 [doi>10.1109/SEFM.2008.8]
• 28: Tightvnc. www.tightvnc.com.
• 29: Raja Vallée-Rai , Phong Co , Etienne Gagnon , Laurie Hendren , Patrick Lam , Vijay Sundaresan, Soot - a Java bytecode optimization framework, Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research, p.13, November 08-11, 1999, Mississauga, Ontario, Canada

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Program analysis

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.5 Object-oriented Programming
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

General Terms:
Experimentation, Languages, Theory

Keywords:
Java, NonNull, annotation, inference, static analysis