In Java, C or C++, attempts to dereference the nil value result in anexception or a segmentation fault. Hence it is importantto identify those program points where this undesired behaviourmight occur or provethe other program points (and possibly the entire program) safe.To that purpose,null-pointer analysis of computer programs checks or infers non-nil annotationsfor variables and object fields. With few notable exceptions, null-pointeranalyses currently use run-time checks or are incorrect or only verifymanually provided annotations. In this paper, we use abstract interpretationto build and prove correct a first, flow and context-sensitivestatic null-pointer analysis for Javabytecode (and hence Java) which infers non-nil annotations. It isbased on Boolean formulas, implemented with binary decisiondiagrams. For better precision, it identifies instance or static fieldsthat remain emph{always} non- il after being initialised.Our experiments show this analysis faster and more precise than the correctnull-pointer analysis by Hubert, Jensen and Pichardie.Moreover, our analysis deals with exceptions, which isnot the case of most others; its formulation istheoretically clean and its implementation strong and scalable.We subsequently improve that analysis by using local reasoning about fieldsthat are not always non-nil,but are actually non- il when they are accessed.This is a frequent situation, since programmers typically checks fornon-nullness of a field before the access. This second,improved analysis is highly precise.We conclude with an example of use of our analyses to infernull-pointer annotations which are more precise than those that otherinference tools can achieve.

Precise Null-Pointer Analysis

SPOTO, Nicola Fausto
2011-01-01

Abstract

In Java, C or C++, attempts to dereference the nil value result in anexception or a segmentation fault. Hence it is importantto identify those program points where this undesired behaviourmight occur or provethe other program points (and possibly the entire program) safe.To that purpose,null-pointer analysis of computer programs checks or infers non-nil annotationsfor variables and object fields. With few notable exceptions, null-pointeranalyses currently use run-time checks or are incorrect or only verifymanually provided annotations. In this paper, we use abstract interpretationto build and prove correct a first, flow and context-sensitivestatic null-pointer analysis for Javabytecode (and hence Java) which infers non-nil annotations. It isbased on Boolean formulas, implemented with binary decisiondiagrams. For better precision, it identifies instance or static fieldsthat remain emph{always} non- il after being initialised.Our experiments show this analysis faster and more precise than the correctnull-pointer analysis by Hubert, Jensen and Pichardie.Moreover, our analysis deals with exceptions, which isnot the case of most others; its formulation istheoretically clean and its implementation strong and scalable.We subsequently improve that analysis by using local reasoning about fieldsthat are not always non-nil,but are actually non- il when they are accessed.This is a frequent situation, since programmers typically checks fornon-nullness of a field before the access. This second,improved analysis is highly precise.We conclude with an example of use of our analyses to infernull-pointer annotations which are more precise than those that otherinference tools can achieve.
2011
Null-pointer analysis; static analysis; abstract interpretation; automatic software verification
File in questo prodotto:
File Dimensione Formato  
PreciseNull-pointerAnalysis.pdf

solo utenti autorizzati

Tipologia: Versione dell'editore
Licenza: Accesso ristretto
Dimensione 1.99 MB
Formato Adobe PDF
1.99 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/332032
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 28
  • ???jsp.display-item.citation.isi??? 19
social impact