Are you able to run a bisect?

Bisected: 83a33d3 is the first bad commit

/cc @randall77 as FYI

It looks like 83a33d3 changed the sequence of checks in sliceBoundsCheck from:

0 <= j
i <= j
0 <= k
j <= k
k <= cap(v)

to

k <= cap(v)
j <= k
i <= j

I've debugged the case above from encode.go:728, and prove needs to learn 0 <= j in order to eliminate the bounds check. Based on their similarities, I think this is the case with the other examples as well.

The bisected CL both removed and reordered the checks, and both changes would need to be reversed in order to make prove, as it is, able to remove the OpIsSliceInBounds. I need to look more at what prove needs to do to remove these going forward.

I fail to understand how the current code manages to check that j or k are non negative. @randall77?

For comparison, it seems like the jump from Go 1.11.5 to 1.12.1 removed three bounds checks, and added one in autogenerated code.

Also, for what it's worth, I'm not implying that this causes some benchmarks to get slower; I was just surprised by some bounds checks I could have sworn weren't there last cycle. Assuming it was an unintended regression, we probably want to fix it and add some tests.

The current checks are more correctly described as:

0 <= k <= cap(v)
0 <= j <= k
0 <= i <= j

The reason why we do these in reverse order is that the opcode we use to check 0 <= x <= y requires that y is nonnegative. In reverse order we bootstrap the nonnegativity down the chain.

@mvdan can you post assembly code for one of those occurrences before and after?

encoded.go:728 seems a case where we were potentially mis-removing a bound check:

encodedLen is an int and the compiler cannot know that it's a positive number, as it's returned by a function (I don't know if base64.StdEncoding.EncodedLen gets inlined, but even if it is, we still can't currently prove that the returned value is positive -- in fact, for very large numbers of len(s) it might become negative because of overflow).

Since encodedLen might effectively be negative, a bound check on e.scratch[:encodedLen] is required.

The same applies to scanner.go:151:

We can't remove the bound check here. It sounds weird that we're doing it in Go 1.12.1, though. I do get a out-of-bound error if I try to reproduce it:
https://play.golang.org/p/lZTXSEGOlaq

The current checks are more correctly described as:

@randall77, apologies, I should have been more precise. I didn't mean that to sound as broad as it did. More precisely: The explicit 0 <= j check in the SSA seems to have been removed by 83a33d3. Prior to that change, sliceBoundsCheck was inserting an OpGeq64 comparing, in this case, j to zero. After the change, no OpGeq64 is added. During the prove pass, there is no longer explicit evidence of that check, so prove can't remove the bounds check. See the SSA snippets below.

seems a case where we were potentially mis-removing a bound check:

@rasky, that was my first thought when I checked the examples. That's why I dug deeper, because it didn't seem like prove should have been removing those bounds checks. The inserted checks were ensuring those were non-negative. See SSA snippets below.

3cf89e5... the commit before the change.

v130 (?) = Const64 <int> [0] (~R0[int])
v153 (?) = Const64 <int> [64]
...
b29: ← b28 b27
    v151 (724) = Phi <int> v143 v150 (~R0[int], encodedLen[int])
    v154 (+725) = Leq64 <bool> v151 v153
If v154 → b31 b32 (725)
...
b31: ← b29
    v158 (+728) = OffPtr <*[64]byte> [40] v6
    // Here is the j >= 0 check
    // v151 is j, v130 is 0
    v161 (728) = Geq64 <bool> v151 v130
If v161 → b33 b34 (likely) (728)
...
b33: ← b31
Plain → b35 (728)

b34: ← b31 b35
    v163 (728) = StaticCall <mem> {runtime.panicslice} v125
Exit v163 (728)

b35: ← b33
    v165 (728) = IsSliceInBounds <bool> v151 v153
First → b36 b34 (likely) (728)

83a33d3... the commit

v153 (?) = Const64 <int> [64]
...
b29: ← b28 b27
    v151 (724) = Phi <int> v143 v150 (~R0[int], encodedLen[int])
    v154 (+725) = Leq64 <bool> v151 v153
