Context

Some “managed” programming languages do automatic, compulsory range checks on array accesses, and invoke some kind of error condition if the array access is out of bounds. This is in contrast to C’ish languages where an out of bounds array access is undefined behavior (even though any sane container will at least assert on bad accesses).

Doing bounds checking on every array access can be expensive, however, and optimizing away redundant array bounds checks is crucial to achieving acceptable performance. To this end, compilers will sometimes split a loop’s iteration space (the values assumed by its induction variable) into sections where the range checks can be proved away and sections where it cannot. This can be a net win in cases where the actual iteration space the loop runs in has a large intersection with the section of the iteration space ranges checks were proved away for.

As an example, consider:

for (i = 0; i < n; i++)
  array[i] = -1;

If we split the loop’s iteration space this way:

len = length(array)
for (i = 0; i < min(n, len); i++)
  array[i] = -1;

for (i = min(n, len); i < n; i++)
  array[i] = -1;

the first loop provably requires no range checks. If n is always length(array) or smaller, the second loop does not run at all, and we’ve eliminated 100% of all range checks.

The Problem

To be able to split iteration spaces as shown above, we would like to derive the set of values of i for which expressions like array[a + b * i] provably pass the bounds check. Normally this is fairly simple arithmetic; but we’d like to consider programming languages with well-defined wrapping overflow semantics (i.e. INT32_MAX + 1 is INT32_MIN). Wrapping overflow semantics makes things difficult because certain basic arithmetic properties we all know and love do not apply – a < (b + 1) does not imply (a - 1) < b, for example. One way to deal with this complexity is to consider the possibility for overflow at every step and either show that it doesn’t happen or that it doesn’t matter. The aim of this post is to develop a different approach that I feel is more principled to think in.

This post does not constitute a proof, but I think it can be extended to be one with some effort.

Notation

We operate on bit machine integers, which really are elements of the set . is an element of (and hence an -tuple) all of whose elements are .

is a mapping from to . is interpreted as an integer in base 2. is injective (one-to-one), but not surjective (onto). is defined on all integers less than and greater than .

is a mapping from to . is interpreted as an integer in 2’s complement. is injective (one-to-one), but not surjective (onto). is defined on all integers less than and greater than .

The following are relations between and (i.e. a subset of )

  • is “signed less than”:
  • is “ or equal”:
  • is “unsigned less than”:
  • is “ or equal”:

We will use as the remainder function: is such that and for some .

The next two are functions from to

  • is wrapping binary addition:

  • is wrapping binary multiplication:

and “just work” on integers represented as twos complement which is brilliant but out of scope for this post.

The Problem

With the above notation, array[a + b * i] does not fail its bounds check if

where is length(array) and . The alternative, , is not interesting since in that case there are no solutions (a negative “length” is also nonsensical in the real world).

The solution set interpreted as integers represented in 2’s complement may not be a contiguous set – e.g. if is , the solution set for is

Solutions

Given that , we can write as

We let , and . Then, by definition of and , if is a solution to , then is a solution to and if is a solution to and is defined on then is a solution to .

We can “common out” the remainder operation:

The interesting thing to note is that is really a family of equations:

Since we are now in -land, we solve using standard arithmetic:

If then

If then

In any case, for every we have a range of values for that satisfy . If we denote the solution set for a given as a function of , then is periodic with an interval of . Thus we can compute the full solution set for as .

Given a set of solutions for , , we map them to solutions for and hence as follows:

  • If and then is a solution for

  • If and or then write as where . Note that if is a solution to then so is . Since is defined, it is a solution to .

Ranges

So far we’ve solved in terms of individual values. In some cases this set of values can be “easily” split into a union of ranges.

For example say for a given we have as a solution to . If such that and and then every such that is a solution to . If such that and and then every such that is a solution to . More such cases can easily be derived.

Being able to split the solution set into ranges is important because that is what allows us to break up a loop’s iteration space cheaply (i.e. with almost zero additional overhead).

Conclusion

I will end with some random notes:

  • It is probably possible to extend this approach to work with non-linear functions like array[a + b * i + c * i * i]. But I doubt that’s anything more than solely interesting on a theoretical level.

  • It will be nice to try to formalize some of this in Coq or Agda. I don’t think I currently have the chops to do that, though.

  • I have not really come across or tried to derive an algebra of comparison operators in a world with wrapping arithmetic. Perhaps there is a simpler approach on those lines I’m missing?