diff options
author | Giovanni Bajo <rasky@develer.com> | 2018-04-15 16:52:49 +0200 |
---|---|---|
committer | Giovanni Bajo <rasky@develer.com> | 2018-04-29 09:38:32 +0000 |
commit | e0d37a33ab6260f5acc68dbb9a02c3135d19bcbb (patch) | |
tree | 7b4b421739d0e12b6a4a964721dcd52560857168 /test/loopbce.go | |
parent | 6d379add0fefcc17ed7b763078526800a3c1d705 (diff) | |
download | go-e0d37a33ab6260f5acc68dbb9a02c3135d19bcbb.tar.gz go-e0d37a33ab6260f5acc68dbb9a02c3135d19bcbb.zip |
cmd/compile: teach prove to handle expressions like len(s)-delta
When a loop has bound len(s)-delta, findIndVar detected it and
returned len(s) as (conservative) upper bound. This little lie
allowed loopbce to drop bound checks.
It is obviously more generic to teach prove about relations like
x+d<w for non-constant "w"; we already handled the case for
constant "w", so we just want to learn that if d<0, then x+d<w
proves that x<w.
To be able to remove the code from findIndVar, we also need
to teach prove that len() and cap() are always non-negative.
This CL allows to prove 633 more checks in cmd+std. Most
of them are cases where the code was already testing before
accessing a slice but the compiler didn't know it. For instance,
take strings.HasSuffix:
func HasSuffix(s, suffix string) bool {
return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
}
When suffix is a literal string, the compiler now understands
that the explicit check is enough to not emit a slice check.
I also found a loopbce test that was incorrectly
written to detect an overflow but had a off-by-one (on the
conservative side), so it unexpectly passed with this CL; I
changed it to really trigger the overflow as intended.
Change-Id: Ib5abade337db46b8811425afebad4719b6e46c4a
Reviewed-on: https://go-review.googlesource.com/105635
Run-TryBot: Giovanni Bajo <rasky@develer.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: David Chase <drchase@google.com>
Diffstat (limited to 'test/loopbce.go')
-rw-r--r-- | test/loopbce.go | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/test/loopbce.go b/test/loopbce.go index 6ef183dea8..c93bfc8f00 100644 --- a/test/loopbce.go +++ b/test/loopbce.go @@ -100,6 +100,22 @@ func g0d(a string) int { return x } +func g0e(a string) int { + x := 0 + for i := len(a) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment -1$" + x += int(a[i]) // ERROR "Proved IsInBounds$" + } + return x +} + +func g0f(a string) int { + x := 0 + for i := len(a) - 1; 0 <= i; i-- { // ERROR "Induction variable: limits \[0,\?\], increment -1$" + x += int(a[i]) // ERROR "Proved IsInBounds$" + } + return x +} + func g1() int { a := "evenlength" x := 0 @@ -265,7 +281,14 @@ func nobce2(a string) { useString(a[i:]) // ERROR "Proved IsSliceInBounds$" } for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" - // tests an overflow of StringLen-MinInt64 + useString(a[i:]) // ERROR "Proved IsSliceInBounds$" + } + j := int64(len(a)) - 123 + for i := int64(0); i < j+123+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" + useString(a[i:]) // ERROR "Proved IsSliceInBounds$" + } + for i := int64(0); i < j+122+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" + // len(a)-123+122+MinInt overflows when len(a) == 0, so a bound check is needed here useString(a[i:]) } } |