Solving Linear Range Checks
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 welldefined 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 (onetoone), 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 (onetoone), 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 nonlinear 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?