-// +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.
last := len(stack) - 1
e = stack[last]
// Buggy compiler prints "Disproved Leq64" for the next line.
- stack = stack[:last] // ERROR "Proved IsSliceInBounds"
+ stack = stack[:last]
return e, nil
}
_ = 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)
// 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$"
+ 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")
}
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] // ERROR "Proved IsInBounds$"
x += a[i+1]
}
if i == len(a)-1 {
// 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$"
+ 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$"
}
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]
+ x += a[i-2] // ERROR "Proved IsInBounds$"
}
if i == 1 {
x += a[i-1]
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) {
}