Field-Sensitive Unreachability and Non-Cyclicity Analysis
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 states 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 use abstract interpretation to approximate the concrete semantics and an analysis framework based on constraint graphs, whose nodes are program points and whose arcs propagate information according to the semantics of each bytecode instruction. Our analysis has been designed with the goal of improving client analyses such as termination analysis, asserting the non-cyclicity of variables w.r.t. specific fields.