cmd/compile: possible prove pass bug

[randall77]

func gcd(a, b uint32) uint32 {
	for b != 0 {
		a, b = b, a%b
	}
	return a
}

This doesn't actually compile to incorrect code yet, but it gets close.

The crux of the problem is that we have the rule that, given r := a%b, we can derive r < b (in the unsigned domain). Which at first looks reasonable. But reading it "backwards" causes trouble: r < b => b > r => b > 0 => b != 0. But that's the loop condition, implying that we don't actually need to do the loop test.

The implication above can only really be relied upon after the modulo operation runs (and thus panics, if b==0). Fortunately for us that's how the current compiler happens to use this information. But it isn't scoped to "after" in the current prove pass, so it is something of a ticking time bomb.

Filing for my own use for later. I'm rewriting some of this code.

[Jorropo]

But it isn't scoped to "after" in the current prove pass, so it is something of a ticking time bomb.

I'm missing why this is a problem, the front-end generate zero-checks branches proving b:

func gcd(a, b uint32) uint32 {
	for b != 0 {
		if b == 0 { runtime.panicdivide() }
		// at this point we already proved b != 0
		a, b = b, a%b
	}
	return a
}

When I wrote that code I assumed it was UB to call Mod(64|32|16|8)u with a zero divisor and should be impossible unless there is a frontend bug.

But that's the loop condition, implying that we don't actually need to do the loop test.

Isn't the loop condition r != 0 ?

if (Phi .Entry(b) .Loop(b_r)) != 0 { goto .Loop }

What am I missing here ?

[randall77]

I think the missing piece is that the rule that says r < b (which implies b != 0) applies across the entire function. Including before the loop even starts. So the fact that the loop condition even gets tested, instead of just assumed always true, is just an accident of missed optimization.

[Jorropo]

Hum, I wasn't aware it could backprop inferences like this, I thought this would only be applied during DFS.
This looks like this needs to ran during the scan stage while doing DFS instead of ahead. Are you gonna send a fix ?

[randall77]

Yes, I think the right fix is to apply/remove it during DFS, at the point of the modulo (or maybe the block after? I'm not sure).
I think the first step though is to actually find a program that fails because of this. I ran into it after doing some pretty extensive modifications, so I'm not sure if it is actually triggerable currently.

I plan on revamping much of this pass for 1.24, so if there isn't a demonstrable bug, it can just wait and may become obsolete.

[randall77]

This should be fixed with the new prove pass implementation.