Stowage/go
2
0
Fork 0
mirror of https://github.com/golang/go.git synced 2026-02-06 18:00:01 +00:00
Code Issues Projects Releases Packages Wiki Activity

cmd/compile: make prove use non-equality in subtraction for a stronger bound

Browse source 
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

Change-Id: I39ba2a18cbabc0559924d4d226dcb99dbe9a06ed
GitHub-Last-Rev: 53f3344d26
GitHub-Pull-Request: golang/go#76609
Reviewed-on: https://go-review.googlesource.com/c/go/+/725100
Reviewed-by: Keith Randall <khr@golang.org>
Reviewed-by: Keith Randall <khr@google.com>
Auto-Submit: Keith Randall <khr@golang.org>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Dmitri Shuralyov <dmitshur@google.com>
This commit is contained in:
Jonah Uellenberg 2026-01-29 19:45:27 +00:00 • committed by Gopher Robot
parent ee7a2119ac
commit 14a4cb13e3
3 changed files with 23 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2187,24 +2187,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)
//}
}
}

6
test/loopbce.go
View file

@ -17,8 +17,8 @@ func f0a(a []int) int {
func f0b(a []int) int {
x := 0
for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
b := a[i:] // ERROR "Proved IsSliceInBounds$"
x += b[0]
b := a[i:] // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed \(by limit\)$"
x += b[0] // ERROR "Proved IsInBounds$"
}
return x
}
@ -417,7 +417,7 @@ func bce1() {
func nobce2(a string) {
for i := int64(0); i < int64(len(a)); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
useString(a[i:]) // ERROR "Proved IsSliceInBounds$"
useString(a[i:]) // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed \(by limit\)$"
}
for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
useString(a[i:]) // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed"

10
test/prove.go
View file

@ -2552,7 +2552,7 @@ func swapbound(v []int) {
for i := 0; i < len(v)/2; i++ { // ERROR "Proved Div64 is unsigned|Induction variable"
v[i], // ERROR "Proved IsInBounds"
v[len(v)-1-i] = // ERROR "Proved IsInBounds"
v[len(v)-1-i],
v[len(v)-1-i], // ERROR "Proved IsInBounds"
v[i] // ERROR "Proved IsInBounds"
}
}
@ -2726,6 +2726,14 @@ func issue76688(x, y uint64) uint64 {
return x * y
}
func issue76429(s []byte, k int) byte {
if k < 0 || k >= len(s) {
return 0
}
s = s[k:] // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
return s[0] // ERROR "Proved IsInBounds"
}
//go:noinline
func prove(x int) {
}