cmd/compile: for range loop reading past slice end

[greyhu]

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

1.13.5,1.14.6

Does this issue reproduce with the latest release?

yes!

What operating system and processor architecture are you using (go env)?

linux,amd64

What did you do?

try this in playground

package main
import "fmt"
func main() {
        rates:=[]int32{1,2,3,4,5,6}
	for star, rate := range rates {
		if star+1 < 1 {
			panic("")
		}

		fmt.Println(star, rate)
	}
}

What did you expect to see?

0,1
1,2
2,3
3,4
4,5
5,6

What did you see instead?

timeout running program
0 1
1 2
2 3
3 4
4 5
5 6
6 180344
7 192
8 4846592
9 0
10 180424
11 192
12 4846720
13 0
14 5822560
15 192
16 438224
17 192
18 4396406
19 0
20 385024
.....

[ALTree]

Thanks for the report. I can reproduce this on tip, too.

cc @randall77 @cherrymui

[ALTree]

(Tentatively labelling as a 1.15 release blocker, feel free to change)

[feilengcui008]

it seems that changing the line if star+1 < 1 { to if start+2 < 2 { (or other number not equal to 1) will work correctly.

[mariecurried]

This issue appears to have been introduced a while ago. According to bisection, commit b812eec seems to be the most likely culprit

[fancl20]

			// Check for i2 < max or max > i2.
 			var max *Value
 			if r == lt && pred.Control.Args[0] == i2 {
 				max = pred.Control.Args[1]
 			} else if r == gt && pred.Control.Args[1] == i2 {
 				max = pred.Control.Args[0]
 			} else {
 				continue
 			}

  			// Check condition 4 now that we have a
 			// candidate max. For this we can query the
 			// fact table. We "prove" min < max by showing
 			// that min >= max is unsat. (This may simply
 			// compare two constants; that's fine.)
 			ft.checkpoint()
 			ft.update(b, min, max, tr.d, gt|eq)
 			proved := ft.unsat
 			ft.restore()

  			if proved {
 				// We know that min <= i1 < max.
 				if b.Func.pass.debug > 0 {
 					printIndVar(b, i1, min, max, 1, 0)
 				}
 				ft.update(b, min, i1, tr.d, lt|eq)
 				ft.update(b, i1, max, tr.d, lt)
 			}

Here the condition is i2 < max and min < max. What we (think we) prove is min <= i1 < max.
The problem is when we put these together,

   i2 < max
-> i1 + 1 < max
-> i1 - min + 1 < max - min && i1 - min >= 0
-> 1 < max - min
-> min + 1 < max

min < max is actually not sufficient.

Here is another way to reproduce (similar to the test in that commit)

package main

func main() {
	i := 0
top:
	if i < 2 {
		i++
		if i < 1 {
			return
		}
		println(i)
		goto top
	}
}

[cherrymui]

Wow, thanks for reporting. Yeah, as you mentioned, this is related to the prove pass. Running with -gcflags=-d=ssa/prove/off gets the correct result.

cc @dr2chase

[toothrot]

Moving the milestone to 1.16, as this issue, while significant, is old enough not to block the 1.15 release at this point in the cycle. Please let me know if I am wrong.

[zdjones]

I'm going to take a crack at patching this in the morning (if noone else has gotten to it by then). It is late here, but my completely unconfirmed guess is that this loop has been compiled to OFORUNTIL (placing the increment and condition after the body) and func addLocalInductiveFacts, which is then trying to infer the loop induction variable by finding the OFORUNTIL pattern, is confusing the star +1 < 1 check with the loop's increment and condition. This would explain why star + 2 < 2 doesn't have the same effect, because any increment other then +1 will not be confused with the loop increment.

[gopherbot]

Change https://golang.org/cl/244579 mentions this issue: cmd/compile: don't add inductive fact if phi block have no direct edge to control block