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  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  	// Note: can't use (-1)<<63 here, because i-min doesn't get rewritten to i+(-min),
   298  	// and it isn't worth adding that special case to prove.
   299  	min := (-1)<<63 + 1
   300  	for i := min; i < min+50; i++ { // ERROR "Induction variable: limits \[-9223372036854775807,-9223372036854775757\), increment 1$"
   301  		a[i-min] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   302  	}
   303  	return a
   304  }
   305  
   306  func k5(a [100]int) [100]int {
   307  	max := (1 << 63) - 1
   308  	for i := max - 50; i < max; i++ { // ERROR "Induction variable: limits \[9223372036854775757,9223372036854775807\), increment 1$"
   309  		a[i-max+50] = i   // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   310  		a[i-(max-70)] = i // ERROR "(\([0-9]+\) )?Proved IsInBounds$"
   311  	}
   312  	return a
   313  }
   314  
   315  func d1(a [100]int) [100]int {
   316  	for i := 0; i < 100; i++ { // ERROR "Induction variable: limits \[0,100\), increment 1$"
   317  		for j := 0; j < i; j++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   318  			a[j] = 0   // ERROR "Proved IsInBounds$"
   319  			a[j+1] = 0 // ERROR "Proved IsInBounds$"
   320  			a[j+2] = 0
   321  		}
   322  	}
   323  	return a
   324  }
   325  
   326  func d2(a [100]int) [100]int {
   327  	for i := 0; i < 100; i++ { // ERROR "Induction variable: limits \[0,100\), increment 1$"
   328  		for j := 0; i > j; j++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   329  			a[j] = 0   // ERROR "Proved IsInBounds$"
   330  			a[j+1] = 0 // ERROR "Proved IsInBounds$"
   331  			a[j+2] = 0
   332  		}
   333  	}
   334  	return a
   335  }
   336  
   337  func d3(a [100]int) [100]int {
   338  	for i := 0; i <= 99; i++ { // ERROR "Induction variable: limits \[0,99\], increment 1$"
   339  		for j := 0; j <= i-1; j++ {
   340  			a[j] = 0
   341  			a[j+1] = 0 // ERROR "Proved IsInBounds$"
   342  			a[j+2] = 0
   343  		}
   344  	}
   345  	return a
   346  }
   347  
   348  func d4() {
   349  	for i := int64(math.MaxInt64 - 9); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775798,9223372036854775802\], increment 4$"
   350  		useString("foo")
   351  	}
   352  	for i := int64(math.MaxInt64 - 8); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775799,9223372036854775803\], increment 4$"
   353  		useString("foo")
   354  	}
   355  	for i := int64(math.MaxInt64 - 7); i < math.MaxInt64-2; i += 4 {
   356  		useString("foo")
   357  	}
   358  	for i := int64(math.MaxInt64 - 6); i < math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775801,9223372036854775801\], increment 4$"
   359  		useString("foo")
   360  	}
   361  	for i := int64(math.MaxInt64 - 9); i <= math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775798,9223372036854775802\], increment 4$"
   362  		useString("foo")
   363  	}
   364  	for i := int64(math.MaxInt64 - 8); i <= math.MaxInt64-2; i += 4 { // ERROR "Induction variable: limits \[9223372036854775799,9223372036854775803\], increment 4$"
   365  		useString("foo")
   366  	}
   367  	for i := int64(math.MaxInt64 - 7); i <= math.MaxInt64-2; i += 4 {
   368  		useString("foo")
   369  	}
   370  	for i := int64(math.MaxInt64 - 6); i <= math.MaxInt64-2; i += 4 {
   371  		useString("foo")
   372  	}
   373  }
   374  
   375  func d5() {
   376  	for i := int64(math.MinInt64 + 9); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775803,-9223372036854775799\], increment 4"
   377  		useString("foo")
   378  	}
   379  	for i := int64(math.MinInt64 + 8); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775804,-9223372036854775800\], increment 4"
   380  		useString("foo")
   381  	}
   382  	for i := int64(math.MinInt64 + 7); i > math.MinInt64+2; i -= 4 {
   383  		useString("foo")
   384  	}
   385  	for i := int64(math.MinInt64 + 6); i > math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775802,-9223372036854775802\], increment 4"
   386  		useString("foo")
   387  	}
   388  	for i := int64(math.MinInt64 + 9); i >= math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775803,-9223372036854775799\], increment 4"
   389  		useString("foo")
   390  	}
   391  	for i := int64(math.MinInt64 + 8); i >= math.MinInt64+2; i -= 4 { // ERROR "Induction variable: limits \[-9223372036854775804,-9223372036854775800\], increment 4"
   392  		useString("foo")
   393  	}
   394  	for i := int64(math.MinInt64 + 7); i >= math.MinInt64+2; i -= 4 {
   395  		useString("foo")
   396  	}
   397  	for i := int64(math.MinInt64 + 6); i >= math.MinInt64+2; i -= 4 {
   398  		useString("foo")
   399  	}
   400  }
   401  
   402  func bce1() {
   403  	// tests overflow of max-min
   404  	a := int64(9223372036854774057)
   405  	b := int64(-1547)
   406  	z := int64(1337)
   407  
   408  	if a%z == b%z {
   409  		panic("invalid test: modulos should differ")
   410  	}
   411  
   412  	for i := b; i < a; i += z { // ERROR "Induction variable: limits \[-1547,9223372036854772720\], increment 1337"
   413  		useString("foobar")
   414  	}
   415  }
   416  
   417  func nobce2(a string) {
   418  	for i := int64(0); i < int64(len(a)); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   419  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   420  	}
   421  	for i := int64(0); i < int64(len(a))-31337; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   422  		useString(a[i:]) // ERROR "(\([0-9]+\) )?Proved IsSliceInBounds$"
   423  	}
   424  	for i := int64(0); i < int64(len(a))+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Disproved Less64"
   425  		useString(a[i:])
   426  	}
   427  	j := int64(len(a)) - 123
   428  	for i := int64(0); i < j+123+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Disproved Less64"
   429  		useString(a[i:])
   430  	}
   431  	for i := int64(0); i < j+122+int64(-1<<63); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   432  		// len(a)-123+122+MinInt overflows when len(a) == 0, so a bound check is needed here
   433  		useString(a[i:])
   434  	}
   435  }
   436  
   437  func nobce3(a [100]int64) [100]int64 {
   438  	min := int64((-1) << 63)
   439  	max := int64((1 << 63) - 1)
   440  	for i := min; i < max; i++ { // ERROR "Induction variable: limits \[-9223372036854775808,9223372036854775807\), increment 1$"
   441  	}
   442  	return a
   443  }
   444  
   445  func issue26116a(a []int) {
   446  	// There is no induction variable here. The comparison is in the wrong direction.
   447  	for i := 3; i > 6; i++ {
   448  		a[i] = 0
   449  	}
   450  	for i := 7; i < 3; i-- {
   451  		a[i] = 1
   452  	}
   453  }
   454  
   455  func stride1(x *[7]int) int {
   456  	s := 0
   457  	for i := 0; i <= 8; i += 3 { // ERROR "Induction variable: limits \[0,6\], increment 3"
   458  		s += x[i] // ERROR "Proved IsInBounds"
   459  	}
   460  	return s
   461  }
   462  
   463  func stride2(x *[7]int) int {
   464  	s := 0
   465  	for i := 0; i < 9; i += 3 { // ERROR "Induction variable: limits \[0,6\], increment 3"
   466  		s += x[i] // ERROR "Proved IsInBounds"
   467  	}
   468  	return s
   469  }
   470  
   471  //go:noinline
   472  func useString(a string) {
   473  }
   474  
   475  //go:noinline
   476  func useSlice(a []int) {
   477  }
   478  
   479  func main() {
   480  }
   481  

View as plain text