Source file test/loopbce.go

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

View as plain text