A Verifiable, Control Flow Aware Constraint Analyzer for Bounds Check Elimination

The Java programming language requires that out-of-bounds array accesses produce runtime exceptions. In general, this requires a dynamic bounds check each time an array element is accessed. However, if it can be proven that the array index does not exceed the bounds of the array, then the bounds check can be eliminated. We present a new algorithm based on extended Static Single Assignment (eSSA) form that builds a directed, weighted inequality graph representing control flow qualified, linear constraints among program variables derived from program statements. Our system then employs a customized depth-first search exploration algorithm to reason about relationships among variables, and provides a verifiable proof of its conclusions. This proof can be passed to and verified by a runtime system to minimize the run time performance impact of this analysis. Our system is novel in several respects. It takes into consideration both control flow and data flow when analyzing the constraint system; it handles general linear inequalities instead of simple difference constraints; and it provides verifiable proofs for its claims. We present experimental results which demonstrate that this method eliminates more bounds checks, and when combined with runtime verification, results in a lower runtime cost than prior work. Overall, this method improves performance by up to about 10% on the reported benchmarks.