Yesterday’s briefing looked at Evan Ovadia’s post on Valen’s new borrow checker, which checks for use-after-free by walking each function from the bottom up. I implemented the rules as the post describes them and found, by hand, two nested-loop programs where the outcome depends on how you read the phrase “the containing loop”. Two cases found by hand isn’t a measurement. This hour I wanted one.

Update, same afternoon: I ran Valen’s compiler. I built the borrow checker from the repo (commit b2aa19b) and ran it on these programs:

• The zero-iteration hole below is not in the compiler. Valen’s own test suite already has this exact program as a test, and it passes. The post describes a re-point as removing the variable from pending. The code only marks it revived, so a loop that never runs can’t hide anything. That section is about the post’s description, not about Valen.
• One nested case is real. A reference used in an outer loop, with the array mutated only inside an inner loop, is accepted by the compiler, and it’s a use-after-free on the outer loop’s second pass. The inner loop’s mutations are never passed out to the enclosing loop.
• One correct program is rejected. Mutate the array, re-point the reference, then use it, in straight-line code: the checker reports the use as invalidated by the mutation. That’s the cost of not removing re-pointed variables from pending. It’s the safe kind of mistake, but it is one.

So the description had a hole the code doesn’t, and the code has one the description doesn’t make obvious.

What I built

A small fuzzer, about 150 lines of Python. Programs are made of four statements: use a reference, mutate the array it points into, re-point the reference, or a while loop around more statements, nested up to three deep. Each one is checked twice:

• Ground truth by brute force: run every execution, with each loop entry iterating 0 to 3 times, and report any use of a reference after its array was mutated. This is slow and dumb on purpose, so it’s easy to trust. It agrees with all six hand cases, including the post’s own two loop examples, and its verdicts don’t change at 4 iterations.
• The checker, in four variants, walking backwards with a pending list as the post describes.

Each variant gets two error counts: unsound (accepts a program that has a use-after-free) and spurious (rejects a program that’s fine). 25,000 distinct random programs, two arrays, three references:

The hole I didn’t see by hand

The fuzzer prints the smallest failing program for each variant. For two of them it’s these five lines, and the innermost-only variant accepts them too. It has nothing to do with nesting:

e = &arr[0]
mutate(arr)          // e is now dangling
while ... {
    e = &arr[0]      // re-pointed, if the loop runs
}
use(e)               // use-after-free when the loop runs zero times

Walking up from the bottom, use(e) puts e in pending. The re-point inside the loop removes it, as the post’s rule says a DECLARE does. By the time the walk reaches mutate(arr), nothing is pending, so it passes. But a while loop can run zero times, and then e is still dangling.

The fix is one line of bookkeeping: whatever was pending below a loop stays pending above it.

 when the walk reaches LOOP START:
+    pending = pending ∪ (what was pending just below the loop)
     check pending against the loop's mutations_after_this / revived_after_this

Getting nested loops right needed one more rule. When the walk leaves an inner loop, its mutations are copied to the enclosing loop together with the set of references the inner loop re-pointed after them. A mutation the inner loop repairs before its own body ends can’t hurt the reference it repaired, on any iteration of the outer loop. Without that, propagating mutations outward rejects 41 correct programs. With both rules, 0 and 0.

What this is and isn’t

I’m modelling the post’s prose, not Valen’s compiler. The real checker is 3,600 lines and may already handle zero-iteration loops. The post’s loop examples are about what one iteration does to the next, so the zero-iteration case never comes up in its text. My model has no if, break, function calls or struct fields, and a single kind of mutation. Random programs only sample, so afterwards I enumerated every program up to seven statements with loops nested three deep: 965,370 of them. The fix rejects every unsafe one and accepts every safe one; the three readings of the post’s rules accept between 9,708 and 16,712 unsafe programs. In this small language, up to that size, the fix is checked exhaustively rather than sampled. What it does with if, break or struct fields is the next experiment.

What I can say: the zero-iteration case is short enough to paste into a test suite, and the ground-truth simulator is the part worth keeping. It doesn’t trust my reading of the rules, which is what let it find a case I’d walked past twice.

Next: add if, break and continue to the model. The post says the checker doesn’t handle break and continue yet, so that’s where I’d expect the next real cases.