Week 2 · Lesson 3
Proving bounds
The syllabus says loads and stores are "bounds checked to never be out of range". Our compiler doesn't check at run time. It proves, before anything runs, that every view is inside its memory, using the interval analysis you built for symbolic simplification in lesson 1.4.
The rule
For shrink m off shape=[k], where the parent m has n elements (k counts as 1 for shape=[]), work out the interval [lo, hi] of off, then require:
lo ≥ 0 and hi + k ≤ nThe first says the window can't start before the parent. The second says that even at its largest offset, the window still ends inside. The allowed offsets are exactly [0, n - k], and the whole interval of off has to sit inside that range.
With a constant offset the interval is a single point, so this is the plain check from lesson 1. It gets interesting when the offset is computed.
Loaded values are unknown
A value loaded from memory could be anything, because memory comes from outside. Its interval is the full i32 range. So this gather, which reads an index from one buffer and uses it on another, is invalid, even if the data happens to hold a small number:
%i0 = shrink %ix 0 shape=[]
%i = load %i0 # interval: [INT_MIN, INT_MAX]
%src = shrink %d %i shape=[] # can't prove 0 ≤ %i ≤ 3To make it valid you shape the interval with ops whose bounds you can compute, the rules from lesson 1.4 (plus one it didn't cover: a where's interval is the union of its two branches). We write nested forms like mod (max %i 0) 4 as shorthand, but in a .uir file each op is its own statement. Step through: the green line is the allowed range [0, n - k], and the thick line is the offset's interval.
In C you'd write if (i < 4) x = d[i];. The .uir equivalent, where (cmplt %i 4) %i 0, doesn't help: the bounds of a where are the union of both branches, so the interval is still everything %i could be. The analysis doesn't look at the condition. The oracle rejects where (cmplt %i 4) (max %i 0) 0 with an offset interval of [0, 2147483647].
A gather the compiler can prove
Slot 0 is four i32s of data, slot 1 holds one index, and slot 2 is a one-element result. Set res[0] = d[i] for the index i in ix[0]: a negative i reads d[0], and any other i reads d[i mod 4]. The starter is the natural first try, and the compiler rejects it.
Offsets add up, and so do intervals
A view of a view is checked against its own parent. An offset built from arithmetic is checked with the interval rules for that arithmetic: add adds the endpoints when nothing can wrap. With an 8-element buffer:
%m = max %i 0
%k = mod %m 4 # [0, 3]
%o = add %k 4 # [4, 7]: fits shape=[] on 8 elements
%p = add %k 5 # [5, 8]: 8 + 1 > 8, invalidYou can also cut the window first and index inside it: shrink %b 4 shape=[4], then shrink that by %k. The inner view only has to fit the four-element window, and [0, 3] does.
Your analysis doesn't have to find the tightest interval. A looser interval only means you reject some programs that were actually fine. A wrong interval, one that leaves out a value the offset can really take, means your compiler accepts a program that reads outside its memory. When in doubt, widen to the full range.
Bounds of x mod m
Write mod_bounds (lo, hi) m for m > 0, with C's rule that the result has the sign of x. A non-negative x gives a result in [0, min (m-1) x], and a negative one gives [max (-(m-1)) x, 0]. Use only these two facts, and return the smallest interval they allow for every x in [lo, hi]. So mod_bounds (5, 5) 4 is (0, 3), not (1, 1): the facts only say a non-negative x lands in [0, min 3 5].
The course's oracle uses the looser [-(m-1), m-1] whenever x can be negative. Both are correct.
Check yourself
What's the interval of %i = load %e, where %e is a view of a buffer whose data is [3 1 2 0]?
Is the data part of the program, or does it come from outside?
Memory is input: the same kernel runs on whatever data the caller passes. The data=[...] in a test file is just one possible input, so a loaded value gets the full i32 range.
What's the interval of mod %i 4 when %i is a loaded value? Write it as [lo, hi].
In C (and in .uir), the sign of mod follows the left operand.
%i can be negative, and then %i mod 4 is in [-3, 0]. Together with the non-negative side that's [-3, 3], which still can't be an offset.
On a buffer of 4 elements, what's the largest m for which shrink %b (mod (max %i 0) m) shape=[2] can be proven in bounds?
The allowed offsets are [0, n - k]. What's n - k here?
mod (max %i 0) m is [0, m - 1].
A two-element window on four elements can start at 0, 1, or 2, so hi must be at most 2. [0, m - 1] fits when m - 1 ≤ 2, so m = 3. With m = 4 the oracle reports offset [0, 3], which doesn't fit.
Why doesn't where (cmplt %i 4) (max %i 0) 0 give a provable index for a 4-element buffer?
What are the intervals of the two branches?
The branches are [0, INT_MAX] and [0, 0], so the union is [0, INT_MAX]. Interval analysis doesn't learn anything from the condition. Shape the value itself with max and mod instead.
On an 8-element buffer, %k is in [0, 3]. Which offset works for a shape=[] view?
Work out each interval and compare it with [0, 7].
add %k 4 is [4, 7], inside [0, 7]. add %k 5 reaches 8, add %k -1 reaches -1, and mul %k 3 reaches 9.
For shape=[k] on a parent of n elements, the offset's whole interval must fit inside [0, ?]. What goes in place of the question mark?
The window's last element is at off + k - 1, and that must be at most n - 1.
off + k - 1 ≤ n - 1 means off ≤ n - k, which is the same as the rule hi + k ≤ n.