1// errorcheck -0 -d=ssa/prove/debug=1 2 3//go:build amd64 4 5package main 6 7import "math" 8 9func 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 17func 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 26func 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 35func 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 43func 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 51func 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 59func 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 67func 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 75func 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 83func 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 91func 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 98func 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 106func 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 114func 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 122func 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 130func 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 138func 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 146func 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 155func 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 168func 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 178func 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 184func 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 190func 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 197func 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 203func 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 220func 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 239func 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 257func 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 270func 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 283func 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 296func 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 304func 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 313func 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 324func 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 335func 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 346func 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 373func 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 400func 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 415func 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 435func 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 443func 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 453func 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 461func 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 470func useString(a string) { 471} 472 473//go:noinline 474func useSlice(a []int) { 475} 476 477func main() { 478} 479