// +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 IsInBounds$" a[6] = 1 a[6] = 1 // ERROR "Proved IsInBounds$" a[5] = 1 // ERROR "Proved IsInBounds$" a[5] = 1 // ERROR "Proved IsInBounds$" return 13 } func f1(a []int) int { if len(a) <= 5 { return 18 } a[0] = 1 // ERROR "Proved IsInBounds$" a[0] = 1 // ERROR "Proved IsInBounds$" a[6] = 1 a[6] = 1 // ERROR "Proved IsInBounds$" a[5] = 1 // ERROR "Proved IsInBounds$" a[5] = 1 // ERROR "Proved IsInBounds$" return 26 } func f1b(a []int, i int, j uint) int { if i >= 0 && i < len(a) { return a[i] // ERROR "Proved IsInBounds$" } if i >= 10 && i < len(a) { return a[i] // ERROR "Proved IsInBounds$" } if i >= 10 && i < len(a) { return a[i] // ERROR "Proved IsInBounds$" } if i >= 10 && i < len(a) { return a[i-10] // ERROR "Proved IsInBounds$" } 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 { // ERROR "Induction variable: limits \[0,\?\), increment 1$" a[i+1] = i a[i+1] = i // ERROR "Proved 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 Less64$" return 53 } // We can't get to this point and prove knows that, so // there's no message for the next (obvious) branch. if a != a { return 56 } 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 Less64$" if a < c { // ERROR "Proved 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 Less64$" a[b] = 5 // ERROR "Proved 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 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 IsInBounds$" } func f11b(a []int, i int) { useSlice(a[i:]) useSlice(a[i:]) // ERROR "Proved IsSliceInBounds$" } func f11c(a []int, i int) { useSlice(a[:i]) useSlice(a[:i]) // ERROR "Proved IsSliceInBounds$" } func f11d(a []int, i int) { useInt(a[2*i+7]) useInt(a[2*i+7]) // ERROR "Proved 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 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 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 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 { if a == 0 { // ERROR "Disproved Eq64$" 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 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 IsSliceInBounds$" } return nil } func f17(b []int) { for i := 0; i < len(b); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" // This tests for i <= cap, which we can only prove // using the derived relation between len and cap. // This depends on finding the contradiction, since we // don't query this condition directly. useSlice(b[:i]) // ERROR "Proved IsSliceInBounds$" } } 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 f19() (e int64, err error) { // Issue 29502: slice[:0] is incorrectly disproved. var stack []int64 stack = append(stack, 123) if len(stack) > 1 { panic("too many elements") } last := len(stack) - 1 e = stack[last] // Buggy compiler prints "Disproved Geq64" for the next line. stack = stack[:last] // ERROR "Proved IsSliceInBounds" return e, nil } func sm1(b []int, x int) { // Test constant argument to slicemask. useSlice(b[2:8]) // ERROR "Proved slicemask not needed$" // Test non-constant argument with known limits. if cap(b) > 10 { useSlice(b[2:]) // ERROR "Proved slicemask not needed$" } } func lim1(x, y, z int) { // Test relations between signed and unsigned limits. if x > 5 { if uint(x) > 5 { // ERROR "Proved Greater64U$" return } } if y >= 0 && y < 4 { if uint(y) > 4 { // ERROR "Disproved Greater64U$" return } if uint(y) < 5 { // ERROR "Proved Less64U$" return } } if z < 4 { if uint(z) > 4 { // Not provable without disjunctions. return } } } // fence1–4 correspond to the four fence-post implications. func fence1(b []int, x, y int) { // Test proofs that rely on fence-post implications. if x+1 > y { if x < y { // ERROR "Disproved Less64$" return } } if len(b) < cap(b) { // This eliminates the growslice path. b = append(b, 1) // ERROR "Disproved Greater64U$" } } func fence2(x, y int) { if x-1 < y { if x > y { // ERROR "Disproved Greater64$" return } } } func fence3(b, c []int, x, y int64) { if x-1 >= y { if x <= y { // Can't prove because x may have wrapped. return } } if x != math.MinInt64 && x-1 >= y { if x <= y { // ERROR "Disproved Leq64$" return } } c[len(c)-1] = 0 // Can't prove because len(c) might be 0 if n := len(b); n > 0 { b[n-1] = 0 // ERROR "Proved IsInBounds$" } } func fence4(x, y int64) { if x >= y+1 { if x <= y { return } } if y != math.MaxInt64 && x >= y+1 { if x <= y { // ERROR "Disproved Leq64$" return } } } // Check transitive relations func trans1(x, y int64) { if x > 5 { if y > x { if y > 2 { // ERROR "Proved Greater64$" return } } else if y == x { if y > 5 { // ERROR "Proved Greater64$" return } } } if x >= 10 { if y > x { if y > 10 { // ERROR "Proved Greater64$" return } } } } func trans2(a, b []int, i int) { if len(a) != len(b) { return } _ = a[i] _ = b[i] // ERROR "Proved IsInBounds$" } func trans3(a, b []int, i int) { if len(a) > len(b) { return } _ = a[i] _ = b[i] // ERROR "Proved IsInBounds$" } // Derived from nat.cmp func natcmp(x, y []uint) (r int) { m := len(x) n := len(y) if m != n || m == 0 { return } i := m - 1 for i > 0 && // ERROR "Induction variable: limits \(0,\?\], increment 1$" x[i] == // ERROR "Proved IsInBounds$" y[i] { // ERROR "Proved IsInBounds$" i-- } switch { case x[i] < // todo, cannot prove this because it's dominated by i<=0 || x[i]==y[i] y[i]: // ERROR "Proved IsInBounds$" r = -1 case x[i] > // ERROR "Proved IsInBounds$" y[i]: // ERROR "Proved IsInBounds$" r = 1 } return } func suffix(s, suffix string) bool { // todo, we're still not able to drop the bound check here in the general case return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix } func constsuffix(s string) bool { return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$" } // oforuntil tests the pattern created by OFORUNTIL blocks. These are // handled by addLocalInductiveFacts rather than findIndVar. func oforuntil(b []int) { i := 0 if len(b) > i { top: println(b[i]) // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Proved IsInBounds$" i++ if i < len(b) { goto top } } } // The range tests below test the index variable of range loops. // range1 compiles to the "efficiently indexable" form of a range loop. func range1(b []int) { for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$" b[i] = v + 1 // ERROR "Proved IsInBounds$" if i < len(b) { // ERROR "Proved Less64$" println("x") } if i >= 0 { // ERROR "Proved Geq64$" println("x") } } } // range2 elements are larger, so they use the general form of a range loop. func range2(b [][32]int) { for i, v := range b { b[i][0] = v[0] + 1 // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Proved IsInBounds$" if i < len(b) { // ERROR "Proved Less64$" println("x") } if i >= 0 { // ERROR "Proved Geq64$" println("x") } } } // signhint1-2 test whether the hint (int >= 0) is propagated into the loop. func signHint1(i int, data []byte) { if i >= 0 { for i < len(data) { // ERROR "Induction variable: limits \[\?,\?\), increment 1$" _ = data[i] // ERROR "Proved IsInBounds$" i++ } } } func signHint2(b []byte, n int) { if n < 0 { panic("") } _ = b[25] for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$" b[i] = 123 // ERROR "Proved IsInBounds$" } } // Induction variable in unrolled loop. func unrollUpExcl(a []int) int { var i, x int for i = 0; i < len(a)-1; i += 2 { // ERROR "Induction variable: limits \[0,\?\), increment 2$" x += a[i] // ERROR "Proved IsInBounds$" x += a[i+1] } if i == len(a)-1 { x += a[i] } return x } // Induction variable in unrolled loop. func unrollUpIncl(a []int) int { var i, x int for i = 0; i <= len(a)-2; i += 2 { // ERROR "Induction variable: limits \[0,\?\], increment 2$" x += a[i] x += a[i+1] } if i == len(a)-1 { x += a[i] } return x } // Induction variable in unrolled loop. func unrollDownExcl0(a []int) int { var i, x int for i = len(a) - 1; i > 0; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$" x += a[i] // ERROR "Proved IsInBounds$" x += a[i-1] // ERROR "Proved IsInBounds$" } if i == 0 { x += a[i] } return x } // Induction variable in unrolled loop. func unrollDownExcl1(a []int) int { var i, x int for i = len(a) - 1; i >= 1; i -= 2 { // ERROR "Induction variable: limits \[1,\?\], increment 2$" x += a[i] // ERROR "Proved IsInBounds$" x += a[i-1] // ERROR "Proved IsInBounds$" } if i == 0 { x += a[i] } return x } // Induction variable in unrolled loop. func unrollDownInclStep(a []int) int { var i, x int for i = len(a); i >= 2; i -= 2 { // ERROR "Induction variable: limits \[2,\?\], increment 2$" x += a[i-1] // ERROR "Proved IsInBounds$" x += a[i-2] } if i == 1 { x += a[i-1] } return x } // Not an induction variable (step too large) func unrollExclStepTooLarge(a []int) int { var i, x int for i = 0; i < len(a)-1; i += 3 { x += a[i] x += a[i+1] } if i == len(a)-1 { x += a[i] } return x } // Not an induction variable (step too large) func unrollInclStepTooLarge(a []int) int { var i, x int for i = 0; i <= len(a)-2; i += 3 { x += a[i] x += a[i+1] } if i == len(a)-1 { x += a[i] } return x } // Not an induction variable (min too small, iterating down) func unrollDecMin(a []int) int { var i, x int for i = len(a); i >= math.MinInt64; i -= 2 { x += a[i-1] x += a[i-2] } if i == 1 { // ERROR "Disproved Eq64$" x += a[i-1] } return x } // Not an induction variable (min too small, iterating up -- perhaps could allow, but why bother?) func unrollIncMin(a []int) int { var i, x int for i = len(a); i >= math.MinInt64; i += 2 { x += a[i-1] x += a[i-2] } if i == 1 { // ERROR "Disproved Eq64$" x += a[i-1] } return x } //go:noinline func useInt(a int) { } //go:noinline func useSlice(a []int) { } func main() { }