Adding upstream version 1.22.1.upstream/1.22.1

Signed-off-by: Daniel Baumann <daniel.baumann@progress-linux.org>

1 files changed, 1127 insertions, 0 deletions

diff --git a/test/prove.go b/test/prove.go
new file mode 100644
index 0000000..1aea282
--- /dev/null
+++ b/test/prove.go
@@ -0,0 +1,1127 @@
+// 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.
+
+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 Less64$"
+			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 Less64$"
+			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 Leq64$"
+			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 Less8U$"
+		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 Leq8U$"
+		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 Leq64$"
+				return 4
+			}
+		}
+		if x {
+			if a > 12 { // ERROR "Proved Less64$"
+				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 Leq64$"
+				return 10
+			}
+		}
+		if x {
+			if a > -9 { // ERROR "Disproved Less64$"
+				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 Leq64$"
+				return 16
+			}
+		}
+		if x {
+			if a > 90 { // ERROR "Disproved Less64$"
+				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 Less64$"
+			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 Less64U$"
+		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 Less64$"
+		return
+	}
+	if y > uint(len(b)) { // ERROR "Disproved Less64U$"
+		return
+	}
+	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:])
+	}
+}
+
+func lim1(x, y, z int) {
+	// Test relations between signed and unsigned limits.
+	if x > 5 {
+		if uint(x) > 5 { // ERROR "Proved Less64U$"
+			return
+		}
+	}
+	if y >= 0 && y < 4 {
+		if uint(y) > 4 { // ERROR "Disproved Less64U$"
+			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 Less64U$"
+	}
+}
+
+func fence2(x, y int) {
+	if x-1 < y {
+		if x > y { // ERROR "Disproved Less64$"
+			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 Less64$"
+				return
+			}
+		} else if y == x {
+			if y > 5 { // ERROR "Proved Less64$"
+				return
+			}
+		}
+	}
+	if x >= 10 {
+		if y > x {
+			if y > 10 { // ERROR "Proved Less64$"
+				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$"
+}
+
+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)
+	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
+		}
+	}
+}
+
+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) {
+}
+
+//go:noinline
+func useSlice(a []int) {
+}
+
+func main() {
+}