Abstract
This experimental paper describes the implementation and evaluation of a static nullness analyser for single-threaded Java and Java bytecode programs, built inside the julia tool. Nullness analysis determines, at compile-time, those program points where the null value might be dereferenced, leading to a run-time exception. In order to improve the quality of software, it is important to prove that such situation does not occur. Our analyser is based on a denotational abstract interpretation of Java bytecode through Boolean logical formulas, strengthened with a set of denotational and constraint-based supporting analyses for locally non-null fields and full arrays and collections. The complete integration of all such analyses results in a correct system of very high precision whose time of analysis remains in the order of minutes, as we show with some examples of analysis of large software.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Eclipse.org Home, http://www.eclipse.org
Jlint, http://artho.com/jlint
Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)
Cok, D.R., Kiniry, J.: Esc/Java2: Uniting ESC/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108–128. Springer, Heidelberg (2005)
Cousot, P., Cousot, R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proc. of the 4th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1977), Los Angeles, California, USA, pp. 238–252. ACM, New York (1977)
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)
Flanagan, C., Leino, K.R.M.: Houdini, an Annotation Assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500–517. Springer, Heidelberg (2001)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended Static Checking for Java. In: Proc. of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2002), Berlin, Germany. SIGPLAN Notices, vol. 37(5), pp. 234–245. ACM, New York (May 2002)
Goetz, B., Peierls, T., Bloch, J., Bowbeer, J., Holmes, D., Lea, D.: Java Concurrency in Practice. Addison-Wesley, Reading (2006)
Hovemeyer, D., Pugh, W.: Finding More Null Pointer Bugs, but Not Too Many. In: Das, M., Grossman, D. (eds.) Proc. of the 7th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE 2007), San Diego, California, USA, pp. 9–14. ACM, New York (June 2007)
Hubert, L., Jensen, T., Pichardie, D.: Semantic Foundations and Inference of non-null Annotations. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 132–149. Springer, Heidelberg (2008)
Lindholm, T., Yellin, F.: The JavaTM Virtual Machine Specification, 2nd edn. Addison-Wesley, Reading (1999)
Palsberg, J., Schwartzbach, M.I.: Object-oriented Type Inference. In: Proc. of the 6th Annual Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 1991), Phoenix, Arizona, USA. ACM SIGPLAN Notices, vol. 26(11), pp. 146–161. ACM, New York (1991)
Papi, M.M., Ali, M., Correa, T.L., Perkins, J.H., Ernst, M.D.: Practical Pluggable Types for Java. In: Ryder, B.G., Zeller, A. (eds.) Proc. of the ACM/SIGSOFT 2008 International Symposium on Software Testing and Analysis (ISSTA 2008), Seattle, Washington, USA, pp. 201–212. ACM, New York (July 2008)
Rutar, N., Almazan, C.B., Foster, J.S.: A Comparison of Bug Finding Tools for Java. In: Proc. of the 15th International Symposium on Software Reliability Engineering (ISSRE 2004), Saint-Malo, France, pp. 245–256. IEEE Computer Society, Los Alamitos (November 2004)
Secci, S., Spoto, F.: Pair-Sharing Analysis of Object-Oriented Programs. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 320–335. Springer, Heidelberg (2005)
Spoto, F.: Nullness Analysis in Boolean Form. In: Proc. of the 6th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2008), Cape Town, South Africa, pp. 21–30. IEEE Computer Society, Los Alamitos (November 2008)
Spoto, F.: Precise null-Pointer Analysis. Software and Systems Modeling (to appear, 2010)
Spoto, F., Ernst, M.: Inference of Field Initialization. Technical Report UW-CSE-10-02-01, University of Washington, Department of Computer Science & Engineering (February 2010)
Spoto, F., Mesnard, F., Payet, E.: A Termination Analyser for Java Bytecode Based on Path-Length. ACM Transactions on Programming Languages and Systems (TOPLAS) 32(3) (March 2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Spoto, F. (2010). The Nullness Analyser of julia . In: Clarke, E.M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science(), vol 6355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17511-4_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-17511-4_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17510-7
Online ISBN: 978-3-642-17511-4
eBook Packages: Computer ScienceComputer Science (R0)