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]    // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
    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  //go:noinline
    92  func f6(a []int) {
    93  	for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
    94  		b := a[0:i] // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
    95  		f6(b)
    96  	}
    97  }
    98  
    99  func g0a(a string) int {
   100  	x := 0
   101  	for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   102  		x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   103  	}
   104  	return x
   105  }
   106  
   107  func g0b(a string) int {
   108  	x := 0
   109  	for i := 0; len(a) > i; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   110  		x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   111  	}
   112  	return x
   113  }
   114  
   115  func g0c(a string) int {
   116  	x := 0
   117  	for i := len(a); i > 0; i-- { // ERROR "Induction variable: limits \(0,\?\], increment 1$"
   118  		x += int(a[i-1]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   119  	}
   120  	return x
   121  }
   122  
   123  func g0d(a string) int {
   124  	x := 0
   125  	for i := len(a); 0 < i; i-- { // ERROR "Induction variable: limits \(0,\?\], increment 1$"
   126  		x += int(a[i-1]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   127  	}
   128  	return x
   129  }
   130  
   131  func g0e(a string) int {
   132  	x := 0
   133  	for i := len(a) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1$"
   134  		x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   135  	}
   136  	return x
   137  }
   138  
   139  func g0f(a string) int {
   140  	x := 0
   141  	for i := len(a) - 1; 0 <= i; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1$"
   142  		x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   143  	}
   144  	return x
   145  }
   146  
   147  func g1() int {
   148  	a := "evenlength"
   149  	x := 0
   150  	for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,8\], increment 2$"
   151  		x += int(a[i]) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   152  	}
   153  	return x
   154  }
   155  
   156  func g2() int {
   157  	a := "evenlength"
   158  	x := 0
   159  	for i := 0; i < len(a); i += 2 { // ERROR "Induction variable: limits \[0,8\], increment 2$"
   160  		j := i
   161  		if a[i] == 'e' { // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   162  			j = j + 1
   163  		}
   164  		x += int(a[j])
   165  	}
   166  	return x
   167  }
   168  
   169  func g3a() {
   170  	a := "this string has length 25"
   171  	for i := 0; i < len(a); i += 5 { // ERROR "Induction variable: limits \[0,20\], increment 5$"
   172  		useString(a[i:])   // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   173  		useString(a[:i+3]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   174  		useString(a[:i+5]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   175  		useString(a[:i+6])
   176  	}
   177  }
   178  
   179  func g3b(a string) {
   180  	for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   181  		useString(a[i+1:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   182  	}
   183  }
   184  
   185  func g3c(a string) {
   186  	for i := 0; i < len(a); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   187  		useString(a[:i+1]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   188  	}
   189  }
   190  
   191  func h1(a []byte) {
   192  	c := a[:128]
   193  	for i := range c { // ERROR "Induction variable: limits \[0,128\), increment 1$"
   194  		c[i] = byte(i) // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   195  	}
   196  }
   197  
   198  func h2(a []byte) {
   199  	for i := range a[:128] { // ERROR "Induction variable: limits \[0,128\), increment 1$"
   200  		a[i] = byte(i)
   201  	}
   202  }
   203  
   204  func k0(a [100]int) [100]int {
   205  	for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
   206  		if a[0] == 0xdeadbeef {
   207  			// This is a trick to prohibit sccp to optimize out the following out of bound check
   208  			continue
   209  		}
   210  		a[i-11] = i
   211  		a[i-10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   212  		a[i-5] = i  // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   213  		a[i] = i    // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   214  		a[i+5] = i  // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   215  		a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   216  		a[i+11] = i
   217  	}
   218  	return a
   219  }
   220  
   221  func k1(a [100]int) [100]int {
   222  	for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
   223  		if a[0] == 0xdeadbeef {
   224  			// This is a trick to prohibit sccp to optimize out the following out of bound check
   225  			continue
   226  		}
   227  		useSlice(a[:i-11])
   228  		useSlice(a[:i-10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   229  		useSlice(a[:i-5])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   230  		useSlice(a[:i])    // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   231  		useSlice(a[:i+5])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   232  		useSlice(a[:i+10]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   233  		useSlice(a[:i+11]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   234  		useSlice(a[:i+12])
   235  
   236  	}
   237  	return a
   238  }
   239  
   240  func k2(a [100]int) [100]int {
   241  	for i := 10; i < 90; i++ { // ERROR "Induction variable: limits \[10,90\), increment 1$"
   242  		if a[0] == 0xdeadbeef {
   243  			// This is a trick to prohibit sccp to optimize out the following out of bound check
   244  			continue
   245  		}
   246  		useSlice(a[i-11:])
   247  		useSlice(a[i-10:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   248  		useSlice(a[i-5:])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   249  		useSlice(a[i:])    // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   250  		useSlice(a[i+5:])  // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   251  		useSlice(a[i+10:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   252  		useSlice(a[i+11:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   253  		useSlice(a[i+12:])
   254  	}
   255  	return a
   256  }
   257  
   258  func k3(a [100]int) [100]int {
   259  	for i := -10; i < 90; i++ { // ERROR "Induction variable: limits \[-10,90\), increment 1$"
   260  		if a[0] == 0xdeadbeef {
   261  			// This is a trick to prohibit sccp to optimize out the following out of bound check
   262  			continue
   263  		}
   264  		a[i+9] = i
   265  		a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   266  		a[i+11] = i
   267  	}
   268  	return a
   269  }
   270  
   271  func k3neg(a [100]int) [100]int {
   272  	for i := 89; i > -11; i-- { // ERROR "Induction variable: limits \(-11,89\], increment 1$"
   273  		if a[0] == 0xdeadbeef {
   274  			// This is a trick to prohibit sccp to optimize out the following out of bound check
   275  			continue
   276  		}
   277  		a[i+9] = i
   278  		a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   279  		a[i+11] = i
   280  	}
   281  	return a
   282  }
   283  
   284  func k3neg2(a [100]int) [100]int {
   285  	for i := 89; i >= -10; i-- { // ERROR "Induction variable: limits \[-10,89\], increment 1$"
   286  		if a[0] == 0xdeadbeef {
   287  			// This is a trick to prohibit sccp to optimize out the following out of bound check
   288  			continue
   289  		}
   290  		a[i+9] = i
   291  		a[i+10] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   292  		a[i+11] = i
   293  	}
   294  	return a
   295  }
   296  
   297  func k4(a [100]int) [100]int {
   298  	// Note: can't use (-1)<<63 here, because i-min doesn't get rewritten to i+(-min),
   299  	// and it isn't worth adding that special case to prove.
   300  	min := (-1)<<63 + 1
   301  	for i := min; i < min+50; i++ { // ERROR "Induction variable: limits \[-9223372036854775807,-9223372036854775757\), increment 1$"
   302  		a[i-min] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   303  	}
   304  	return a
   305  }
   306  
   307  func k5(a [100]int) [100]int {
   308  	max := (1 << 63) - 1
   309  	for i := max - 50; i < max; i++ { // ERROR "Induction variable: limits \[9223372036854775757,9223372036854775807\), increment 1$"
   310  		a[i-max+50] = i   // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   311  		a[i-(max-70)] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   312  	}
   313  	return a
   314  }
   315  
   316  func d1(a [100]int) [100]int {
   317  	for i := 0; i < 100; i++ { // ERROR "Induction variable: limits \[0,100\), increment 1$"
   318  		for j := 0; j < i; j++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   319  			a[j] = 0   // ERROR "Proved IsInBounds$"
   320  			a[j+1] = 0 // ERROR "Proved IsInBounds$"
   321  			a[j+2] = 0
   322  		}
   323  	}
   324  	return a
   325  }
   326  
   327  func d2(a [100]int) [100]int {
   328  	for i := 0; i < 100; i++ { // ERROR "Induction variable: limits \[0,100\), increment 1$"
   329  		for j := 0; i > j; j++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   330  			a[j] = 0   // ERROR "Proved IsInBounds$"
   331  			a[j+1] = 0 // ERROR "Proved IsInBounds$"
   332  			a[j+2] = 0
   333  		}
   334  	}
   335  	return a
   336  }
   337  
   338  func d3(a [100]int) [100]int {
   339  	for i := 0; i <= 99; i++ { // ERROR "Induction variable: limits \[0,99\], increment 1$"
   340  		for j := 0; j <= i-1; j++ {
   341  			a[j] = 0
   342  			a[j+1] = 0 // ERROR "Proved IsInBounds$"
   343  			a[j+2] = 0
   344  		}
   345  	}
   346  	return a
   347  }
   348  
   349  func d4() {
   350  	for i := int64(math.MaxInt64 - 9); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775798,9223372036854775802\], increment 4$"
   351  		useString("foo")
   352  	}
   353  	for i := int64(math.MaxInt64 - 8); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775799,9223372036854775803\], increment 4$"
   354  		useString("foo")
   355  	}
   356  	for i := int64(math.MaxInt64 - 7); i < math.MaxInt64-2; i += 4 {
   357  		useString("foo")
   358  	}
   359  	for i := int64(math.MaxInt64 - 6); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775801,9223372036854775801\], increment 4$"
   360  		useString("foo")
   361  	}
   362  	for i := int64(math.MaxInt64 - 9); i <= math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775798,9223372036854775802\], increment 4$"
   363  		useString("foo")
   364  	}
   365  	for i := int64(math.MaxInt64 - 8); i <= math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775799,9223372036854775803\], increment 4$"
   366  		useString("foo")
   367  	}
   368  	for i := int64(math.MaxInt64 - 7); i <= math.MaxInt64-2; i += 4 {
   369  		useString("foo")
   370  	}
   371  	for i := int64(math.MaxInt64 - 6); i <= math.MaxInt64-2; i += 4 {
   372  		useString("foo")
   373  	}
   374  }
   375  
   376  func d5() {
   377  	for i := int64(math.MinInt64 + 9); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775803,-9223372036854775799\], increment 4"
   378  		useString("foo")
   379  	}
   380  	for i := int64(math.MinInt64 + 8); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775804,-9223372036854775800\], increment 4"
   381  		useString("foo")
   382  	}
   383  	for i := int64(math.MinInt64 + 7); i > math.MinInt64+2; i -= 4 {
   384  		useString("foo")
   385  	}
   386  	for i := int64(math.MinInt64 + 6); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775802,-9223372036854775802\], increment 4"
   387  		useString("foo")
   388  	}
   389  	for i := int64(math.MinInt64 + 9); i >= math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775803,-9223372036854775799\], increment 4"
   390  		useString("foo")
   391  	}
   392  	for i := int64(math.MinInt64 + 8); i >= math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775804,-9223372036854775800\], increment 4"
   393  		useString("foo")
   394  	}
   395  	for i := int64(math.MinInt64 + 7); i >= math.MinInt64+2; i -= 4 {
   396  		useString("foo")
   397  	}
   398  	for i := int64(math.MinInt64 + 6); i >= math.MinInt64+2; i -= 4 {
   399  		useString("foo")
   400  	}
   401  }
   402  
   403  func bce1() {
   404  	// tests overflow of max-min
   405  	a := int64(9223372036854774057)
   406  	b := int64(-1547)
   407  	z := int64(1337)
   408  
   409  	if a%z == b%z {
   410  		panic("invalid test: modulos should differ")
   411  	}
   412  
   413  	for i := b; i < a; i += z { // ERROR "Induction variable: limits \[-1547,9223372036854772720\], increment 1337"
   414  		useString("foobar")
   415  	}
   416  }
   417  
   418  func nobce2(a string) {
   419  	for i := int64(0); i < int64(len(a)); 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))-31337; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   423  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   424  	}
   425  	for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Disproved Less64"
   426  		useString(a[i:])
   427  	}
   428  	j := int64(len(a)) - 123
   429  	for i := int64(0); i < j+123+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Disproved Less64"
   430  		useString(a[i:])
   431  	}
   432  	for i := int64(0); i < j+122+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   433  		// len(a)-123+122+MinInt overflows when len(a) == 0, so a bound check is needed here
   434  		useString(a[i:])
   435  	}
   436  }
   437  
   438  func nobce3(a [100]int64) [100]int64 {
   439  	min := int64((-1) << 63)
   440  	max := int64((1 << 63) - 1)
   441  	for i := min; i < max; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,9223372036854775807\), increment 1$"
   442  	}
   443  	return a
   444  }
   445  
   446  func issue26116a(a []int) {
   447  	// There is no induction variable here. The comparison is in the wrong direction.
   448  	for i := 3; i > 6; i++ {
   449  		a[i] = 0
   450  	}
   451  	for i := 7; i < 3; i-- {
   452  		a[i] = 1
   453  	}
   454  }
   455  
   456  func stride1(x *[7]int) int {
   457  	s := 0
   458  	for i := 0; i <= 8; i += 3 { // ERROR "Induction variable: limits \[0,6\], increment 3"
   459  		s += x[i] // ERROR "Proved IsInBounds"
   460  	}
   461  	return s
   462  }
   463  
   464  func stride2(x *[7]int) int {
   465  	s := 0
   466  	for i := 0; i < 9; i += 3 { // ERROR "Induction variable: limits \[0,6\], increment 3"
   467  		s += x[i] // ERROR "Proved IsInBounds"
   468  	}
   469  	return s
   470  }
   471  
   472  //go:noinline
   473  func useString(a string) {
   474  }
   475  
   476  //go:noinline
   477  func useSlice(a []int) {
   478  }
   479  
   480  func main() {
   481  }
   482  

View as plain text