From a3295df873bb22b3ba427124b1220370a5ca5cdb Mon Sep 17 00:00:00 2001 From: Daniel Morsing Date: Wed, 4 Jun 2025 09:22:21 +0100 Subject: [PATCH] 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 Reviewed-by: Keith Randall LUCI-TryBot-Result: Go LUCI Reviewed-by: Keith Randall --- src/cmd/compile/internal/ssa/prove.go | 73 ++++++++++++--------------- 1 file changed, 32 insertions(+), 41 deletions(-) diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go index b8c952ef33..be70226695 100644 --- 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< == 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 >=. @@ -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 -- 2.51.0