Source file 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$"
    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])
   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$"
   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 d1(a [100]int) [100]int {
   261  	for i := 0; i < 100; i++ { // ERROR "Induction variable: limits \[0,100\), increment 1$"
   262  		for j := 0; j < i; j++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   263  			a[j] = 0   // ERROR "Proved IsInBounds$"
   264  			a[j+1] = 0 // FIXME: this boundcheck should be eliminated
   265  			a[j+2] = 0
   266  		}
   267  	}
   268  	return a
   269  }
   270  
   271  func d2(a [100]int) [100]int {
   272  	for i := 0; i < 100; i++ { // ERROR "Induction variable: limits \[0,100\), increment 1$"
   273  		for j := 0; i > j; j++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   274  			a[j] = 0   // ERROR "Proved IsInBounds$"
   275  			a[j+1] = 0 // FIXME: this boundcheck should be eliminated
   276  			a[j+2] = 0
   277  		}
   278  	}
   279  	return a
   280  }
   281  
   282  func d3(a [100]int) [100]int {
   283  	for i := 0; i <= 99; i++ { // ERROR "Induction variable: limits \[0,99\], increment 1$"
   284  		for j := 0; j <= i-1; j++ { // ERROR "Induction variable: limits \[0,\?\], increment 1$"
   285  			a[j] = 0   // ERROR "Proved IsInBounds$"
   286  			a[j+1] = 0 // ERROR "Proved IsInBounds$"
   287  			a[j+2] = 0
   288  		}
   289  	}
   290  	return a
   291  }
   292  
   293  func nobce1() {
   294  	// tests overflow of max-min
   295  	a := int64(9223372036854774057)
   296  	b := int64(-1547)
   297  	z := int64(1337)
   298  
   299  	if a%z == b%z {
   300  		panic("invalid test: modulos should differ")
   301  	}
   302  
   303  	for i := b; i < a; i += z {
   304  		// No induction variable is possible because i will overflow a first iteration.
   305  		useString("foobar")
   306  	}
   307  }
   308  
   309  func nobce2(a string) {
   310  	for i := int64(0); i < int64(len(a)); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   311  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   312  	}
   313  	for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   314  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   315  	}
   316  	for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   317  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   318  	}
   319  	j := int64(len(a)) - 123
   320  	for i := int64(0); i < j+123+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   321  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   322  	}
   323  	for i := int64(0); i < j+122+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   324  		// len(a)-123+122+MinInt overflows when len(a) == 0, so a bound check is needed here
   325  		useString(a[i:])
   326  	}
   327  }
   328  
   329  func nobce3(a [100]int64) [100]int64 {
   330  	min := int64((-1) << 63)
   331  	max := int64((1 << 63) - 1)
   332  	for i := min; i < max; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,9223372036854775807\), increment 1$"
   333  		a[i] = i
   334  	}
   335  	return a
   336  }
   337  
   338  func issue26116a(a []int) {
   339  	// There is no induction variable here. The comparison is in the wrong direction.
   340  	for i := 3; i > 6; i++ {
   341  		a[i] = 0
   342  	}
   343  	for i := 7; i < 3; i-- {
   344  		a[i] = 1
   345  	}
   346  }
   347  
   348  //go:noinline
   349  func useString(a string) {
   350  }
   351  
   352  //go:noinline
   353  func useSlice(a []int) {
   354  }
   355  
   356  func main() {
   357  }
   358  

View as plain text