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 unsigned rounding-up divide

Browse source 
Change-Id: Ia7b5242c723f83ba85d12e4ca64a19fbbd126016
Reviewed-on: https://go-review.googlesource.com/c/go/+/714622
Auto-Submit: Jorropo <jorropo.pgm@gmail.com>
Reviewed-by: Keith Randall <khr@golang.org>
Reviewed-by: Keith Randall <khr@google.com>
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Michael Knyszek <mknyszek@google.com>
This commit is contained in:
Jorropo 2025-10-25 09:25:27 +02:00 • committed by Gopher Robot
parent a0f33b2887
commit 77dc138030
2 changed files with 52 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2473,6 +2473,41 @@ func addLocalFacts(ft *factsTable, b *Block) {
OpRsh16Ux64, OpRsh16Ux32, OpRsh16Ux16, OpRsh16Ux8,
OpRsh32Ux64, OpRsh32Ux32, OpRsh32Ux16, OpRsh32Ux8,
OpRsh64Ux64, OpRsh64Ux32, OpRsh64Ux16, OpRsh64Ux8:
switch add := v.Args[0]; add.Op {
// round-up division pattern; given:
// v = (x + y) / z
// if y < z then v <= x
case OpAdd64, OpAdd32, OpAdd16, OpAdd8:
z := v.Args[1]
zl := ft.limits[z.ID]
var uminDivisor uint64
switch v.Op {
case OpDiv64u, OpDiv32u, OpDiv16u, OpDiv8u:
uminDivisor = zl.umin
case OpRsh8Ux64, OpRsh8Ux32, OpRsh8Ux16, OpRsh8Ux8,
OpRsh16Ux64, OpRsh16Ux32, OpRsh16Ux16, OpRsh16Ux8,
OpRsh32Ux64, OpRsh32Ux32, OpRsh32Ux16, OpRsh32Ux8,
OpRsh64Ux64, OpRsh64Ux32, OpRsh64Ux16, OpRsh64Ux8:
uminDivisor = 1 << zl.umin
default:
panic("unreachable")
}
x := add.Args[0]
xl := ft.limits[x.ID]
y := add.Args[1]
yl := ft.limits[y.ID]
if unsignedAddOverflows(xl.umax, yl.umax, add.Type) {
continue
}
if xl.umax < uminDivisor {
ft.update(b, v, y, unsigned, lt|eq)
}
if yl.umax < uminDivisor {
ft.update(b, v, x, unsigned, lt|eq)
}
}
ft.update(b, v, v.Args[0], unsigned, lt|eq)
case OpMod64, OpMod32, OpMod16, OpMod8:
a := ft.limits[v.Args[0].ID]

17
test/prove.go
View file

@ -1078,6 +1078,23 @@ func divu(x, y uint) int {
return 0
}
func divuRoundUp(x, y, z uint) int {
x &= ^uint(0) >> 8 // can't overflow in add
y = min(y, 0xff-1)
z = max(z, 0xff)
r := (x + y) / z // ERROR "Proved Neq64$"
if r <= x { // ERROR "Proved Leq64U$"
return 1
}
return 0
}
func divuRoundUpSlice(x []string) {
halfRoundedUp := uint(len(x)+1) / 2
_ = x[:halfRoundedUp] // ERROR "Proved IsSliceInBounds$"
_ = x[halfRoundedUp:] // ERROR "Proved IsSliceInBounds$"
}
func modu1(x, y uint) int {
z := x % y
if z < y { // ERROR "Proved Less64U$"