1 // errorcheck -0 -d=ssa/prove/debug=1
6 // Copyright 2016 The Go Authors. All rights reserved.
7 // Use of this source code is governed by a BSD-style
8 // license that can be found in the LICENSE file.
14 func f0(a []int) int {
16 a[0] = 1 // ERROR "Proved IsInBounds$"
18 a[6] = 1 // ERROR "Proved IsInBounds$"
19 a[5] = 1 // ERROR "Proved IsInBounds$"
20 a[5] = 1 // ERROR "Proved IsInBounds$"
24 func f1(a []int) int {
28 a[0] = 1 // ERROR "Proved IsInBounds$"
29 a[0] = 1 // ERROR "Proved IsInBounds$"
31 a[6] = 1 // ERROR "Proved IsInBounds$"
32 a[5] = 1 // ERROR "Proved IsInBounds$"
33 a[5] = 1 // ERROR "Proved IsInBounds$"
37 func f1b(a []int, i int, j uint) int {
38 if i >= 0 && i < len(a) {
39 return a[i] // ERROR "Proved IsInBounds$"
41 if i >= 10 && i < len(a) {
42 return a[i] // ERROR "Proved IsInBounds$"
44 if i >= 10 && i < len(a) {
45 return a[i] // ERROR "Proved IsInBounds$"
47 if i >= 10 && i < len(a) {
48 return a[i-10] // ERROR "Proved IsInBounds$"
51 return a[j] // ERROR "Proved IsInBounds$"
56 func f1c(a []int, i int64) int {
57 c := uint64(math.MaxInt64 + 10) // overflows int
59 if i >= d && i < int64(len(a)) {
60 // d overflows, should not be handled.
66 func f2(a []int) int {
67 for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
69 a[i+1] = i // ERROR "Proved IsInBounds$"
74 func f3(a []uint) int {
75 for i := uint(0); i < uint(len(a)); i++ {
76 a[i] = i // ERROR "Proved IsInBounds$"
81 func f4a(a, b, c int) int {
83 if a == b { // ERROR "Disproved Eq64$"
86 if a > b { // ERROR "Disproved Less64$"
89 if a < b { // ERROR "Proved Less64$"
92 // We can't get to this point and prove knows that, so
93 // there's no message for the next (obvious) branch.
102 func f4b(a, b, c int) int {
105 if a == b { // ERROR "Proved Eq64$"
115 func f4c(a, b, c int) int {
118 if a != b { // ERROR "Disproved Neq64$"
128 func f4d(a, b, c int) int {
131 if a < b { // ERROR "Proved Less64$"
132 if a < c { // ERROR "Proved Less64$"
144 func f4e(a, b, c int) int {
146 if b > a { // ERROR "Proved Less64$"
154 func f4f(a, b, c int) int {
157 if b == a { // ERROR "Disproved Eq64$"
162 if b >= a { // ERROR "Proved Leq64$"
163 if b == a { // ERROR "Proved Eq64$"
173 func f5(a, b uint) int {
175 if a <= b { // ERROR "Proved Leq64U$"
183 // These comparisons are compile time constants.
184 func f6a(a uint8) int {
185 if a < a { // ERROR "Disproved Less8U$"
191 func f6b(a uint8) int {
192 if a < a { // ERROR "Disproved Less8U$"
198 func f6x(a uint8) int {
199 if a > a { // ERROR "Disproved Less8U$"
205 func f6d(a uint8) int {
206 if a <= a { // ERROR "Proved Leq8U$"
212 func f6e(a uint8) int {
213 if a >= a { // ERROR "Proved Leq8U$"
219 func f7(a []int, b int) int {
222 if b < len(a) { // ERROR "Proved Less64$"
223 a[b] = 5 // ERROR "Proved IsInBounds$"
229 func f8(a, b uint) int {
236 if a < b { // ERROR "Proved Less64U$"
242 func f9(a, b bool) int {
246 if a || b { // ERROR "Disproved Arg$"
252 func f10(a string) int {
254 // We optimize comparisons with small constant strings (see cmd/compile/internal/gc/walk.go),
255 // so this string literal must be long.
256 if a[:n>>1] == "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" {
262 func f11a(a []int, i int) {
264 useInt(a[i]) // ERROR "Proved IsInBounds$"
267 func f11b(a []int, i int) {
269 useSlice(a[i:]) // ERROR "Proved IsSliceInBounds$"
272 func f11c(a []int, i int) {
274 useSlice(a[:i]) // ERROR "Proved IsSliceInBounds$"
277 func f11d(a []int, i int) {
279 useInt(a[2*i+7]) // ERROR "Proved IsInBounds$"
282 func f12(a []int, b int) {
286 func f13a(a, b, c int, x bool) int {
289 if a < 12 { // ERROR "Disproved Less64$"
294 if a <= 12 { // ERROR "Disproved Leq64$"
299 if a == 12 { // ERROR "Disproved Eq64$"
304 if a >= 12 { // ERROR "Proved Leq64$"
309 if a > 12 { // ERROR "Proved Less64$"
318 func f13b(a int, x bool) int {
321 if a < -9 { // ERROR "Disproved Less64$"
326 if a <= -9 { // ERROR "Proved Leq64$"
331 if a == -9 { // ERROR "Proved Eq64$"
336 if a >= -9 { // ERROR "Proved Leq64$"
341 if a > -9 { // ERROR "Disproved Less64$"
350 func f13c(a int, x bool) int {
353 if a < 90 { // ERROR "Proved Less64$"
358 if a <= 90 { // ERROR "Proved Leq64$"
363 if a == 90 { // ERROR "Disproved Eq64$"
368 if a >= 90 { // ERROR "Disproved Leq64$"
373 if a > 90 { // ERROR "Disproved Less64$"
382 func f13d(a int) int {
384 if a < 9 { // ERROR "Proved Less64$"
391 func f13e(a int) int {
393 if a > 5 { // ERROR "Proved Less64$"
400 func f13f(a int64) int64 {
401 if a > math.MaxInt64 {
402 if a == 0 { // ERROR "Disproved Eq64$"
409 func f13g(a int) int {
416 if a == 3 { // ERROR "Proved Eq64$"
422 func f13h(a int) int {
425 if a == 2 { // ERROR "Proved Eq64$"
433 func f13i(a uint) int {
437 if a > 0 { // ERROR "Proved Less64U$"
443 func f14(p, q *int, a []int) {
444 // This crazy ordering usually gives i1 the lowest value ID,
445 // j the middle value ID, and i2 the highest value ID.
446 // That used to confuse CSE because it ordered the args
447 // of the two + ops below differently.
448 // That in turn foiled bounds check elimination.
453 useInt(a[i2+j]) // ERROR "Proved IsInBounds$"
456 func f15(s []int, x int) {
458 useSlice(s[:x]) // ERROR "Proved IsSliceInBounds$"
461 func f16(s []int) []int {
463 return s[:10] // ERROR "Proved IsSliceInBounds$"
469 for i := 0; i < len(b); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
470 // This tests for i <= cap, which we can only prove
471 // using the derived relation between len and cap.
472 // This depends on finding the contradiction, since we
473 // don't query this condition directly.
474 useSlice(b[:i]) // ERROR "Proved IsSliceInBounds$"
478 func f18(b []int, x int, y uint) {
482 if x > len(b) { // ERROR "Disproved Less64$"
485 if y > uint(len(b)) { // ERROR "Disproved Less64U$"
488 if int(y) > len(b) { // ERROR "Disproved Less64$"
493 func f19() (e int64, err error) {
494 // Issue 29502: slice[:0] is incorrectly disproved.
496 stack = append(stack, 123)
498 panic("too many elements")
500 last := len(stack) - 1
502 // Buggy compiler prints "Disproved Leq64" for the next line.
507 func sm1(b []int, x int) {
508 // Test constant argument to slicemask.
509 useSlice(b[2:8]) // ERROR "Proved slicemask not needed$"
510 // Test non-constant argument with known limits.
516 func lim1(x, y, z int) {
517 // Test relations between signed and unsigned limits.
519 if uint(x) > 5 { // ERROR "Proved Less64U$"
524 if uint(y) > 4 { // ERROR "Disproved Less64U$"
527 if uint(y) < 5 { // ERROR "Proved Less64U$"
532 if uint(z) > 4 { // Not provable without disjunctions.
538 // fence1–4 correspond to the four fence-post implications.
540 func fence1(b []int, x, y int) {
541 // Test proofs that rely on fence-post implications.
543 if x < y { // ERROR "Disproved Less64$"
548 // This eliminates the growslice path.
549 b = append(b, 1) // ERROR "Disproved Less64U$"
553 func fence2(x, y int) {
555 if x > y { // ERROR "Disproved Less64$"
561 func fence3(b, c []int, x, y int64) {
563 if x <= y { // Can't prove because x may have wrapped.
568 if x != math.MinInt64 && x-1 >= y {
569 if x <= y { // ERROR "Disproved Leq64$"
574 c[len(c)-1] = 0 // Can't prove because len(c) might be 0
576 if n := len(b); n > 0 {
577 b[n-1] = 0 // ERROR "Proved IsInBounds$"
581 func fence4(x, y int64) {
587 if y != math.MaxInt64 && x >= y+1 {
588 if x <= y { // ERROR "Disproved Leq64$"
594 // Check transitive relations
595 func trans1(x, y int64) {
598 if y > 2 { // ERROR "Proved Less64$"
602 if y > 5 { // ERROR "Proved Less64$"
609 if y > 10 { // ERROR "Proved Less64$"
616 func trans2(a, b []int, i int) {
617 if len(a) != len(b) {
622 _ = b[i] // ERROR "Proved IsInBounds$"
625 func trans3(a, b []int, i int) {
631 _ = b[i] // ERROR "Proved IsInBounds$"
634 func trans4(b []byte, x int) {
635 // Issue #42603: slice len/cap transitive relations.
641 _ = b[:2] // ERROR "Proved IsSliceInBounds$"
646 _ = b[:2] // ERROR "Proved IsSliceInBounds$"
650 // Derived from nat.cmp
651 func natcmp(x, y []uint) (r int) {
654 if m != n || m == 0 {
659 for i > 0 && // ERROR "Induction variable: limits \(0,\?\], increment 1$"
660 x[i] == // ERROR "Proved IsInBounds$"
661 y[i] { // ERROR "Proved IsInBounds$"
666 case x[i] < // todo, cannot prove this because it's dominated by i<=0 || x[i]==y[i]
667 y[i]: // ERROR "Proved IsInBounds$"
669 case x[i] > // ERROR "Proved IsInBounds$"
670 y[i]: // ERROR "Proved IsInBounds$"
676 func suffix(s, suffix string) bool {
677 // todo, we're still not able to drop the bound check here in the general case
678 return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
681 func constsuffix(s string) bool {
682 return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$"
685 // oforuntil tests the pattern created by OFORUNTIL blocks. These are
686 // handled by addLocalInductiveFacts rather than findIndVar.
687 func oforuntil(b []int) {
691 println(b[i]) // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Proved IsInBounds$"
699 func atexit(foobar []func()) {
700 for i := len(foobar) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1"
702 foobar = foobar[:i] // ERROR "IsSliceInBounds"
707 func make1(n int) []int {
709 for i := 0; i < n; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1"
710 s[i] = 1 // ERROR "Proved IsInBounds$"
715 func make2(n int) []int {
717 for i := range s { // ERROR "Induction variable: limits \[0,\?\), increment 1"
718 s[i] = 1 // ERROR "Proved IsInBounds$"
723 // The range tests below test the index variable of range loops.
725 // range1 compiles to the "efficiently indexable" form of a range loop.
726 func range1(b []int) {
727 for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
728 b[i] = v + 1 // ERROR "Proved IsInBounds$"
729 if i < len(b) { // ERROR "Proved Less64$"
732 if i >= 0 { // ERROR "Proved Leq64$"
738 // range2 elements are larger, so they use the general form of a range loop.
739 func range2(b [][32]int) {
740 for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
741 b[i][0] = v[0] + 1 // ERROR "Proved IsInBounds$"
742 if i < len(b) { // ERROR "Proved Less64$"
745 if i >= 0 { // ERROR "Proved Leq64$"
751 // signhint1-2 test whether the hint (int >= 0) is propagated into the loop.
752 func signHint1(i int, data []byte) {
754 for i < len(data) { // ERROR "Induction variable: limits \[\?,\?\), increment 1$"
755 _ = data[i] // ERROR "Proved IsInBounds$"
761 func signHint2(b []byte, n int) {
766 for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
767 b[i] = 123 // ERROR "Proved IsInBounds$"
771 // indexGT0 tests whether prove learns int index >= 0 from bounds check.
772 func indexGT0(b []byte, n int) {
776 for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
777 b[i] = 123 // ERROR "Proved IsInBounds$"
781 // Induction variable in unrolled loop.
782 func unrollUpExcl(a []int) int {
784 for i = 0; i < len(a)-1; i += 2 { // ERROR "Induction variable: limits \[0,\?\), increment 2$"
785 x += a[i] // ERROR "Proved IsInBounds$"
794 // Induction variable in unrolled loop.
795 func unrollUpIncl(a []int) int {
797 for i = 0; i <= len(a)-2; i += 2 { // ERROR "Induction variable: limits \[0,\?\], increment 2$"
798 x += a[i] // ERROR "Proved IsInBounds$"
807 // Induction variable in unrolled loop.
808 func unrollDownExcl0(a []int) int {
810 for i = len(a) - 1; i > 0; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
811 x += a[i] // ERROR "Proved IsInBounds$"
812 x += a[i-1] // ERROR "Proved IsInBounds$"
820 // Induction variable in unrolled loop.
821 func unrollDownExcl1(a []int) int {
823 for i = len(a) - 1; i >= 1; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
824 x += a[i] // ERROR "Proved IsInBounds$"
825 x += a[i-1] // ERROR "Proved IsInBounds$"
833 // Induction variable in unrolled loop.
834 func unrollDownInclStep(a []int) int {
836 for i = len(a); i >= 2; i -= 2 { // ERROR "Induction variable: limits \[2,\?\], increment 2$"
837 x += a[i-1] // ERROR "Proved IsInBounds$"
838 x += a[i-2] // ERROR "Proved IsInBounds$"
846 // Not an induction variable (step too large)
847 func unrollExclStepTooLarge(a []int) int {
849 for i = 0; i < len(a)-1; i += 3 {
859 // Not an induction variable (step too large)
860 func unrollInclStepTooLarge(a []int) int {
862 for i = 0; i <= len(a)-2; i += 3 {
872 // Not an induction variable (min too small, iterating down)
873 func unrollDecMin(a []int) int {
875 for i = len(a); i >= math.MinInt64; i -= 2 {
879 if i == 1 { // ERROR "Disproved Eq64$"
885 // Not an induction variable (min too small, iterating up -- perhaps could allow, but why bother?)
886 func unrollIncMin(a []int) int {
888 for i = len(a); i >= math.MinInt64; i += 2 {
892 if i == 1 { // ERROR "Disproved Eq64$"
898 // The 4 xxxxExtNto64 functions below test whether prove is looking
899 // through value-preserving sign/zero extensions of index values (issue #26292).
901 // Look through all extensions
902 func signExtNto64(x []int, j8 int8, j16 int16, j32 int32) int {
906 if j8 >= 0 && j8 < 22 {
907 return x[j8] // ERROR "Proved IsInBounds$"
909 if j16 >= 0 && j16 < 22 {
910 return x[j16] // ERROR "Proved IsInBounds$"
912 if j32 >= 0 && j32 < 22 {
913 return x[j32] // ERROR "Proved IsInBounds$"
918 func zeroExtNto64(x []int, j8 uint8, j16 uint16, j32 uint32) int {
922 if j8 >= 0 && j8 < 22 {
923 return x[j8] // ERROR "Proved IsInBounds$"
925 if j16 >= 0 && j16 < 22 {
926 return x[j16] // ERROR "Proved IsInBounds$"
928 if j32 >= 0 && j32 < 22 {
929 return x[j32] // ERROR "Proved IsInBounds$"
934 // Process fence-post implications through 32to64 extensions (issue #29964)
935 func signExt32to64Fence(x []int, j int32) int {
939 if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
945 func zeroExt32to64Fence(x []int, j uint32) int {
949 if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
955 // Ensure that bounds checks with negative indexes are not incorrectly removed.
958 for i := -1; i <= 0; i++ { // ERROR "Induction variable: limits \[-1,0\], increment 1$"
962 func negIndex2(n int) {
966 for i := -1; i <= 0; i-- {
977 // Check that prove is zeroing these right shifts of positive ints by bit-width - 1.
978 // e.g (Rsh64x64 <t> n (Const64 <typ.UInt64> [63])) && ft.isNonNegative(n) -> 0
979 func sh64(n int64) int64 {
983 return n >> 63 // ERROR "Proved Rsh64x64 shifts to zero"
986 func sh32(n int32) int32 {
990 return n >> 31 // ERROR "Proved Rsh32x64 shifts to zero"
993 func sh32x64(n int32) int32 {
997 return n >> uint64(31) // ERROR "Proved Rsh32x64 shifts to zero"
1000 func sh16(n int16) int16 {
1004 return n >> 15 // ERROR "Proved Rsh16x64 shifts to zero"
1007 func sh64noopt(n int64) int64 {
1008 return n >> 63 // not optimized; n could be negative
1011 // These cases are division of a positive signed integer by a power of 2.
1012 // The opt pass doesnt have sufficient information to see that n is positive.
1013 // So, instead, opt rewrites the division with a less-than-optimal replacement.
1014 // Prove, which can see that n is nonnegative, cannot see the division because
1015 // opt, an earlier pass, has already replaced it.
1016 // The fix for this issue allows prove to zero a right shift that was added as
1017 // part of the less-than-optimal reqwrite. That change by prove then allows
1018 // lateopt to clean up all the unnecessary parts of the original division
1019 // replacement. See issue #36159.
1020 func divShiftClean(n int) int {
1024 return n / int(8) // ERROR "Proved Rsh64x64 shifts to zero"
1027 func divShiftClean64(n int64) int64 {
1031 return n / int64(16) // ERROR "Proved Rsh64x64 shifts to zero"
1034 func divShiftClean32(n int32) int32 {
1038 return n / int32(16) // ERROR "Proved Rsh32x64 shifts to zero"
1041 // Bounds check elimination
1043 func sliceBCE1(p []string, h uint) string {
1048 i := h & uint(len(p)-1)
1049 return p[i] // ERROR "Proved IsInBounds$"
1052 func sliceBCE2(p []string, h int) string {
1056 i := h & (len(p) - 1)
1057 return p[i] // ERROR "Proved IsInBounds$"
1060 func and(p []byte) ([]byte, []byte) { // issue #52563
1061 const blocksize = 16
1062 fullBlocks := len(p) &^ (blocksize - 1)
1063 blk := p[:fullBlocks] // ERROR "Proved IsSliceInBounds$"
1064 rem := p[fullBlocks:] // ERROR "Proved IsSliceInBounds$"
1068 func rshu(x, y uint) int {
1070 if z <= x { // ERROR "Proved Leq64U$"
1076 func divu(x, y uint) int {
1078 if z <= x { // ERROR "Proved Leq64U$"
1084 func modu1(x, y uint) int {
1086 if z < y { // ERROR "Proved Less64U$"
1092 func modu2(x, y uint) int {
1094 if z <= x { // ERROR "Proved Leq64U$"
1100 func issue57077(s []int) (left, right []int) {
1101 middle := len(s) / 2
1102 left = s[:middle] // ERROR "Proved IsSliceInBounds$"
1103 right = s[middle:] // ERROR "Proved IsSliceInBounds$"
1107 func issue51622(b []byte) int {
1108 if len(b) >= 3 && b[len(b)-3] == '#' { // ERROR "Proved IsInBounds$"
1114 func issue45928(x int) {
1115 combinedFrac := x / (x | (1 << 31)) // ERROR "Proved Neq64$"
1116 useInt(combinedFrac)
1120 func useInt(a int) {
1124 func useSlice(a []int) {