From 7c1e7789a5ab19ee4b04c355df1c2129a40c5d3e Mon Sep 17 00:00:00 2001 From: Jonah Uellenberg Date: Thu, 27 Nov 2025 18:31:12 -0800 Subject: [PATCH] cmd/compile: make prove use non-equality in subtraction for a stronger bound Given: s := /* slice */ k := /* proved valid index in s (0 <= k < len(s)) */ v := s[k:] len(v) >= 1, so v[0] needs no bounds check. However, for len(v) = len(s) - k, we only checked if len(s) >= k and so could only prove len(v) >= 0, thus the bounds check wasn't removed. As far as I can tell these checks were commented out for performance, but after benchmarking prove I see no difference. Fixes: #76429 --- src/cmd/compile/internal/ssa/prove.go | 24 +++++++++++------------- 1 file changed, 11 insertions(+), 13 deletions(-) diff --git a/src/cmd/compile/internal/ssa/prove.go b/src/cmd/compile/internal/ssa/prove.go index 1aab7e3eb775e9..c4f491f13ddc2a 100644 --- a/src/cmd/compile/internal/ssa/prove.go +++ b/src/cmd/compile/internal/ssa/prove.go @@ -2162,24 +2162,22 @@ func (ft *factsTable) detectSubRelations(v *Value) { return // x-y might overflow } - // Subtracting a positive number only makes - // things smaller. - if yLim.min >= 0 { + // Subtracting a positive non-zero number only makes + // things smaller. If it's positive or zero, it might + // also do nothing (x-0 == v). + if yLim.min > 0 { + ft.update(v.Block, v, x, signed, lt) + } else if yLim.min == 0 { ft.update(v.Block, v, x, signed, lt|eq) - // TODO: is this worth it? - //if yLim.min > 0 { - // ft.update(v.Block, v, x, signed, lt) - //} } // Subtracting a number from a bigger one - // can't go below 0. - if ft.orderS.OrderedOrEqual(y, x) { + // can't go below 1. If the numbers might be + // equal, then it can't go below 0. + if ft.orderS.Ordered(y, x) { + ft.signedMin(v, 1) + } else if ft.orderS.OrderedOrEqual(y, x) { ft.setNonNegative(v) - // TODO: is this worth it? - //if ft.orderS.Ordered(y, x) { - // ft.signedMin(v, 1) - //} } }