Abstract
Java’s annotation mechanism allows us to extend its type system with non-null types. However, checking such types cannot be done using the existing bytecode verification algorithm. We extend this algorithm to verify non-null types using a novel technique that identifies aliasing relationships between local variables and stack locations in the JVM. We formalise this for a subset of Java Bytecode and report on experiences using our implementation.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Aiken, A.: Introduction to set constraint-based program analysis. Science of Computer Programming 35(2–3), 79–111 (1999)
Andreae, C., Noble, J., Markstrum, S., Millstein, T.: A framework for implementing pluggable type systems. In: OOPSLA, pp. 57–74. ACM Press, New York (2006)
Chalin, P., James, P.R.: Non-null references by default in Java: Alleviating the nullity annotation burden. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 227–247. Springer, Heidelberg (2007)
Chang, B.-Y.E., Leino, K.R.M.: Abstract interpretation with alien expressions and heap structures. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 147–163. Springer, Heidelberg (2005)
Chin, B., Markstrum, S., Millstein, T.: Semantic type qualifiers. In: PLDI, pp. 85–95. ACM Press, New York (2005)
Chin, B., Markstrum, S., Millstein, T., Palsberg, J.: Inference of user-defined type qualifiers and qualifier rules. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 264–278. Springer, Heidelberg (2006)
Cielecki, M., Fulara, J., Jakubczyk, K., Jancewicz, L.: Propagation of JML non-null annotations in Java programs. In: PPPJ, pp. 135–140. ACM Press, New York (2006)
Ekman, T., Hedin, G.: Pluggable checking and inferencing of non-null types for Java. Journal of Object Technology 6(9), 455–475 (2007)
Ernst, M.: Annotations on Java types. Java Specification Request (JSR) 308 (2007)
Fähndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: OOPSLA, pp. 302–312. ACM Press, New York (2003)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proc. PLDI, pp. 234–245. ACM Press, New York (2002)
Foster, J.S., Fähndrich, M., Aiken, A.: A theory of type qualifiers. In: Proc. PLDI, pp. 192–203. ACM Press, New York (1999)
Foster, J.S., Terauchi, T., Aiken, A.: Flow-sensitive type qualifiers. In: Proc. PLDI, pp. 1–12. ACM Press, New York (2002)
Goldberg, A.: A Specification of Java Loading and Bytecode Verification. In: Conference on Computer & Communications Security, pp. 49–58. ACM Press, New York (1998)
Hovemeyer, D., Pugh, W.: Finding more null pointer bugs, but not too many. In: Proc. PASTE, pp. 9–14. ACM Press, New York (2007)
Hovemeyer, D., Spacco, J., Pugh, W.: Evaluating and tuning a static analysis to find null pointer bugs. In: Proc. PASTE, pp. 13–19. ACM Press, New York (2005)
Leroy, X.: Java bytecode verification: algorithms and formalizations. Journal of Automated Reasoning 30(3/4), 235–269 (2003)
Lhoták, O., Hendren, L.J.: Context-sensitive points-to analysis: Is it worth it? In: Mycroft, A., Zeller, A. (eds.) CC 2006. LNCS, vol. 3923, pp. 47–64. Springer, Heidelberg (2006)
Lindholm, T., Yellin, F.: The Java Virtual Machine Specification, 2nd edn. The Java Series. Addison Wesley Longman, Inc., Amsterdam (1999)
Male, C., Pearce, D.J., Potanin, A., Dymnikov, C.: Java bytecode verification for @NonNull types. Technical report, Victoria University of Wellington (2007)
Palsberg, J., Schwartzbach, M.I.: Object-oriented type inference. In: Proc. OOPSLA, pp. 146–161. ACM Press, New York (1991)
Pearce, D.J., Kelly, P.H.J., Hankin, C.: Online cycle detection and difference propagation: Applications to pointer analysis. Software Quality Journal 12(4), 309–335 (2004)
Pearce, D.J., Kelly, P.H.J., Hankin, C.: Efficient field-sensitive pointer analysis for C. Transactions on Programming Languages and Systems 30(1) (2008)
Plevyak, J., Chien, A.A.: Precise concrete type inference for object-oriented languages. In: Proc. OOPSLA, pp. 324–340. ACM Press, New York (1994)
Pominville, P., Qian, F., Vallée-Rai, R., Hendren, L., Verbrugge, C.: A framework for optimizing Java using attributes. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol. 2027, pp. 334–554. Springer, Heidelberg (2001)
Rountev, A., Milanova, A., Ryder, B.G.: Points-to analysis for Java using annotated constraints. In: Proc. OOPSLA, pp. 43–55. ACM Press, New York (2001)
Smith, F., Walker, D., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 366–381. Springer, Heidelberg (2000)
Wang, T., Smith, S.F.: Precise constraint-based type inference for Java. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 99–117. Springer, Heidelberg (2001)
Zhang, Y., Nielson, F.: A scalable inclusion constraint solver using unification. In: King, A. (ed.) LOPSTR 2007. LNCS, vol. 4915, Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Male, C., Pearce, D.J., Potanin, A., Dymnikov, C. (2008). Java Bytecode Verification for @NonNull Types. In: Hendren, L. (eds) Compiler Construction. CC 2008. Lecture Notes in Computer Science, vol 4959. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78791-4_16
Download citation
DOI: https://doi.org/10.1007/978-3-540-78791-4_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78790-7
Online ISBN: 978-3-540-78791-4
eBook Packages: Computer ScienceComputer Science (R0)