qbit/go
1
0
Fork 0
mirror of https://github.com/golang/go synced 2024-11-22 19:14:53 -07:00
Code Releases Activity

cmd/compile: tighten bounds for induction variables in strided loops

Browse Source 
for i := 0; i < 9; i += 3

Currently we compute bounds of [0,8]. Really we know that it is [0,6].

CL 415874 computed the better bound as part of overflow detection.
This CL just incorporates that better info to the prove pass.

R=go1.20

Change-Id: Ife82cc415321f6652c2b5d132a40ec23e3385766
Reviewed-on: https://go-review.googlesource.com/c/go/+/415937
Reviewed-by: Heschi Kreinick <heschi@google.com>
TryBot-Result: Gopher Robot <gobot@golang.org>
Reviewed-by: David Chase <drchase@google.com>
Run-TryBot: Keith Randall <khr@golang.org>
This commit is contained in:
Keith Randall 2022-07-03 14:52:47 -07:00
parent 52d9e7f543
commit af7f067e0d
2 changed files with 53 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
src/cmd/compile/internal/ssa/loopbce.go
View File

@ -200,8 +200,15 @@ func findIndVar(f *Func) []indVar {
} }
v = addU(init.AuxInt, diff(v, init.AuxInt)/uint64(step)*uint64(step)) v = addU(init.AuxInt, diff(v, init.AuxInt)/uint64(step)*uint64(step))
} }
// It is ok if we can't overflow when incrementing from the largest value. if addWillOverflow(v, step) {
return !addWillOverflow(v, step) return false
}
if inclusive && v != limit.AuxInt || !inclusive && v+1 != limit.AuxInt {
// We know a better limit than the programmer did. Use our limit instead.
limit = f.ConstInt64(f.Config.Types.Int64, v)
inclusive = true
}
return true
} }
if step == 1 && !inclusive { if step == 1 && !inclusive {
// Can't overflow because maxint is never a possible value. // Can't overflow because maxint is never a possible value.
@ -238,8 +245,15 @@ func findIndVar(f *Func) []indVar {
} }
v = subU(init.AuxInt, diff(init.AuxInt, v)/uint64(-step)*uint64(-step)) v = subU(init.AuxInt, diff(init.AuxInt, v)/uint64(-step)*uint64(-step))
} }
// It is ok if we can't underflow when decrementing from the smallest value. if subWillUnderflow(v, -step) {
return !subWillUnderflow(v, -step) return false
}
if inclusive && v != limit.AuxInt || !inclusive && v-1 != limit.AuxInt {
// We know a better limit than the programmer did. Use our limit instead.
limit = f.ConstInt64(f.Config.Types.Int64, v)
inclusive = true
}
return true
} }
if step == -1 && !inclusive { if step == -1 && !inclusive {
// Can't underflow because minint is never a possible value. // Can't underflow because minint is never a possible value.

52
test/loopbce.go
View File

@ -49,7 +49,7 @@ func f2(a []int) int {
func f4(a [10]int) int { func f4(a [10]int) int {
x := 0 x := 0
for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$" for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,8\], increment 2$"
x += a[i] // ERROR "(\([0-9]+\) )?Proved IsInBounds$" x += a[i] // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
} }
return x return x
@ -57,7 +57,7 @@ func f4(a [10]int) int {
func f5(a [10]int) int { func f5(a [10]int) int {
x := 0 x := 0
for i := -10; i < len(a); i += 2 { // ERROR "Induction variable: limits \[-10,10\), increment 2$" for i := -10; i < len(a); i += 2 { // ERROR "Induction variable: limits \[-10,8\], increment 2$"
x += a[i] x += a[i]
} }
return x return x
@ -121,7 +121,7 @@ func g0f(a string) int {
func g1() int { func g1() int {
a := "evenlength" a := "evenlength"
x := 0 x := 0
for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$" for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,8\], increment 2$"
x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$" x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
} }
return x return x
@ -130,7 +130,7 @@ func g1() int {
func g2() int { func g2() int {
a := "evenlength" a := "evenlength"
x := 0 x := 0
for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$" for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,8\], increment 2$"
j := i j := i
if a[i] == 'e' { // ERROR "(\([0-9]+\) )?Proved IsInBounds$" if a[i] == 'e' { // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
j = j + 1 j = j + 1
@ -142,9 +142,11 @@ func g2() int {
func g3a() { func g3a() {
a := "this string has length 25" a := "this string has length 25"
for i := 0; i < len(a); i += 5 { // ERROR "Induction variable: limits \[0,25\), increment 5$" for i := 0; i < len(a); i += 5 { // ERROR "Induction variable: limits \[0,20\], increment 5$"
useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
useString(a[:i+3]) useString(a[:i+3]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
useString(a[:i+5]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
useString(a[:i+6])
} }
} }
@ -293,22 +295,22 @@ func d3(a [100]int) [100]int {
} }
func d4() { func d4() {
for i := int64(math.MaxInt64 - 9); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775798,9223372036854775805\), increment 4$" for i := int64(math.MaxInt64 - 9); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775798,9223372036854775802\], increment 4$"
useString("foo") useString("foo")
} }
for i := int64(math.MaxInt64 - 8); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775799,9223372036854775805\), increment 4$" for i := int64(math.MaxInt64 - 8); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775799,9223372036854775803\], increment 4$"
useString("foo") useString("foo")
} }
for i := int64(math.MaxInt64 - 7); i < math.MaxInt64-2; i += 4 { for i := int64(math.MaxInt64 - 7); i < math.MaxInt64-2; i += 4 {
useString("foo") useString("foo")
} }
for i := int64(math.MaxInt64 - 6); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775801,9223372036854775805\), increment 4$" for i := int64(math.MaxInt64 - 6); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775801,9223372036854775801\], increment 4$"
useString("foo") useString("foo")
} }
for i := int64(math.MaxInt64 - 9); i <= math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775798,9223372036854775805\], increment 4$" for i := int64(math.MaxInt64 - 9); i <= math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775798,9223372036854775802\], increment 4$"
useString("foo") useString("foo")
} }
for i := int64(math.MaxInt64 - 8); i <= math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775799,9223372036854775805\], increment 4$" for i := int64(math.MaxInt64 - 8); i <= math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775799,9223372036854775803\], increment 4$"
useString("foo") useString("foo")
} }
for i := int64(math.MaxInt64 - 7); i <= math.MaxInt64-2; i += 4 { for i := int64(math.MaxInt64 - 7); i <= math.MaxInt64-2; i += 4 {
@ -320,22 +322,22 @@ func d4() {
} }
func d5() { func d5() {
for i := int64(math.MinInt64 + 9); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \(-9223372036854775806,-9223372036854775799\], increment 4" for i := int64(math.MinInt64 + 9); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775803,-9223372036854775799\], increment 4"
useString("foo") useString("foo")
} }
for i := int64(math.MinInt64 + 8); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \(-9223372036854775806,-9223372036854775800\], increment 4" for i := int64(math.MinInt64 + 8); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775804,-9223372036854775800\], increment 4"
useString("foo") useString("foo")
} }
for i := int64(math.MinInt64 + 7); i > math.MinInt64+2; i -= 4 { for i := int64(math.MinInt64 + 7); i > math.MinInt64+2; i -= 4 {
useString("foo") useString("foo")
} }
for i := int64(math.MinInt64 + 6); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \(-9223372036854775806,-9223372036854775802\], increment 4" for i := int64(math.MinInt64 + 6); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775802,-9223372036854775802\], increment 4"
useString("foo") useString("foo")
} }
for i := int64(math.MinInt64 + 9); i >= math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775806,-9223372036854775799\], increment 4" for i := int64(math.MinInt64 + 9); i >= math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775803,-9223372036854775799\], increment 4"
useString("foo") useString("foo")
} }
for i := int64(math.MinInt64 + 8); i >= math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775806,-9223372036854775800\], increment 4" for i := int64(math.MinInt64 + 8); i >= math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775804,-9223372036854775800\], increment 4"
useString("foo") useString("foo")
} }
for i := int64(math.MinInt64 + 7); i >= math.MinInt64+2; i -= 4 { for i := int64(math.MinInt64 + 7); i >= math.MinInt64+2; i -= 4 {
@ -356,7 +358,7 @@ func bce1() {
panic("invalid test: modulos should differ") panic("invalid test: modulos should differ")
} }
for i := b; i < a; i += z { // ERROR "Induction variable: limits \[-1547,9223372036854774057\), increment 1337" for i := b; i < a; i += z { // ERROR "Induction variable: limits \[-1547,9223372036854772720\], increment 1337"
useString("foobar") useString("foobar")
} }
} }
@ -400,6 +402,22 @@ func issue26116a(a []int) {
} }
} }
func stride1(x *[7]int) int {
s := 0
for i := 0; i <= 8; i += 3 { // ERROR "Induction variable: limits \[0,6\], increment 3"
s += x[i] // ERROR "Proved IsInBounds"
}
return s
}
func stride2(x *[7]int) int {
s := 0
for i := 0; i < 9; i += 3 { // ERROR "Induction variable: limits \[0,6\], increment 3"
s += x[i] // ERROR "Proved IsInBounds"
}
return s
}
//go:noinline //go:noinline
func useString(a string) { func useString(a string) {
} }