Source file test/prove.go

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

View as plain text