-// +build amd64
// errorcheck -0 -d=ssa/prove/debug=1
+//go:build amd64
+
// 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.
}
func f2(a []int) int {
- for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1"
+ for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
a[i+1] = i
a[i+1] = i // ERROR "Proved IsInBounds$"
}
if a == b { // ERROR "Disproved Eq64$"
return 47
}
- if a > b { // ERROR "Disproved Greater64$"
+ if a > b { // ERROR "Disproved Less64$"
return 50
}
if a < b { // ERROR "Proved Less64$"
func f4e(a, b, c int) int {
if a < b {
- if b > a { // ERROR "Proved Greater64$"
+ if b > a { // ERROR "Proved Less64$"
return 101
}
return 103
}
return 114
}
- if b >= a { // ERROR "Proved Geq64$"
+ if b >= a { // ERROR "Proved Leq64$"
if b == a { // ERROR "Proved Eq64$"
return 118
}
}
func f6x(a uint8) int {
- if a > a { // ERROR "Disproved Greater8U$"
+ if a > a { // ERROR "Disproved Less8U$"
return 143
}
return 151
}
func f6e(a uint8) int {
- if a >= a { // ERROR "Proved Geq8U$"
+ if a >= a { // ERROR "Proved Leq8U$"
return 149
}
return 151
}
}
if x {
- if a >= 12 { // ERROR "Proved Geq64$"
+ if a >= 12 { // ERROR "Proved Leq64$"
return 4
}
}
if x {
- if a > 12 { // ERROR "Proved Greater64$"
+ if a > 12 { // ERROR "Proved Less64$"
return 5
}
}
}
}
if x {
- if a >= -9 { // ERROR "Proved Geq64$"
+ if a >= -9 { // ERROR "Proved Leq64$"
return 10
}
}
if x {
- if a > -9 { // ERROR "Disproved Greater64$"
+ if a > -9 { // ERROR "Disproved Less64$"
return 11
}
}
}
}
if x {
- if a >= 90 { // ERROR "Disproved Geq64$"
+ if a >= 90 { // ERROR "Disproved Leq64$"
return 16
}
}
if x {
- if a > 90 { // ERROR "Disproved Greater64$"
+ if a > 90 { // ERROR "Disproved Less64$"
return 17
}
}
func f13e(a int) int {
if a > 9 {
- if a > 5 { // ERROR "Proved Greater64$"
+ if a > 5 { // ERROR "Proved Less64$"
return 1
}
}
if a == 0 {
return 1
}
- if a > 0 { // ERROR "Proved Greater64U$"
+ if a > 0 { // ERROR "Proved Less64U$"
return 2
}
return 3
}
func f17(b []int) {
- for i := 0; i < len(b); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1"
+ 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
_ = b[x]
_ = b[y]
- if x > len(b) { // ERROR "Disproved Greater64$"
+ if x > len(b) { // ERROR "Disproved Less64$"
return
}
- if y > uint(len(b)) { // ERROR "Disproved Greater64U$"
+ if y > uint(len(b)) { // ERROR "Disproved Less64U$"
return
}
- if int(y) > len(b) { // ERROR "Disproved Greater64$"
+ if int(y) > len(b) { // ERROR "Disproved Less64$"
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 Leq64" for the next line.
+ stack = stack[:last]
+ 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$"
+ useSlice(b[2:])
}
}
func lim1(x, y, z int) {
// Test relations between signed and unsigned limits.
if x > 5 {
- if uint(x) > 5 { // ERROR "Proved Greater64U$"
+ if uint(x) > 5 { // ERROR "Proved Less64U$"
return
}
}
if y >= 0 && y < 4 {
- if uint(y) > 4 { // ERROR "Disproved Greater64U$"
+ if uint(y) > 4 { // ERROR "Disproved Less64U$"
return
}
if uint(y) < 5 { // ERROR "Proved Less64U$"
}
if len(b) < cap(b) {
// This eliminates the growslice path.
- b = append(b, 1) // ERROR "Disproved Greater64$"
+ b = append(b, 1) // ERROR "Disproved Less64U$"
}
}
func fence2(x, y int) {
if x-1 < y {
- if x > y { // ERROR "Disproved Greater64$"
+ if x > y { // ERROR "Disproved Less64$"
return
}
}
}
-func fence3(b []int, x, y int64) {
+func fence3(b, c []int, x, y int64) {
if x-1 >= y {
if x <= y { // Can't prove because x may have wrapped.
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 trans1(x, y int64) {
if x > 5 {
if y > x {
- if y > 2 { // ERROR "Proved Greater64"
+ if y > 2 { // ERROR "Proved Less64$"
return
}
} else if y == x {
- if y > 5 { // ERROR "Proved Greater64"
+ if y > 5 { // ERROR "Proved Less64$"
return
}
}
}
if x >= 10 {
if y > x {
- if y > 10 { // ERROR "Proved Greater64"
+ if y > 10 { // ERROR "Proved Less64$"
return
}
}
_ = b[i] // ERROR "Proved IsInBounds$"
}
+func trans4(b []byte, x int) {
+ // Issue #42603: slice len/cap transitive relations.
+ switch x {
+ case 0:
+ if len(b) < 20 {
+ return
+ }
+ _ = b[:2] // ERROR "Proved IsSliceInBounds$"
+ case 1:
+ if len(b) < 40 {
+ return
+ }
+ _ = b[:2] // ERROR "Proved IsSliceInBounds$"
+ }
+}
+
// Derived from nat.cmp
func natcmp(x, y []uint) (r int) {
m := len(x)
}
i := m - 1
- for i > 0 && // ERROR "Induction variable: limits \(0,\?\], increment -1"
+ for i > 0 && // ERROR "Induction variable: limits \(0,\?\], increment 1$"
x[i] == // ERROR "Proved IsInBounds$"
y[i] { // ERROR "Proved IsInBounds$"
i--
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
+ }
+ }
+}
+
+func atexit(foobar []func()) {
+ for i := len(foobar) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1"
+ f := foobar[i]
+ foobar = foobar[:i] // ERROR "IsSliceInBounds"
+ f()
+ }
+}
+
+func make1(n int) []int {
+ s := make([]int, n)
+ for i := 0; i < n; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1"
+ s[i] = 1 // ERROR "Proved IsInBounds$"
+ }
+ return s
+}
+
+func make2(n int) []int {
+ s := make([]int, n)
+ for i := range s { // ERROR "Induction variable: limits \[0,\?\), increment 1"
+ s[i] = 1 // ERROR "Proved IsInBounds$"
+ }
+ return s
+}
+
+// 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 Leq64$"
+ 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 { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
+ b[i][0] = v[0] + 1 // ERROR "Proved IsInBounds$"
+ if i < len(b) { // ERROR "Proved Less64$"
+ println("x")
+ }
+ if i >= 0 { // ERROR "Proved Leq64$"
+ 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$"
+ }
+}
+
+// indexGT0 tests whether prove learns int index >= 0 from bounds check.
+func indexGT0(b []byte, n int) {
+ _ = b[n]
+ _ = 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] // ERROR "Proved IsInBounds$"
+ 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 \(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 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] // ERROR "Proved IsInBounds$"
+ }
+ 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
+}
+
+// The 4 xxxxExtNto64 functions below test whether prove is looking
+// through value-preserving sign/zero extensions of index values (issue #26292).
+
+// Look through all extensions
+func signExtNto64(x []int, j8 int8, j16 int16, j32 int32) int {
+ if len(x) < 22 {
+ return 0
+ }
+ if j8 >= 0 && j8 < 22 {
+ return x[j8] // ERROR "Proved IsInBounds$"
+ }
+ if j16 >= 0 && j16 < 22 {
+ return x[j16] // ERROR "Proved IsInBounds$"
+ }
+ if j32 >= 0 && j32 < 22 {
+ return x[j32] // ERROR "Proved IsInBounds$"
+ }
+ return 0
+}
+
+func zeroExtNto64(x []int, j8 uint8, j16 uint16, j32 uint32) int {
+ if len(x) < 22 {
+ return 0
+ }
+ if j8 >= 0 && j8 < 22 {
+ return x[j8] // ERROR "Proved IsInBounds$"
+ }
+ if j16 >= 0 && j16 < 22 {
+ return x[j16] // ERROR "Proved IsInBounds$"
+ }
+ if j32 >= 0 && j32 < 22 {
+ return x[j32] // ERROR "Proved IsInBounds$"
+ }
+ return 0
+}
+
+// Process fence-post implications through 32to64 extensions (issue #29964)
+func signExt32to64Fence(x []int, j int32) int {
+ if x[j] != 0 {
+ return 1
+ }
+ if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
+ return 1
+ }
+ return 0
+}
+
+func zeroExt32to64Fence(x []int, j uint32) int {
+ if x[j] != 0 {
+ return 1
+ }
+ if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
+ return 1
+ }
+ return 0
+}
+
+// Ensure that bounds checks with negative indexes are not incorrectly removed.
+func negIndex() {
+ n := make([]int, 1)
+ for i := -1; i <= 0; i++ { // ERROR "Induction variable: limits \[-1,0\], increment 1$"
+ n[i] = 1
+ }
+}
+func negIndex2(n int) {
+ a := make([]int, 5)
+ b := make([]int, 5)
+ c := make([]int, 5)
+ for i := -1; i <= 0; i-- {
+ b[i] = i
+ n++
+ if n > 10 {
+ break
+ }
+ }
+ useSlice(a)
+ useSlice(c)
+}
+
+// Check that prove is zeroing these right shifts of positive ints by bit-width - 1.
+// e.g (Rsh64x64 <t> n (Const64 <typ.UInt64> [63])) && ft.isNonNegative(n) -> 0
+func sh64(n int64) int64 {
+ if n < 0 {
+ return n
+ }
+ return n >> 63 // ERROR "Proved Rsh64x64 shifts to zero"
+}
+
+func sh32(n int32) int32 {
+ if n < 0 {
+ return n
+ }
+ return n >> 31 // ERROR "Proved Rsh32x64 shifts to zero"
+}
+
+func sh32x64(n int32) int32 {
+ if n < 0 {
+ return n
+ }
+ return n >> uint64(31) // ERROR "Proved Rsh32x64 shifts to zero"
+}
+
+func sh16(n int16) int16 {
+ if n < 0 {
+ return n
+ }
+ return n >> 15 // ERROR "Proved Rsh16x64 shifts to zero"
+}
+
+func sh64noopt(n int64) int64 {
+ return n >> 63 // not optimized; n could be negative
+}
+
+// These cases are division of a positive signed integer by a power of 2.
+// The opt pass doesnt have sufficient information to see that n is positive.
+// So, instead, opt rewrites the division with a less-than-optimal replacement.
+// Prove, which can see that n is nonnegative, cannot see the division because
+// opt, an earlier pass, has already replaced it.
+// The fix for this issue allows prove to zero a right shift that was added as
+// part of the less-than-optimal reqwrite. That change by prove then allows
+// lateopt to clean up all the unnecessary parts of the original division
+// replacement. See issue #36159.
+func divShiftClean(n int) int {
+ if n < 0 {
+ return n
+ }
+ return n / int(8) // ERROR "Proved Rsh64x64 shifts to zero"
+}
+
+func divShiftClean64(n int64) int64 {
+ if n < 0 {
+ return n
+ }
+ return n / int64(16) // ERROR "Proved Rsh64x64 shifts to zero"
+}
+
+func divShiftClean32(n int32) int32 {
+ if n < 0 {
+ return n
+ }
+ return n / int32(16) // ERROR "Proved Rsh32x64 shifts to zero"
+}
+
+// Bounds check elimination
+
+func sliceBCE1(p []string, h uint) string {
+ if len(p) == 0 {
+ return ""
+ }
+
+ i := h & uint(len(p)-1)
+ return p[i] // ERROR "Proved IsInBounds$"
+}
+
+func sliceBCE2(p []string, h int) string {
+ if len(p) == 0 {
+ return ""
+ }
+ i := h & (len(p) - 1)
+ return p[i] // ERROR "Proved IsInBounds$"
+}
+
+func and(p []byte) ([]byte, []byte) { // issue #52563
+ const blocksize = 16
+ fullBlocks := len(p) &^ (blocksize - 1)
+ blk := p[:fullBlocks] // ERROR "Proved IsSliceInBounds$"
+ rem := p[fullBlocks:] // ERROR "Proved IsSliceInBounds$"
+ return blk, rem
+}
+
+func rshu(x, y uint) int {
+ z := x >> y
+ if z <= x { // ERROR "Proved Leq64U$"
+ return 1
+ }
+ return 0
+}
+
+func divu(x, y uint) int {
+ z := x / y
+ if z <= x { // ERROR "Proved Leq64U$"
+ return 1
+ }
+ return 0
+}
+
+func modu1(x, y uint) int {
+ z := x % y
+ if z < y { // ERROR "Proved Less64U$"
+ return 1
+ }
+ return 0
+}
+
+func modu2(x, y uint) int {
+ z := x % y
+ if z <= x { // ERROR "Proved Leq64U$"
+ return 1
+ }
+ return 0
+}
+
+func issue57077(s []int) (left, right []int) {
+ middle := len(s) / 2
+ left = s[:middle] // ERROR "Proved IsSliceInBounds$"
+ right = s[middle:] // ERROR "Proved IsSliceInBounds$"
+ return
+}
+
+func issue51622(b []byte) int {
+ if len(b) >= 3 && b[len(b)-3] == '#' { // ERROR "Proved IsInBounds$"
+ return len(b)
+ }
+ return 0
+}
+
+func issue45928(x int) {
+ combinedFrac := x / (x | (1 << 31)) // ERROR "Proved Neq64$"
+ useInt(combinedFrac)
+}
+
//go:noinline
func useInt(a int) {
}