2 // errorcheck -0 -d=ssa/prove/debug=1
4 // Copyright 2016 The Go Authors. All rights reserved.
5 // Use of this source code is governed by a BSD-style
6 // license that can be found in the LICENSE file.
12 func f0(a []int) int {
14 a[0] = 1 // ERROR "Proved IsInBounds$"
16 a[6] = 1 // ERROR "Proved IsInBounds$"
17 a[5] = 1 // ERROR "Proved IsInBounds$"
18 a[5] = 1 // ERROR "Proved IsInBounds$"
22 func f1(a []int) int {
26 a[0] = 1 // ERROR "Proved IsInBounds$"
27 a[0] = 1 // ERROR "Proved IsInBounds$"
29 a[6] = 1 // ERROR "Proved IsInBounds$"
30 a[5] = 1 // ERROR "Proved IsInBounds$"
31 a[5] = 1 // ERROR "Proved IsInBounds$"
35 func f1b(a []int, i int, j uint) int {
36 if i >= 0 && i < len(a) {
37 return a[i] // ERROR "Proved IsInBounds$"
39 if i >= 10 && i < len(a) {
40 return a[i] // ERROR "Proved IsInBounds$"
42 if i >= 10 && i < len(a) {
43 return a[i] // ERROR "Proved IsInBounds$"
45 if i >= 10 && i < len(a) {
46 return a[i-10] // ERROR "Proved IsInBounds$"
49 return a[j] // ERROR "Proved IsInBounds$"
54 func f1c(a []int, i int64) int {
55 c := uint64(math.MaxInt64 + 10) // overflows int
57 if i >= d && i < int64(len(a)) {
58 // d overflows, should not be handled.
64 func f2(a []int) int {
65 for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
67 a[i+1] = i // ERROR "Proved IsInBounds$"
72 func f3(a []uint) int {
73 for i := uint(0); i < uint(len(a)); i++ {
74 a[i] = i // ERROR "Proved IsInBounds$"
79 func f4a(a, b, c int) int {
81 if a == b { // ERROR "Disproved Eq64$"
84 if a > b { // ERROR "Disproved Less64$"
87 if a < b { // ERROR "Proved Less64$"
90 // We can't get to this point and prove knows that, so
91 // there's no message for the next (obvious) branch.
100 func f4b(a, b, c int) int {
103 if a == b { // ERROR "Proved Eq64$"
113 func f4c(a, b, c int) int {
116 if a != b { // ERROR "Disproved Neq64$"
126 func f4d(a, b, c int) int {
129 if a < b { // ERROR "Proved Less64$"
130 if a < c { // ERROR "Proved Less64$"
142 func f4e(a, b, c int) int {
144 if b > a { // ERROR "Proved Less64$"
152 func f4f(a, b, c int) int {
155 if b == a { // ERROR "Disproved Eq64$"
160 if b >= a { // ERROR "Proved Leq64$"
161 if b == a { // ERROR "Proved Eq64$"
171 func f5(a, b uint) int {
173 if a <= b { // ERROR "Proved Leq64U$"
181 // These comparisons are compile time constants.
182 func f6a(a uint8) int {
183 if a < a { // ERROR "Disproved Less8U$"
189 func f6b(a uint8) int {
190 if a < a { // ERROR "Disproved Less8U$"
196 func f6x(a uint8) int {
197 if a > a { // ERROR "Disproved Less8U$"
203 func f6d(a uint8) int {
204 if a <= a { // ERROR "Proved Leq8U$"
210 func f6e(a uint8) int {
211 if a >= a { // ERROR "Proved Leq8U$"
217 func f7(a []int, b int) int {
220 if b < len(a) { // ERROR "Proved Less64$"
221 a[b] = 5 // ERROR "Proved IsInBounds$"
227 func f8(a, b uint) int {
234 if a < b { // ERROR "Proved Less64U$"
240 func f9(a, b bool) int {
244 if a || b { // ERROR "Disproved Arg$"
250 func f10(a string) int {
252 // We optimize comparisons with small constant strings (see cmd/compile/internal/gc/walk.go),
253 // so this string literal must be long.
254 if a[:n>>1] == "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" {
260 func f11a(a []int, i int) {
262 useInt(a[i]) // ERROR "Proved IsInBounds$"
265 func f11b(a []int, i int) {
267 useSlice(a[i:]) // ERROR "Proved IsSliceInBounds$"
270 func f11c(a []int, i int) {
272 useSlice(a[:i]) // ERROR "Proved IsSliceInBounds$"
275 func f11d(a []int, i int) {
277 useInt(a[2*i+7]) // ERROR "Proved IsInBounds$"
280 func f12(a []int, b int) {
284 func f13a(a, b, c int, x bool) int {
287 if a < 12 { // ERROR "Disproved Less64$"
292 if a <= 12 { // ERROR "Disproved Leq64$"
297 if a == 12 { // ERROR "Disproved Eq64$"
302 if a >= 12 { // ERROR "Proved Leq64$"
307 if a > 12 { // ERROR "Proved Less64$"
316 func f13b(a int, x bool) int {
319 if a < -9 { // ERROR "Disproved Less64$"
324 if a <= -9 { // ERROR "Proved Leq64$"
329 if a == -9 { // ERROR "Proved Eq64$"
334 if a >= -9 { // ERROR "Proved Leq64$"
339 if a > -9 { // ERROR "Disproved Less64$"
348 func f13c(a int, x bool) int {
351 if a < 90 { // ERROR "Proved Less64$"
356 if a <= 90 { // ERROR "Proved Leq64$"
361 if a == 90 { // ERROR "Disproved Eq64$"
366 if a >= 90 { // ERROR "Disproved Leq64$"
371 if a > 90 { // ERROR "Disproved Less64$"
380 func f13d(a int) int {
382 if a < 9 { // ERROR "Proved Less64$"
389 func f13e(a int) int {
391 if a > 5 { // ERROR "Proved Less64$"
398 func f13f(a int64) int64 {
399 if a > math.MaxInt64 {
400 if a == 0 { // ERROR "Disproved Eq64$"
407 func f13g(a int) int {
414 if a == 3 { // ERROR "Proved Eq64$"
420 func f13h(a int) int {
423 if a == 2 { // ERROR "Proved Eq64$"
431 func f13i(a uint) int {
435 if a > 0 { // ERROR "Proved Less64U$"
441 func f14(p, q *int, a []int) {
442 // This crazy ordering usually gives i1 the lowest value ID,
443 // j the middle value ID, and i2 the highest value ID.
444 // That used to confuse CSE because it ordered the args
445 // of the two + ops below differently.
446 // That in turn foiled bounds check elimination.
451 useInt(a[i2+j]) // ERROR "Proved IsInBounds$"
454 func f15(s []int, x int) {
456 useSlice(s[:x]) // ERROR "Proved IsSliceInBounds$"
459 func f16(s []int) []int {
461 return s[:10] // ERROR "Proved IsSliceInBounds$"
467 for i := 0; i < len(b); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
468 // This tests for i <= cap, which we can only prove
469 // using the derived relation between len and cap.
470 // This depends on finding the contradiction, since we
471 // don't query this condition directly.
472 useSlice(b[:i]) // ERROR "Proved IsSliceInBounds$"
476 func f18(b []int, x int, y uint) {
480 if x > len(b) { // ERROR "Disproved Less64$"
483 if y > uint(len(b)) { // ERROR "Disproved Less64U$"
486 if int(y) > len(b) { // ERROR "Disproved Less64$"
491 func f19() (e int64, err error) {
492 // Issue 29502: slice[:0] is incorrectly disproved.
494 stack = append(stack, 123)
496 panic("too many elements")
498 last := len(stack) - 1
500 // Buggy compiler prints "Disproved Leq64" for the next line.
501 stack = stack[:last] // ERROR "Proved IsSliceInBounds"
505 func sm1(b []int, x int) {
506 // Test constant argument to slicemask.
507 useSlice(b[2:8]) // ERROR "Proved slicemask not needed$"
508 // Test non-constant argument with known limits.
514 func lim1(x, y, z int) {
515 // Test relations between signed and unsigned limits.
517 if uint(x) > 5 { // ERROR "Proved Less64U$"
522 if uint(y) > 4 { // ERROR "Disproved Less64U$"
525 if uint(y) < 5 { // ERROR "Proved Less64U$"
530 if uint(z) > 4 { // Not provable without disjunctions.
536 // fence1–4 correspond to the four fence-post implications.
538 func fence1(b []int, x, y int) {
539 // Test proofs that rely on fence-post implications.
541 if x < y { // ERROR "Disproved Less64$"
546 // This eliminates the growslice path.
547 b = append(b, 1) // ERROR "Disproved Less64U$"
551 func fence2(x, y int) {
553 if x > y { // ERROR "Disproved Less64$"
559 func fence3(b, c []int, x, y int64) {
561 if x <= y { // Can't prove because x may have wrapped.
566 if x != math.MinInt64 && x-1 >= y {
567 if x <= y { // ERROR "Disproved Leq64$"
572 c[len(c)-1] = 0 // Can't prove because len(c) might be 0
574 if n := len(b); n > 0 {
575 b[n-1] = 0 // ERROR "Proved IsInBounds$"
579 func fence4(x, y int64) {
585 if y != math.MaxInt64 && x >= y+1 {
586 if x <= y { // ERROR "Disproved Leq64$"
592 // Check transitive relations
593 func trans1(x, y int64) {
596 if y > 2 { // ERROR "Proved Less64$"
600 if y > 5 { // ERROR "Proved Less64$"
607 if y > 10 { // ERROR "Proved Less64$"
614 func trans2(a, b []int, i int) {
615 if len(a) != len(b) {
620 _ = b[i] // ERROR "Proved IsInBounds$"
623 func trans3(a, b []int, i int) {
629 _ = b[i] // ERROR "Proved IsInBounds$"
632 // Derived from nat.cmp
633 func natcmp(x, y []uint) (r int) {
636 if m != n || m == 0 {
641 for i > 0 && // ERROR "Induction variable: limits \(0,\?\], increment 1$"
642 x[i] == // ERROR "Proved IsInBounds$"
643 y[i] { // ERROR "Proved IsInBounds$"
648 case x[i] < // todo, cannot prove this because it's dominated by i<=0 || x[i]==y[i]
649 y[i]: // ERROR "Proved IsInBounds$"
651 case x[i] > // ERROR "Proved IsInBounds$"
652 y[i]: // ERROR "Proved IsInBounds$"
658 func suffix(s, suffix string) bool {
659 // todo, we're still not able to drop the bound check here in the general case
660 return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
663 func constsuffix(s string) bool {
664 return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$"
667 // oforuntil tests the pattern created by OFORUNTIL blocks. These are
668 // handled by addLocalInductiveFacts rather than findIndVar.
669 func oforuntil(b []int) {
673 println(b[i]) // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Proved IsInBounds$"
681 func atexit(foobar []func()) {
682 for i := len(foobar) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1"
684 foobar = foobar[:i] // ERROR "IsSliceInBounds"
689 func make1(n int) []int {
691 for i := 0; i < n; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1"
692 s[i] = 1 // ERROR "Proved IsInBounds$"
697 func make2(n int) []int {
699 for i := range s { // ERROR "Induction variable: limits \[0,\?\), increment 1"
700 s[i] = 1 // ERROR "Proved IsInBounds$"
705 // The range tests below test the index variable of range loops.
707 // range1 compiles to the "efficiently indexable" form of a range loop.
708 func range1(b []int) {
709 for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
710 b[i] = v + 1 // ERROR "Proved IsInBounds$"
711 if i < len(b) { // ERROR "Proved Less64$"
714 if i >= 0 { // ERROR "Proved Leq64$"
720 // range2 elements are larger, so they use the general form of a range loop.
721 func range2(b [][32]int) {
722 for i, v := range b {
723 b[i][0] = v[0] + 1 // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Proved IsInBounds$"
724 if i < len(b) { // ERROR "Proved Less64$"
727 if i >= 0 { // ERROR "Proved Leq64$"
733 // signhint1-2 test whether the hint (int >= 0) is propagated into the loop.
734 func signHint1(i int, data []byte) {
736 for i < len(data) { // ERROR "Induction variable: limits \[\?,\?\), increment 1$"
737 _ = data[i] // ERROR "Proved IsInBounds$"
743 func signHint2(b []byte, n int) {
748 for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
749 b[i] = 123 // ERROR "Proved IsInBounds$"
753 // indexGT0 tests whether prove learns int index >= 0 from bounds check.
754 func indexGT0(b []byte, n int) {
758 for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
759 b[i] = 123 // ERROR "Proved IsInBounds$"
763 // Induction variable in unrolled loop.
764 func unrollUpExcl(a []int) int {
766 for i = 0; i < len(a)-1; i += 2 { // ERROR "Induction variable: limits \[0,\?\), increment 2$"
767 x += a[i] // ERROR "Proved IsInBounds$"
776 // Induction variable in unrolled loop.
777 func unrollUpIncl(a []int) int {
779 for i = 0; i <= len(a)-2; i += 2 { // ERROR "Induction variable: limits \[0,\?\], increment 2$"
789 // Induction variable in unrolled loop.
790 func unrollDownExcl0(a []int) int {
792 for i = len(a) - 1; i > 0; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
793 x += a[i] // ERROR "Proved IsInBounds$"
794 x += a[i-1] // ERROR "Proved IsInBounds$"
802 // Induction variable in unrolled loop.
803 func unrollDownExcl1(a []int) int {
805 for i = len(a) - 1; i >= 1; i -= 2 { // ERROR "Induction variable: limits \[1,\?\], increment 2$"
806 x += a[i] // ERROR "Proved IsInBounds$"
807 x += a[i-1] // ERROR "Proved IsInBounds$"
815 // Induction variable in unrolled loop.
816 func unrollDownInclStep(a []int) int {
818 for i = len(a); i >= 2; i -= 2 { // ERROR "Induction variable: limits \[2,\?\], increment 2$"
819 x += a[i-1] // ERROR "Proved IsInBounds$"
828 // Not an induction variable (step too large)
829 func unrollExclStepTooLarge(a []int) int {
831 for i = 0; i < len(a)-1; i += 3 {
841 // Not an induction variable (step too large)
842 func unrollInclStepTooLarge(a []int) int {
844 for i = 0; i <= len(a)-2; i += 3 {
854 // Not an induction variable (min too small, iterating down)
855 func unrollDecMin(a []int) int {
857 for i = len(a); i >= math.MinInt64; i -= 2 {
861 if i == 1 { // ERROR "Disproved Eq64$"
867 // Not an induction variable (min too small, iterating up -- perhaps could allow, but why bother?)
868 func unrollIncMin(a []int) int {
870 for i = len(a); i >= math.MinInt64; i += 2 {
874 if i == 1 { // ERROR "Disproved Eq64$"
880 // The 4 xxxxExtNto64 functions below test whether prove is looking
881 // through value-preserving sign/zero extensions of index values (issue #26292).
883 // Look through all extensions
884 func signExtNto64(x []int, j8 int8, j16 int16, j32 int32) int {
888 if j8 >= 0 && j8 < 22 {
889 return x[j8] // ERROR "Proved IsInBounds$"
891 if j16 >= 0 && j16 < 22 {
892 return x[j16] // ERROR "Proved IsInBounds$"
894 if j32 >= 0 && j32 < 22 {
895 return x[j32] // ERROR "Proved IsInBounds$"
900 func zeroExtNto64(x []int, j8 uint8, j16 uint16, j32 uint32) int {
904 if j8 >= 0 && j8 < 22 {
905 return x[j8] // ERROR "Proved IsInBounds$"
907 if j16 >= 0 && j16 < 22 {
908 return x[j16] // ERROR "Proved IsInBounds$"
910 if j32 >= 0 && j32 < 22 {
911 return x[j32] // ERROR "Proved IsInBounds$"
916 // Process fence-post implications through 32to64 extensions (issue #29964)
917 func signExt32to64Fence(x []int, j int32) int {
921 if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
927 func zeroExt32to64Fence(x []int, j uint32) int {
931 if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
937 // Ensure that bounds checks with negative indexes are not incorrectly removed.
940 for i := -1; i <= 0; i++ { // ERROR "Induction variable: limits \[-1,0\], increment 1$"
944 func negIndex2(n int) {
948 for i := -1; i <= 0; i-- {
959 // Check that prove is zeroing these right shifts of positive ints by bit-width - 1.
960 // e.g (Rsh64x64 <t> n (Const64 <typ.UInt64> [63])) && ft.isNonNegative(n) -> 0
961 func sh64(n int64) int64 {
965 return n >> 63 // ERROR "Proved Rsh64x64 shifts to zero"
968 func sh32(n int32) int32 {
972 return n >> 31 // ERROR "Proved Rsh32x64 shifts to zero"
975 func sh32x64(n int32) int32 {
979 return n >> uint64(31) // ERROR "Proved Rsh32x64 shifts to zero"
982 func sh16(n int16) int16 {
986 return n >> 15 // ERROR "Proved Rsh16x64 shifts to zero"
989 func sh64noopt(n int64) int64 {
990 return n >> 63 // not optimized; n could be negative
993 // These cases are division of a positive signed integer by a power of 2.
994 // The opt pass doesnt have sufficient information to see that n is positive.
995 // So, instead, opt rewrites the division with a less-than-optimal replacement.
996 // Prove, which can see that n is nonnegative, cannot see the division because
997 // opt, an earlier pass, has already replaced it.
998 // The fix for this issue allows prove to zero a right shift that was added as
999 // part of the less-than-optimal reqwrite. That change by prove then allows
1000 // lateopt to clean up all the unneccesary parts of the original division
1001 // replacement. See issue #36159.
1002 func divShiftClean(n int) int {
1006 return n / int(8) // ERROR "Proved Rsh64x64 shifts to zero"
1009 func divShiftClean64(n int64) int64 {
1013 return n / int64(16) // ERROR "Proved Rsh64x64 shifts to zero"
1016 func divShiftClean32(n int32) int32 {
1020 return n / int32(16) // ERROR "Proved Rsh32x64 shifts to zero"
1024 func useInt(a int) {
1028 func useSlice(a []int) {