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>

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index bbcab3efa56a51f172715c7d8dd3ed508b506e2a..4b2cedc8be9b98c05212efb57486896892bafeb4 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/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

diff --git a/test/prove.go b/test/prove.go
index 365e8ba006ee4af184d67ad76502b051accf592a..3f8990615e2250467bb8285e17b5494b6dff04b9 100644 (file)
--- a/test/prove.go
+++ b/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
-       return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
+       // Note: issue 76304
+       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) {
 }