cmd/compile: rewrite the constant parts of the prove pass

Handles a lot more cases where constant ranges can eliminate
various (mostly bounds failure) paths.

Fixes #66826
Fixes #66692
Fixes #48213
Update #57959

TODO: remove constant logic from poset code, no longer needed.

Change-Id: Id196436fcd8a0c84c7d59c04f93bd92e26a0fd7e
Reviewed-on: https://go-review.googlesource.com/c/go/+/599096
Reviewed-by: David Chase <drchase@google.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Michael Knyszek <mknyszek@google.com>

src/cmd/compile/internal/ssa/func.go

@@ -796,7 +796,7 @@ func (f *Func) invalidateCFG() {
 //	base.DebugHashMatch(this function's package.name)
 //
 // for use in bug isolation.  The return value is true unless
-// environment variable GOSSAHASH is set, in which case "it depends".
+// environment variable GOCOMPILEDEBUG=gossahash=X is set, in which case "it depends on X".
 // See [base.DebugHashMatch] for more information.
 func (f *Func) DebugHashMatch() bool {
 	if !base.HasDebugHash() {

src/cmd/compile/internal/ssa/rewrite.go

@@ -1188,6 +1188,8 @@ func logRule(s string) {
 
 var ruleFile io.Writer
 
+// TODO: replace these with the built-in min/max once they are available
+// during bootstrap (when bootstrapping with 1.21 or later).
 func min(x, y int64) int64 {
 	if x < y {
 		return x
@@ -1200,6 +1202,18 @@ func max(x, y int64) int64 {
 	}
 	return y
 }
+func minU(x, y uint64) uint64 {
+	if x < y {
+		return x
+	}
+	return y
+}
+func maxU(x, y uint64) uint64 {
+	if x > y {
+		return x
+	}
+	return y
+}
 
 func isConstZero(v *Value) bool {
 	switch v.Op {

test/checkbce.go

@@ -159,16 +159,14 @@ func decode1(data []byte) (x uint64) {
 }
 
 func decode2(data []byte) (x uint64) {
-	// TODO(rasky): this should behave like decode1 and compile to no
-	// boundchecks. We're currently not able to remove all of them.
 	for len(data) >= 32 {
 		x += binary.BigEndian.Uint64(data)
 		data = data[8:]
-		x += binary.BigEndian.Uint64(data) // ERROR "Found IsInBounds$"
+		x += binary.BigEndian.Uint64(data)
 		data = data[8:]
-		x += binary.BigEndian.Uint64(data) // ERROR "Found IsInBounds$"
+		x += binary.BigEndian.Uint64(data)
 		data = data[8:]
-		x += binary.BigEndian.Uint64(data) // ERROR "Found IsInBounds$"
+		x += binary.BigEndian.Uint64(data)
 		data = data[8:]
 	}
 	return x

test/codegen/comparisons.go

@@ -268,7 +268,7 @@ func CmpToZero(a, b, d int32, e, f int64, deOptC0, deOptC1 bool) int32 {
 	}
 }
 
-func CmpLogicalToZero(a, b, c uint32, d, e uint64) uint64 {
+func CmpLogicalToZero(a, b, c uint32, d, e, f, g uint64) uint64 {
 
 	// ppc64x:"ANDCC",-"CMPW"
 	// wasm:"I64Eqz",-"I32Eqz",-"I64ExtendI32U",-"I32WrapI64"
@@ -289,7 +289,7 @@ func CmpLogicalToZero(a, b, c uint32, d, e uint64) uint64 {
 	}
 	// ppc64x:"ORCC",-"CMP"
 	// wasm:"I64Eqz",-"I32Eqz",-"I64ExtendI32U",-"I32WrapI64"
-	if d|e == 0 {
+	if f|g == 0 {
 		return 1
 	}
 

test/loopbce.go

@@ -27,7 +27,7 @@ func f0c(a []int) int {
 	x := 0
 	for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 		b := a[:i+1] // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
-		x += b[0]
+		x += b[0]    // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 	}
 	return x
 }
@@ -168,7 +168,7 @@ func g2() int {
 func g3a() {
 	a := "this string has length 25"
 	for i := 0; i < len(a); i += 5 { // ERROR "Induction variable: limits \[0,20\], increment 5$"
-		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
+		useString(a[i:])   // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 		useString(a[:i+3]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 		useString(a[:i+5]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 		useString(a[:i+6])
@@ -294,8 +294,10 @@ func k3neg2(a [100]int) [100]int {
 }
 
 func k4(a [100]int) [100]int {
-	min := (-1) << 63
+	// Note: can't use (-1)<<63 here, because i-min doesn't get rewritten to i+(-min),
-	for i := min; i < min+50; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,-9223372036854775758\), increment 1$"
+	// and it isn't worth adding that special case to prove.
+	min := (-1)<<63 + 1
+	for i := min; i < min+50; i++ { // ERROR "Induction variable: limits \[-9223372036854775807,-9223372036854775757\), increment 1$"
 		a[i-min] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 	}
 	return a
@@ -314,7 +316,7 @@ func d1(a [100]int) [100]int {
 	for i := 0; i < 100; i++ { // ERROR "Induction variable: limits \[0,100\), increment 1$"
 		for j := 0; j < i; j++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 			a[j] = 0   // ERROR "Proved IsInBounds$"
-			a[j+1] = 0 // FIXME: this boundcheck should be eliminated
+			a[j+1] = 0 // ERROR "Proved IsInBounds$"
 			a[j+2] = 0
 		}
 	}
@@ -325,7 +327,7 @@ func d2(a [100]int) [100]int {
 	for i := 0; i < 100; i++ { // ERROR "Induction variable: limits \[0,100\), increment 1$"
 		for j := 0; i > j; j++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 			a[j] = 0   // ERROR "Proved IsInBounds$"
-			a[j+1] = 0 // FIXME: this boundcheck should be eliminated
+			a[j+1] = 0 // ERROR "Proved IsInBounds$"
 			a[j+2] = 0
 		}
 	}
@@ -419,12 +421,12 @@ func nobce2(a string) {
 	for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 	}
-	for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
+	for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Disproved Less64"
-		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
+		useString(a[i:])
 	}
 	j := int64(len(a)) - 123
-	for i := int64(0); i < j+123+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
+	for i := int64(0); i < j+123+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Disproved Less64"
-		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
+		useString(a[i:])
 	}
 	for i := int64(0); i < j+122+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 		// len(a)-123+122+MinInt overflows when len(a) == 0, so a bound check is needed here

test/prove.go

@@ -400,8 +400,8 @@ func f13f(a, b int64) int64 {
 	if b != math.MaxInt64 {
 		return 42
 	}
-	if a > b {
+	if a > b { // ERROR "Disproved Less64$"
-		if a == 0 { // ERROR "Disproved Eq64$"
+		if a == 0 {
 			return 1
 		}
 	}
@@ -684,20 +684,6 @@ func constsuffix(s string) bool {
 	return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$"
 }
 
-// oforuntil tests the pattern created by OFORUNTIL blocks. These are
-// handled by addLocalInductiveFacts rather than findIndVar.
-func oforuntil(b []int) {
-	i := 0
-	if len(b) > i {
-	top:
-		println(b[i]) // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Proved IsInBounds$"
-		i++
-		if i < len(b) {
-			goto top
-		}
-	}
-}
-
 func atexit(foobar []func()) {
 	for i := len(foobar) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1"
 		f := foobar[i]
@@ -877,11 +863,11 @@ func unrollDecMin(a []int, b int) int {
 		return 42
 	}
 	var i, x int
-	for i = len(a); i >= b; i -= 2 {
+	for i = len(a); i >= b; i -= 2 { // ERROR "Proved Leq64"
 		x += a[i-1]
 		x += a[i-2]
 	}
-	if i == 1 { // ERROR "Disproved Eq64$"
+	if i == 1 {
 		x += a[i-1]
 	}
 	return x
@@ -893,11 +879,11 @@ func unrollIncMin(a []int, b int) int {
 		return 42
 	}
 	var i, x int
-	for i = len(a); i >= b; i += 2 {
+	for i = len(a); i >= b; i += 2 { // ERROR "Proved Leq64"
 		x += a[i-1]
 		x += a[i-2]
 	}
-	if i == 1 { // ERROR "Disproved Eq64$"
+	if i == 1 {
 		x += a[i-1]
 	}
 	return x
@@ -1107,7 +1093,7 @@ func modu2(x, y uint) int {
 
 func issue57077(s []int) (left, right []int) {
 	middle := len(s) / 2
-	left = s[:middle] // ERROR "Proved IsSliceInBounds$"
+	left = s[:middle]  // ERROR "Proved IsSliceInBounds$"
 	right = s[middle:] // ERROR "Proved IsSliceInBounds$"
 	return
 }
@@ -1124,6 +1110,43 @@ func issue45928(x int) {
 	useInt(combinedFrac)
 }
 
+func constantBounds1(i, j uint) int {
+	var a [10]int
+	if j < 11 && i < j {
+		return a[i] // ERROR "Proved IsInBounds$"
+	}
+	return 0
+}
+
+func constantBounds2(i, j uint) int {
+	var a [10]int
+	if i < j && j < 11 {
+		return a[i] // ERROR "Proved IsInBounds"
+	}
+	return 0
+}
+
+func constantBounds3(i, j, k, l uint) int {
+	var a [8]int
+	if i < j && j < k && k < l && l < 11 {
+		return a[i] // ERROR "Proved IsInBounds"
+	}
+	return 0
+}
+
+func equalityPropagation(a [1]int, i, j uint) int {
+	if i == j && i == 5 {
+		return a[j-5] // ERROR "Proved IsInBounds"
+	}
+	return 0
+}
+func inequalityPropagation(a [1]int, i, j uint) int {
+	if i != j && j >= 5 && j <= 6 && i == 5 {
+		return a[j-6] // ERROR "Proved IsInBounds"
+	}
+	return 0
+}
+
 //go:noinline
 func useInt(a int) {
 }

test/prove_constant_folding.go

@@ -14,7 +14,7 @@ func f0i(x int) int {
   }
 
   if (x + 20) == 20 {
-    return x + 5 // ERROR "Proved.+is constant 0$"
+    return x + 5 // ERROR "Proved.+is constant 0$" "Proved.+is constant 5$"
   }
 
   return x / 2
@@ -26,7 +26,7 @@ func f0u(x uint) uint {
   }
 
   if (x + 20) == 20 {
-    return x + 5 // ERROR "Proved.+is constant 0$"
+    return x + 5 // ERROR "Proved.+is constant 0$" "Proved.+is constant 5$"
   }
 
   return x / 2