languages/go
languages/go
1
0
Fork 0
mirror of https://github.com/golang/go synced 2024-09-04 23:44:16 +00:00
Code Issues Packages Projects Releases Wiki Activity

cmd/compile: teach prove about unsigned division, modulus and rsh

Browse source 
Fixes: #57077
Change-Id: Icffcac42e28622eadecdba26e3cd7ceca6c4aacc
Reviewed-on: https://go-review.googlesource.com/c/go/+/455095
Reviewed-by: Keith Randall <khr@golang.org>
Reviewed-by: Keith Randall <khr@google.com>
Auto-Submit: Keith Randall <khr@golang.org>
TryBot-Result: Gopher Robot <gobot@golang.org>
Run-TryBot: Keith Randall <khr@golang.org>
Reviewed-by: David Chase <drchase@google.com>
This commit is contained in:
Jorropo 2022-12-04 21:41:47 +01:00 committed by Gopher Robot
parent 5e03c634b8
commit 35755d772f
2 changed files with 48 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -859,6 +859,15 @@ func prove(f *Func) {
case OpOr64, OpOr32, OpOr16, OpOr8:
ft.update(b, v, v.Args[1], unsigned, gt|eq)
ft.update(b, v, v.Args[0], unsigned, gt|eq)
case OpDiv64u, OpDiv32u, OpDiv16u, OpDiv8u,
OpRsh8Ux64, OpRsh8Ux32, OpRsh8Ux16, OpRsh8Ux8,
OpRsh16Ux64, OpRsh16Ux32, OpRsh16Ux16, OpRsh16Ux8,
OpRsh32Ux64, OpRsh32Ux32, OpRsh32Ux16, OpRsh32Ux8,
OpRsh64Ux64, OpRsh64Ux32, OpRsh64Ux16, OpRsh64Ux8:
ft.update(b, v, v.Args[0], unsigned, lt|eq)
case OpMod64u, OpMod32u, OpMod16u, OpMod8u:
ft.update(b, v, v.Args[0], unsigned, lt|eq)
ft.update(b, v, v.Args[1], unsigned, lt)
case OpPhi:
// Determine the min and max value of OpPhi composed entirely of integer constants.
//

39
test/prove.go
View file

@ -1046,6 +1046,45 @@ func and(p []byte) ([]byte, []byte) { // issue #52563
return blk, rem
}
func rshu(x, y uint) int {
z := x >> y
if z <= x { // ERROR "Proved Leq64U$"
return 1
}
return 0
}
func divu(x, y uint) int {
z := x / y
if z <= x { // ERROR "Proved Leq64U$"
return 1
}
return 0
}
func modu1(x, y uint) int {
z := x % y
if z < y { // ERROR "Proved Less64U$"
return 1
}
return 0
}
func modu2(x, y uint) int {
z := x % y
if z <= x { // ERROR "Proved Leq64U$"
return 1
}
return 0
}
func issue57077(s []int) (left, right []int) {
middle := len(s) / 2
left = s[:middle] // ERROR "Proved IsSliceInBounds$"
right = s[middle:] // ERROR "Proved IsSliceInBounds$"
return
}
func issue51622(b []byte) int {
if len(b) >= 3 && b[len(b)-3] == '#' { // ERROR "Proved IsInBounds$"
return len(b)