Source file 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,10\), 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,10\), increment 2$"
    61  		x += a[i]
    62  	}
    63  	return x
    64  }
    65  
    66  func f6(a []int) {
    67  	for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
    68  		b := a[0:i] // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
    69  		f6(b)
    70  	}
    71  }
    72  
    73  func g0a(a string) int {
    74  	x := 0
    75  	for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
    76  		x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
    77  	}
    78  	return x
    79  }
    80  
    81  func g0b(a string) int {
    82  	x := 0
    83  	for i := 0; len(a) > i; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
    84  		x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
    85  	}
    86  	return x
    87  }
    88  
    89  func g0c(a string) int {
    90  	x := 0
    91  	for i := len(a); i > 0; i-- { // ERROR "Induction variable: limits \(0,\?\], increment 1$"
    92  		x += int(a[i-1]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
    93  	}
    94  	return x
    95  }
    96  
    97  func g0d(a string) int {
    98  	x := 0
    99  	for i := len(a); 0 < i; i-- { // ERROR "Induction variable: limits \(0,\?\], increment 1$"
   100  		x += int(a[i-1]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   101  	}
   102  	return x
   103  }
   104  
   105  func g0e(a string) int {
   106  	x := 0
   107  	for i := len(a) - 1; i >= 0; 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 g0f(a string) int {
   114  	x := 0
   115  	for i := len(a) - 1; 0 <= i; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1$"
   116  		x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   117  	}
   118  	return x
   119  }
   120  
   121  func g1() int {
   122  	a := "evenlength"
   123  	x := 0
   124  	for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$"
   125  		x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   126  	}
   127  	return x
   128  }
   129  
   130  func g2() int {
   131  	a := "evenlength"
   132  	x := 0
   133  	for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,10\), increment 2$"
   134  		j := i
   135  		if a[i] == 'e' { // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   136  			j = j + 1
   137  		}
   138  		x += int(a[j])
   139  	}
   140  	return x
   141  }
   142  
   143  func g3a() {
   144  	a := "this string has length 25"
   145  	for i := 0; i < len(a); i += 5 { // ERROR "Induction variable: limits \[0,25\), increment 5$"
   146  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   147  		useString(a[:i+3])
   148  	}
   149  }
   150  
   151  func g3b(a string) {
   152  	for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   153  		useString(a[i+1:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   154  	}
   155  }
   156  
   157  func g3c(a string) {
   158  	for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   159  		useString(a[:i+1]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   160  	}
   161  }
   162  
   163  func h1(a []byte) {
   164  	c := a[:128]
   165  	for i := range c { // ERROR "Induction variable: limits \[0,128\), increment 1$"
   166  		c[i] = byte(i) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   167  	}
   168  }
   169  
   170  func h2(a []byte) {
   171  	for i := range a[:128] { // ERROR "Induction variable: limits \[0,128\), increment 1$"
   172  		a[i] = byte(i)
   173  	}
   174  }
   175  
   176  func k0(a [100]int) [100]int {
   177  	for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
   178  		a[i-11] = i
   179  		a[i-10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   180  		a[i-5] = i  // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   181  		a[i] = i    // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   182  		a[i+5] = i  // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   183  		a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   184  		a[i+11] = i
   185  	}
   186  	return a
   187  }
   188  
   189  func k1(a [100]int) [100]int {
   190  	for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
   191  		useSlice(a[:i-11])
   192  		useSlice(a[:i-10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   193  		useSlice(a[:i-5])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   194  		useSlice(a[:i])    // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   195  		useSlice(a[:i+5])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   196  		useSlice(a[:i+10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   197  		useSlice(a[:i+11]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   198  		useSlice(a[:i+12])
   199  
   200  	}
   201  	return a
   202  }
   203  
   204  func k2(a [100]int) [100]int {
   205  	for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
   206  		useSlice(a[i-11:])
   207  		useSlice(a[i-10:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   208  		useSlice(a[i-5:])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   209  		useSlice(a[i:])    // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   210  		useSlice(a[i+5:])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   211  		useSlice(a[i+10:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   212  		useSlice(a[i+11:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   213  		useSlice(a[i+12:])
   214  	}
   215  	return a
   216  }
   217  
   218  func k3(a [100]int) [100]int {
   219  	for i := -10; i < 90; i++ { // ERROR "Induction variable: limits \[-10,90\), increment 1$"
   220  		a[i+9] = i
   221  		a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   222  		a[i+11] = i
   223  	}
   224  	return a
   225  }
   226  
   227  func k3neg(a [100]int) [100]int {
   228  	for i := 89; i > -11; i-- { // ERROR "Induction variable: limits \(-11,89\], increment 1$"
   229  		a[i+9] = i
   230  		a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   231  		a[i+11] = i
   232  	}
   233  	return a
   234  }
   235  
   236  func k3neg2(a [100]int) [100]int {
   237  	for i := 89; i >= -10; i-- { // ERROR "Induction variable: limits \[-10,89\], increment 1$"
   238  		a[i+9] = i
   239  		a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   240  		a[i+11] = i
   241  	}
   242  	return a
   243  }
   244  
   245  func k4(a [100]int) [100]int {
   246  	min := (-1) << 63
   247  	for i := min; i < min+50; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,-9223372036854775758\), increment 1$"
   248  		a[i-min] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   249  	}
   250  	return a
   251  }
   252  
   253  func k5(a [100]int) [100]int {
   254  	max := (1 << 63) - 1
   255  	for i := max - 50; i < max; i++ { // ERROR "Induction variable: limits \[9223372036854775757,9223372036854775807\), increment 1$"
   256  		a[i-max+50] = i   // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   257  		a[i-(max-70)] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   258  	}
   259  	return a
   260  }
   261  
   262  func d1(a [100]int) [100]int {
   263  	for i := 0; i < 100; i++ { // ERROR "Induction variable: limits \[0,100\), increment 1$"
   264  		for j := 0; j < i; j++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   265  			a[j] = 0   // ERROR "Proved IsInBounds$"
   266  			a[j+1] = 0 // FIXME: this boundcheck should be eliminated
   267  			a[j+2] = 0
   268  		}
   269  	}
   270  	return a
   271  }
   272  
   273  func d2(a [100]int) [100]int {
   274  	for i := 0; i < 100; i++ { // ERROR "Induction variable: limits \[0,100\), increment 1$"
   275  		for j := 0; i > j; j++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   276  			a[j] = 0   // ERROR "Proved IsInBounds$"
   277  			a[j+1] = 0 // FIXME: this boundcheck should be eliminated
   278  			a[j+2] = 0
   279  		}
   280  	}
   281  	return a
   282  }
   283  
   284  func d3(a [100]int) [100]int {
   285  	for i := 0; i <= 99; i++ { // ERROR "Induction variable: limits \[0,99\], increment 1$"
   286  		for j := 0; j <= i-1; j++ {
   287  			a[j] = 0
   288  			a[j+1] = 0 // ERROR "Proved IsInBounds$"
   289  			a[j+2] = 0
   290  		}
   291  	}
   292  	return a
   293  }
   294  
   295  func d4() {
   296  	for i := int64(math.MaxInt64 - 9); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775798,9223372036854775805\), increment 4$"
   297  		useString("foo")
   298  	}
   299  	for i := int64(math.MaxInt64 - 8); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775799,9223372036854775805\), increment 4$"
   300  		useString("foo")
   301  	}
   302  	for i := int64(math.MaxInt64 - 7); i < math.MaxInt64-2; i += 4 {
   303  		useString("foo")
   304  	}
   305  	for i := int64(math.MaxInt64 - 6); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775801,9223372036854775805\), increment 4$"
   306  		useString("foo")
   307  	}
   308  	for i := int64(math.MaxInt64 - 9); i <= math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775798,9223372036854775805\], increment 4$"
   309  		useString("foo")
   310  	}
   311  	for i := int64(math.MaxInt64 - 8); i <= math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775799,9223372036854775805\], increment 4$"
   312  		useString("foo")
   313  	}
   314  	for i := int64(math.MaxInt64 - 7); i <= math.MaxInt64-2; i += 4 {
   315  		useString("foo")
   316  	}
   317  	for i := int64(math.MaxInt64 - 6); i <= math.MaxInt64-2; i += 4 {
   318  		useString("foo")
   319  	}
   320  }
   321  
   322  func d5() {
   323  	for i := int64(math.MinInt64 + 9); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \(-9223372036854775806,-9223372036854775799\], increment 4"
   324  		useString("foo")
   325  	}
   326  	for i := int64(math.MinInt64 + 8); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \(-9223372036854775806,-9223372036854775800\], increment 4"
   327  		useString("foo")
   328  	}
   329  	for i := int64(math.MinInt64 + 7); i > math.MinInt64+2; i -= 4 {
   330  		useString("foo")
   331  	}
   332  	for i := int64(math.MinInt64 + 6); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \(-9223372036854775806,-9223372036854775802\], increment 4"
   333  		useString("foo")
   334  	}
   335  	for i := int64(math.MinInt64 + 9); i >= math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775806,-9223372036854775799\], increment 4"
   336  		useString("foo")
   337  	}
   338  	for i := int64(math.MinInt64 + 8); i >= math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775806,-9223372036854775800\], increment 4"
   339  		useString("foo")
   340  	}
   341  	for i := int64(math.MinInt64 + 7); i >= math.MinInt64+2; i -= 4 {
   342  		useString("foo")
   343  	}
   344  	for i := int64(math.MinInt64 + 6); i >= math.MinInt64+2; i -= 4 {
   345  		useString("foo")
   346  	}
   347  }
   348  
   349  func bce1() {
   350  	// tests overflow of max-min
   351  	a := int64(9223372036854774057)
   352  	b := int64(-1547)
   353  	z := int64(1337)
   354  
   355  	if a%z == b%z {
   356  		panic("invalid test: modulos should differ")
   357  	}
   358  
   359  	for i := b; i < a; i += z { // ERROR "Induction variable: limits \[-1547,9223372036854774057\), increment 1337"
   360  		useString("foobar")
   361  	}
   362  }
   363  
   364  func nobce2(a string) {
   365  	for i := int64(0); i < int64(len(a)); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   366  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   367  	}
   368  	for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   369  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   370  	}
   371  	for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   372  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   373  	}
   374  	j := int64(len(a)) - 123
   375  	for i := int64(0); i < j+123+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   376  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   377  	}
   378  	for i := int64(0); i < j+122+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   379  		// len(a)-123+122+MinInt overflows when len(a) == 0, so a bound check is needed here
   380  		useString(a[i:])
   381  	}
   382  }
   383  
   384  func nobce3(a [100]int64) [100]int64 {
   385  	min := int64((-1) << 63)
   386  	max := int64((1 << 63) - 1)
   387  	for i := min; i < max; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,9223372036854775807\), increment 1$"
   388  		a[i] = i
   389  	}
   390  	return a
   391  }
   392  
   393  func issue26116a(a []int) {
   394  	// There is no induction variable here. The comparison is in the wrong direction.
   395  	for i := 3; i > 6; i++ {
   396  		a[i] = 0
   397  	}
   398  	for i := 7; i < 3; i-- {
   399  		a[i] = 1
   400  	}
   401  }
   402  
   403  //go:noinline
   404  func useString(a string) {
   405  }
   406  
   407  //go:noinline
   408  func useSlice(a []int) {
   409  }
   410  
   411  func main() {
   412  }
   413  

View as plain text