cmd/compile/internal/ssa: Use transitive properties for len/cap

Remove the special casing for len/cap and rely on the posets.

After removing the special logic, I ran `go build -gcflags='-d
ssa/prove/debug=2' all` to verify my results. During this, I found 2
common cases where the old implicit unsigned->signed domain conversion
made proving a branch possible that shouldn't be strictly possible and
added these.

The 2 cases are shifting a non-negative signed integer and unsigned
comparisons that happen with arguments that fits entirely inside the
unsigned argument

Change-Id: Ic88049ff69efc5602fc15f5dad02028e704f5483
Reviewed-on: https://go-review.googlesource.com/c/go/+/679155
Reviewed-by: Mark Freeman <mark@golang.org>
Reviewed-by: Keith Randall <khr@google.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Keith Randall <khr@golang.org>

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index b8c952ef3350ad692cc730c8c11d008913995aee..be70226695a91dffec2a545ef7ddbe20129c1e3b 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -409,12 +409,6 @@ type factsTable struct {
        limits       []limit     // indexed by value ID
        limitStack   []limitFact // previous entries
        recurseCheck []bool      // recursion detector for limit propagation
-
-       // For each slice s, a map from s to a len(s)/cap(s) value (if any)
-       // TODO: check if there are cases that matter where we have
-       // more than one len(s) for a slice. We could keep a list if necessary.
-       lens map[ID]*Value
-       caps map[ID]*Value
 }
 
 // checkpointBound is an invalid value used for checkpointing
@@ -666,6 +660,11 @@ func (ft *factsTable) newLimit(v *Value, newLim limit) bool {
                        }
                        if !isTrue {
                                r ^= lt | gt | eq
+                       } else if d == unsigned && (r == lt || r == lt|eq) && ft.isNonNegative(v.Args[1]) {
+                               // Since every representation of a non-negative signed number is the same
+                               // as in the unsigned domain, we can transfer x <= y to the signed domain,
+                               // but only for the true branch.
+                               d |= signed
                        }
                        // TODO: v.Block is wrong?
                        addRestrictions(v.Block, ft, d, v.Args[0], v.Args[1], r)
@@ -730,7 +729,7 @@ func (ft *factsTable) addOrdering(v, w *Value, d domain, r relation) {
 // restricting it to r.
 func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
        if parent.Func.pass.debug > 2 {
-               parent.Func.Warnl(parent.Pos, "parent=%s, update %s %s %s", parent, v, w, r)
+               parent.Func.Warnl(parent.Pos, "parent=%s, update %s %s %s %s", parent, d, v, w, r)
        }
        // No need to do anything else if we already found unsat.
        if ft.unsat {
@@ -942,32 +941,6 @@ func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
                return
        }
 
-       // Additional facts we know given the relationship between len and cap.
-       //
-       // TODO: Since prove now derives transitive relations, it
-       // should be sufficient to learn that len(w) <= cap(w) at the
-       // beginning of prove where we look for all len/cap ops.
-       if v.Op == OpSliceLen && r&lt == 0 && ft.caps[v.Args[0].ID] != nil {
-               // len(s) > w implies cap(s) > w
-               // len(s) >= w implies cap(s) >= w
-               // len(s) == w implies cap(s) >= w
-               ft.update(parent, ft.caps[v.Args[0].ID], w, d, r|gt)
-       }
-       if w.Op == OpSliceLen && r&gt == 0 && ft.caps[w.Args[0].ID] != nil {
-               // same, length on the RHS.
-               ft.update(parent, v, ft.caps[w.Args[0].ID], d, r|lt)
-       }
-       if v.Op == OpSliceCap && r&gt == 0 && ft.lens[v.Args[0].ID] != nil {
-               // cap(s) < w implies len(s) < w
-               // cap(s) <= w implies len(s) <= w
-               // cap(s) == w implies len(s) <= w
-               ft.update(parent, ft.lens[v.Args[0].ID], w, d, r|lt)
-       }
-       if w.Op == OpSliceCap && r&lt == 0 && ft.lens[w.Args[0].ID] != nil {
-               // same, capacity on the RHS.
-               ft.update(parent, v, ft.lens[w.Args[0].ID], d, r|gt)
-       }
-
        // Process fence-post implications.
        //
        // First, make the condition > or >=.
@@ -1421,6 +1394,8 @@ func prove(f *Func) {
        ft := newFactsTable(f)
        ft.checkpoint()
 
+       var lens map[ID]*Value
+       var caps map[ID]*Value
        // Find length and capacity ops.
        for _, b := range f.Blocks {
                for _, v := range b.Values {
@@ -1431,26 +1406,39 @@ func prove(f *Func) {
                        }
                        switch v.Op {
                        case OpSliceLen:
-                               if ft.lens == nil {
-                                       ft.lens = map[ID]*Value{}
+                               if lens == nil {
+                                       lens = map[ID]*Value{}
                                }
                                // Set all len Values for the same slice as equal in the poset.
                                // The poset handles transitive relations, so Values related to
                                // any OpSliceLen for this slice will be correctly related to others.
-                               if l, ok := ft.lens[v.Args[0].ID]; ok {
+                               //
+                               // Since we know that lens/caps are non-negative, their relation
+                               // can be added in both the signed and unsigned domain.
+                               if l, ok := lens[v.Args[0].ID]; ok {
                                        ft.update(b, v, l, signed, eq)
+                                       ft.update(b, v, l, unsigned, eq)
                                } else {
-                                       ft.lens[v.Args[0].ID] = v
+                                       lens[v.Args[0].ID] = v
+                               }
+                               if c, ok := caps[v.Args[0].ID]; ok {
+                                       ft.update(b, v, c, signed, lt|eq)
+                                       ft.update(b, v, c, unsigned, lt|eq)
                                }
                        case OpSliceCap:
-                               if ft.caps == nil {
-                                       ft.caps = map[ID]*Value{}
+                               if caps == nil {
+                                       caps = map[ID]*Value{}
                                }
                                // Same as case OpSliceLen above, but for slice cap.
-                               if c, ok := ft.caps[v.Args[0].ID]; ok {
+                               if c, ok := caps[v.Args[0].ID]; ok {
                                        ft.update(b, v, c, signed, eq)
+                                       ft.update(b, v, c, unsigned, eq)
                                } else {
-                                       ft.caps[v.Args[0].ID] = v
+                                       caps[v.Args[0].ID] = v
+                               }
+                               if l, ok := lens[v.Args[0].ID]; ok {
+                                       ft.update(b, v, l, signed, gt|eq)
+                                       ft.update(b, v, l, unsigned, gt|eq)
                                }
                        }
                }
@@ -2260,6 +2248,9 @@ func addLocalFacts(ft *factsTable, b *Block) {
                        OpRsh32Ux64, OpRsh32Ux32, OpRsh32Ux16, OpRsh32Ux8,
                        OpRsh64Ux64, OpRsh64Ux32, OpRsh64Ux16, OpRsh64Ux8:
                        ft.update(b, v, v.Args[0], unsigned, lt|eq)
+                       if ft.isNonNegative(v.Args[0]) {
+                               ft.update(b, v, v.Args[0], signed, lt|eq)
+                       }
                case OpMod64u, OpMod32u, OpMod16u, OpMod8u:
                        ft.update(b, v, v.Args[0], unsigned, lt|eq)
                        // Note: we have to be careful that this doesn't imply