]> Cypherpunks repositories - gostls13.git/commit
cmd/compile: teach prove to handle expressions like len(s)-delta
authorGiovanni Bajo <rasky@develer.com>
Sun, 15 Apr 2018 14:52:49 +0000 (16:52 +0200)
committerGiovanni Bajo <rasky@develer.com>
Sun, 29 Apr 2018 09:38:32 +0000 (09:38 +0000)
commite0d37a33ab6260f5acc68dbb9a02c3135d19bcbb
tree7b4b421739d0e12b6a4a964721dcd52560857168
parent6d379add0fefcc17ed7b763078526800a3c1d705
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>
src/cmd/compile/internal/ssa/loopbce.go
src/cmd/compile/internal/ssa/prove.go
test/loopbce.go
test/prove.go