diff options
author | Giovanni Bajo <rasky@develer.com> | 2018-04-03 18:58:01 +0200 |
---|---|---|
committer | Giovanni Bajo <rasky@develer.com> | 2018-04-03 20:25:34 +0000 |
commit | ac43de3ae5027f61e6b028c806f6b83f80ee5d3b (patch) | |
tree | c3d475d6f15a36e856a2d7353bcbec0282be5e1b /test/prove.go | |
parent | b846edfd5979d1cf53d55ea8fd6e4bbcfefb2e75 (diff) | |
download | go-ac43de3ae5027f61e6b028c806f6b83f80ee5d3b.tar.gz go-ac43de3ae5027f61e6b028c806f6b83f80ee5d3b.zip |
cmd/compile: in prove, complete support for OpIsInBounds/OpIsSliceInBounds
The logic in addBranchRestrictions didn't allow to correctly
model OpIs(Slice)Bound for signed domain, and it was also partly
implemented within addRestrictions.
Thanks to the previous changes, it is now possible to handle
the negative conditions correctly, so that we can learn
both signed/LT + unsigned/LT on the positive side, and
signed/GE + unsigned/GE on the negative side (but only if
the index can be proved to be non-negative).
This is able to prove ~50 more slice accesses in std+cmd.
Change-Id: I9858080dc03b16f85993a55983dbc4b00f8491b0
Reviewed-on: https://go-review.googlesource.com/104037
Run-TryBot: Giovanni Bajo <rasky@develer.com>
TryBot-Result: Gobot Gobot <gobot@golang.org>
Reviewed-by: Austin Clements <austin@google.com>
Diffstat (limited to 'test/prove.go')
-rw-r--r-- | test/prove.go | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test/prove.go b/test/prove.go index 97614939ac..197bdb0aef 100644 --- a/test/prove.go +++ b/test/prove.go @@ -475,6 +475,21 @@ func f17(b []int) { } } +func f18(b []int, x int, y uint) { + _ = b[x] + _ = b[y] + + if x > len(b) { // ERROR "Disproved Greater64$" + return + } + if y > uint(len(b)) { // ERROR "Disproved Greater64U$" + return + } + if int(y) > len(b) { // ERROR "Disproved Greater64$" + return + } +} + func sm1(b []int, x int) { // Test constant argument to slicemask. useSlice(b[2:8]) // ERROR "Proved slicemask not needed$" |