cmd/compile: teach prove about subtract idioms

For v = x-y:
    if y >= 0 then v <= x
    if y <= x then v >= 0

(With appropriate guards against overflow/underflow.)

Fixes #76304

Change-Id: I8f8f1254156c347fa97802bd057a8379676720ae
Reviewed-on: https://go-review.googlesource.com/c/go/+/720740
Reviewed-by: Mark Freeman <markfreeman@google.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Jorropo <jorropo.pgm@gmail.com>
Reviewed-by: Keith Randall <khr@google.com>

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

@@ -1945,6 +1945,7 @@ func (ft *factsTable) flowLimit(v *Value) {
 		ft.newLimit(v, a.sub(b, uint(v.Type.Size())*8))
 		ft.detectMod(v)
 		ft.detectSliceLenRelation(v)
+		ft.detectSubRelations(v)
 	case OpNeg64, OpNeg32, OpNeg16, OpNeg8:
 		a := ft.limits[v.Args[0].ID]
 		bitsize := uint(v.Type.Size()) * 8
@@ -2091,6 +2092,48 @@ func (ft *factsTable) detectSliceLenRelation(v *Value) {
 	}
 }
 
+// v must be Sub{64,32,16,8}.
+func (ft *factsTable) detectSubRelations(v *Value) {
+	// v = x-y
+	x := v.Args[0]
+	y := v.Args[1]
+	if x == y {
+		ft.signedMinMax(v, 0, 0)
+		return
+	}
+	xLim := ft.limits[x.ID]
+	yLim := ft.limits[y.ID]
+
+	// Check if we might wrap around. If so, give up.
+	width := uint(v.Type.Size()) * 8
+	if _, ok := safeSub(xLim.min, yLim.max, width); !ok {
+		return // x-y might underflow
+	}
+	if _, ok := safeSub(xLim.max, yLim.min, width); !ok {
+		return // x-y might overflow
+	}
+
+	// Subtracting a positive number only makes
+	// things smaller.
+	if yLim.min >= 0 {
+		ft.update(v.Block, v, x, signed, lt|eq)
+		// TODO: is this worth it?
+		//if yLim.min > 0 {
+		//	ft.update(v.Block, v, x, signed, lt)
+		//}
+	}
+
+	// Subtracting a number from a bigger one
+	// can't go below 0.
+	if ft.orderS.OrderedOrEqual(y, x) {
+		ft.setNonNegative(v)
+		// TODO: is this worth it?
+		//if ft.orderS.Ordered(y, x) {
+		//	ft.signedMin(v, 1)
+		//}
+	}
+}
+
 // x%d has been rewritten to x - (x/d)*d.
 func (ft *factsTable) detectMod(v *Value) {
 	var opDiv, opDivU, opMul, opConst Op

test/prove.go

@@ -679,12 +679,12 @@ func natcmp(x, y []uint) (r int) {
 }
 
 func suffix(s, suffix string) bool {
-	// todo, we're still not able to drop the bound check here in the general case
+	// Note: issue 76304
-	return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
+	return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix // ERROR "Proved IsSliceInBounds"
 }
 
 func constsuffix(s string) bool {
-	return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$"
+	return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed$" "Proved Eq64$"
 }
 
 func atexit(foobar []func()) {
@@ -2639,6 +2639,18 @@ func unsignedRightShiftBounds(v uint, s int) {
 	}
 }
 
+func subLengths1(b []byte, i int) {
+	if i >= 0 && i <= len(b) {
+		_ = b[len(b)-i:] // ERROR "Proved IsSliceInBounds"
+	}
+}
+
+func subLengths2(b []byte, i int) {
+	if i >= 0 && i <= len(b) {
+		_ = b[:len(b)-i] // ERROR "Proved IsSliceInBounds"
+	}
+}
+
 //go:noinline
 func prove(x int) {
 }