| // +build amd64 |
| // errorcheck -0 -d=ssa/prove/debug=1 |
| |
| // Copyright 2016 The Go Authors. All rights reserved. |
| // Use of this source code is governed by a BSD-style |
| // license that can be found in the LICENSE file. |
| |
| package main |
| |
| import "math" |
| |
| func f0(a []int) int { |
| a[0] = 1 |
| a[0] = 1 // ERROR "Proved boolean IsInBounds$" |
| a[6] = 1 |
| a[6] = 1 // ERROR "Proved boolean IsInBounds$" |
| a[5] = 1 // ERROR "Proved IsInBounds$" |
| a[5] = 1 // ERROR "Proved boolean IsInBounds$" |
| return 13 |
| } |
| |
| func f1(a []int) int { |
| if len(a) <= 5 { |
| return 18 |
| } |
| a[0] = 1 // ERROR "Proved non-negative bounds IsInBounds$" |
| a[0] = 1 // ERROR "Proved boolean IsInBounds$" |
| a[6] = 1 |
| a[6] = 1 // ERROR "Proved boolean IsInBounds$" |
| a[5] = 1 // ERROR "Proved IsInBounds$" |
| a[5] = 1 // ERROR "Proved boolean IsInBounds$" |
| return 26 |
| } |
| |
| func f1b(a []int, i int, j uint) int { |
| if i >= 0 && i < len(a) { |
| return a[i] // ERROR "Proved non-negative bounds IsInBounds$" |
| } |
| if i >= 10 && i < len(a) { |
| return a[i] // ERROR "Proved non-negative bounds IsInBounds$" |
| } |
| if i >= 10 && i < len(a) { |
| return a[i] // ERROR "Proved non-negative bounds IsInBounds$" |
| } |
| if i >= 10 && i < len(a) { // todo: handle this case |
| return a[i-10] |
| } |
| if j < uint(len(a)) { |
| return a[j] // ERROR "Proved IsInBounds$" |
| } |
| return 0 |
| } |
| |
| func f1c(a []int, i int64) int { |
| c := uint64(math.MaxInt64 + 10) // overflows int |
| d := int64(c) |
| if i >= d && i < int64(len(a)) { |
| // d overflows, should not be handled. |
| return a[i] |
| } |
| return 0 |
| } |
| |
| func f2(a []int) int { |
| for i := range a { |
| a[i+1] = i |
| a[i+1] = i // ERROR "Proved boolean IsInBounds$" |
| } |
| return 34 |
| } |
| |
| func f3(a []uint) int { |
| for i := uint(0); i < uint(len(a)); i++ { |
| a[i] = i // ERROR "Proved IsInBounds$" |
| } |
| return 41 |
| } |
| |
| func f4a(a, b, c int) int { |
| if a < b { |
| if a == b { // ERROR "Disproved Eq64$" |
| return 47 |
| } |
| if a > b { // ERROR "Disproved Greater64$" |
| return 50 |
| } |
| if a < b { // ERROR "Proved boolean Less64$" |
| return 53 |
| } |
| if a == b { // ERROR "Disproved boolean Eq64$" |
| return 56 |
| } |
| if a > b { // ERROR "Disproved boolean Greater64$" |
| return 59 |
| } |
| return 61 |
| } |
| return 63 |
| } |
| |
| func f4b(a, b, c int) int { |
| if a <= b { |
| if a >= b { |
| if a == b { // ERROR "Proved Eq64$" |
| return 70 |
| } |
| return 75 |
| } |
| return 77 |
| } |
| return 79 |
| } |
| |
| func f4c(a, b, c int) int { |
| if a <= b { |
| if a >= b { |
| if a != b { // ERROR "Disproved Neq64$" |
| return 73 |
| } |
| return 75 |
| } |
| return 77 |
| } |
| return 79 |
| } |
| |
| func f4d(a, b, c int) int { |
| if a < b { |
| if a < c { |
| if a < b { // ERROR "Proved boolean Less64$" |
| if a < c { // ERROR "Proved boolean Less64$" |
| return 87 |
| } |
| return 89 |
| } |
| return 91 |
| } |
| return 93 |
| } |
| return 95 |
| } |
| |
| func f4e(a, b, c int) int { |
| if a < b { |
| if b > a { // ERROR "Proved Greater64$" |
| return 101 |
| } |
| return 103 |
| } |
| return 105 |
| } |
| |
| func f4f(a, b, c int) int { |
| if a <= b { |
| if b > a { |
| if b == a { // ERROR "Disproved Eq64$" |
| return 112 |
| } |
| return 114 |
| } |
| if b >= a { // ERROR "Proved Geq64$" |
| if b == a { // ERROR "Proved Eq64$" |
| return 118 |
| } |
| return 120 |
| } |
| return 122 |
| } |
| return 124 |
| } |
| |
| func f5(a, b uint) int { |
| if a == b { |
| if a <= b { // ERROR "Proved Leq64U$" |
| return 130 |
| } |
| return 132 |
| } |
| return 134 |
| } |
| |
| // These comparisons are compile time constants. |
| func f6a(a uint8) int { |
| if a < a { // ERROR "Disproved Less8U$" |
| return 140 |
| } |
| return 151 |
| } |
| |
| func f6b(a uint8) int { |
| if a < a { // ERROR "Disproved Less8U$" |
| return 140 |
| } |
| return 151 |
| } |
| |
| func f6x(a uint8) int { |
| if a > a { // ERROR "Disproved Greater8U$" |
| return 143 |
| } |
| return 151 |
| } |
| |
| func f6d(a uint8) int { |
| if a <= a { // ERROR "Proved Leq8U$" |
| return 146 |
| } |
| return 151 |
| } |
| |
| func f6e(a uint8) int { |
| if a >= a { // ERROR "Proved Geq8U$" |
| return 149 |
| } |
| return 151 |
| } |
| |
| func f7(a []int, b int) int { |
| if b < len(a) { |
| a[b] = 3 |
| if b < len(a) { // ERROR "Proved boolean Less64$" |
| a[b] = 5 // ERROR "Proved boolean IsInBounds$" |
| } |
| } |
| return 161 |
| } |
| |
| func f8(a, b uint) int { |
| if a == b { |
| return 166 |
| } |
| if a > b { |
| return 169 |
| } |
| if a < b { // ERROR "Proved Less64U$" |
| return 172 |
| } |
| return 174 |
| } |
| |
| func f9(a, b bool) int { |
| if a { |
| return 1 |
| } |
| if a || b { // ERROR "Disproved boolean Arg$" |
| return 2 |
| } |
| return 3 |
| } |
| |
| func f10(a string) int { |
| n := len(a) |
| // We optimize comparisons with small constant strings (see cmd/compile/internal/gc/walk.go), |
| // so this string literal must be long. |
| if a[:n>>1] == "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" { |
| return 0 |
| } |
| return 1 |
| } |
| |
| func f11a(a []int, i int) { |
| useInt(a[i]) |
| useInt(a[i]) // ERROR "Proved boolean IsInBounds$" |
| } |
| |
| func f11b(a []int, i int) { |
| useSlice(a[i:]) |
| useSlice(a[i:]) // ERROR "Proved boolean IsSliceInBounds$" |
| } |
| |
| func f11c(a []int, i int) { |
| useSlice(a[:i]) |
| useSlice(a[:i]) // ERROR "Proved boolean IsSliceInBounds$" |
| } |
| |
| func f11d(a []int, i int) { |
| useInt(a[2*i+7]) |
| useInt(a[2*i+7]) // ERROR "Proved boolean IsInBounds$" |
| } |
| |
| func f12(a []int, b int) { |
| useSlice(a[:b]) |
| } |
| |
| func f13a(a, b, c int, x bool) int { |
| if a > 12 { |
| if x { |
| if a < 12 { // ERROR "Disproved Less64$" |
| return 1 |
| } |
| } |
| if x { |
| if a <= 12 { // ERROR "Disproved Leq64$" |
| return 2 |
| } |
| } |
| if x { |
| if a == 12 { // ERROR "Disproved Eq64$" |
| return 3 |
| } |
| } |
| if x { |
| if a >= 12 { // ERROR "Proved Geq64$" |
| return 4 |
| } |
| } |
| if x { |
| if a > 12 { // ERROR "Proved boolean Greater64$" |
| return 5 |
| } |
| } |
| return 6 |
| } |
| return 0 |
| } |
| |
| func f13b(a int, x bool) int { |
| if a == -9 { |
| if x { |
| if a < -9 { // ERROR "Disproved Less64$" |
| return 7 |
| } |
| } |
| if x { |
| if a <= -9 { // ERROR "Proved Leq64$" |
| return 8 |
| } |
| } |
| if x { |
| if a == -9 { // ERROR "Proved boolean Eq64$" |
| return 9 |
| } |
| } |
| if x { |
| if a >= -9 { // ERROR "Proved Geq64$" |
| return 10 |
| } |
| } |
| if x { |
| if a > -9 { // ERROR "Disproved Greater64$" |
| return 11 |
| } |
| } |
| return 12 |
| } |
| return 0 |
| } |
| |
| func f13c(a int, x bool) int { |
| if a < 90 { |
| if x { |
| if a < 90 { // ERROR "Proved boolean Less64$" |
| return 13 |
| } |
| } |
| if x { |
| if a <= 90 { // ERROR "Proved Leq64$" |
| return 14 |
| } |
| } |
| if x { |
| if a == 90 { // ERROR "Disproved Eq64$" |
| return 15 |
| } |
| } |
| if x { |
| if a >= 90 { // ERROR "Disproved Geq64$" |
| return 16 |
| } |
| } |
| if x { |
| if a > 90 { // ERROR "Disproved Greater64$" |
| return 17 |
| } |
| } |
| return 18 |
| } |
| return 0 |
| } |
| |
| func f13d(a int) int { |
| if a < 5 { |
| if a < 9 { // ERROR "Proved Less64$" |
| return 1 |
| } |
| } |
| return 0 |
| } |
| |
| func f13e(a int) int { |
| if a > 9 { |
| if a > 5 { // ERROR "Proved Greater64$" |
| return 1 |
| } |
| } |
| return 0 |
| } |
| |
| func f13f(a int64) int64 { |
| if a > math.MaxInt64 { |
| // Unreachable, but prove doesn't know that. |
| if a == 0 { |
| return 1 |
| } |
| } |
| return 0 |
| } |
| |
| func f13g(a int) int { |
| if a < 3 { |
| return 5 |
| } |
| if a > 3 { |
| return 6 |
| } |
| if a == 3 { // ERROR "Proved Eq64$" |
| return 7 |
| } |
| return 8 |
| } |
| |
| func f13h(a int) int { |
| if a < 3 { |
| if a > 1 { |
| if a == 2 { // ERROR "Proved Eq64$" |
| return 5 |
| } |
| } |
| } |
| return 0 |
| } |
| |
| func f13i(a uint) int { |
| if a == 0 { |
| return 1 |
| } |
| if a > 0 { // ERROR "Proved Greater64U$" |
| return 2 |
| } |
| return 3 |
| } |
| |
| func f14(p, q *int, a []int) { |
| // This crazy ordering usually gives i1 the lowest value ID, |
| // j the middle value ID, and i2 the highest value ID. |
| // That used to confuse CSE because it ordered the args |
| // of the two + ops below differently. |
| // That in turn foiled bounds check elimination. |
| i1 := *p |
| j := *q |
| i2 := *p |
| useInt(a[i1+j]) |
| useInt(a[i2+j]) // ERROR "Proved boolean IsInBounds$" |
| } |
| |
| func f15(s []int, x int) { |
| useSlice(s[x:]) |
| useSlice(s[:x]) // ERROR "Proved IsSliceInBounds$" |
| } |
| |
| func f16(s []int) []int { |
| if len(s) >= 10 { |
| return s[:10] // ERROR "Proved non-negative bounds IsSliceInBounds$" |
| } |
| return nil |
| } |
| |
| //go:noinline |
| func useInt(a int) { |
| } |
| |
| //go:noinline |
| func useSlice(a []int) { |
| } |
| |
| func main() { |
| } |