Stowage/go
2
0
Fork 0
mirror of https://github.com/golang/go.git synced 2025-12-08 06:10:04 +00:00
Code Issues Projects Releases Packages Wiki Activity

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

Browse source 
This reverts commit a3295df873 (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>
This commit is contained in:
Keith Randall 2025-08-12 07:33:33 -07:00 • committed by Gopher Robot
parent 00a7bdcb55
commit d0a64f7969
1 changed files with 41 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

73
src/cmd/compile/internal/ssa/prove.go
View file

@ -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