cmd/compile: make prove use poset to check non-negatives

Prove currently fails to remove bounds checks of the form:

if i >= 0 {              // hint that i is non-negative
    for i < len(data) {  // i becomes Phi in the loop SSA
        _ = data[i]      // data[Phi]; bounds check!!
	i++
    }
}

addIndVarRestrictions fails to identify that the loop induction
variable, (Phi), is non-negative. As a result, the restrictions,
i <= Phi < len(data), are only added for the signed domain. When
testing the bounds check, addBranchRestrictions is similarly unable
to infer that Phi is non-negative. As a result, the restriction,
Phi >= len(data), is only added/tested for the unsigned domain.

This CL changes the isNonNegative method to utilise the factTable's
partially ordered set (poset). It also adds field factTable.zero to
allow isNonNegative to query the poset using the zero(0) constant
found or created early in prove.

Fixes #28956

Change-Id: I792f886c652eeaa339b0d57d5faefbf5922fe44f
Reviewed-on: https://go-review.googlesource.com/c/go/+/161437
Run-TryBot: Brad Fitzpatrick <bradfitz@golang.org>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: Giovanni Bajo <rasky@develer.com>

1 files changed, 20 insertions, 0 deletions

diff --git a/test/prove.go b/test/prove.go
index 2db0a841e2..275528dde7 100644
--- a/test/prove.go
+++ b/test/prove.go
@@ -706,6 +706,26 @@ func range2(b [][32]int) {
 	}
 }
 
+// signhint1-2 test whether the hint (int >= 0) is propagated into the loop.
+func signHint1(i int, data []byte) {
+	if i >= 0 {
+		for i < len(data) { // ERROR "Induction variable: limits \[\?,\?\), increment 1$"
+			_ = data[i] // ERROR "Proved IsInBounds$"
+			i++
+		}
+	}
+}
+
+func signHint2(b []byte, n int) {
+	if n < 0 {
+		panic("")
+	}
+	_ = b[25]
+	for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
+		b[i] = 123 // ERROR "Proved IsInBounds$"
+	}
+}
+
 //go:noinline
 func useInt(a int) {
 }