test/prove.go

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