Abstract:

Arrays are intensively used in many software programs, including the more popular graphics and game programming area. To support both safety and efficiency, it is important to deploy good techniques for removing redundant array bound checks. Although the problem of eliminating array bound checks has been studied for a long time, there are few work that attempt to be both aggressively precise and practical.
We propose an inference mechanism that achieves both aims by combining a forward relational analysis with a backward precondition derivation. Our inference algorithm works for a core imperative language with assignments, and analyses each method once through a summary-based approach. Through a novel technique that can strengthen preconditions, we can selectively reduce the sizes of our formulae to support a practical inference algorithm. Our inference is also precise as it is both path and context sensitive. Moreover, we subject each inferred program to a flexivariant specialization that can achieve good tradeoff between elimination of array checks and code explosion concerns. We have proven the soundness of our approach and have also implemented a prototype inference and specialization system. Initial experiments suggest that such a desired system is possible.

Paper: