test/loopbce.go

   1 // errorcheck -0 -d=ssa/prove/debug=1
   2
   3 //go:build amd64
   4
   5 package main
   6
   7 import "math"
   8
   9 func f0a(a []int) int {
  10         x := 0
  11         for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
  12                 x += a[i] // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
  13         }
  14         return x
  15 }
  16
  17 func f0b(a []int) int {
  18         x := 0
  19         for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
  20                 b := a[i:] // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
  21                 x += b[0]
  22         }
  23         return x
  24 }
  25
  26 func f0c(a []int) int {
  27         x := 0
  28         for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
  29                 b := a[:i+1] // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
  30                 x += b[0]
  31         }
  32         return x
  33 }
  34
  35 func f1(a []int) int {
  36         x := 0
  37         for _, i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
  38                 x += i
  39         }
  40         return x
  41 }
  42
  43 func f2(a []int) int {
  44         x := 0
  45         for i := 1; i < len(a); i++ { // ERROR "Induction variable: limits \[1,\?\), increment 1$"
  46                 x += a[i] // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
  47         }
  48         return x
  49 }
  50
  51 func f4(a [10]int) int {
  52         x := 0
  53         for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,8\], increment 2$"
  54                 x += a[i] // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
  55         }
  56         return x
  57 }
  58
  59 func f5(a [10]int) int {
  60         x := 0
  61         for i := -10; i < len(a); i += 2 { // ERROR "Induction variable: limits \[-10,8\], increment 2$"
  62                 x += a[i+10]
  63         }
  64         return x
  65 }
  66
  67 func f5_int32(a [10]int) int {
  68         x := 0
  69         for i := int32(-10); i < int32(len(a)); i += 2 { // ERROR "Induction variable: limits \[-10,8\], increment 2$"
  70                 x += a[i+10]
  71         }
  72         return x
  73 }
  74
  75 func f5_int16(a [10]int) int {
  76         x := 0
  77         for i := int16(-10); i < int16(len(a)); i += 2 { // ERROR "Induction variable: limits \[-10,8\], increment 2$"
  78                 x += a[i+10]
  79         }
  80         return x
  81 }
  82
  83 func f5_int8(a [10]int) int {
  84         x := 0
  85         for i := int8(-10); i < int8(len(a)); i += 2 { // ERROR "Induction variable: limits \[-10,8\], increment 2$"
  86                 x += a[i+10]
  87         }
  88         return x
  89 }
  90
  91 func f6(a []int) {
  92         for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
  93                 b := a[0:i] // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
  94                 f6(b)
  95         }
  96 }
  97
  98 func g0a(a string) int {
  99         x := 0
 100         for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 101                 x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 102         }
 103         return x
 104 }
 105
 106 func g0b(a string) int {
 107         x := 0
 108         for i := 0; len(a) > i; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 109                 x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 110         }
 111         return x
 112 }
 113
 114 func g0c(a string) int {
 115         x := 0
 116         for i := len(a); i > 0; i-- { // ERROR "Induction variable: limits \(0,\?\], increment 1$"
 117                 x += int(a[i-1]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 118         }
 119         return x
 120 }
 121
 122 func g0d(a string) int {
 123         x := 0
 124         for i := len(a); 0 < i; i-- { // ERROR "Induction variable: limits \(0,\?\], increment 1$"
 125                 x += int(a[i-1]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 126         }
 127         return x
 128 }
 129
 130 func g0e(a string) int {
 131         x := 0
 132         for i := len(a) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1$"
 133                 x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 134         }
 135         return x
 136 }
 137
 138 func g0f(a string) int {
 139         x := 0
 140         for i := len(a) - 1; 0 <= i; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1$"
 141                 x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 142         }
 143         return x
 144 }
 145
 146 func g1() int {
 147         a := "evenlength"
 148         x := 0
 149         for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,8\], increment 2$"
 150                 x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 151         }
 152         return x
 153 }
 154
 155 func g2() int {
 156         a := "evenlength"
 157         x := 0
 158         for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,8\], increment 2$"
 159                 j := i
 160                 if a[i] == 'e' { // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 161                         j = j + 1
 162                 }
 163                 x += int(a[j])
 164         }
 165         return x
 166 }
 167
 168 func g3a() {
 169         a := "this string has length 25"
 170         for i := 0; i < len(a); i += 5 { // ERROR "Induction variable: limits \[0,20\], increment 5$"
 171                 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 172                 useString(a[:i+3]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 173                 useString(a[:i+5]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 174                 useString(a[:i+6])
 175         }
 176 }
 177
 178 func g3b(a string) {
 179         for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 180                 useString(a[i+1:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 181         }
 182 }
 183
 184 func g3c(a string) {
 185         for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 186                 useString(a[:i+1]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 187         }
 188 }
 189
 190 func h1(a []byte) {
 191         c := a[:128]
 192         for i := range c { // ERROR "Induction variable: limits \[0,128\), increment 1$"
 193                 c[i] = byte(i) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 194         }
 195 }
 196
 197 func h2(a []byte) {
 198         for i := range a[:128] { // ERROR "Induction variable: limits \[0,128\), increment 1$"
 199                 a[i] = byte(i)
 200         }
 201 }
 202
 203 func k0(a [100]int) [100]int {
 204         for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
 205                 if a[0] == 0xdeadbeef {
 206                         // This is a trick to prohibit sccp to optimize out the following out of bound check
 207                         continue
 208                 }
 209                 a[i-11] = i
 210                 a[i-10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 211                 a[i-5] = i  // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 212                 a[i] = i    // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 213                 a[i+5] = i  // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 214                 a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 215                 a[i+11] = i
 216         }
 217         return a
 218 }
 219
 220 func k1(a [100]int) [100]int {
 221         for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
 222                 if a[0] == 0xdeadbeef {
 223                         // This is a trick to prohibit sccp to optimize out the following out of bound check
 224                         continue
 225                 }
 226                 useSlice(a[:i-11])
 227                 useSlice(a[:i-10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 228                 useSlice(a[:i-5])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 229                 useSlice(a[:i])    // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 230                 useSlice(a[:i+5])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 231                 useSlice(a[:i+10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 232                 useSlice(a[:i+11]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 233                 useSlice(a[:i+12])
 234
 235         }
 236         return a
 237 }
 238
 239 func k2(a [100]int) [100]int {
 240         for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
 241                 if a[0] == 0xdeadbeef {
 242                         // This is a trick to prohibit sccp to optimize out the following out of bound check
 243                         continue
 244                 }
 245                 useSlice(a[i-11:])
 246                 useSlice(a[i-10:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 247                 useSlice(a[i-5:])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 248                 useSlice(a[i:])    // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 249                 useSlice(a[i+5:])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 250                 useSlice(a[i+10:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 251                 useSlice(a[i+11:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 252                 useSlice(a[i+12:])
 253         }
 254         return a
 255 }
 256
 257 func k3(a [100]int) [100]int {
 258         for i := -10; i < 90; i++ { // ERROR "Induction variable: limits \[-10,90\), increment 1$"
 259                 if a[0] == 0xdeadbeef {
 260                         // This is a trick to prohibit sccp to optimize out the following out of bound check
 261                         continue
 262                 }
 263                 a[i+9] = i
 264                 a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 265                 a[i+11] = i
 266         }
 267         return a
 268 }
 269
 270 func k3neg(a [100]int) [100]int {
 271         for i := 89; i > -11; i-- { // ERROR "Induction variable: limits \(-11,89\], increment 1$"
 272                 if a[0] == 0xdeadbeef {
 273                         // This is a trick to prohibit sccp to optimize out the following out of bound check
 274                         continue
 275                 }
 276                 a[i+9] = i
 277                 a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 278                 a[i+11] = i
 279         }
 280         return a
 281 }
 282
 283 func k3neg2(a [100]int) [100]int {
 284         for i := 89; i >= -10; i-- { // ERROR "Induction variable: limits \[-10,89\], increment 1$"
 285                 if a[0] == 0xdeadbeef {
 286                         // This is a trick to prohibit sccp to optimize out the following out of bound check
 287                         continue
 288                 }
 289                 a[i+9] = i
 290                 a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 291                 a[i+11] = i
 292         }
 293         return a
 294 }
 295
 296 func k4(a [100]int) [100]int {
 297         min := (-1) << 63
 298         for i := min; i < min+50; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,-9223372036854775758\), increment 1$"
 299                 a[i-min] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 300         }
 301         return a
 302 }
 303
 304 func k5(a [100]int) [100]int {
 305         max := (1 << 63) - 1
 306         for i := max - 50; i < max; i++ { // ERROR "Induction variable: limits \[9223372036854775757,9223372036854775807\), increment 1$"
 307                 a[i-max+50] = i   // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 308                 a[i-(max-70)] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 309         }
 310         return a
 311 }
 312
 313 func d1(a [100]int) [100]int {
 314         for i := 0; i < 100; i++ { // ERROR "Induction variable: limits \[0,100\), increment 1$"
 315                 for j := 0; j < i; j++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 316                         a[j] = 0   // ERROR "Proved IsInBounds$"
 317                         a[j+1] = 0 // FIXME: this boundcheck should be eliminated
 318                         a[j+2] = 0
 319                 }
 320         }
 321         return a
 322 }
 323
 324 func d2(a [100]int) [100]int {
 325         for i := 0; i < 100; i++ { // ERROR "Induction variable: limits \[0,100\), increment 1$"
 326                 for j := 0; i > j; j++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 327                         a[j] = 0   // ERROR "Proved IsInBounds$"
 328                         a[j+1] = 0 // FIXME: this boundcheck should be eliminated
 329                         a[j+2] = 0
 330                 }
 331         }
 332         return a
 333 }
 334
 335 func d3(a [100]int) [100]int {
 336         for i := 0; i <= 99; i++ { // ERROR "Induction variable: limits \[0,99\], increment 1$"
 337                 for j := 0; j <= i-1; j++ {
 338                         a[j] = 0
 339                         a[j+1] = 0 // ERROR "Proved IsInBounds$"
 340                         a[j+2] = 0
 341                 }
 342         }
 343         return a
 344 }
 345
 346 func d4() {
 347         for i := int64(math.MaxInt64 - 9); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775798,9223372036854775802\], increment 4$"
 348                 useString("foo")
 349         }
 350         for i := int64(math.MaxInt64 - 8); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775799,9223372036854775803\], increment 4$"
 351                 useString("foo")
 352         }
 353         for i := int64(math.MaxInt64 - 7); i < math.MaxInt64-2; i += 4 {
 354                 useString("foo")
 355         }
 356         for i := int64(math.MaxInt64 - 6); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775801,9223372036854775801\], increment 4$"
 357                 useString("foo")
 358         }
 359         for i := int64(math.MaxInt64 - 9); i <= math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775798,9223372036854775802\], increment 4$"
 360                 useString("foo")
 361         }
 362         for i := int64(math.MaxInt64 - 8); i <= math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775799,9223372036854775803\], increment 4$"
 363                 useString("foo")
 364         }
 365         for i := int64(math.MaxInt64 - 7); i <= math.MaxInt64-2; i += 4 {
 366                 useString("foo")
 367         }
 368         for i := int64(math.MaxInt64 - 6); i <= math.MaxInt64-2; i += 4 {
 369                 useString("foo")
 370         }
 371 }
 372
 373 func d5() {
 374         for i := int64(math.MinInt64 + 9); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775803,-9223372036854775799\], increment 4"
 375                 useString("foo")
 376         }
 377         for i := int64(math.MinInt64 + 8); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775804,-9223372036854775800\], increment 4"
 378                 useString("foo")
 379         }
 380         for i := int64(math.MinInt64 + 7); i > math.MinInt64+2; i -= 4 {
 381                 useString("foo")
 382         }
 383         for i := int64(math.MinInt64 + 6); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775802,-9223372036854775802\], increment 4"
 384                 useString("foo")
 385         }
 386         for i := int64(math.MinInt64 + 9); i >= math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775803,-9223372036854775799\], increment 4"
 387                 useString("foo")
 388         }
 389         for i := int64(math.MinInt64 + 8); i >= math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775804,-9223372036854775800\], increment 4"
 390                 useString("foo")
 391         }
 392         for i := int64(math.MinInt64 + 7); i >= math.MinInt64+2; i -= 4 {
 393                 useString("foo")
 394         }
 395         for i := int64(math.MinInt64 + 6); i >= math.MinInt64+2; i -= 4 {
 396                 useString("foo")
 397         }
 398 }
 399
 400 func bce1() {
 401         // tests overflow of max-min
 402         a := int64(9223372036854774057)
 403         b := int64(-1547)
 404         z := int64(1337)
 405
 406         if a%z == b%z {
 407                 panic("invalid test: modulos should differ")
 408         }
 409
 410         for i := b; i < a; i += z { // ERROR "Induction variable: limits \[-1547,9223372036854772720\], increment 1337"
 411                 useString("foobar")
 412         }
 413 }
 414
 415 func nobce2(a string) {
 416         for i := int64(0); i < int64(len(a)); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 417                 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 418         }
 419         for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 420                 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 421         }
 422         for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 423                 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 424         }
 425         j := int64(len(a)) - 123
 426         for i := int64(0); i < j+123+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 427                 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 428         }
 429         for i := int64(0); i < j+122+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 430                 // len(a)-123+122+MinInt overflows when len(a) == 0, so a bound check is needed here
 431                 useString(a[i:])
 432         }
 433 }
 434
 435 func nobce3(a [100]int64) [100]int64 {
 436         min := int64((-1) << 63)
 437         max := int64((1 << 63) - 1)
 438         for i := min; i < max; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,9223372036854775807\), increment 1$"
 439         }
 440         return a
 441 }
 442
 443 func issue26116a(a []int) {
 444         // There is no induction variable here. The comparison is in the wrong direction.
 445         for i := 3; i > 6; i++ {
 446                 a[i] = 0
 447         }
 448         for i := 7; i < 3; i-- {
 449                 a[i] = 1
 450         }
 451 }
 452
 453 func stride1(x *[7]int) int {
 454         s := 0
 455         for i := 0; i <= 8; i += 3 { // ERROR "Induction variable: limits \[0,6\], increment 3"
 456                 s += x[i] // ERROR "Proved IsInBounds"
 457         }
 458         return s
 459 }
 460
 461 func stride2(x *[7]int) int {
 462         s := 0
 463         for i := 0; i < 9; i += 3 { // ERROR "Induction variable: limits \[0,6\], increment 3"
 464                 s += x[i] // ERROR "Proved IsInBounds"
 465         }
 466         return s
 467 }
 468
 469 //go:noinline
 470 func useString(a string) {
 471 }
 472
 473 //go:noinline
 474 func useSlice(a []int) {
 475 }
 476
 477 func main() {
 478 }