Precise null-pointer analysis

摘要

In Java, C or C++, attempts to dereference the null value result in an exception or a segmentation fault. Hence, it is important to identify those program points where this undesired behaviour might occur or prove the other pro gram points (and possibly the entire program) safe. To that purpose, null-pointer analysis of computer programs checks or infers non-null annotations for variables and object fields. With few notable exceptions, null-pointer analyses currently use run-time checks or are incorrect or only verify manually provided annotations. In this paper, we use abstract interpretation to build and prove correct a first, flow and con text-sensitive static null-pointer analysis for Java bytecode (and hence Java) which infers non-null annotations. It is based on Boolean formulas, implemented with binary deci sion diagrams. For better precision, it identifies instance or static fields that remain always non-null after being initial ised. Our experiments show this analysis faster and more pre cise than the correct null-pointer analysis by Hubert, Jensen and Pichardie. Moreover, our analysis deals with exceptions, which is not the case of most others; its formulation is the oretically clean and its implementation strong and scalable. We subsequently improve that analysis by using local reason ing about fields that are not always non-nul l, but happen to hold a non-null value when they are accessed. This is a fre quent situation, since programmers typically check a field for non-nullness before its access. We conclude with an exam ple of use of our analyses to infer null-pointer annotations which are more precise than those that other inference tools can achieve.