test/loopbce.go

   1 // +build amd64
   2 // errorcheck -0 -d=ssa/prove/debug=1
   3
   4 package main
   5
   6 func f0a(a []int) int {
   7         x := 0
   8         for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   9                 x += a[i] // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
  10         }
  11         return x
  12 }
  13
  14 func f0b(a []int) int {
  15         x := 0
  16         for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
  17                 b := a[i:] // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
  18                 x += b[0]
  19         }
  20         return x
  21 }
  22
  23 func f0c(a []int) int {
  24         x := 0
  25         for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
  26                 b := a[:i+1] // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
  27                 x += b[0]
  28         }
  29         return x
  30 }
  31
  32 func f1(a []int) int {
  33         x := 0
  34         for _, i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
  35                 x += i
  36         }
  37         return x
  38 }
  39
  40 func f2(a []int) int {
  41         x := 0
  42         for i := 1; i < len(a); i++ { // ERROR "Induction variable: limits \[1,\?\), increment 1$"
  43                 x += a[i] // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
  44         }
  45         return x
  46 }
  47
  48 func f4(a [10]int) int {
  49         x := 0
  50         for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$"
  51                 x += a[i] // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
  52         }
  53         return x
  54 }
  55
  56 func f5(a [10]int) int {
  57         x := 0
  58         for i := -10; i < len(a); i += 2 { // ERROR "Induction variable: limits \[-10,10\), increment 2$"
  59                 x += a[i]
  60         }
  61         return x
  62 }
  63
  64 func f6(a []int) {
  65         for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
  66                 b := a[0:i] // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" "(\([0-9]+\) )?Proved Geq64$"
  67                 f6(b)
  68         }
  69 }
  70
  71 func g0a(a string) int {
  72         x := 0
  73         for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
  74                 x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
  75         }
  76         return x
  77 }
  78
  79 func g0b(a string) int {
  80         x := 0
  81         for i := 0; len(a) > i; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
  82                 x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
  83         }
  84         return x
  85 }
  86
  87 func g0c(a string) int {
  88         x := 0
  89         for i := len(a); i > 0; i-- { // ERROR "Induction variable: limits \(0,\?\], increment 1$"
  90                 x += int(a[i-1]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
  91         }
  92         return x
  93 }
  94
  95 func g0d(a string) int {
  96         x := 0
  97         for i := len(a); 0 < i; i-- { // ERROR "Induction variable: limits \(0,\?\], increment 1$"
  98                 x += int(a[i-1]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
  99         }
 100         return x
 101 }
 102
 103 func g0e(a string) int {
 104         x := 0
 105         for i := len(a) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1$"
 106                 x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 107         }
 108         return x
 109 }
 110
 111 func g0f(a string) int {
 112         x := 0
 113         for i := len(a) - 1; 0 <= i; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1$"
 114                 x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 115         }
 116         return x
 117 }
 118
 119 func g1() int {
 120         a := "evenlength"
 121         x := 0
 122         for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$"
 123                 x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 124         }
 125         return x
 126 }
 127
 128 func g2() int {
 129         a := "evenlength"
 130         x := 0
 131         for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$"
 132                 j := i
 133                 if a[i] == 'e' { // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 134                         j = j + 1
 135                 }
 136                 x += int(a[j])
 137         }
 138         return x
 139 }
 140
 141 func g3a() {
 142         a := "this string has length 25"
 143         for i := 0; i < len(a); i += 5 { // ERROR "Induction variable: limits \[0,25\), increment 5$"
 144                 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 145                 useString(a[:i+3])
 146         }
 147 }
 148
 149 func g3b(a string) {
 150         for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 151                 useString(a[i+1:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 152         }
 153 }
 154
 155 func g3c(a string) {
 156         for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 157                 useString(a[:i+1]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 158         }
 159 }
 160
 161 func h1(a []byte) {
 162         c := a[:128]
 163         for i := range c { // ERROR "Induction variable: limits \[0,128\), increment 1$"
 164                 c[i] = byte(i) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 165         }
 166 }
 167
 168 func h2(a []byte) {
 169         for i := range a[:128] { // ERROR "Induction variable: limits \[0,128\), increment 1$"
 170                 a[i] = byte(i)
 171         }
 172 }
 173
 174 func k0(a [100]int) [100]int {
 175         for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
 176                 a[i-11] = i
 177                 a[i-10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 178                 a[i-5] = i  // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 179                 a[i] = i    // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 180                 a[i+5] = i  // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 181                 a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 182                 a[i+11] = i
 183         }
 184         return a
 185 }
 186
 187 func k1(a [100]int) [100]int {
 188         for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
 189                 useSlice(a[:i-11]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 190                 useSlice(a[:i-10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 191                 useSlice(a[:i-5])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 192                 useSlice(a[:i])    // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$" "(\([0-9]+\) )?Proved Geq64$"
 193                 useSlice(a[:i+5])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 194                 useSlice(a[:i+10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 195                 useSlice(a[:i+11]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 196                 useSlice(a[:i+12])
 197
 198         }
 199         return a
 200 }
 201
 202 func k2(a [100]int) [100]int {
 203         for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
 204                 useSlice(a[i-11:])
 205                 useSlice(a[i-10:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 206                 useSlice(a[i-5:])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 207                 useSlice(a[i:])    // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 208                 useSlice(a[i+5:])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 209                 useSlice(a[i+10:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 210                 useSlice(a[i+11:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 211                 useSlice(a[i+12:])
 212         }
 213         return a
 214 }
 215
 216 func k3(a [100]int) [100]int {
 217         for i := -10; i < 90; i++ { // ERROR "Induction variable: limits \[-10,90\), increment 1$"
 218                 a[i+9] = i
 219                 a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 220                 a[i+11] = i
 221         }
 222         return a
 223 }
 224
 225 func k3neg(a [100]int) [100]int {
 226         for i := 89; i > -11; i-- { // ERROR "Induction variable: limits \(-11,89\], increment 1$"
 227                 a[i+9] = i
 228                 a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 229                 a[i+11] = i
 230         }
 231         return a
 232 }
 233
 234 func k3neg2(a [100]int) [100]int {
 235         for i := 89; i >= -10; i-- { // ERROR "Induction variable: limits \[-10,89\], increment 1$"
 236                 a[i+9] = i
 237                 a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 238                 a[i+11] = i
 239         }
 240         return a
 241 }
 242
 243 func k4(a [100]int) [100]int {
 244         min := (-1) << 63
 245         for i := min; i < min+50; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,-9223372036854775758\), increment 1$"
 246                 a[i-min] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 247         }
 248         return a
 249 }
 250
 251 func k5(a [100]int) [100]int {
 252         max := (1 << 63) - 1
 253         for i := max - 50; i < max; i++ { // ERROR "Induction variable: limits \[9223372036854775757,9223372036854775807\), increment 1$"
 254                 a[i-max+50] = i   // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 255                 a[i-(max-70)] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
 256         }
 257         return a
 258 }
 259
 260 func nobce1() {
 261         // tests overflow of max-min
 262         a := int64(9223372036854774057)
 263         b := int64(-1547)
 264         z := int64(1337)
 265
 266         if a%z == b%z {
 267                 panic("invalid test: modulos should differ")
 268         }
 269
 270         for i := b; i < a; i += z {
 271                 // No induction variable is possible because i will overflow a first iteration.
 272                 useString("foobar")
 273         }
 274 }
 275
 276 func nobce2(a string) {
 277         for i := int64(0); i < int64(len(a)); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 278                 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 279         }
 280         for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 281                 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 282         }
 283         for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 284                 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 285         }
 286         j := int64(len(a)) - 123
 287         for i := int64(0); i < j+123+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 288                 useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
 289         }
 290         for i := int64(0); i < j+122+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
 291                 // len(a)-123+122+MinInt overflows when len(a) == 0, so a bound check is needed here
 292                 useString(a[i:])
 293         }
 294 }
 295
 296 func nobce3(a [100]int64) [100]int64 {
 297         min := int64((-1) << 63)
 298         max := int64((1 << 63) - 1)
 299         for i := min; i < max; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,9223372036854775807\), increment 1$"
 300                 a[i] = i
 301         }
 302         return a
 303 }
 304
 305 func issue26116a(a []int) {
 306         // There is no induction variable here. The comparison is in the wrong direction.
 307         for i := 3; i > 6; i++ {
 308                 a[i] = 0
 309         }
 310         for i := 7; i < 3; i-- {
 311                 a[i] = 1
 312         }
 313 }
 314
 315 //go:noinline
 316 func useString(a string) {
 317 }
 318
 319 //go:noinline
 320 func useSlice(a []int) {
 321 }
 322
 323 func main() {
 324 }