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 it's 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 constr...

• Type: Conference
• Year: 2009
• Where: SAS
• Authors: David Niedzielski, Jeffery von Ronne, Andreas Gampe, Kleanthis Psarris
• Keywords: Accesses Produce Runtime, Bounds Checks, Formal Methods, Lower Runtime Cost, SAS 2009