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>

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 1e5f4e9c6cce28530a14717913e20956a3df7ee9..2ab9aafaa136ed8d736f11e06087ad01b6b6317b 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/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
        }
 

diff --git a/test/prove.go b/test/prove.go
index 2db0a841e214e9d920fe740b42c728babde72f70..275528dde71ebdad16b9bba4eff115ffec736415 100644 (file)
--- 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) {
 }