Source file test/prove.go

     1  // errorcheck -0 -d=ssa/prove/debug=1
     2  
     3  //go:build amd64
     4  
     5  // Copyright 2016 The Go Authors. All rights reserved.
     6  // Use of this source code is governed by a BSD-style
     7  // license that can be found in the LICENSE file.
     8  
     9  package main
    10  
    11  import "math"
    12  
    13  func f0(a []int) int {
    14  	a[0] = 1
    15  	a[0] = 1 // ERROR "Proved IsInBounds$"
    16  	a[6] = 1
    17  	a[6] = 1 // ERROR "Proved IsInBounds$"
    18  	a[5] = 1 // ERROR "Proved IsInBounds$"
    19  	a[5] = 1 // ERROR "Proved IsInBounds$"
    20  	return 13
    21  }
    22  
    23  func f1(a []int) int {
    24  	if len(a) <= 5 {
    25  		return 18
    26  	}
    27  	a[0] = 1 // ERROR "Proved IsInBounds$"
    28  	a[0] = 1 // ERROR "Proved IsInBounds$"
    29  	a[6] = 1
    30  	a[6] = 1 // ERROR "Proved IsInBounds$"
    31  	a[5] = 1 // ERROR "Proved IsInBounds$"
    32  	a[5] = 1 // ERROR "Proved IsInBounds$"
    33  	return 26
    34  }
    35  
    36  func f1b(a []int, i int, j uint) int {
    37  	if i >= 0 && i < len(a) {
    38  		return a[i] // ERROR "Proved IsInBounds$"
    39  	}
    40  	if i >= 10 && i < len(a) {
    41  		return a[i] // ERROR "Proved IsInBounds$"
    42  	}
    43  	if i >= 10 && i < len(a) {
    44  		return a[i] // ERROR "Proved IsInBounds$"
    45  	}
    46  	if i >= 10 && i < len(a) {
    47  		return a[i-10] // ERROR "Proved IsInBounds$"
    48  	}
    49  	if j < uint(len(a)) {
    50  		return a[j] // ERROR "Proved IsInBounds$"
    51  	}
    52  	return 0
    53  }
    54  
    55  func f1c(a []int, i int64) int {
    56  	c := uint64(math.MaxInt64 + 10) // overflows int
    57  	d := int64(c)
    58  	if i >= d && i < int64(len(a)) {
    59  		// d overflows, should not be handled.
    60  		return a[i]
    61  	}
    62  	return 0
    63  }
    64  
    65  func f2(a []int) int {
    66  	for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
    67  		a[i+1] = i
    68  		a[i+1] = i // ERROR "Proved IsInBounds$"
    69  	}
    70  	return 34
    71  }
    72  
    73  func f3(a []uint) int {
    74  	for i := uint(0); i < uint(len(a)); i++ {
    75  		a[i] = i // ERROR "Proved IsInBounds$"
    76  	}
    77  	return 41
    78  }
    79  
    80  func f4a(a, b, c int) int {
    81  	if a < b {
    82  		if a == b { // ERROR "Disproved Eq64$"
    83  			return 47
    84  		}
    85  		if a > b { // ERROR "Disproved Less64$"
    86  			return 50
    87  		}
    88  		if a < b { // ERROR "Proved Less64$"
    89  			return 53
    90  		}
    91  		// We can't get to this point and prove knows that, so
    92  		// there's no message for the next (obvious) branch.
    93  		if a != a {
    94  			return 56
    95  		}
    96  		return 61
    97  	}
    98  	return 63
    99  }
   100  
   101  func f4b(a, b, c int) int {
   102  	if a <= b {
   103  		if a >= b {
   104  			if a == b { // ERROR "Proved Eq64$"
   105  				return 70
   106  			}
   107  			return 75
   108  		}
   109  		return 77
   110  	}
   111  	return 79
   112  }
   113  
   114  func f4c(a, b, c int) int {
   115  	if a <= b {
   116  		if a >= b {
   117  			if a != b { // ERROR "Disproved Neq64$"
   118  				return 73
   119  			}
   120  			return 75
   121  		}
   122  		return 77
   123  	}
   124  	return 79
   125  }
   126  
   127  func f4d(a, b, c int) int {
   128  	if a < b {
   129  		if a < c {
   130  			if a < b { // ERROR "Proved Less64$"
   131  				if a < c { // ERROR "Proved Less64$"
   132  					return 87
   133  				}
   134  				return 89
   135  			}
   136  			return 91
   137  		}
   138  		return 93
   139  	}
   140  	return 95
   141  }
   142  
   143  func f4e(a, b, c int) int {
   144  	if a < b {
   145  		if b > a { // ERROR "Proved Less64$"
   146  			return 101
   147  		}
   148  		return 103
   149  	}
   150  	return 105
   151  }
   152  
   153  func f4f(a, b, c int) int {
   154  	if a <= b {
   155  		if b > a {
   156  			if b == a { // ERROR "Disproved Eq64$"
   157  				return 112
   158  			}
   159  			return 114
   160  		}
   161  		if b >= a { // ERROR "Proved Leq64$"
   162  			if b == a { // ERROR "Proved Eq64$"
   163  				return 118
   164  			}
   165  			return 120
   166  		}
   167  		return 122
   168  	}
   169  	return 124
   170  }
   171  
   172  func f5(a, b uint) int {
   173  	if a == b {
   174  		if a <= b { // ERROR "Proved Leq64U$"
   175  			return 130
   176  		}
   177  		return 132
   178  	}
   179  	return 134
   180  }
   181  
   182  // These comparisons are compile time constants.
   183  func f6a(a uint8) int {
   184  	if a < a { // ERROR "Disproved Less8U$"
   185  		return 140
   186  	}
   187  	return 151
   188  }
   189  
   190  func f6b(a uint8) int {
   191  	if a < a { // ERROR "Disproved Less8U$"
   192  		return 140
   193  	}
   194  	return 151
   195  }
   196  
   197  func f6x(a uint8) int {
   198  	if a > a { // ERROR "Disproved Less8U$"
   199  		return 143
   200  	}
   201  	return 151
   202  }
   203  
   204  func f6d(a uint8) int {
   205  	if a <= a { // ERROR "Proved Leq8U$"
   206  		return 146
   207  	}
   208  	return 151
   209  }
   210  
   211  func f6e(a uint8) int {
   212  	if a >= a { // ERROR "Proved Leq8U$"
   213  		return 149
   214  	}
   215  	return 151
   216  }
   217  
   218  func f7(a []int, b int) int {
   219  	if b < len(a) {
   220  		a[b] = 3
   221  		if b < len(a) { // ERROR "Proved Less64$"
   222  			a[b] = 5 // ERROR "Proved IsInBounds$"
   223  		}
   224  	}
   225  	return 161
   226  }
   227  
   228  func f8(a, b uint) int {
   229  	if a == b {
   230  		return 166
   231  	}
   232  	if a > b {
   233  		return 169
   234  	}
   235  	if a < b { // ERROR "Proved Less64U$"
   236  		return 172
   237  	}
   238  	return 174
   239  }
   240  
   241  func f9(a, b bool) int {
   242  	if a {
   243  		return 1
   244  	}
   245  	if a || b { // ERROR "Disproved Arg$"
   246  		return 2
   247  	}
   248  	return 3
   249  }
   250  
   251  func f10(a string) int {
   252  	n := len(a)
   253  	// We optimize comparisons with small constant strings (see cmd/compile/internal/gc/walk.go),
   254  	// so this string literal must be long.
   255  	if a[:n>>1] == "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" {
   256  		return 0
   257  	}
   258  	return 1
   259  }
   260  
   261  func f11a(a []int, i int) {
   262  	useInt(a[i])
   263  	useInt(a[i]) // ERROR "Proved IsInBounds$"
   264  }
   265  
   266  func f11b(a []int, i int) {
   267  	useSlice(a[i:])
   268  	useSlice(a[i:]) // ERROR "Proved IsSliceInBounds$"
   269  }
   270  
   271  func f11c(a []int, i int) {
   272  	useSlice(a[:i])
   273  	useSlice(a[:i]) // ERROR "Proved IsSliceInBounds$"
   274  }
   275  
   276  func f11d(a []int, i int) {
   277  	useInt(a[2*i+7])
   278  	useInt(a[2*i+7]) // ERROR "Proved IsInBounds$"
   279  }
   280  
   281  func f12(a []int, b int) {
   282  	useSlice(a[:b])
   283  }
   284  
   285  func f13a(a, b, c int, x bool) int {
   286  	if a > 12 {
   287  		if x {
   288  			if a < 12 { // ERROR "Disproved Less64$"
   289  				return 1
   290  			}
   291  		}
   292  		if x {
   293  			if a <= 12 { // ERROR "Disproved Leq64$"
   294  				return 2
   295  			}
   296  		}
   297  		if x {
   298  			if a == 12 { // ERROR "Disproved Eq64$"
   299  				return 3
   300  			}
   301  		}
   302  		if x {
   303  			if a >= 12 { // ERROR "Proved Leq64$"
   304  				return 4
   305  			}
   306  		}
   307  		if x {
   308  			if a > 12 { // ERROR "Proved Less64$"
   309  				return 5
   310  			}
   311  		}
   312  		return 6
   313  	}
   314  	return 0
   315  }
   316  
   317  func f13b(a int, x bool) int {
   318  	if a == -9 {
   319  		if x {
   320  			if a < -9 { // ERROR "Disproved Less64$"
   321  				return 7
   322  			}
   323  		}
   324  		if x {
   325  			if a <= -9 { // ERROR "Proved Leq64$"
   326  				return 8
   327  			}
   328  		}
   329  		if x {
   330  			if a == -9 { // ERROR "Proved Eq64$"
   331  				return 9
   332  			}
   333  		}
   334  		if x {
   335  			if a >= -9 { // ERROR "Proved Leq64$"
   336  				return 10
   337  			}
   338  		}
   339  		if x {
   340  			if a > -9 { // ERROR "Disproved Less64$"
   341  				return 11
   342  			}
   343  		}
   344  		return 12
   345  	}
   346  	return 0
   347  }
   348  
   349  func f13c(a int, x bool) int {
   350  	if a < 90 {
   351  		if x {
   352  			if a < 90 { // ERROR "Proved Less64$"
   353  				return 13
   354  			}
   355  		}
   356  		if x {
   357  			if a <= 90 { // ERROR "Proved Leq64$"
   358  				return 14
   359  			}
   360  		}
   361  		if x {
   362  			if a == 90 { // ERROR "Disproved Eq64$"
   363  				return 15
   364  			}
   365  		}
   366  		if x {
   367  			if a >= 90 { // ERROR "Disproved Leq64$"
   368  				return 16
   369  			}
   370  		}
   371  		if x {
   372  			if a > 90 { // ERROR "Disproved Less64$"
   373  				return 17
   374  			}
   375  		}
   376  		return 18
   377  	}
   378  	return 0
   379  }
   380  
   381  func f13d(a int) int {
   382  	if a < 5 {
   383  		if a < 9 { // ERROR "Proved Less64$"
   384  			return 1
   385  		}
   386  	}
   387  	return 0
   388  }
   389  
   390  func f13e(a int) int {
   391  	if a > 9 {
   392  		if a > 5 { // ERROR "Proved Less64$"
   393  			return 1
   394  		}
   395  	}
   396  	return 0
   397  }
   398  
   399  func f13f(a, b int64) int64 {
   400  	if b != math.MaxInt64 {
   401  		return 42
   402  	}
   403  	if a > b {
   404  		if a == 0 { // ERROR "Disproved Eq64$"
   405  			return 1
   406  		}
   407  	}
   408  	return 0
   409  }
   410  
   411  func f13g(a int) int {
   412  	if a < 3 {
   413  		return 5
   414  	}
   415  	if a > 3 {
   416  		return 6
   417  	}
   418  	if a == 3 { // ERROR "Proved Eq64$"
   419  		return 7
   420  	}
   421  	return 8
   422  }
   423  
   424  func f13h(a int) int {
   425  	if a < 3 {
   426  		if a > 1 {
   427  			if a == 2 { // ERROR "Proved Eq64$"
   428  				return 5
   429  			}
   430  		}
   431  	}
   432  	return 0
   433  }
   434  
   435  func f13i(a uint) int {
   436  	if a == 0 {
   437  		return 1
   438  	}
   439  	if a > 0 { // ERROR "Proved Less64U$"
   440  		return 2
   441  	}
   442  	return 3
   443  }
   444  
   445  func f14(p, q *int, a []int) {
   446  	// This crazy ordering usually gives i1 the lowest value ID,
   447  	// j the middle value ID, and i2 the highest value ID.
   448  	// That used to confuse CSE because it ordered the args
   449  	// of the two + ops below differently.
   450  	// That in turn foiled bounds check elimination.
   451  	i1 := *p
   452  	j := *q
   453  	i2 := *p
   454  	useInt(a[i1+j])
   455  	useInt(a[i2+j]) // ERROR "Proved IsInBounds$"
   456  }
   457  
   458  func f15(s []int, x int) {
   459  	useSlice(s[x:])
   460  	useSlice(s[:x]) // ERROR "Proved IsSliceInBounds$"
   461  }
   462  
   463  func f16(s []int) []int {
   464  	if len(s) >= 10 {
   465  		return s[:10] // ERROR "Proved IsSliceInBounds$"
   466  	}
   467  	return nil
   468  }
   469  
   470  func f17(b []int) {
   471  	for i := 0; i < len(b); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   472  		// This tests for i <= cap, which we can only prove
   473  		// using the derived relation between len and cap.
   474  		// This depends on finding the contradiction, since we
   475  		// don't query this condition directly.
   476  		useSlice(b[:i]) // ERROR "Proved IsSliceInBounds$"
   477  	}
   478  }
   479  
   480  func f18(b []int, x int, y uint) {
   481  	_ = b[x]
   482  	_ = b[y]
   483  
   484  	if x > len(b) { // ERROR "Disproved Less64$"
   485  		return
   486  	}
   487  	if y > uint(len(b)) { // ERROR "Disproved Less64U$"
   488  		return
   489  	}
   490  	if int(y) > len(b) { // ERROR "Disproved Less64$"
   491  		return
   492  	}
   493  }
   494  
   495  func f19() (e int64, err error) {
   496  	// Issue 29502: slice[:0] is incorrectly disproved.
   497  	var stack []int64
   498  	stack = append(stack, 123)
   499  	if len(stack) > 1 {
   500  		panic("too many elements")
   501  	}
   502  	last := len(stack) - 1
   503  	e = stack[last]
   504  	// Buggy compiler prints "Disproved Leq64" for the next line.
   505  	stack = stack[:last]
   506  	return e, nil
   507  }
   508  
   509  func sm1(b []int, x int) {
   510  	// Test constant argument to slicemask.
   511  	useSlice(b[2:8]) // ERROR "Proved slicemask not needed$"
   512  	// Test non-constant argument with known limits.
   513  	if cap(b) > 10 {
   514  		useSlice(b[2:])
   515  	}
   516  }
   517  
   518  func lim1(x, y, z int) {
   519  	// Test relations between signed and unsigned limits.
   520  	if x > 5 {
   521  		if uint(x) > 5 { // ERROR "Proved Less64U$"
   522  			return
   523  		}
   524  	}
   525  	if y >= 0 && y < 4 {
   526  		if uint(y) > 4 { // ERROR "Disproved Less64U$"
   527  			return
   528  		}
   529  		if uint(y) < 5 { // ERROR "Proved Less64U$"
   530  			return
   531  		}
   532  	}
   533  	if z < 4 {
   534  		if uint(z) > 4 { // Not provable without disjunctions.
   535  			return
   536  		}
   537  	}
   538  }
   539  
   540  // fence1–4 correspond to the four fence-post implications.
   541  
   542  func fence1(b []int, x, y int) {
   543  	// Test proofs that rely on fence-post implications.
   544  	if x+1 > y {
   545  		if x < y { // ERROR "Disproved Less64$"
   546  			return
   547  		}
   548  	}
   549  	if len(b) < cap(b) {
   550  		// This eliminates the growslice path.
   551  		b = append(b, 1) // ERROR "Disproved Less64U$"
   552  	}
   553  }
   554  
   555  func fence2(x, y int) {
   556  	if x-1 < y {
   557  		if x > y { // ERROR "Disproved Less64$"
   558  			return
   559  		}
   560  	}
   561  }
   562  
   563  func fence3(b, c []int, x, y int64) {
   564  	if x-1 >= y {
   565  		if x <= y { // Can't prove because x may have wrapped.
   566  			return
   567  		}
   568  	}
   569  
   570  	if x != math.MinInt64 && x-1 >= y {
   571  		if x <= y { // ERROR "Disproved Leq64$"
   572  			return
   573  		}
   574  	}
   575  
   576  	c[len(c)-1] = 0 // Can't prove because len(c) might be 0
   577  
   578  	if n := len(b); n > 0 {
   579  		b[n-1] = 0 // ERROR "Proved IsInBounds$"
   580  	}
   581  }
   582  
   583  func fence4(x, y int64) {
   584  	if x >= y+1 {
   585  		if x <= y {
   586  			return
   587  		}
   588  	}
   589  	if y != math.MaxInt64 && x >= y+1 {
   590  		if x <= y { // ERROR "Disproved Leq64$"
   591  			return
   592  		}
   593  	}
   594  }
   595  
   596  // Check transitive relations
   597  func trans1(x, y int64) {
   598  	if x > 5 {
   599  		if y > x {
   600  			if y > 2 { // ERROR "Proved Less64$"
   601  				return
   602  			}
   603  		} else if y == x {
   604  			if y > 5 { // ERROR "Proved Less64$"
   605  				return
   606  			}
   607  		}
   608  	}
   609  	if x >= 10 {
   610  		if y > x {
   611  			if y > 10 { // ERROR "Proved Less64$"
   612  				return
   613  			}
   614  		}
   615  	}
   616  }
   617  
   618  func trans2(a, b []int, i int) {
   619  	if len(a) != len(b) {
   620  		return
   621  	}
   622  
   623  	_ = a[i]
   624  	_ = b[i] // ERROR "Proved IsInBounds$"
   625  }
   626  
   627  func trans3(a, b []int, i int) {
   628  	if len(a) > len(b) {
   629  		return
   630  	}
   631  
   632  	_ = a[i]
   633  	_ = b[i] // ERROR "Proved IsInBounds$"
   634  }
   635  
   636  func trans4(b []byte, x int) {
   637  	// Issue #42603: slice len/cap transitive relations.
   638  	switch x {
   639  	case 0:
   640  		if len(b) < 20 {
   641  			return
   642  		}
   643  		_ = b[:2] // ERROR "Proved IsSliceInBounds$"
   644  	case 1:
   645  		if len(b) < 40 {
   646  			return
   647  		}
   648  		_ = b[:2] // ERROR "Proved IsSliceInBounds$"
   649  	}
   650  }
   651  
   652  // Derived from nat.cmp
   653  func natcmp(x, y []uint) (r int) {
   654  	m := len(x)
   655  	n := len(y)
   656  	if m != n || m == 0 {
   657  		return
   658  	}
   659  
   660  	i := m - 1
   661  	for i > 0 && // ERROR "Induction variable: limits \(0,\?\], increment 1$"
   662  		x[i] == // ERROR "Proved IsInBounds$"
   663  			y[i] { // ERROR "Proved IsInBounds$"
   664  		i--
   665  	}
   666  
   667  	switch {
   668  	case x[i] < // todo, cannot prove this because it's dominated by i<=0 || x[i]==y[i]
   669  		y[i]: // ERROR "Proved IsInBounds$"
   670  		r = -1
   671  	case x[i] > // ERROR "Proved IsInBounds$"
   672  		y[i]: // ERROR "Proved IsInBounds$"
   673  		r = 1
   674  	}
   675  	return
   676  }
   677  
   678  func suffix(s, suffix string) bool {
   679  	// todo, we're still not able to drop the bound check here in the general case
   680  	return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
   681  }
   682  
   683  func constsuffix(s string) bool {
   684  	return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$"
   685  }
   686  
   687  // oforuntil tests the pattern created by OFORUNTIL blocks. These are
   688  // handled by addLocalInductiveFacts rather than findIndVar.
   689  func oforuntil(b []int) {
   690  	i := 0
   691  	if len(b) > i {
   692  	top:
   693  		println(b[i]) // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Proved IsInBounds$"
   694  		i++
   695  		if i < len(b) {
   696  			goto top
   697  		}
   698  	}
   699  }
   700  
   701  func atexit(foobar []func()) {
   702  	for i := len(foobar) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1"
   703  		f := foobar[i]
   704  		foobar = foobar[:i] // ERROR "IsSliceInBounds"
   705  		f()
   706  	}
   707  }
   708  
   709  func make1(n int) []int {
   710  	s := make([]int, n)
   711  	for i := 0; i < n; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1"
   712  		s[i] = 1 // ERROR "Proved IsInBounds$"
   713  	}
   714  	return s
   715  }
   716  
   717  func make2(n int) []int {
   718  	s := make([]int, n)
   719  	for i := range s { // ERROR "Induction variable: limits \[0,\?\), increment 1"
   720  		s[i] = 1 // ERROR "Proved IsInBounds$"
   721  	}
   722  	return s
   723  }
   724  
   725  // The range tests below test the index variable of range loops.
   726  
   727  // range1 compiles to the "efficiently indexable" form of a range loop.
   728  func range1(b []int) {
   729  	for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   730  		b[i] = v + 1    // ERROR "Proved IsInBounds$"
   731  		if i < len(b) { // ERROR "Proved Less64$"
   732  			println("x")
   733  		}
   734  		if i >= 0 { // ERROR "Proved Leq64$"
   735  			println("x")
   736  		}
   737  	}
   738  }
   739  
   740  // range2 elements are larger, so they use the general form of a range loop.
   741  func range2(b [][32]int) {
   742  	for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   743  		b[i][0] = v[0] + 1 // ERROR "Proved IsInBounds$"
   744  		if i < len(b) {    // ERROR "Proved Less64$"
   745  			println("x")
   746  		}
   747  		if i >= 0 { // ERROR "Proved Leq64$"
   748  			println("x")
   749  		}
   750  	}
   751  }
   752  
   753  // signhint1-2 test whether the hint (int >= 0) is propagated into the loop.
   754  func signHint1(i int, data []byte) {
   755  	if i >= 0 {
   756  		for i < len(data) { // ERROR "Induction variable: limits \[\?,\?\), increment 1$"
   757  			_ = data[i] // ERROR "Proved IsInBounds$"
   758  			i++
   759  		}
   760  	}
   761  }
   762  
   763  func signHint2(b []byte, n int) {
   764  	if n < 0 {
   765  		panic("")
   766  	}
   767  	_ = b[25]
   768  	for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
   769  		b[i] = 123 // ERROR "Proved IsInBounds$"
   770  	}
   771  }
   772  
   773  // indexGT0 tests whether prove learns int index >= 0 from bounds check.
   774  func indexGT0(b []byte, n int) {
   775  	_ = b[n]
   776  	_ = b[25]
   777  
   778  	for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
   779  		b[i] = 123 // ERROR "Proved IsInBounds$"
   780  	}
   781  }
   782  
   783  // Induction variable in unrolled loop.
   784  func unrollUpExcl(a []int) int {
   785  	var i, x int
   786  	for i = 0; i < len(a)-1; i += 2 { // ERROR "Induction variable: limits \[0,\?\), increment 2$"
   787  		x += a[i] // ERROR "Proved IsInBounds$"
   788  		x += a[i+1]
   789  	}
   790  	if i == len(a)-1 {
   791  		x += a[i]
   792  	}
   793  	return x
   794  }
   795  
   796  // Induction variable in unrolled loop.
   797  func unrollUpIncl(a []int) int {
   798  	var i, x int
   799  	for i = 0; i <= len(a)-2; i += 2 { // ERROR "Induction variable: limits \[0,\?\], increment 2$"
   800  		x += a[i] // ERROR "Proved IsInBounds$"
   801  		x += a[i+1]
   802  	}
   803  	if i == len(a)-1 {
   804  		x += a[i]
   805  	}
   806  	return x
   807  }
   808  
   809  // Induction variable in unrolled loop.
   810  func unrollDownExcl0(a []int) int {
   811  	var i, x int
   812  	for i = len(a) - 1; i > 0; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
   813  		x += a[i]   // ERROR "Proved IsInBounds$"
   814  		x += a[i-1] // ERROR "Proved IsInBounds$"
   815  	}
   816  	if i == 0 {
   817  		x += a[i]
   818  	}
   819  	return x
   820  }
   821  
   822  // Induction variable in unrolled loop.
   823  func unrollDownExcl1(a []int) int {
   824  	var i, x int
   825  	for i = len(a) - 1; i >= 1; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
   826  		x += a[i]   // ERROR "Proved IsInBounds$"
   827  		x += a[i-1] // ERROR "Proved IsInBounds$"
   828  	}
   829  	if i == 0 {
   830  		x += a[i]
   831  	}
   832  	return x
   833  }
   834  
   835  // Induction variable in unrolled loop.
   836  func unrollDownInclStep(a []int) int {
   837  	var i, x int
   838  	for i = len(a); i >= 2; i -= 2 { // ERROR "Induction variable: limits \[2,\?\], increment 2$"
   839  		x += a[i-1] // ERROR "Proved IsInBounds$"
   840  		x += a[i-2] // ERROR "Proved IsInBounds$"
   841  	}
   842  	if i == 1 {
   843  		x += a[i-1]
   844  	}
   845  	return x
   846  }
   847  
   848  // Not an induction variable (step too large)
   849  func unrollExclStepTooLarge(a []int) int {
   850  	var i, x int
   851  	for i = 0; i < len(a)-1; i += 3 {
   852  		x += a[i]
   853  		x += a[i+1]
   854  	}
   855  	if i == len(a)-1 {
   856  		x += a[i]
   857  	}
   858  	return x
   859  }
   860  
   861  // Not an induction variable (step too large)
   862  func unrollInclStepTooLarge(a []int) int {
   863  	var i, x int
   864  	for i = 0; i <= len(a)-2; i += 3 {
   865  		x += a[i]
   866  		x += a[i+1]
   867  	}
   868  	if i == len(a)-1 {
   869  		x += a[i]
   870  	}
   871  	return x
   872  }
   873  
   874  // Not an induction variable (min too small, iterating down)
   875  func unrollDecMin(a []int, b int) int {
   876  	if b != math.MinInt64 {
   877  		return 42
   878  	}
   879  	var i, x int
   880  	for i = len(a); i >= b; i -= 2 {
   881  		x += a[i-1]
   882  		x += a[i-2]
   883  	}
   884  	if i == 1 { // ERROR "Disproved Eq64$"
   885  		x += a[i-1]
   886  	}
   887  	return x
   888  }
   889  
   890  // Not an induction variable (min too small, iterating up -- perhaps could allow, but why bother?)
   891  func unrollIncMin(a []int, b int) int {
   892  	if b != math.MinInt64 {
   893  		return 42
   894  	}
   895  	var i, x int
   896  	for i = len(a); i >= b; i += 2 {
   897  		x += a[i-1]
   898  		x += a[i-2]
   899  	}
   900  	if i == 1 { // ERROR "Disproved Eq64$"
   901  		x += a[i-1]
   902  	}
   903  	return x
   904  }
   905  
   906  // The 4 xxxxExtNto64 functions below test whether prove is looking
   907  // through value-preserving sign/zero extensions of index values (issue #26292).
   908  
   909  // Look through all extensions
   910  func signExtNto64(x []int, j8 int8, j16 int16, j32 int32) int {
   911  	if len(x) < 22 {
   912  		return 0
   913  	}
   914  	if j8 >= 0 && j8 < 22 {
   915  		return x[j8] // ERROR "Proved IsInBounds$"
   916  	}
   917  	if j16 >= 0 && j16 < 22 {
   918  		return x[j16] // ERROR "Proved IsInBounds$"
   919  	}
   920  	if j32 >= 0 && j32 < 22 {
   921  		return x[j32] // ERROR "Proved IsInBounds$"
   922  	}
   923  	return 0
   924  }
   925  
   926  func zeroExtNto64(x []int, j8 uint8, j16 uint16, j32 uint32) int {
   927  	if len(x) < 22 {
   928  		return 0
   929  	}
   930  	if j8 >= 0 && j8 < 22 {
   931  		return x[j8] // ERROR "Proved IsInBounds$"
   932  	}
   933  	if j16 >= 0 && j16 < 22 {
   934  		return x[j16] // ERROR "Proved IsInBounds$"
   935  	}
   936  	if j32 >= 0 && j32 < 22 {
   937  		return x[j32] // ERROR "Proved IsInBounds$"
   938  	}
   939  	return 0
   940  }
   941  
   942  // Process fence-post implications through 32to64 extensions (issue #29964)
   943  func signExt32to64Fence(x []int, j int32) int {
   944  	if x[j] != 0 {
   945  		return 1
   946  	}
   947  	if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
   948  		return 1
   949  	}
   950  	return 0
   951  }
   952  
   953  func zeroExt32to64Fence(x []int, j uint32) int {
   954  	if x[j] != 0 {
   955  		return 1
   956  	}
   957  	if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
   958  		return 1
   959  	}
   960  	return 0
   961  }
   962  
   963  // Ensure that bounds checks with negative indexes are not incorrectly removed.
   964  func negIndex() {
   965  	n := make([]int, 1)
   966  	for i := -1; i <= 0; i++ { // ERROR "Induction variable: limits \[-1,0\], increment 1$"
   967  		n[i] = 1
   968  	}
   969  }
   970  func negIndex2(n int) {
   971  	a := make([]int, 5)
   972  	b := make([]int, 5)
   973  	c := make([]int, 5)
   974  	for i := -1; i <= 0; i-- {
   975  		b[i] = i
   976  		n++
   977  		if n > 10 {
   978  			break
   979  		}
   980  	}
   981  	useSlice(a)
   982  	useSlice(c)
   983  }
   984  
   985  // Check that prove is zeroing these right shifts of positive ints by bit-width - 1.
   986  // e.g (Rsh64x64 <t> n (Const64 <typ.UInt64> [63])) && ft.isNonNegative(n) -> 0
   987  func sh64(n int64) int64 {
   988  	if n < 0 {
   989  		return n
   990  	}
   991  	return n >> 63 // ERROR "Proved Rsh64x64 shifts to zero"
   992  }
   993  
   994  func sh32(n int32) int32 {
   995  	if n < 0 {
   996  		return n
   997  	}
   998  	return n >> 31 // ERROR "Proved Rsh32x64 shifts to zero"
   999  }
  1000  
  1001  func sh32x64(n int32) int32 {
  1002  	if n < 0 {
  1003  		return n
  1004  	}
  1005  	return n >> uint64(31) // ERROR "Proved Rsh32x64 shifts to zero"
  1006  }
  1007  
  1008  func sh16(n int16) int16 {
  1009  	if n < 0 {
  1010  		return n
  1011  	}
  1012  	return n >> 15 // ERROR "Proved Rsh16x64 shifts to zero"
  1013  }
  1014  
  1015  func sh64noopt(n int64) int64 {
  1016  	return n >> 63 // not optimized; n could be negative
  1017  }
  1018  
  1019  // These cases are division of a positive signed integer by a power of 2.
  1020  // The opt pass doesnt have sufficient information to see that n is positive.
  1021  // So, instead, opt rewrites the division with a less-than-optimal replacement.
  1022  // Prove, which can see that n is nonnegative, cannot see the division because
  1023  // opt, an earlier pass, has already replaced it.
  1024  // The fix for this issue allows prove to zero a right shift that was added as
  1025  // part of the less-than-optimal reqwrite. That change by prove then allows
  1026  // lateopt to clean up all the unnecessary parts of the original division
  1027  // replacement. See issue #36159.
  1028  func divShiftClean(n int) int {
  1029  	if n < 0 {
  1030  		return n
  1031  	}
  1032  	return n / int(8) // ERROR "Proved Rsh64x64 shifts to zero"
  1033  }
  1034  
  1035  func divShiftClean64(n int64) int64 {
  1036  	if n < 0 {
  1037  		return n
  1038  	}
  1039  	return n / int64(16) // ERROR "Proved Rsh64x64 shifts to zero"
  1040  }
  1041  
  1042  func divShiftClean32(n int32) int32 {
  1043  	if n < 0 {
  1044  		return n
  1045  	}
  1046  	return n / int32(16) // ERROR "Proved Rsh32x64 shifts to zero"
  1047  }
  1048  
  1049  // Bounds check elimination
  1050  
  1051  func sliceBCE1(p []string, h uint) string {
  1052  	if len(p) == 0 {
  1053  		return ""
  1054  	}
  1055  
  1056  	i := h & uint(len(p)-1)
  1057  	return p[i] // ERROR "Proved IsInBounds$"
  1058  }
  1059  
  1060  func sliceBCE2(p []string, h int) string {
  1061  	if len(p) == 0 {
  1062  		return ""
  1063  	}
  1064  	i := h & (len(p) - 1)
  1065  	return p[i] // ERROR "Proved IsInBounds$"
  1066  }
  1067  
  1068  func and(p []byte) ([]byte, []byte) { // issue #52563
  1069  	const blocksize = 16
  1070  	fullBlocks := len(p) &^ (blocksize - 1)
  1071  	blk := p[:fullBlocks] // ERROR "Proved IsSliceInBounds$"
  1072  	rem := p[fullBlocks:] // ERROR "Proved IsSliceInBounds$"
  1073  	return blk, rem
  1074  }
  1075  
  1076  func rshu(x, y uint) int {
  1077  	z := x >> y
  1078  	if z <= x { // ERROR "Proved Leq64U$"
  1079  		return 1
  1080  	}
  1081  	return 0
  1082  }
  1083  
  1084  func divu(x, y uint) int {
  1085  	z := x / y
  1086  	if z <= x { // ERROR "Proved Leq64U$"
  1087  		return 1
  1088  	}
  1089  	return 0
  1090  }
  1091  
  1092  func modu1(x, y uint) int {
  1093  	z := x % y
  1094  	if z < y { // ERROR "Proved Less64U$"
  1095  		return 1
  1096  	}
  1097  	return 0
  1098  }
  1099  
  1100  func modu2(x, y uint) int {
  1101  	z := x % y
  1102  	if z <= x { // ERROR "Proved Leq64U$"
  1103  		return 1
  1104  	}
  1105  	return 0
  1106  }
  1107  
  1108  func issue57077(s []int) (left, right []int) {
  1109  	middle := len(s) / 2
  1110  	left = s[:middle] // ERROR "Proved IsSliceInBounds$"
  1111  	right = s[middle:] // ERROR "Proved IsSliceInBounds$"
  1112  	return
  1113  }
  1114  
  1115  func issue51622(b []byte) int {
  1116  	if len(b) >= 3 && b[len(b)-3] == '#' { // ERROR "Proved IsInBounds$"
  1117  		return len(b)
  1118  	}
  1119  	return 0
  1120  }
  1121  
  1122  func issue45928(x int) {
  1123  	combinedFrac := x / (x | (1 << 31)) // ERROR "Proved Neq64$"
  1124  	useInt(combinedFrac)
  1125  }
  1126  
  1127  //go:noinline
  1128  func useInt(a int) {
  1129  }
  1130  
  1131  //go:noinline
  1132  func useSlice(a []int) {
  1133  }
  1134  
  1135  func main() {
  1136  }
  1137  

View as plain text