Reachability Analysis of Program Variables

A variable v reaches a variable w if there is a path from the memory location bound to v to the one bound to w. This information is important for improving the precision of other static analyses, such as side-eects, field initialization, cyclicity and path-length, as well as of more complex analyses built upon them, such as nullness and termination. We present a provably correct constraint-based reachability analysis for Java bytecode. Our constraint is a graph whose nodes are program points and whose arcs propagate reachability information according to the semantics of bytecodes. The analysis has been implemented in the Julia static analyzer. Experiments that we performed on non-trivial Java and Android programs show an improvement of precision due to a reachability information, whose presence also reduces the cost of nullness and termination analyses.