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) { // todo: handle this case
  46                 return a[i-10]
  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 {
  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 Greater64$"
  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 Greater64$"
 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 Geq64$"
 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 Greater8U$"
 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 Geq8U$"
 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 Geq64$"
 303                                 return 4
 304                         }
 305                 }
 306                 if x {
 307                         if a > 12 { // ERROR "Proved Greater64$"
 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 Geq64$"
 335                                 return 10
 336                         }
 337                 }
 338                 if x {
 339                         if a > -9 { // ERROR "Disproved Greater64$"
 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 Geq64$"
 367                                 return 16
 368                         }
 369                 }
 370                 if x {
 371                         if a > 90 { // ERROR "Disproved Greater64$"
 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 Greater64$"
 392                         return 1
 393                 }
 394         }
 395         return 0
 396 }
 397
 398 func f13f(a int64) int64 {
 399         if a > math.MaxInt64 {
 400                 // Unreachable, but prove doesn't know that.
 401                 if a == 0 {
 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 Greater64U$"
 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++ {
 469                 useSlice(b[i:]) // Learns i <= len
 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 sm1(b []int, x int) {
 479         // Test constant argument to slicemask.
 480         useSlice(b[2:8]) // ERROR "Proved slicemask not needed$"
 481         // Test non-constant argument with known limits.
 482         // Right now prove only uses the unsigned limit.
 483         if uint(cap(b)) > 10 {
 484                 useSlice(b[2:]) // ERROR "Proved slicemask not needed$"
 485         }
 486 }
 487
 488 //go:noinline
 489 func useInt(a int) {
 490 }
 491
 492 //go:noinline
 493 func useSlice(a []int) {
 494 }
 495
 496 func main() {
 497 }