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]
  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]
  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]
  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]
  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                 a[i-11] = i
 205                 a[i-10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 206                 a[i-5] = i  // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 207                 a[i] = i    // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 208                 a[i+5] = i  // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 209                 a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 210                 a[i+11] = i
 211         }
 212         return a
 213 }
 214
 215 func k1(a [100]int) [100]int {
 216         for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
 217                 useSlice(a[:i-11])
 218                 useSlice(a[:i-10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 219                 useSlice(a[:i-5])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 220                 useSlice(a[:i])    // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 221                 useSlice(a[:i+5])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 222                 useSlice(a[:i+10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 223                 useSlice(a[:i+11]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 224                 useSlice(a[:i+12])
 225
 226         }
 227         return a
 228 }
 229
 230 func k2(a [100]int) [100]int {
 231         for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
 232                 useSlice(a[i-11:])
 233                 useSlice(a[i-10:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 234                 useSlice(a[i-5:])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 235                 useSlice(a[i:])    // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 236                 useSlice(a[i+5:])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 237                 useSlice(a[i+10:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 238                 useSlice(a[i+11:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 239                 useSlice(a[i+12:])
 240         }
 241         return a
 242 }
 243
 244 func k3(a [100]int) [100]int {
 245         for i := -10; i < 90; i++ { // ERROR "Induction variable: limits \[-10,90\), increment 1$"
 246                 a[i+9] = i
 247                 a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 248                 a[i+11] = i
 249         }
 250         return a
 251 }
 252
 253 func k3neg(a [100]int) [100]int {
 254         for i := 89; i > -11; i-- { // ERROR "Induction variable: limits \(-11,89\], increment 1$"
 255                 a[i+9] = i
 256                 a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 257                 a[i+11] = i
 258         }
 259         return a
 260 }
 261
 262 func k3neg2(a [100]int) [100]int {
 263         for i := 89; i >= -10; i-- { // ERROR "Induction variable: limits \[-10,89\], increment 1$"
 264                 a[i+9] = i
 265                 a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 266                 a[i+11] = i
 267         }
 268         return a
 269 }
 270
 271 func k4(a [100]int) [100]int {
 272         min := (-1) << 63
 273         for i := min; i < min+50; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,-9223372036854775758\), increment 1$"
 274                 a[i-min] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 275         }
 276         return a
 277 }
 278
 279 func k5(a [100]int) [100]int {
 280         max := (1 << 63) - 1
 281         for i := max - 50; i < max; i++ { // ERROR "Induction variable: limits \[9223372036854775757,9223372036854775807\), increment 1$"
 282                 a[i-max+50] = i   // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 283                 a[i-(max-70)] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 284         }
 285         return a
 286 }
 287
 288 func d1(a [100]int) [100]int {
 289         for i := 0; i < 100; i++ { // ERROR "Induction variable: limits \[0,100\), increment 1$"
 290                 for j := 0; j < i; j++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 291                         a[j] = 0   // ERROR "Proved IsInBounds$"
 292                         a[j+1] = 0 // FIXME: this boundcheck should be eliminated
 293                         a[j+2] = 0
 294                 }
 295         }
 296         return a
 297 }
 298
 299 func d2(a [100]int) [100]int {
 300         for i := 0; i < 100; i++ { // ERROR "Induction variable: limits \[0,100\), increment 1$"
 301                 for j := 0; i > j; j++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 302                         a[j] = 0   // ERROR "Proved IsInBounds$"
 303                         a[j+1] = 0 // FIXME: this boundcheck should be eliminated
 304                         a[j+2] = 0
 305                 }
 306         }
 307         return a
 308 }
 309
 310 func d3(a [100]int) [100]int {
 311         for i := 0; i <= 99; i++ { // ERROR "Induction variable: limits \[0,99\], increment 1$"
 312                 for j := 0; j <= i-1; j++ {
 313                         a[j] = 0
 314                         a[j+1] = 0 // ERROR "Proved IsInBounds$"
 315                         a[j+2] = 0
 316                 }
 317         }
 318         return a
 319 }
 320
 321 func d4() {
 322         for i := int64(math.MaxInt64 - 9); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775798,9223372036854775802\], increment 4$"
 323                 useString("foo")
 324         }
 325         for i := int64(math.MaxInt64 - 8); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775799,9223372036854775803\], increment 4$"
 326                 useString("foo")
 327         }
 328         for i := int64(math.MaxInt64 - 7); i < math.MaxInt64-2; i += 4 {
 329                 useString("foo")
 330         }
 331         for i := int64(math.MaxInt64 - 6); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775801,9223372036854775801\], increment 4$"
 332                 useString("foo")
 333         }
 334         for i := int64(math.MaxInt64 - 9); i <= math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775798,9223372036854775802\], increment 4$"
 335                 useString("foo")
 336         }
 337         for i := int64(math.MaxInt64 - 8); i <= math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775799,9223372036854775803\], increment 4$"
 338                 useString("foo")
 339         }
 340         for i := int64(math.MaxInt64 - 7); i <= math.MaxInt64-2; i += 4 {
 341                 useString("foo")
 342         }
 343         for i := int64(math.MaxInt64 - 6); i <= math.MaxInt64-2; i += 4 {
 344                 useString("foo")
 345         }
 346 }
 347
 348 func d5() {
 349         for i := int64(math.MinInt64 + 9); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775803,-9223372036854775799\], increment 4"
 350                 useString("foo")
 351         }
 352         for i := int64(math.MinInt64 + 8); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775804,-9223372036854775800\], increment 4"
 353                 useString("foo")
 354         }
 355         for i := int64(math.MinInt64 + 7); i > math.MinInt64+2; i -= 4 {
 356                 useString("foo")
 357         }
 358         for i := int64(math.MinInt64 + 6); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775802,-9223372036854775802\], increment 4"
 359                 useString("foo")
 360         }
 361         for i := int64(math.MinInt64 + 9); i >= math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775803,-9223372036854775799\], increment 4"
 362                 useString("foo")
 363         }
 364         for i := int64(math.MinInt64 + 8); i >= math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775804,-9223372036854775800\], increment 4"
 365                 useString("foo")
 366         }
 367         for i := int64(math.MinInt64 + 7); i >= math.MinInt64+2; i -= 4 {
 368                 useString("foo")
 369         }
 370         for i := int64(math.MinInt64 + 6); i >= math.MinInt64+2; i -= 4 {
 371                 useString("foo")
 372         }
 373 }
 374
 375 func bce1() {
 376         // tests overflow of max-min
 377         a := int64(9223372036854774057)
 378         b := int64(-1547)
 379         z := int64(1337)
 380
 381         if a%z == b%z {
 382                 panic("invalid test: modulos should differ")
 383         }
 384
 385         for i := b; i < a; i += z { // ERROR "Induction variable: limits \[-1547,9223372036854772720\], increment 1337"
 386                 useString("foobar")
 387         }
 388 }
 389
 390 func nobce2(a string) {
 391         for i := int64(0); i < int64(len(a)); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 392                 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 393         }
 394         for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 395                 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 396         }
 397         for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 398                 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 399         }
 400         j := int64(len(a)) - 123
 401         for i := int64(0); i < j+123+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 402                 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 403         }
 404         for i := int64(0); i < j+122+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 405                 // len(a)-123+122+MinInt overflows when len(a) == 0, so a bound check is needed here
 406                 useString(a[i:])
 407         }
 408 }
 409
 410 func nobce3(a [100]int64) [100]int64 {
 411         min := int64((-1) << 63)
 412         max := int64((1 << 63) - 1)
 413         for i := min; i < max; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,9223372036854775807\), increment 1$"
 414                 a[i] = i
 415         }
 416         return a
 417 }
 418
 419 func issue26116a(a []int) {
 420         // There is no induction variable here. The comparison is in the wrong direction.
 421         for i := 3; i > 6; i++ {
 422                 a[i] = 0
 423         }
 424         for i := 7; i < 3; i-- {
 425                 a[i] = 1
 426         }
 427 }
 428
 429 func stride1(x *[7]int) int {
 430         s := 0
 431         for i := 0; i <= 8; i += 3 { // ERROR "Induction variable: limits \[0,6\], increment 3"
 432                 s += x[i] // ERROR "Proved IsInBounds"
 433         }
 434         return s
 435 }
 436
 437 func stride2(x *[7]int) int {
 438         s := 0
 439         for i := 0; i < 9; i += 3 { // ERROR "Induction variable: limits \[0,6\], increment 3"
 440                 s += x[i] // ERROR "Proved IsInBounds"
 441         }
 442         return s
 443 }
 444
 445 //go:noinline
 446 func useString(a string) {
 447 }
 448
 449 //go:noinline
 450 func useSlice(a []int) {
 451 }
 452
 453 func main() {
 454 }