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: propagate unsigned limits for Div and Mod if arguments are positive

Browse source 
I didn't implemented negative limits since prove is most useful for BCE which
should never be negative in the first place.

Change-Id: I302ee462cdc20bd4edff0618f7e49ff66fc2a007
Reviewed-on: https://go-review.googlesource.com/c/go/+/605136
LUCI-TryBot-Result: Go LUCI <golang-scoped@luci-project-accounts.iam.gserviceaccount.com>
Reviewed-by: Keith Randall <khr@google.com>
Reviewed-by: Keith Randall <khr@golang.org>
Reviewed-by: Cherry Mui <cherryyz@google.com>
This commit is contained in:
Jorropo 2024-08-13 18:40:44 +02:00 • committed by Keith Randall
parent d91a2e5b11
commit 68c431e89f
2 changed files with 101 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1775,11 +1775,27 @@ func (ft *factsTable) flowLimit(v *Value) bool {
a := ft.limits[v.Args[0].ID]
b := ft.limits[v.Args[1].ID]
return ft.newLimit(v, a.mul(b.exp2(8), 8))
case OpMod64, OpMod32, OpMod16, OpMod8:
a := ft.limits[v.Args[0].ID]
b := ft.limits[v.Args[1].ID]
if !(a.nonnegative() && b.nonnegative()) {
// TODO: we could handle signed limits but I didn't bother.
break
}
fallthrough
case OpMod64u, OpMod32u, OpMod16u, OpMod8u:
a := ft.limits[v.Args[0].ID]
b := ft.limits[v.Args[1].ID]
// Underflow in the arithmetic below is ok, it gives to MaxUint64 which does nothing to the limit.
return ft.unsignedMax(v, minU(a.umax, b.umax-1))
case OpDiv64, OpDiv32, OpDiv16, OpDiv8:
a := ft.limits[v.Args[0].ID]
b := ft.limits[v.Args[1].ID]
if !(a.nonnegative() && b.nonnegative()) {
// TODO: we could handle signed limits but I didn't bother.
break
}
fallthrough
case OpDiv64u, OpDiv32u, OpDiv16u, OpDiv8u:
a := ft.limits[v.Args[0].ID]
b := ft.limits[v.Args[1].ID]

85
test/prove.go
View file

@ -1477,6 +1477,66 @@ func mod64uWithIdenticalMax(a, b uint64, ensureBothBranchesCouldHappen bool) int
}
return z
}
func mod64sPositiveWithSmallerDividendMax(a, b int64, ensureBothBranchesCouldHappen bool) int64 {
if a < 0 || b < 0 {
return 42
}
a &= 0xff
b &= 0xfff
z := a % b // ERROR "Proved Mod64 does not need fix-up$"
if ensureBothBranchesCouldHappen {
if z > 0xff { // ERROR "Disproved Less64$"
return 42
}
} else {
if z <= 0xff { // ERROR "Proved Leq64$"
return 1337
}
}
return z
}
func mod64sPositiveWithSmallerDivisorMax(a, b int64, ensureBothBranchesCouldHappen bool) int64 {
if a < 0 || b < 0 {
return 42
}
a &= 0xfff
b &= 0xff
z := a % b // ERROR "Proved Mod64 does not need fix-up$"
if ensureBothBranchesCouldHappen {
if z > 0xff-1 { // ERROR "Disproved Less64$"
return 42
}
} else {
if z <= 0xff-1 { // ERROR "Proved Leq64$"
return 1337
}
}
return z
}
func mod64sPositiveWithIdenticalMax(a, b int64, ensureBothBranchesCouldHappen bool) int64 {
if a < 0 || b < 0 {
return 42
}
a &= 0xfff
b &= 0xfff
z := a % b // ERROR "Proved Mod64 does not need fix-up$"
if ensureBothBranchesCouldHappen {
if z > 0xfff-1 { // ERROR "Disproved Less64$"
return 42
}
} else {
if z <= 0xfff-1 { // ERROR "Proved Leq64$"
return 1337
}
}
return z
}
func div64u(a, b uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
a &= 0xffff
@ -1500,6 +1560,31 @@ func div64u(a, b uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
}
return z
}
func div64s(a, b int64, ensureAllBranchesCouldHappen func() bool) int64 {
if a < 0 || b < 0 {
return 42
}
a &= 0xffff
a |= 0xfff
b &= 0xff
b |= 0xf
z := a / b // ERROR "(Proved Div64 does not need fix-up|Proved Neq64)$"
if ensureAllBranchesCouldHappen() && z > 0xffff/0xf { // ERROR "Disproved Less64$"
return 42
}
if ensureAllBranchesCouldHappen() && z <= 0xffff/0xf { // ERROR "Proved Leq64$"
return 1337
}
if ensureAllBranchesCouldHappen() && z < 0xfff/0xff { // ERROR "Disproved Less64$"
return 42
}
if ensureAllBranchesCouldHappen() && z >= 0xfff/0xff { // ERROR "Proved Leq64$"
return 42
}
return z
}
//go:noinline
func useInt(a int) {