cmd/compile: add fence-post implications to prove

This adds four new deductions to the prove pass, all related to adding
or subtracting one from a value. This is the first hint of actual
arithmetic relations in the prove pass.

The most effective of these is

   x-1 >= w && x > min  ⇒  x > w

This helps eliminate bounds checks in code like

  if x > 0 {
    // do something with s[x-1]
  }

Altogether, these deductions prove an additional 260 branches in std
and cmd. Furthermore, they will let us eliminate some tricky
compiler-inserted panics in the runtime that are interfering with
static analysis.

Fixes #23354.

Change-Id: I7088223e0e0cd6ff062a75c127eb4bb60e6dce02
Reviewed-on: https://go-review.googlesource.com/87480
Reviewed-by: Keith Randall <khr@golang.org>
Reviewed-by: Alexandru Moșoi <alexandru@mosoi.ro>

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 10a16917b67ce8c3b2f0d9334bb06cb23136208d..f723ea5e908bb980e52c38309be23bd6c5371df2 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -305,6 +305,53 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
                        v.Block.Func.Warnl(parent.Pos, "parent=%s, new limits %s %s %s", parent, v, w, lim.String())
                }
        }
+
+       // Process fence-post implications.
+       //
+       // First, make the condition > or >=.
+       if r == lt || r == lt|eq {
+               v, w = w, v
+               r = reverseBits[r]
+       }
+       switch r {
+       case gt:
+               if x, delta := isConstDelta(v); x != nil && delta == 1 {
+                       // x+1 > w  ⇒  x >= w
+                       //
+                       // This is useful for eliminating the
+                       // growslice branch of append.
+                       ft.update(parent, x, w, d, gt|eq)
+               } else if x, delta := isConstDelta(w); x != nil && delta == -1 {
+                       // v > x-1  ⇒  v >= x
+                       ft.update(parent, v, x, d, gt|eq)
+               }
+       case gt | eq:
+               if x, delta := isConstDelta(v); x != nil && delta == -1 {
+                       // x-1 >= w && x > min  ⇒  x > w
+                       //
+                       // Useful for i > 0; s[i-1].
+                       lim, ok := ft.limits[x.ID]
+                       if ok && lim.min > opMin[v.Op] {
+                               ft.update(parent, x, w, d, gt)
+                       }
+               } else if x, delta := isConstDelta(w); x != nil && delta == 1 {
+                       // v >= x+1 && x < max  ⇒  v > x
+                       lim, ok := ft.limits[x.ID]
+                       if ok && lim.max < opMax[w.Op] {
+                               ft.update(parent, v, x, d, gt)
+                       }
+               }
+       }
+}
+
+var opMin = map[Op]int64{
+       OpAdd64: math.MinInt64, OpSub64: math.MinInt64,
+       OpAdd32: math.MinInt32, OpSub32: math.MinInt32,
+}
+
+var opMax = map[Op]int64{
+       OpAdd64: math.MaxInt64, OpSub64: math.MaxInt64,
+       OpAdd32: math.MaxInt32, OpSub32: math.MaxInt32,
 }
 
 // isNonNegative returns true if v is known to be non-negative.
@@ -803,3 +850,29 @@ func isNonNegative(v *Value) bool {
        }
        return false
 }
+
+// isConstDelta returns non-nil if v is equivalent to w+delta (signed).
+func isConstDelta(v *Value) (w *Value, delta int64) {
+       cop := OpConst64
+       switch v.Op {
+       case OpAdd32, OpSub32:
+               cop = OpConst32
+       }
+       switch v.Op {
+       case OpAdd64, OpAdd32:
+               if v.Args[0].Op == cop {
+                       return v.Args[1], v.Args[0].AuxInt
+               }
+               if v.Args[1].Op == cop {
+                       return v.Args[0], v.Args[1].AuxInt
+               }
+       case OpSub64, OpSub32:
+               if v.Args[1].Op == cop {
+                       aux := v.Args[1].AuxInt
+                       if aux != -aux { // Overflow; too bad
+                               return v.Args[0], -aux
+                       }
+               }
+       }
+       return nil, 0
+}

diff --git a/test/prove.go b/test/prove.go
index 13e18cd72806b75dd9058ca4c062e60b7b502e80..97614939aceb3d052a40f9e993ce0be53d0a9761 100644 (file)
--- a/test/prove.go
+++ b/test/prove.go
@@ -506,6 +506,60 @@ func lim1(x, y, z int) {
        }
 }
 
+// fence1–4 correspond to the four fence-post implications.
+
+func fence1(b []int, x, y int) {
+       // Test proofs that rely on fence-post implications.
+       if x+1 > y {
+               if x < y { // ERROR "Disproved Less64$"
+                       return
+               }
+       }
+       if len(b) < cap(b) {
+               // This eliminates the growslice path.
+               b = append(b, 1) // ERROR "Disproved Greater64$"
+       }
+}
+
+func fence2(x, y int) {
+       if x-1 < y {
+               if x > y { // ERROR "Disproved Greater64$"
+                       return
+               }
+       }
+}
+
+func fence3(b []int, x, y int64) {
+       if x-1 >= y {
+               if x <= y { // Can't prove because x may have wrapped.
+                       return
+               }
+       }
+
+       if x != math.MinInt64 && x-1 >= y {
+               if x <= y { // ERROR "Disproved Leq64$"
+                       return
+               }
+       }
+
+       if n := len(b); n > 0 {
+               b[n-1] = 0 // ERROR "Proved IsInBounds$"
+       }
+}
+
+func fence4(x, y int64) {
+       if x >= y+1 {
+               if x <= y {
+                       return
+               }
+       }
+       if y != math.MaxInt64 && x >= y+1 {
+               if x <= y { // ERROR "Disproved Leq64$"
+                       return
+               }
+       }
+}
+
 //go:noinline
 func useInt(a int) {
 }