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

This reverts commit a3295df873bb22b3ba427124b1220370a5ca5cdb (CL 679155)

Reason for revert: leads to a very expensive prove pass, see #74974

(Maybe not this CL's fault, just tickling some superlinear behavior.)

Change-Id: I75302c04cfc5e1e075aeb80edb73080bfb1efcac
Reviewed-on: https://go-review.googlesource.com/c/go/+/695175
Reviewed-by: Cuong Manh Le <cuong.manhle.vn@gmail.com>
Reviewed-by: Keith Randall <khr@google.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Daniel Morsing <daniel.morsing@gmail.com>
Reviewed-by: Dmitri Shuralyov <dmitshur@google.com>
Auto-Submit: Keith Randall <khr@golang.org>

diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go
index 3f85bd2351f25c98ef3f18fd47aaf5eaf5ab162b..b9b5d3386d7b1c733add377f657a3f472bf25623 100644 (file)
--- a/src/cmd/compile/internal/ssa/prove.go
+++ b/src/cmd/compile/internal/ssa/prove.go
@@ -406,6 +406,12 @@ 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
@@ -657,11 +663,6 @@ 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)
@@ -726,7 +727,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 %s", parent, d, v, w, r)
+               parent.Func.Warnl(parent.Pos, "parent=%s, update %s %s %s", parent, v, w, r)
        }
        // No need to do anything else if we already found unsat.
        if ft.unsat {
@@ -938,6 +939,32 @@ 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 >=.
@@ -1391,8 +1418,6 @@ 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 {
@@ -1403,39 +1428,26 @@ func prove(f *Func) {
                        }
                        switch v.Op {
                        case OpSliceLen:
-                               if lens == nil {
-                                       lens = map[ID]*Value{}
+                               if ft.lens == nil {
+                                       ft.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.
-                               //
-                               // 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 {
+                               if l, ok := ft.lens[v.Args[0].ID]; ok {
                                        ft.update(b, v, l, signed, eq)
-                                       ft.update(b, v, l, unsigned, eq)
                                } else {
-                                       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)
+                                       ft.lens[v.Args[0].ID] = v
                                }
                        case OpSliceCap:
-                               if caps == nil {
-                                       caps = map[ID]*Value{}
+                               if ft.caps == nil {
+                                       ft.caps = map[ID]*Value{}
                                }
                                // Same as case OpSliceLen above, but for slice cap.
-                               if c, ok := caps[v.Args[0].ID]; ok {
+                               if c, ok := ft.caps[v.Args[0].ID]; ok {
                                        ft.update(b, v, c, signed, eq)
-                                       ft.update(b, v, c, unsigned, eq)
                                } else {
-                                       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)
+                                       ft.caps[v.Args[0].ID] = v
                                }
                        }
                }
@@ -2245,9 +2257,6 @@ 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