If v154 → b31 b32 (725)
...
b31: ← b29
    v158 (+728) = OffPtr <*[64]byte> [40] v6
    v161 (728) = IsSliceInBounds <bool> v151 v153
If v161 → b33 b34 (likely) (728)

b32: ← b29
    v188 (+731) = Leq64 <bool> v151 v187
If v188 → b37 b38 (731)

Full ssa dumps
3cf89ssa
83a33dssa

Debug output from each:
3cf89prove.txt
83a33prove.txt

Perhaps you're right that the old compiler was buggy in these cases; I didn't investigate the details at all. If that's the case, and we fixed them without even noticing, we probably want to add a regression test.

@randall77, apologies, I should have been more precise. I didn't mean that to sound as broad as it did. More precisely: The explicit 0 <= j check in the SSA seems to have been removed by 83a33d3. Prior to that change, sliceBoundsCheck was inserting an OpGeq64 comparing, in this case, j to zero. After the change, no OpGeq64 is added. During the prove pass, there is no longer explicit evidence of that check, so prove can't remove the bounds check. See the SSA snippets below.

Right. It's partly just a matter of accounting: we're removing a j >= 0 check, which isn't classified as a bounds check (even though it is, really) and adding a 0 <= j <= cap check, which is classified as a bounds check. They are still both one instruction (although the latter needs cap in a register - maybe if we know j <= cap already we can optimize).

I See. What I'm understanding then:

OpIsSliceInBounds will ultimately be three instructions, each of which will check both the upper and lower bounds of one of i, j, k. The instruction used for each of those checks requires that the upper bound value be non-negative.

In the previous implementation, in addition to actually doing the bounds check, we needed to first check whether each upper bound value was non-negative. The non-negative check(s) was an additional OpGeq64 in the SSA, just before the OpSliceIsInBounds proper. Prove was learning from that additional op (which, like you said, is actually half of the bounds check) before arriving at the OpIsSliceInBounds, at which point it was legitimately able to remove the bounds check as a whole in the examples at hand.

In the current implementation, because we know that the cap(s) upper bound is guaranteed non-negative, we can bootstrap that guarantee down the chain of checks. That means the non-negative check is no longer necessary, and has therefore been removed. The slice bounds check, in it's entirety, is now represented by just the OpIsSliceInBounds in the SSA.

@randall77 As an aside because I'd like to learn more about it: which instruction do we use to check both the lower and upper bounds? Is it just done as an unsigned comparison?

OpIsSliceInBounds will ultimately be three instructions, each of which will check both the upper and lower bounds of one of i, j, k. The instruction used for each of those checks requires that the upper bound value be non-negative.

IsSliceInBounds is a single instruction. For s[i:j:k] we issue 3 of them:

   IsSliceInBounds k cap(s)
   IsSliceInBounds j k
   IsSliceInBounds i j

In the previous implementation, in addition to actually doing the bounds check, we needed to first check whether each upper bound value was non-negative. The non-negative check(s) was an additional OpGeq64 in the SSA, just before the OpSliceIsInBounds proper. Prove was learning from that additional op (which, like you said, is actually half of the bounds check) before arriving at the OpIsSliceInBounds, at which point it was legitimately able to remove the bounds check as a whole in the examples at hand.

In the current implementation, because we know that the cap(s) upper bound is guaranteed non-negative, we can bootstrap that guarantee down the chain of checks. That means the non-negative check is no longer necessary, and has therefore been removed. The slice bounds check, in it's entirety, is now represented by just the OpIsSliceInBounds in the SSA.

Exactly.

@randall77 As an aside because I'd like to learn more about it: which instruction do we use to check both the lower and upper bounds? Is it just done as an unsigned comparison?

Yes.

I think we can close this issue at this point - I spotted a potential prove regression, but after some discussion that doesn't seem to be the case. And this issue is pretty old now, so I don't think it's useful anymore. Thanks all for the digging :)