Precise null-pointer analysis

Precise null-pointer analysis (Citations: 4)


	BibTex \| RIS \| RefWorks Download

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 program 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 context-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 decision diagrams. For better precision, it identifies instance or static fields that remain always non-null after being initialised. Our experiments show this analysis faster and more precise 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 theoretically clean and its implementation strong and scalable. We subsequently improve that analysis by using local reasoning about fields that are not always non-null, but happen to hold a non-null value when they are accessed. This is a frequent situation, since programmers typically check a field for non-nullness before its access. We conclude with an example of use of our analyses to infer null-pointer annotations which are more precise than those that other inference tools can achieve.

Journal: Software and System Modeling - SOSYM , vol. 10, no. 2, pp. 219-252, 2011

DOI: 10.1007/s10270-009-0132-5

Cumulative Annual

View Publication

( www.springerlink.com )

( www.informatik.uni-trier.de )

- ...Julia’s nullness inference uses a notion of globally non-null fields, that are always initialized to a non-null value, in all constructors, before being read [22]...
- ...An earlier version of Julia’s nullness analysis [22] does no initialization analysis: the receiver of private methods are conservatively annotated with @Raw, but no variables, fields, or return values are annotated...
- ...This section presents an operational semantics for Java bytecode [22]...
- ...For comparison, these numbers are around 80% in the case of Nit [22]...
Fausto Spoto, et al. Inference of field initialization
- ...It is faster than julia, but this comes at the price of precision, since its latest version 0.5d is almost as precise as an old version of julia (see the experiments in [18]) that used only the techniques up to Subsection 3.2 of this paper...
- ...In particular, [17] reports a formal description and proofs of correctness for the techniques of Subsections 3.1 and 3.2; [18] includes the same for Subsection 3.3 also; [19] reports definitions and proofs for the rawness analysis of Section 4 and formalises the constraint-based techniques used in julia...
- ...This technique yields almost the same results as Nit ,a s the experiments in [18] show...
- ...In [18], a static analysis is coupled to that described in Subsection 3.2, which computes a set of definitely non-null fields at a given program point .T hislocal non-nullness information is performed through a denotational, bottom-up analysis of the program, which is proved correct in [18]...
- ...In [18], a static analysis is coupled to that described in Subsection 3.2, which computes a set of definitely non-null fields at a given program point .T hislocal non-nullness information is performed through a denotational, bottom-up analysis of the program, which is proved correct in [18]...
Fausto Spoto. The Nullness Analyser of julia
- ...To evaluate the resulting analysis framework, we instantiate it with five domains for pair-sharing [38], cyclicity [35], nullness [39, 41], class initialisation and size analysis of program variables [42, 43]...
- ...We implement our nullness analysis with the domain in [39], showing that the results are still more precise but the analysis becomes more expensive...
- ...All this material, including proofs, can be found in [41 ]a nd [39]...
- ...We discuss Java bytecode and hence by variable we mean both a local variable li and a stack element si ,w herei is the index of the local variable or the height of the stack element from the bottom s0. The abstract domain N for nullness analysis [39, 41] is made of Boolean formulas over ˇ v and ˆ v, for every variable v which is in scope at a given program point...
- ...See [39, 41] for an abstraction that considers exceptional output states also...
- ...The only conservative assumption is to leave the nullness of the new top of the stack undefined (see [41 ]a nd [39] for a better solution): getfield κ.f :t N = U ∧¬ ˇh...
- ... composition of denotations ; .I n the abstract semantics, the sequential composition of two formulas φ1 and φ2 is defined by renaming the output variables of φ1 and the input variables of φ2 into the same new set of fresh variables; the renamed formulas are then conjuncted (through ∧) and the new fresh variables are existentially quantified through Schröder elimination (hence removed from the resulting Boolean formula). See [41 ]a nd [39] ...
- ... which for the Java bytecode means local variables or stack elements, that share i.e., reach the same memory location; it is used for automatic program parallelisation and to support other analyses; 2. The second [35] over-approximates the set of cyclical program variables, those that reach a loop of memory locations; it needs a preliminary pair-sharing analysis; 3. The third, which comes in two versions of different precision [39, 41], ...
- ...JULIA computes a formula containing the conjunct ¬ ˆ s2 as abstract denotation for the blocks that precede, immediately, the calls to head.copy() in Fig. 1. This means that the top value of the stack just before those calls (i.e., their receiver) is never null .A recent evolution of the domain in [41], defined in [39], computes a formula containing also the conjunct ¬ ˆ s3 as abstract denotation for the block that precedes, ...
- ...getfield’s. Figure 11 also shows more precise nullness analyses performed with JULIA and the abstract domain in [39], that is able to spot locally non-null fields...
- ...The more precise nullness analysis in [39] is run by a medium nullness analysis...
Fausto Spoto, et al. Magic-sets for localised analysis of Java bytecode
- ...Julia performs a very precise nullness analysis for Java [4]...
- ...A basic analysis is strengthened with others, to get a high degree of precision [4]...
Étienne Payet, et al. Static Analysis of Android Programs