Field-sensitive unreachability and non-cyclicity analysis

•We model a novel and sound data-flow analysis for Java bytecode.•Our interprocedural definite analysis approximates two related heap properties.•Abstract Interpretation is used to soundly approximate the program semantics.•An abstract constraint graph of the program is built to compute the solution.•The final aim is to improve other analyses by also considering program fields.

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.