From: Keith Randall Date: Tue, 12 Aug 2025 14:33:33 +0000 (-0700) Subject: Revert "cmd/compile/internal/ssa: Use transitive properties for len/cap" X-Git-Url: http://www.git.cypherpunks.su/?a=commitdiff_plain;h=d0a64f7969954add113ea9c3283d3200c4ead7a1;p=gostls13.git 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 Reviewed-by: Keith Randall LUCI-TryBot-Result: Go LUCI Reviewed-by: Daniel Morsing Reviewed-by: Dmitri Shuralyov Auto-Submit: Keith Randall --- diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go index 3f85bd2351..b9b5d3386d 100644 --- 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< == 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> == 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> == 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< == 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