cmd/compile: bounds check elimination for len(x) - 1

[aclements]

What version of Go are you using (go version)?

go version devel +1a9f27d503 Thu Jan 4 02:17:33 2018 +0000 linux/amd64

Does this issue reproduce with the latest release?

Yes.

What did you do?

package main

var x []int

func main() {
	if n := len(x); n > 0 {
		x[n-1] = 0
	}
}

What did you expect to see?

There should be no bounds check for x[n-1].

What did you see instead?

There is a bounds check.

This comes up in practice for two reasons:

1. The range loop construction @dr2chase experimented with to eliminate the out-of-bounds pointer produces exactly this sort of pattern, which in turn causes additional bounds checks to be produced.

2. This pattern appears in runtime.newdefer, which must be recursively go:nosplit. I'm adding a static check of this for cmd/compile, runtime: add and use go:nosplitrec compilation directive #21314. Unfortunately, while I can see that the generated call to panic here can't happen dynamically, the linker can't, so the static check fails. I can contort the code to the following, but it would be nicer if I didn't have to:

	if n := len(x) - 1; n >= 0 && n < len(x) {
		x[n-1] = 0
	}

/cc @dr2chase

[aclements]

In general the prove pass doesn't know about arithmetic, but I wonder if it could cover several more cases if we just taught it about n-1 and n+1. In particular:

n > m   ==> n-1 >= m
n+1 > m ==> n >= m
n < m   ==> n+1 <= m
n-1 < m ==> n <= m

If I understand the pass correctly, cases 2 and 4 could be done by adding the RHS to the fact set if we see the LHS. Cases 1 and 3 could be done by looking for the LHS in the fact set if we're trying to prove the RHS.

I went down this path because of another similar case:

package main

var x []int

func main() {
	if len(x) < cap(x) {
		x = append(x, 1)
	}
}

In this case, we fail to eliminate the growslice path of append because the lowering generates a condition of the form len(x) + 1 > cap(x). As an experiment, I modified the append lowering for the case of a single argument to produce len(x) >= cap(x) and the prove pass was able to eliminate the growslice.

[aclements]

Hmm. Those implications are enough for the append case, but not quite enough for the original case. You can use them to prove n-1 >= 0, but not to prove n-1 < len(x). For that you need a slightly stronger condition because of wrap-around: n <= m && n > min ==> n-1 < m (where min is the minimum value representable by n). In other words, to prove n-1 < len(x), you need to prove both that n > min (which follows from n > 0 and that n <= len(x) (which follows from n == len(x)). It looks like the facts table tracks relations with constants, too, so I think this is actually pretty easy.

The full set of pseudo-inverses is:

n-1 >= m && n > min ==> n > m
n >= m   && n < max ==> n+1 > m
n+1 <= m && n < max ==> n < m
n <= m   && n > min ==> n-1 < m

[gopherbot]

Change https://golang.org/cl/87478 mentions this issue: cmd/compile: make prove pass use unsatisfiability

[gopherbot]

Change https://golang.org/cl/87477 mentions this issue: cmd/compile: simplify limit logic in prove

[gopherbot]

Change https://golang.org/cl/87480 mentions this issue: cmd/compile: add fence-post implications to prove

[dgryski]

In dgryski/go-metro@1308eab I got a major performance boost by changing the loop to remove the reassignments to ptr which, even though they were still within range, I assume invalidated somehow the bounds checks for that were valid for ptr before the assignment. Does the new prover handle this case? Should it?

[aclements]

@dgryski, unfortunately the new prover still won't understand this. I taught it about x+1 and x-1 in some very limited cases, but in general the prover doesn't do arithmetic. For example, going into the loop, it knows that len(ptr) >= 32, but when it sees the effective len(ptr1) = len(ptr) - 8 caused by the slice, it can't follow the subtraction, so it doesn't know that that implies len(ptr1) >= 24. It's an interesting test case, though. You could file a bug if you haven't already, though I don't know if/when we'd get to it.

(I did spend a while thinking about how to teach it more generally about x ± C, but since it's on a modular ring, it gets really complicated really fast.)

[dr2chase]

You can work with the modular ring, but it requires additional facts to prove that x ± C doesn't "go around" the ring.

[aclements]

Then you're not really working with the modular ring. :) I mostly worked out a way to do with it general intervals on the modular ring (including intervals that wrapped). It had some nice properties, like supporting any fact of the form "x ± C op y ± D" in both signed and unsigned under one unified umbrella, but that umbrella got quite complicated so I didn't finish working out all the details.