Field-sensitive static analyses of object-oriented code use approximations of the computational states where fields are taken into account, for better precision. This article presents a novel and sound definite analysis of Java bytecode that approximates two strictly related properties: field-sensitive unreachability between program variables and field-sensitive non-cyclicity of program variables. The latter exploits the former for better precision. We build a data-flow analysis based on constraint graphs, whose nodes are program points and whose arcs propagate information according to the semantics of each bytecode instruction. We follow abstract interpretation both to approximate the concrete semantics and to prove our results formally correct. Our analysis has been designed with the goal of improving client analyses such as termination analysis, asserting the non-cyclicity of variables with respect to specific fields.
Field-sensitive unreachability and non-cyclicity analysis
SCAPIN, ENRICO;SPOTO, Nicola Fausto
2014-01-01
Abstract
Field-sensitive static analyses of object-oriented code use approximations of the computational states where fields are taken into account, for better precision. This article presents a novel and sound definite analysis of Java bytecode that approximates two strictly related properties: field-sensitive unreachability between program variables and field-sensitive non-cyclicity of program variables. The latter exploits the former for better precision. We build a data-flow analysis based on constraint graphs, whose nodes are program points and whose arcs propagate information according to the semantics of each bytecode instruction. We follow abstract interpretation both to approximate the concrete semantics and to prove our results formally correct. Our analysis has been designed with the goal of improving client analyses such as termination analysis, asserting the non-cyclicity of variables with respect to specific fields.File | Dimensione | Formato | |
---|---|---|---|
FieldSensitiveUnreachability.pdf
accesso aperto
Tipologia:
Versione dell'editore
Licenza:
Dominio pubblico
Dimensione
1.22 MB
Formato
Adobe PDF
|
1.22 MB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.