Deriving pre-conditions for array bound check elimination

Abstract. We present a high-level approach to array bound check op-timization that is neither hampered by recursive functions, nor disabled by the presence of partially redundant checks. Our approach combines a forward analysis to infer precise contextual constraint at designated pro-gram points, and a backward method for deriving a safety pre-condition for each bound check. Both analyses are formulated with the help of a practical constraint solver based on Presburger formulae; resulting in an accurate and fully automatable optimization. The derived pre-conditions are also used to guide bound check specialization, for the purpose of elim-inating partially redundant checks.