Bounds Checking: An Instance of Hybrid Analysis

This paper presents an analysis for bounds checking of array sub-scripts that lifts checking assertions to program level under the form of an arbitrarily-complex predicate (inspector), whose run-time evaluation guards the execution of the code of interest. Sepa-rating the predicate from the computation makes it more amenable to optimization, and allows it to be split into a cascade of sufficient conditions of increasing complexity that optimizes the common-inspection path. While synthesizing the bounds checking invari-ant resembles type checking techniques, we rely on compiler sim-plification and runtime evaluation rather than employing complex inference and annotation systems that might discourage the non-specialist user. We integrate the analysis in the compiler’s reper-toire of Futhark: a purely-functional core language supporting map-reduce nested parallelism on regular arrays, and show how the high-level language invariants enable a relatively straightforward analy-sis. Finally, we report a qualitative evaluation of our technique on three real-world applications from the financial domain that indi-cates that the runtime overhead of predicates is negligible