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

cmd/compile: teach prove about subtract idioms

Browse source 
For v = x-y:
    if y >= 0 then v <= x
    if y <= x then v >= 0

(With appropriate guards against overflow/underflow.)

Fixes #76304

Change-Id: I8f8f1254156c347fa97802bd057a8379676720ae
Reviewed-on: https://go-review.googlesource.com/c/go/+/720740
Reviewed-by: Mark Freeman <markfreeman@google.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Jorropo <jorropo.pgm@gmail.com>
Reviewed-by: Keith Randall <khr@google.com>
This commit is contained in:
Keith Randall 2025-11-14 15:26:36 -08:00
parent bc15963813
commit c12c337099
2 changed files with 58 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1945,6 +1945,7 @@ func (ft *factsTable) flowLimit(v *Value) {
ft.newLimit(v, a.sub(b, uint(v.Type.Size())*8))
ft.detectMod(v)
ft.detectSliceLenRelation(v)
ft.detectSubRelations(v)
case OpNeg64, OpNeg32, OpNeg16, OpNeg8:
a := ft.limits[v.Args[0].ID]
bitsize := uint(v.Type.Size()) * 8
@ -2091,6 +2092,48 @@ func (ft *factsTable) detectSliceLenRelation(v *Value) {
}
}
// v must be Sub{64,32,16,8}.
func (ft *factsTable) detectSubRelations(v *Value) {
// v = x-y
x := v.Args[0]
y := v.Args[1]
if x == y {
ft.signedMinMax(v, 0, 0)
return
}
xLim := ft.limits[x.ID]
yLim := ft.limits[y.ID]
// Check if we might wrap around. If so, give up.
width := uint(v.Type.Size()) * 8
if _, ok := safeSub(xLim.min, yLim.max, width); !ok {
return // x-y might underflow
}
if _, ok := safeSub(xLim.max, yLim.min, width); !ok {
return // x-y might overflow
}
// Subtracting a positive number only makes
// things smaller.
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) {
ft.setNonNegative(v)
// TODO: is this worth it?
//if ft.orderS.Ordered(y, x) {
// ft.signedMin(v, 1)
//}
}
}
// x%d has been rewritten to x - (x/d)*d.
func (ft *factsTable) detectMod(v *Value) {
var opDiv, opDivU, opMul, opConst Op

18
test/prove.go
View file

@ -679,12 +679,12 @@ func natcmp(x, y []uint) (r int) {
}
func suffix(s, suffix string) bool {
// todo, we're still not able to drop the bound check here in the general case
return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
// Note: issue 76304
return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix // ERROR "Proved IsSliceInBounds"
}
func constsuffix(s string) bool {
return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$"
return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed$" "Proved Eq64$"
}
func atexit(foobar []func()) {
@ -2639,6 +2639,18 @@ func unsignedRightShiftBounds(v uint, s int) {
}
}
func subLengths1(b []byte, i int) {
if i >= 0 && i <= len(b) {
_ = b[len(b)-i:] // ERROR "Proved IsSliceInBounds"
}
}
func subLengths2(b []byte, i int) {
if i >= 0 && i <= len(b) {
_ = b[:len(b)-i] // ERROR "Proved IsSliceInBounds"
}
}
//go:noinline
func prove(x int) {
}