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>

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

@@ -174,6 +174,10 @@ type factsTable struct {
 	// more than one len(s) for a slice. We could keep a list if necessary.
 	lens map[ID]*Value
 	caps map[ID]*Value
+
+	// zero is a reference to the zero-valued constant assigned or created
+	// during the len/cap sweep that begins prove.
+	zero *Value
 }
 
 // checkpointFact is an invalid value used for checkpointing
@@ -566,7 +570,11 @@ func (ft *factsTable) isNonNegative(v *Value) bool {
 		}
 	}
 
-	return false
+	// Check if the signed poset can prove that the value is >= 0
+	if ft.zero == nil {
+		ft.zero = v.Block.NewValue0I(v.Block.Pos, OpConst64, v.Block.Func.Config.Types.Int64, 0)
+	}
+	return ft.order[0].OrderedOrEqual(ft.zero, v)
 }
 
 // checkpoint saves the current state of known relations.
@@ -734,13 +742,12 @@ func prove(f *Func) {
 	ft.checkpoint()
 
 	// Find length and capacity ops.
-	var zero *Value
 	for _, b := range f.Blocks {
 		for _, v := range b.Values {
 			// If we found a zero constant, save it (so we don't have
 			// to build one later).
-			if zero == nil && v.Op == OpConst64 && v.AuxInt == 0 {
-				zero = v
+			if ft.zero == nil && v.Op == OpConst64 && v.AuxInt == 0 {
+				ft.zero = v
 			}
 			if v.Uses == 0 {
 				// We don't care about dead values.
@@ -749,28 +756,28 @@ func prove(f *Func) {
 			}
 			switch v.Op {
 			case OpStringLen:
-				if zero == nil {
-					zero = b.NewValue0I(b.Pos, OpConst64, f.Config.Types.Int64, 0)
+				if ft.zero == nil {
+					ft.zero = b.NewValue0I(b.Pos, OpConst64, f.Config.Types.Int64, 0)
 				}
-				ft.update(b, v, zero, signed, gt|eq)
+				ft.update(b, v, ft.zero, signed, gt|eq)
 			case OpSliceLen:
 				if ft.lens == nil {
 					ft.lens = map[ID]*Value{}
 				}
 				ft.lens[v.Args[0].ID] = v
-				if zero == nil {
-					zero = b.NewValue0I(b.Pos, OpConst64, f.Config.Types.Int64, 0)
+				if ft.zero == nil {
+					ft.zero = b.NewValue0I(b.Pos, OpConst64, f.Config.Types.Int64, 0)
 				}
-				ft.update(b, v, zero, signed, gt|eq)
+				ft.update(b, v, ft.zero, signed, gt|eq)
 			case OpSliceCap:
 				if ft.caps == nil {
 					ft.caps = map[ID]*Value{}
 				}
 				ft.caps[v.Args[0].ID] = v
-				if zero == nil {
-					zero = b.NewValue0I(b.Pos, OpConst64, f.Config.Types.Int64, 0)
+				if ft.zero == nil {
+					ft.zero = b.NewValue0I(b.Pos, OpConst64, f.Config.Types.Int64, 0)
 				}
-				ft.update(b, v, zero, signed, gt|eq)
+				ft.update(b, v, ft.zero, signed, gt|eq)
 			}
 		}
 	}
@@ -904,7 +911,7 @@ func getBranch(sdom SparseTree, p *Block, b *Block) branch {
 // starting in Block b.
 func addIndVarRestrictions(ft *factsTable, b *Block, iv indVar) {
 	d := signed
-	if isNonNegative(iv.min) && isNonNegative(iv.max) {
+	if ft.isNonNegative(iv.min) && ft.isNonNegative(iv.max) {
 		d |= unsigned
 	}
 

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) {
 }