test/prove.go

   1 // +build amd64
   2 // errorcheck -0 -d=ssa/prove/debug=1
   3
   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.
   7
   8 package main
   9
  10 import "math"
  11
  12 func f0(a []int) int {
  13         a[0] = 1
  14         a[0] = 1 // ERROR "Proved IsInBounds$"
  15         a[6] = 1
  16         a[6] = 1 // ERROR "Proved IsInBounds$"
  17         a[5] = 1 // ERROR "Proved IsInBounds$"
  18         a[5] = 1 // ERROR "Proved IsInBounds$"
  19         return 13
  20 }
  21
  22 func f1(a []int) int {
  23         if len(a) <= 5 {
  24                 return 18
  25         }
  26         a[0] = 1 // ERROR "Proved IsInBounds$"
  27         a[0] = 1 // ERROR "Proved IsInBounds$"
  28         a[6] = 1
  29         a[6] = 1 // ERROR "Proved IsInBounds$"
  30         a[5] = 1 // ERROR "Proved IsInBounds$"
  31         a[5] = 1 // ERROR "Proved IsInBounds$"
  32         return 26
  33 }
  34
  35 func f1b(a []int, i int, j uint) int {
  36         if i >= 0 && i < len(a) {
  37                 return a[i] // ERROR "Proved IsInBounds$"
  38         }
  39         if i >= 10 && i < len(a) {
  40                 return a[i] // ERROR "Proved IsInBounds$"
  41         }
  42         if i >= 10 && i < len(a) {
  43                 return a[i] // ERROR "Proved IsInBounds$"
  44         }
  45         if i >= 10 && i < len(a) {
  46                 return a[i-10] // ERROR "Proved IsInBounds$"
  47         }
  48         if j < uint(len(a)) {
  49                 return a[j] // ERROR "Proved IsInBounds$"
  50         }
  51         return 0
  52 }
  53
  54 func f1c(a []int, i int64) int {
  55         c := uint64(math.MaxInt64 + 10) // overflows int
  56         d := int64(c)
  57         if i >= d && i < int64(len(a)) {
  58                 // d overflows, should not be handled.
  59                 return a[i]
  60         }
  61         return 0
  62 }
  63
  64 func f2(a []int) int {
  65         for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
  66                 a[i+1] = i
  67                 a[i+1] = i // ERROR "Proved IsInBounds$"
  68         }
  69         return 34
  70 }
  71
  72 func f3(a []uint) int {
  73         for i := uint(0); i < uint(len(a)); i++ {
  74                 a[i] = i // ERROR "Proved IsInBounds$"
  75         }
  76         return 41
  77 }
  78
  79 func f4a(a, b, c int) int {
  80         if a < b {
  81                 if a == b { // ERROR "Disproved Eq64$"
  82                         return 47
  83                 }
  84                 if a > b { // ERROR "Disproved Less64$"
  85                         return 50
  86                 }
  87                 if a < b { // ERROR "Proved Less64$"
  88                         return 53
  89                 }
  90                 // We can't get to this point and prove knows that, so
  91                 // there's no message for the next (obvious) branch.
  92                 if a != a {
  93                         return 56
  94                 }
  95                 return 61
  96         }
  97         return 63
  98 }
  99
 100 func f4b(a, b, c int) int {
 101         if a <= b {
 102                 if a >= b {
 103                         if a == b { // ERROR "Proved Eq64$"
 104                                 return 70
 105                         }
 106                         return 75
 107                 }
 108                 return 77
 109         }
 110         return 79
 111 }
 112
 113 func f4c(a, b, c int) int {
 114         if a <= b {
 115                 if a >= b {
 116                         if a != b { // ERROR "Disproved Neq64$"
 117                                 return 73
 118                         }
 119                         return 75
 120                 }
 121                 return 77
 122         }
 123         return 79
 124 }
 125
 126 func f4d(a, b, c int) int {
 127         if a < b {
 128                 if a < c {
 129                         if a < b { // ERROR "Proved Less64$"
 130                                 if a < c { // ERROR "Proved Less64$"
 131                                         return 87
 132                                 }
 133                                 return 89
 134                         }
 135                         return 91
 136                 }
 137                 return 93
 138         }
 139         return 95
 140 }
 141
 142 func f4e(a, b, c int) int {
 143         if a < b {
 144                 if b > a { // ERROR "Proved Less64$"
 145                         return 101
 146                 }
 147                 return 103
 148         }
 149         return 105
 150 }
 151
 152 func f4f(a, b, c int) int {
 153         if a <= b {
 154                 if b > a {
 155                         if b == a { // ERROR "Disproved Eq64$"
 156                                 return 112
 157                         }
 158                         return 114
 159                 }
 160                 if b >= a { // ERROR "Proved Leq64$"
 161                         if b == a { // ERROR "Proved Eq64$"
 162                                 return 118
 163                         }
 164                         return 120
 165                 }
 166                 return 122
 167         }
 168         return 124
 169 }
 170
 171 func f5(a, b uint) int {
 172         if a == b {
 173                 if a <= b { // ERROR "Proved Leq64U$"
 174                         return 130
 175                 }
 176                 return 132
 177         }
 178         return 134
 179 }
 180
 181 // These comparisons are compile time constants.
 182 func f6a(a uint8) int {
 183         if a < a { // ERROR "Disproved Less8U$"
 184                 return 140
 185         }
 186         return 151
 187 }
 188
 189 func f6b(a uint8) int {
 190         if a < a { // ERROR "Disproved Less8U$"
 191                 return 140
 192         }
 193         return 151
 194 }
 195
 196 func f6x(a uint8) int {
 197         if a > a { // ERROR "Disproved Less8U$"
 198                 return 143
 199         }
 200         return 151
 201 }
 202
 203 func f6d(a uint8) int {
 204         if a <= a { // ERROR "Proved Leq8U$"
 205                 return 146
 206         }
 207         return 151
 208 }
 209
 210 func f6e(a uint8) int {
 211         if a >= a { // ERROR "Proved Leq8U$"
 212                 return 149
 213         }
 214         return 151
 215 }
 216
 217 func f7(a []int, b int) int {
 218         if b < len(a) {
 219                 a[b] = 3
 220                 if b < len(a) { // ERROR "Proved Less64$"
 221                         a[b] = 5 // ERROR "Proved IsInBounds$"
 222                 }
 223         }
 224         return 161
 225 }
 226
 227 func f8(a, b uint) int {
 228         if a == b {
 229                 return 166
 230         }
 231         if a > b {
 232                 return 169
 233         }
 234         if a < b { // ERROR "Proved Less64U$"
 235                 return 172
 236         }
 237         return 174
 238 }
 239
 240 func f9(a, b bool) int {
 241         if a {
 242                 return 1
 243         }
 244         if a || b { // ERROR "Disproved Arg$"
 245                 return 2
 246         }
 247         return 3
 248 }
 249
 250 func f10(a string) int {
 251         n := len(a)
 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" {
 255                 return 0
 256         }
 257         return 1
 258 }
 259
 260 func f11a(a []int, i int) {
 261         useInt(a[i])
 262         useInt(a[i]) // ERROR "Proved IsInBounds$"
 263 }
 264
 265 func f11b(a []int, i int) {
 266         useSlice(a[i:])
 267         useSlice(a[i:]) // ERROR "Proved IsSliceInBounds$"
 268 }
 269
 270 func f11c(a []int, i int) {
 271         useSlice(a[:i])
 272         useSlice(a[:i]) // ERROR "Proved IsSliceInBounds$"
 273 }
 274
 275 func f11d(a []int, i int) {
 276         useInt(a[2*i+7])
 277         useInt(a[2*i+7]) // ERROR "Proved IsInBounds$"
 278 }
 279
 280 func f12(a []int, b int) {
 281         useSlice(a[:b])
 282 }
 283
 284 func f13a(a, b, c int, x bool) int {
 285         if a > 12 {
 286                 if x {
 287                         if a < 12 { // ERROR "Disproved Less64$"
 288                                 return 1
 289                         }
 290                 }
 291                 if x {
 292                         if a <= 12 { // ERROR "Disproved Leq64$"
 293                                 return 2
 294                         }
 295                 }
 296                 if x {
 297                         if a == 12 { // ERROR "Disproved Eq64$"
 298                                 return 3
 299                         }
 300                 }
 301                 if x {
 302                         if a >= 12 { // ERROR "Proved Leq64$"
 303                                 return 4
 304                         }
 305                 }
 306                 if x {
 307                         if a > 12 { // ERROR "Proved Less64$"
 308                                 return 5
 309                         }
 310                 }
 311                 return 6
 312         }
 313         return 0
 314 }
 315
 316 func f13b(a int, x bool) int {
 317         if a == -9 {
 318                 if x {
 319                         if a < -9 { // ERROR "Disproved Less64$"
 320                                 return 7
 321                         }
 322                 }
 323                 if x {
 324                         if a <= -9 { // ERROR "Proved Leq64$"
 325                                 return 8
 326                         }
 327                 }
 328                 if x {
 329                         if a == -9 { // ERROR "Proved Eq64$"
 330                                 return 9
 331                         }
 332                 }
 333                 if x {
 334                         if a >= -9 { // ERROR "Proved Leq64$"
 335                                 return 10
 336                         }
 337                 }
 338                 if x {
 339                         if a > -9 { // ERROR "Disproved Less64$"
 340                                 return 11
 341                         }
 342                 }
 343                 return 12
 344         }
 345         return 0
 346 }
 347
 348 func f13c(a int, x bool) int {
 349         if a < 90 {
 350                 if x {
 351                         if a < 90 { // ERROR "Proved Less64$"
 352                                 return 13
 353                         }
 354                 }
 355                 if x {
 356                         if a <= 90 { // ERROR "Proved Leq64$"
 357                                 return 14
 358                         }
 359                 }
 360                 if x {
 361                         if a == 90 { // ERROR "Disproved Eq64$"
 362                                 return 15
 363                         }
 364                 }
 365                 if x {
 366                         if a >= 90 { // ERROR "Disproved Leq64$"
 367                                 return 16
 368                         }
 369                 }
 370                 if x {
 371                         if a > 90 { // ERROR "Disproved Less64$"
 372                                 return 17
 373                         }
 374                 }
 375                 return 18
 376         }
 377         return 0
 378 }
 379
 380 func f13d(a int) int {
 381         if a < 5 {
 382                 if a < 9 { // ERROR "Proved Less64$"
 383                         return 1
 384                 }
 385         }
 386         return 0
 387 }
 388
 389 func f13e(a int) int {
 390         if a > 9 {
 391                 if a > 5 { // ERROR "Proved Less64$"
 392                         return 1
 393                 }
 394         }
 395         return 0
 396 }
 397
 398 func f13f(a int64) int64 {
 399         if a > math.MaxInt64 {
 400                 if a == 0 { // ERROR "Disproved Eq64$"
 401                         return 1
 402                 }
 403         }
 404         return 0
 405 }
 406
 407 func f13g(a int) int {
 408         if a < 3 {
 409                 return 5
 410         }
 411         if a > 3 {
 412                 return 6
 413         }
 414         if a == 3 { // ERROR "Proved Eq64$"
 415                 return 7
 416         }
 417         return 8
 418 }
 419
 420 func f13h(a int) int {
 421         if a < 3 {
 422                 if a > 1 {
 423                         if a == 2 { // ERROR "Proved Eq64$"
 424                                 return 5
 425                         }
 426                 }
 427         }
 428         return 0
 429 }
 430
 431 func f13i(a uint) int {
 432         if a == 0 {
 433                 return 1
 434         }
 435         if a > 0 { // ERROR "Proved Less64U$"
 436                 return 2
 437         }
 438         return 3
 439 }
 440
 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.
 447         i1 := *p
 448         j := *q
 449         i2 := *p
 450         useInt(a[i1+j])
 451         useInt(a[i2+j]) // ERROR "Proved IsInBounds$"
 452 }
 453
 454 func f15(s []int, x int) {
 455         useSlice(s[x:])
 456         useSlice(s[:x]) // ERROR "Proved IsSliceInBounds$"
 457 }
 458
 459 func f16(s []int) []int {
 460         if len(s) >= 10 {
 461                 return s[:10] // ERROR "Proved IsSliceInBounds$"
 462         }
 463         return nil
 464 }
 465
 466 func f17(b []int) {
 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$"
 473         }
 474 }
 475
 476 func f18(b []int, x int, y uint) {
 477         _ = b[x]
 478         _ = b[y]
 479
 480         if x > len(b) { // ERROR "Disproved Less64$"
 481                 return
 482         }
 483         if y > uint(len(b)) { // ERROR "Disproved Less64U$"
 484                 return
 485         }
 486         if int(y) > len(b) { // ERROR "Disproved Less64$"
 487                 return
 488         }
 489 }
 490
 491 func f19() (e int64, err error) {
 492         // Issue 29502: slice[:0] is incorrectly disproved.
 493         var stack []int64
 494         stack = append(stack, 123)
 495         if len(stack) > 1 {
 496                 panic("too many elements")
 497         }
 498         last := len(stack) - 1
 499         e = stack[last]
 500         // Buggy compiler prints "Disproved Leq64" for the next line.
 501         stack = stack[:last] // ERROR "Proved IsSliceInBounds"
 502         return e, nil
 503 }
 504
 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.
 509         if cap(b) > 10 {
 510                 useSlice(b[2:])
 511         }
 512 }
 513
 514 func lim1(x, y, z int) {
 515         // Test relations between signed and unsigned limits.
 516         if x > 5 {
 517                 if uint(x) > 5 { // ERROR "Proved Less64U$"
 518                         return
 519                 }
 520         }
 521         if y >= 0 && y < 4 {
 522                 if uint(y) > 4 { // ERROR "Disproved Less64U$"
 523                         return
 524                 }
 525                 if uint(y) < 5 { // ERROR "Proved Less64U$"
 526                         return
 527                 }
 528         }
 529         if z < 4 {
 530                 if uint(z) > 4 { // Not provable without disjunctions.
 531                         return
 532                 }
 533         }
 534 }
 535
 536 // fence1–4 correspond to the four fence-post implications.
 537
 538 func fence1(b []int, x, y int) {
 539         // Test proofs that rely on fence-post implications.
 540         if x+1 > y {
 541                 if x < y { // ERROR "Disproved Less64$"
 542                         return
 543                 }
 544         }
 545         if len(b) < cap(b) {
 546                 // This eliminates the growslice path.
 547                 b = append(b, 1) // ERROR "Disproved Less64U$"
 548         }
 549 }
 550
 551 func fence2(x, y int) {
 552         if x-1 < y {
 553                 if x > y { // ERROR "Disproved Less64$"
 554                         return
 555                 }
 556         }
 557 }
 558
 559 func fence3(b, c []int, x, y int64) {
 560         if x-1 >= y {
 561                 if x <= y { // Can't prove because x may have wrapped.
 562                         return
 563                 }
 564         }
 565
 566         if x != math.MinInt64 && x-1 >= y {
 567                 if x <= y { // ERROR "Disproved Leq64$"
 568                         return
 569                 }
 570         }
 571
 572         c[len(c)-1] = 0 // Can't prove because len(c) might be 0
 573
 574         if n := len(b); n > 0 {
 575                 b[n-1] = 0 // ERROR "Proved IsInBounds$"
 576         }
 577 }
 578
 579 func fence4(x, y int64) {
 580         if x >= y+1 {
 581                 if x <= y {
 582                         return
 583                 }
 584         }
 585         if y != math.MaxInt64 && x >= y+1 {
 586                 if x <= y { // ERROR "Disproved Leq64$"
 587                         return
 588                 }
 589         }
 590 }
 591
 592 // Check transitive relations
 593 func trans1(x, y int64) {
 594         if x > 5 {
 595                 if y > x {
 596                         if y > 2 { // ERROR "Proved Less64$"
 597                                 return
 598                         }
 599                 } else if y == x {
 600                         if y > 5 { // ERROR "Proved Less64$"
 601                                 return
 602                         }
 603                 }
 604         }
 605         if x >= 10 {
 606                 if y > x {
 607                         if y > 10 { // ERROR "Proved Less64$"
 608                                 return
 609                         }
 610                 }
 611         }
 612 }
 613
 614 func trans2(a, b []int, i int) {
 615         if len(a) != len(b) {
 616                 return
 617         }
 618
 619         _ = a[i]
 620         _ = b[i] // ERROR "Proved IsInBounds$"
 621 }
 622
 623 func trans3(a, b []int, i int) {
 624         if len(a) > len(b) {
 625                 return
 626         }
 627
 628         _ = a[i]
 629         _ = b[i] // ERROR "Proved IsInBounds$"
 630 }
 631
 632 func trans4(b []byte, x int) {
 633         // Issue #42603: slice len/cap transitive relations.
 634         switch x {
 635         case 0:
 636                 if len(b) < 20 {
 637                         return
 638                 }
 639                 _ = b[:2] // ERROR "Proved IsSliceInBounds$"
 640         case 1:
 641                 if len(b) < 40 {
 642                         return
 643                 }
 644                 _ = b[:2] // ERROR "Proved IsSliceInBounds$"
 645         }
 646 }
 647
 648 // Derived from nat.cmp
 649 func natcmp(x, y []uint) (r int) {
 650         m := len(x)
 651         n := len(y)
 652         if m != n || m == 0 {
 653                 return
 654         }
 655
 656         i := m - 1
 657         for i > 0 && // ERROR "Induction variable: limits \(0,\?\], increment 1$"
 658                 x[i] == // ERROR "Proved IsInBounds$"
 659                         y[i] { // ERROR "Proved IsInBounds$"
 660                 i--
 661         }
 662
 663         switch {
 664         case x[i] < // todo, cannot prove this because it's dominated by i<=0 || x[i]==y[i]
 665                 y[i]: // ERROR "Proved IsInBounds$"
 666                 r = -1
 667         case x[i] > // ERROR "Proved IsInBounds$"
 668                 y[i]: // ERROR "Proved IsInBounds$"
 669                 r = 1
 670         }
 671         return
 672 }
 673
 674 func suffix(s, suffix string) bool {
 675         // todo, we're still not able to drop the bound check here in the general case
 676         return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
 677 }
 678
 679 func constsuffix(s string) bool {
 680         return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$"
 681 }
 682
 683 // oforuntil tests the pattern created by OFORUNTIL blocks. These are
 684 // handled by addLocalInductiveFacts rather than findIndVar.
 685 func oforuntil(b []int) {
 686         i := 0
 687         if len(b) > i {
 688         top:
 689                 println(b[i]) // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Proved IsInBounds$"
 690                 i++
 691                 if i < len(b) {
 692                         goto top
 693                 }
 694         }
 695 }
 696
 697 func atexit(foobar []func()) {
 698         for i := len(foobar) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1"
 699                 f := foobar[i]
 700                 foobar = foobar[:i] // ERROR "IsSliceInBounds"
 701                 f()
 702         }
 703 }
 704
 705 func make1(n int) []int {
 706         s := make([]int, n)
 707         for i := 0; i < n; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1"
 708                 s[i] = 1 // ERROR "Proved IsInBounds$"
 709         }
 710         return s
 711 }
 712
 713 func make2(n int) []int {
 714         s := make([]int, n)
 715         for i := range s { // ERROR "Induction variable: limits \[0,\?\), increment 1"
 716                 s[i] = 1 // ERROR "Proved IsInBounds$"
 717         }
 718         return s
 719 }
 720
 721 // The range tests below test the index variable of range loops.
 722
 723 // range1 compiles to the "efficiently indexable" form of a range loop.
 724 func range1(b []int) {
 725         for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 726                 b[i] = v + 1    // ERROR "Proved IsInBounds$"
 727                 if i < len(b) { // ERROR "Proved Less64$"
 728                         println("x")
 729                 }
 730                 if i >= 0 { // ERROR "Proved Leq64$"
 731                         println("x")
 732                 }
 733         }
 734 }
 735
 736 // range2 elements are larger, so they use the general form of a range loop.
 737 func range2(b [][32]int) {
 738         for i, v := range b {
 739                 b[i][0] = v[0] + 1 // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Proved IsInBounds$"
 740                 if i < len(b) {    // ERROR "Proved Less64$"
 741                         println("x")
 742                 }
 743                 if i >= 0 { // ERROR "Proved Leq64$"
 744                         println("x")
 745                 }
 746         }
 747 }
 748
 749 // signhint1-2 test whether the hint (int >= 0) is propagated into the loop.
 750 func signHint1(i int, data []byte) {
 751         if i >= 0 {
 752                 for i < len(data) { // ERROR "Induction variable: limits \[\?,\?\), increment 1$"
 753                         _ = data[i] // ERROR "Proved IsInBounds$"
 754                         i++
 755                 }
 756         }
 757 }
 758
 759 func signHint2(b []byte, n int) {
 760         if n < 0 {
 761                 panic("")
 762         }
 763         _ = b[25]
 764         for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
 765                 b[i] = 123 // ERROR "Proved IsInBounds$"
 766         }
 767 }
 768
 769 // indexGT0 tests whether prove learns int index >= 0 from bounds check.
 770 func indexGT0(b []byte, n int) {
 771         _ = b[n]
 772         _ = b[25]
 773
 774         for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
 775                 b[i] = 123 // ERROR "Proved IsInBounds$"
 776         }
 777 }
 778
 779 // Induction variable in unrolled loop.
 780 func unrollUpExcl(a []int) int {
 781         var i, x int
 782         for i = 0; i < len(a)-1; i += 2 { // ERROR "Induction variable: limits \[0,\?\), increment 2$"
 783                 x += a[i] // ERROR "Proved IsInBounds$"
 784                 x += a[i+1]
 785         }
 786         if i == len(a)-1 {
 787                 x += a[i]
 788         }
 789         return x
 790 }
 791
 792 // Induction variable in unrolled loop.
 793 func unrollUpIncl(a []int) int {
 794         var i, x int
 795         for i = 0; i <= len(a)-2; i += 2 { // ERROR "Induction variable: limits \[0,\?\], increment 2$"
 796                 x += a[i]
 797                 x += a[i+1]
 798         }
 799         if i == len(a)-1 {
 800                 x += a[i]
 801         }
 802         return x
 803 }
 804
 805 // Induction variable in unrolled loop.
 806 func unrollDownExcl0(a []int) int {
 807         var i, x int
 808         for i = len(a) - 1; i > 0; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
 809                 x += a[i]   // ERROR "Proved IsInBounds$"
 810                 x += a[i-1] // ERROR "Proved IsInBounds$"
 811         }
 812         if i == 0 {
 813                 x += a[i]
 814         }
 815         return x
 816 }
 817
 818 // Induction variable in unrolled loop.
 819 func unrollDownExcl1(a []int) int {
 820         var i, x int
 821         for i = len(a) - 1; i >= 1; i -= 2 { // ERROR "Induction variable: limits \[1,\?\], increment 2$"
 822                 x += a[i]   // ERROR "Proved IsInBounds$"
 823                 x += a[i-1] // ERROR "Proved IsInBounds$"
 824         }
 825         if i == 0 {
 826                 x += a[i]
 827         }
 828         return x
 829 }
 830
 831 // Induction variable in unrolled loop.
 832 func unrollDownInclStep(a []int) int {
 833         var i, x int
 834         for i = len(a); i >= 2; i -= 2 { // ERROR "Induction variable: limits \[2,\?\], increment 2$"
 835                 x += a[i-1] // ERROR "Proved IsInBounds$"
 836                 x += a[i-2]
 837         }
 838         if i == 1 {
 839                 x += a[i-1]
 840         }
 841         return x
 842 }
 843
 844 // Not an induction variable (step too large)
 845 func unrollExclStepTooLarge(a []int) int {
 846         var i, x int
 847         for i = 0; i < len(a)-1; i += 3 {
 848                 x += a[i]
 849                 x += a[i+1]
 850         }
 851         if i == len(a)-1 {
 852                 x += a[i]
 853         }
 854         return x
 855 }
 856
 857 // Not an induction variable (step too large)
 858 func unrollInclStepTooLarge(a []int) int {
 859         var i, x int
 860         for i = 0; i <= len(a)-2; i += 3 {
 861                 x += a[i]
 862                 x += a[i+1]
 863         }
 864         if i == len(a)-1 {
 865                 x += a[i]
 866         }
 867         return x
 868 }
 869
 870 // Not an induction variable (min too small, iterating down)
 871 func unrollDecMin(a []int) int {
 872         var i, x int
 873         for i = len(a); i >= math.MinInt64; i -= 2 {
 874                 x += a[i-1]
 875                 x += a[i-2]
 876         }
 877         if i == 1 { // ERROR "Disproved Eq64$"
 878                 x += a[i-1]
 879         }
 880         return x
 881 }
 882
 883 // Not an induction variable (min too small, iterating up -- perhaps could allow, but why bother?)
 884 func unrollIncMin(a []int) int {
 885         var i, x int
 886         for i = len(a); i >= math.MinInt64; i += 2 {
 887                 x += a[i-1]
 888                 x += a[i-2]
 889         }
 890         if i == 1 { // ERROR "Disproved Eq64$"
 891                 x += a[i-1]
 892         }
 893         return x
 894 }
 895
 896 // The 4 xxxxExtNto64 functions below test whether prove is looking
 897 // through value-preserving sign/zero extensions of index values (issue #26292).
 898
 899 // Look through all extensions
 900 func signExtNto64(x []int, j8 int8, j16 int16, j32 int32) int {
 901         if len(x) < 22 {
 902                 return 0
 903         }
 904         if j8 >= 0 && j8 < 22 {
 905                 return x[j8] // ERROR "Proved IsInBounds$"
 906         }
 907         if j16 >= 0 && j16 < 22 {
 908                 return x[j16] // ERROR "Proved IsInBounds$"
 909         }
 910         if j32 >= 0 && j32 < 22 {
 911                 return x[j32] // ERROR "Proved IsInBounds$"
 912         }
 913         return 0
 914 }
 915
 916 func zeroExtNto64(x []int, j8 uint8, j16 uint16, j32 uint32) int {
 917         if len(x) < 22 {
 918                 return 0
 919         }
 920         if j8 >= 0 && j8 < 22 {
 921                 return x[j8] // ERROR "Proved IsInBounds$"
 922         }
 923         if j16 >= 0 && j16 < 22 {
 924                 return x[j16] // ERROR "Proved IsInBounds$"
 925         }
 926         if j32 >= 0 && j32 < 22 {
 927                 return x[j32] // ERROR "Proved IsInBounds$"
 928         }
 929         return 0
 930 }
 931
 932 // Process fence-post implications through 32to64 extensions (issue #29964)
 933 func signExt32to64Fence(x []int, j int32) int {
 934         if x[j] != 0 {
 935                 return 1
 936         }
 937         if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
 938                 return 1
 939         }
 940         return 0
 941 }
 942
 943 func zeroExt32to64Fence(x []int, j uint32) int {
 944         if x[j] != 0 {
 945                 return 1
 946         }
 947         if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
 948                 return 1
 949         }
 950         return 0
 951 }
 952
 953 // Ensure that bounds checks with negative indexes are not incorrectly removed.
 954 func negIndex() {
 955         n := make([]int, 1)
 956         for i := -1; i <= 0; i++ { // ERROR "Induction variable: limits \[-1,0\], increment 1$"
 957                 n[i] = 1
 958         }
 959 }
 960 func negIndex2(n int) {
 961         a := make([]int, 5)
 962         b := make([]int, 5)
 963         c := make([]int, 5)
 964         for i := -1; i <= 0; i-- {
 965                 b[i] = i
 966                 n++
 967                 if n > 10 {
 968                         break
 969                 }
 970         }
 971         useSlice(a)
 972         useSlice(c)
 973 }
 974
 975 // Check that prove is zeroing these right shifts of positive ints by bit-width - 1.
 976 // e.g (Rsh64x64 <t> n (Const64 <typ.UInt64> [63])) && ft.isNonNegative(n) -> 0
 977 func sh64(n int64) int64 {
 978         if n < 0 {
 979                 return n
 980         }
 981         return n >> 63 // ERROR "Proved Rsh64x64 shifts to zero"
 982 }
 983
 984 func sh32(n int32) int32 {
 985         if n < 0 {
 986                 return n
 987         }
 988         return n >> 31 // ERROR "Proved Rsh32x64 shifts to zero"
 989 }
 990
 991 func sh32x64(n int32) int32 {
 992         if n < 0 {
 993                 return n
 994         }
 995         return n >> uint64(31) // ERROR "Proved Rsh32x64 shifts to zero"
 996 }
 997
 998 func sh16(n int16) int16 {
 999         if n < 0 {
1000                 return n
1001         }
1002         return n >> 15 // ERROR "Proved Rsh16x64 shifts to zero"
1003 }
1004
1005 func sh64noopt(n int64) int64 {
1006         return n >> 63 // not optimized; n could be negative
1007 }
1008
1009 // These cases are division of a positive signed integer by a power of 2.
1010 // The opt pass doesnt have sufficient information to see that n is positive.
1011 // So, instead, opt rewrites the division with a less-than-optimal replacement.
1012 // Prove, which can see that n is nonnegative, cannot see the division because
1013 // opt, an earlier pass, has already replaced it.
1014 // The fix for this issue allows prove to zero a right shift that was added as
1015 // part of the less-than-optimal reqwrite. That change by prove then allows
1016 // lateopt to clean up all the unnecessary parts of the original division
1017 // replacement. See issue #36159.
1018 func divShiftClean(n int) int {
1019         if n < 0 {
1020                 return n
1021         }
1022         return n / int(8) // ERROR "Proved Rsh64x64 shifts to zero"
1023 }
1024
1025 func divShiftClean64(n int64) int64 {
1026         if n < 0 {
1027                 return n
1028         }
1029         return n / int64(16) // ERROR "Proved Rsh64x64 shifts to zero"
1030 }
1031
1032 func divShiftClean32(n int32) int32 {
1033         if n < 0 {
1034                 return n
1035         }
1036         return n / int32(16) // ERROR "Proved Rsh32x64 shifts to zero"
1037 }
1038
1039 //go:noinline
1040 func useInt(a int) {
1041 }
1042
1043 //go:noinline
1044 func useSlice(a []int) {
1045 }
1046
1047 func main() {
1048 }