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

View as plain text