test/loopbce.go

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