From 73df946d56c74384511a194dd01dbe099584fd1a Mon Sep 17 00:00:00 2001 From: Daniel Baumann Date: Sun, 28 Apr 2024 15:14:23 +0200 Subject: Adding upstream version 1.16.10. Signed-off-by: Daniel Baumann --- test/prove.go | 1032 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1032 insertions(+) create mode 100644 test/prove.go (limited to 'test/prove.go') diff --git a/test/prove.go b/test/prove.go new file mode 100644 index 0000000..d37021d --- /dev/null +++ b/test/prove.go @@ -0,0 +1,1032 @@ +// +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 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] // 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:]) + } +} + +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$" +} + +// 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 { + 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 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] + 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 +} + +// 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 n (Const64 [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 unneccesary 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" +} + +//go:noinline +func useInt(a int) { +} + +//go:noinline +func useSlice(a []int) { +} + +func main() { +} -- cgit v1.2.3