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>

1 files changed, 54 insertions, 0 deletions

diff --git a/test/prove.go b/test/prove.go
index 13e18cd728..97614939ac 100644
--- 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) {
 }