test/prove.go

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