Identifying Unnecessary Bounds Checks Through Block-Qualified Variable Elimination




von Ronne, Jeffery

Journal Title

Journal ISSN

Volume Title


UTSA Department of Computer Science


Java’s memory-safety relies on the Java Virtual Machine checking that each access to an array does not exceed the bounds of that array. When static analysis can determine that some array access instruction will never use an out of bounds index, the cost of dynamically checking the index each time the instruction is executed can be avoided.

This report introduces Block-Qualified Variable Elimination (BQVE) as a program analysis technique that extends Fourier-Motzkin Elimination [5, 3], so that it can be applied directly to programs in Static Single Assignment Form (SSA) [2] in order to determine whether array accesses of such programs are in bounds. This is accomplished by performing the variable elimination on a constraint system, where each constraint consists of a linear inequality the program’s variables and a block-validity qualifier that specifies in what program regions the linear inequality holds. Additional modifications handle SSA’s φ-functions.

In summary, the BQVE algorithm works as follows: BQVE operates on SSA programs for which a control flow graph and a dominator tree have been computed. From such a program, a set of block-qualified linear program constraints consistent with the program’s semantics is extracted from the program code. These constraints are combined with additional constraints derived from properties that are to be tested (e.g., that a particular array access never exceeds its upper bounds) to form a system of constraints. The BQVE algorithm then operates by eliminating non-φ variables from the constraint system and introducing new constraints derived from the old constraints that involved the eliminated variables or were related to φ-functions. After all variables have been eliminated and the φ-functions have been processed, the resulting constraint system can be examined to determine whether the property in question holds.

The BQVE algorithm described here is simpler and more precise than our previous Constraint Analysis System (CAS) algorithm [6]. The main differences from the prior CAS algorithm is the use of block-validity qualifiers (as described in Section 4) instead of CAS’s direction flags to limit the validity of constraints and BQVE’s explicit representation of constraints holding for φ-functions on different predecessor blocks allowing for more constraints to be discovered to hold on φ-result variables (Section 6).

The concepts underlying the BQVE algorithm are presented the following sections, and a full specification of the algorithm is found in Appendix A.





Computer Science