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 int64) int64 {
   400  	if a > math.MaxInt64 {
   401  		if a == 0 { // ERROR "Disproved Eq64$"
   402  			return 1
   403  		}
   404  	}
   405  	return 0
   406  }
   407  
   408  func f13g(a int) int {
   409  	if a < 3 {
   410  		return 5
   411  	}
   412  	if a > 3 {
   413  		return 6
   414  	}
   415  	if a == 3 { // ERROR "Proved Eq64$"
   416  		return 7
   417  	}
   418  	return 8
   419  }
   420  
   421  func f13h(a int) int {
   422  	if a < 3 {
   423  		if a > 1 {
   424  			if a == 2 { // ERROR "Proved Eq64$"
   425  				return 5
   426  			}
   427  		}
   428  	}
   429  	return 0
   430  }
   431  
   432  func f13i(a uint) int {
   433  	if a == 0 {
   434  		return 1
   435  	}
   436  	if a > 0 { // ERROR "Proved Less64U$"
   437  		return 2
   438  	}
   439  	return 3
   440  }
   441  
   442  func f14(p, q *int, a []int) {
   443  	// This crazy ordering usually gives i1 the lowest value ID,
   444  	// j the middle value ID, and i2 the highest value ID.
   445  	// That used to confuse CSE because it ordered the args
   446  	// of the two + ops below differently.
   447  	// That in turn foiled bounds check elimination.
   448  	i1 := *p
   449  	j := *q
   450  	i2 := *p
   451  	useInt(a[i1+j])
   452  	useInt(a[i2+j]) // ERROR "Proved IsInBounds$"
   453  }
   454  
   455  func f15(s []int, x int) {
   456  	useSlice(s[x:])
   457  	useSlice(s[:x]) // ERROR "Proved IsSliceInBounds$"
   458  }
   459  
   460  func f16(s []int) []int {
   461  	if len(s) >= 10 {
   462  		return s[:10] // ERROR "Proved IsSliceInBounds$"
   463  	}
   464  	return nil
   465  }
   466  
   467  func f17(b []int) {
   468  	for i := 0; i < len(b); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   469  		// This tests for i <= cap, which we can only prove
   470  		// using the derived relation between len and cap.
   471  		// This depends on finding the contradiction, since we
   472  		// don't query this condition directly.
   473  		useSlice(b[:i]) // ERROR "Proved IsSliceInBounds$"
   474  	}
   475  }
   476  
   477  func f18(b []int, x int, y uint) {
   478  	_ = b[x]
   479  	_ = b[y]
   480  
   481  	if x > len(b) { // ERROR "Disproved Less64$"
   482  		return
   483  	}
   484  	if y > uint(len(b)) { // ERROR "Disproved Less64U$"
   485  		return
   486  	}
   487  	if int(y) > len(b) { // ERROR "Disproved Less64$"
   488  		return
   489  	}
   490  }
   491  
   492  func f19() (e int64, err error) {
   493  	// Issue 29502: slice[:0] is incorrectly disproved.
   494  	var stack []int64
   495  	stack = append(stack, 123)
   496  	if len(stack) > 1 {
   497  		panic("too many elements")
   498  	}
   499  	last := len(stack) - 1
   500  	e = stack[last]
   501  	// Buggy compiler prints "Disproved Leq64" for the next line.
   502  	stack = stack[:last]
   503  	return e, nil
   504  }
   505  
   506  func sm1(b []int, x int) {
   507  	// Test constant argument to slicemask.
   508  	useSlice(b[2:8]) // ERROR "Proved slicemask not needed$"
   509  	// Test non-constant argument with known limits.
   510  	if cap(b) > 10 {
   511  		useSlice(b[2:])
   512  	}
   513  }
   514  
   515  func lim1(x, y, z int) {
   516  	// Test relations between signed and unsigned limits.
   517  	if x > 5 {
   518  		if uint(x) > 5 { // ERROR "Proved Less64U$"
   519  			return
   520  		}
   521  	}
   522  	if y >= 0 && y < 4 {
   523  		if uint(y) > 4 { // ERROR "Disproved Less64U$"
   524  			return
   525  		}
   526  		if uint(y) < 5 { // ERROR "Proved Less64U$"
   527  			return
   528  		}
   529  	}
   530  	if z < 4 {
   531  		if uint(z) > 4 { // Not provable without disjunctions.
   532  			return
   533  		}
   534  	}
   535  }
   536  
   537  // fence1–4 correspond to the four fence-post implications.
   538  
   539  func fence1(b []int, x, y int) {
   540  	// Test proofs that rely on fence-post implications.
   541  	if x+1 > y {
   542  		if x < y { // ERROR "Disproved Less64$"
   543  			return
   544  		}
   545  	}
   546  	if len(b) < cap(b) {
   547  		// This eliminates the growslice path.
   548  		b = append(b, 1) // ERROR "Disproved Less64U$"
   549  	}
   550  }
   551  
   552  func fence2(x, y int) {
   553  	if x-1 < y {
   554  		if x > y { // ERROR "Disproved Less64$"
   555  			return
   556  		}
   557  	}
   558  }
   559  
   560  func fence3(b, c []int, x, y int64) {
   561  	if x-1 >= y {
   562  		if x <= y { // Can't prove because x may have wrapped.
   563  			return
   564  		}
   565  	}
   566  
   567  	if x != math.MinInt64 && x-1 >= y {
   568  		if x <= y { // ERROR "Disproved Leq64$"
   569  			return
   570  		}
   571  	}
   572  
   573  	c[len(c)-1] = 0 // Can't prove because len(c) might be 0
   574  
   575  	if n := len(b); n > 0 {
   576  		b[n-1] = 0 // ERROR "Proved IsInBounds$"
   577  	}
   578  }
   579  
   580  func fence4(x, y int64) {
   581  	if x >= y+1 {
   582  		if x <= y {
   583  			return
   584  		}
   585  	}
   586  	if y != math.MaxInt64 && x >= y+1 {
   587  		if x <= y { // ERROR "Disproved Leq64$"
   588  			return
   589  		}
   590  	}
   591  }
   592  
   593  // Check transitive relations
   594  func trans1(x, y int64) {
   595  	if x > 5 {
   596  		if y > x {
   597  			if y > 2 { // ERROR "Proved Less64$"
   598  				return
   599  			}
   600  		} else if y == x {
   601  			if y > 5 { // ERROR "Proved Less64$"
   602  				return
   603  			}
   604  		}
   605  	}
   606  	if x >= 10 {
   607  		if y > x {
   608  			if y > 10 { // ERROR "Proved Less64$"
   609  				return
   610  			}
   611  		}
   612  	}
   613  }
   614  
   615  func trans2(a, b []int, i int) {
   616  	if len(a) != len(b) {
   617  		return
   618  	}
   619  
   620  	_ = a[i]
   621  	_ = b[i] // ERROR "Proved IsInBounds$"
   622  }
   623  
   624  func trans3(a, b []int, i int) {
   625  	if len(a) > len(b) {
   626  		return
   627  	}
   628  
   629  	_ = a[i]
   630  	_ = b[i] // ERROR "Proved IsInBounds$"
   631  }
   632  
   633  func trans4(b []byte, x int) {
   634  	// Issue #42603: slice len/cap transitive relations.
   635  	switch x {
   636  	case 0:
   637  		if len(b) < 20 {
   638  			return
   639  		}
   640  		_ = b[:2] // ERROR "Proved IsSliceInBounds$"
   641  	case 1:
   642  		if len(b) < 40 {
   643  			return
   644  		}
   645  		_ = b[:2] // ERROR "Proved IsSliceInBounds$"
   646  	}
   647  }
   648  
   649  // Derived from nat.cmp
   650  func natcmp(x, y []uint) (r int) {
   651  	m := len(x)
   652  	n := len(y)
   653  	if m != n || m == 0 {
   654  		return
   655  	}
   656  
   657  	i := m - 1
   658  	for i > 0 && // ERROR "Induction variable: limits \(0,\?\], increment 1$"
   659  		x[i] == // ERROR "Proved IsInBounds$"
   660  			y[i] { // ERROR "Proved IsInBounds$"
   661  		i--
   662  	}
   663  
   664  	switch {
   665  	case x[i] < // todo, cannot prove this because it's dominated by i<=0 || x[i]==y[i]
   666  		y[i]: // ERROR "Proved IsInBounds$"
   667  		r = -1
   668  	case x[i] > // ERROR "Proved IsInBounds$"
   669  		y[i]: // ERROR "Proved IsInBounds$"
   670  		r = 1
   671  	}
   672  	return
   673  }
   674  
   675  func suffix(s, suffix string) bool {
   676  	// todo, we're still not able to drop the bound check here in the general case
   677  	return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
   678  }
   679  
   680  func constsuffix(s string) bool {
   681  	return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$"
   682  }
   683  
   684  // oforuntil tests the pattern created by OFORUNTIL blocks. These are
   685  // handled by addLocalInductiveFacts rather than findIndVar.
   686  func oforuntil(b []int) {
   687  	i := 0
   688  	if len(b) > i {
   689  	top:
   690  		println(b[i]) // ERROR "Induction variable: limits \[0,\?\), increment 1$" "Proved IsInBounds$"
   691  		i++
   692  		if i < len(b) {
   693  			goto top
   694  		}
   695  	}
   696  }
   697  
   698  func atexit(foobar []func()) {
   699  	for i := len(foobar) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1"
   700  		f := foobar[i]
   701  		foobar = foobar[:i] // ERROR "IsSliceInBounds"
   702  		f()
   703  	}
   704  }
   705  
   706  func make1(n int) []int {
   707  	s := make([]int, n)
   708  	for i := 0; i < n; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1"
   709  		s[i] = 1 // ERROR "Proved IsInBounds$"
   710  	}
   711  	return s
   712  }
   713  
   714  func make2(n int) []int {
   715  	s := make([]int, n)
   716  	for i := range s { // ERROR "Induction variable: limits \[0,\?\), increment 1"
   717  		s[i] = 1 // ERROR "Proved IsInBounds$"
   718  	}
   719  	return s
   720  }
   721  
   722  // The range tests below test the index variable of range loops.
   723  
   724  // range1 compiles to the "efficiently indexable" form of a range loop.
   725  func range1(b []int) {
   726  	for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   727  		b[i] = v + 1    // ERROR "Proved IsInBounds$"
   728  		if i < len(b) { // ERROR "Proved Less64$"
   729  			println("x")
   730  		}
   731  		if i >= 0 { // ERROR "Proved Leq64$"
   732  			println("x")
   733  		}
   734  	}
   735  }
   736  
   737  // range2 elements are larger, so they use the general form of a range loop.
   738  func range2(b [][32]int) {
   739  	for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   740  		b[i][0] = v[0] + 1 // ERROR "Proved IsInBounds$"
   741  		if i < len(b) {    // ERROR "Proved Less64$"
   742  			println("x")
   743  		}
   744  		if i >= 0 { // ERROR "Proved Leq64$"
   745  			println("x")
   746  		}
   747  	}
   748  }
   749  
   750  // signhint1-2 test whether the hint (int >= 0) is propagated into the loop.
   751  func signHint1(i int, data []byte) {
   752  	if i >= 0 {
   753  		for i < len(data) { // ERROR "Induction variable: limits \[\?,\?\), increment 1$"
   754  			_ = data[i] // ERROR "Proved IsInBounds$"
   755  			i++
   756  		}
   757  	}
   758  }
   759  
   760  func signHint2(b []byte, n int) {
   761  	if n < 0 {
   762  		panic("")
   763  	}
   764  	_ = b[25]
   765  	for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
   766  		b[i] = 123 // ERROR "Proved IsInBounds$"
   767  	}
   768  }
   769  
   770  // indexGT0 tests whether prove learns int index >= 0 from bounds check.
   771  func indexGT0(b []byte, n int) {
   772  	_ = b[n]
   773  	_ = b[25]
   774  
   775  	for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
   776  		b[i] = 123 // ERROR "Proved IsInBounds$"
   777  	}
   778  }
   779  
   780  // Induction variable in unrolled loop.
   781  func unrollUpExcl(a []int) int {
   782  	var i, x int
   783  	for i = 0; i < len(a)-1; i += 2 { // ERROR "Induction variable: limits \[0,\?\), increment 2$"
   784  		x += a[i] // ERROR "Proved IsInBounds$"
   785  		x += a[i+1]
   786  	}
   787  	if i == len(a)-1 {
   788  		x += a[i]
   789  	}
   790  	return x
   791  }
   792  
   793  // Induction variable in unrolled loop.
   794  func unrollUpIncl(a []int) int {
   795  	var i, x int
   796  	for i = 0; i <= len(a)-2; i += 2 { // ERROR "Induction variable: limits \[0,\?\], increment 2$"
   797  		x += a[i] // ERROR "Proved IsInBounds$"
   798  		x += a[i+1]
   799  	}
   800  	if i == len(a)-1 {
   801  		x += a[i]
   802  	}
   803  	return x
   804  }
   805  
   806  // Induction variable in unrolled loop.
   807  func unrollDownExcl0(a []int) int {
   808  	var i, x int
   809  	for i = len(a) - 1; i > 0; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
   810  		x += a[i]   // ERROR "Proved IsInBounds$"
   811  		x += a[i-1] // ERROR "Proved IsInBounds$"
   812  	}
   813  	if i == 0 {
   814  		x += a[i]
   815  	}
   816  	return x
   817  }
   818  
   819  // Induction variable in unrolled loop.
   820  func unrollDownExcl1(a []int) int {
   821  	var i, x int
   822  	for i = len(a) - 1; i >= 1; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
   823  		x += a[i]   // ERROR "Proved IsInBounds$"
   824  		x += a[i-1] // ERROR "Proved IsInBounds$"
   825  	}
   826  	if i == 0 {
   827  		x += a[i]
   828  	}
   829  	return x
   830  }
   831  
   832  // Induction variable in unrolled loop.
   833  func unrollDownInclStep(a []int) int {
   834  	var i, x int
   835  	for i = len(a); i >= 2; i -= 2 { // ERROR "Induction variable: limits \[2,\?\], increment 2$"
   836  		x += a[i-1] // ERROR "Proved IsInBounds$"
   837  		x += a[i-2] // ERROR "Proved IsInBounds$"
   838  	}
   839  	if i == 1 {
   840  		x += a[i-1]
   841  	}
   842  	return x
   843  }
   844  
   845  // Not an induction variable (step too large)
   846  func unrollExclStepTooLarge(a []int) int {
   847  	var i, x int
   848  	for i = 0; i < len(a)-1; i += 3 {
   849  		x += a[i]
   850  		x += a[i+1]
   851  	}
   852  	if i == len(a)-1 {
   853  		x += a[i]
   854  	}
   855  	return x
   856  }
   857  
   858  // Not an induction variable (step too large)
   859  func unrollInclStepTooLarge(a []int) int {
   860  	var i, x int
   861  	for i = 0; i <= len(a)-2; i += 3 {
   862  		x += a[i]
   863  		x += a[i+1]
   864  	}
   865  	if i == len(a)-1 {
   866  		x += a[i]
   867  	}
   868  	return x
   869  }
   870  
   871  // Not an induction variable (min too small, iterating down)
   872  func unrollDecMin(a []int) int {
   873  	var i, x int
   874  	for i = len(a); i >= math.MinInt64; i -= 2 {
   875  		x += a[i-1]
   876  		x += a[i-2]
   877  	}
   878  	if i == 1 { // ERROR "Disproved Eq64$"
   879  		x += a[i-1]
   880  	}
   881  	return x
   882  }
   883  
   884  // Not an induction variable (min too small, iterating up -- perhaps could allow, but why bother?)
   885  func unrollIncMin(a []int) int {
   886  	var i, x int
   887  	for i = len(a); i >= math.MinInt64; i += 2 {
   888  		x += a[i-1]
   889  		x += a[i-2]
   890  	}
   891  	if i == 1 { // ERROR "Disproved Eq64$"
   892  		x += a[i-1]
   893  	}
   894  	return x
   895  }
   896  
   897  // The 4 xxxxExtNto64 functions below test whether prove is looking
   898  // through value-preserving sign/zero extensions of index values (issue #26292).
   899  
   900  // Look through all extensions
   901  func signExtNto64(x []int, j8 int8, j16 int16, j32 int32) int {
   902  	if len(x) < 22 {
   903  		return 0
   904  	}
   905  	if j8 >= 0 && j8 < 22 {
   906  		return x[j8] // ERROR "Proved IsInBounds$"
   907  	}
   908  	if j16 >= 0 && j16 < 22 {
   909  		return x[j16] // ERROR "Proved IsInBounds$"
   910  	}
   911  	if j32 >= 0 && j32 < 22 {
   912  		return x[j32] // ERROR "Proved IsInBounds$"
   913  	}
   914  	return 0
   915  }
   916  
   917  func zeroExtNto64(x []int, j8 uint8, j16 uint16, j32 uint32) int {
   918  	if len(x) < 22 {
   919  		return 0
   920  	}
   921  	if j8 >= 0 && j8 < 22 {
   922  		return x[j8] // ERROR "Proved IsInBounds$"
   923  	}
   924  	if j16 >= 0 && j16 < 22 {
   925  		return x[j16] // ERROR "Proved IsInBounds$"
   926  	}
   927  	if j32 >= 0 && j32 < 22 {
   928  		return x[j32] // ERROR "Proved IsInBounds$"
   929  	}
   930  	return 0
   931  }
   932  
   933  // Process fence-post implications through 32to64 extensions (issue #29964)
   934  func signExt32to64Fence(x []int, j int32) int {
   935  	if x[j] != 0 {
   936  		return 1
   937  	}
   938  	if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
   939  		return 1
   940  	}
   941  	return 0
   942  }
   943  
   944  func zeroExt32to64Fence(x []int, j uint32) int {
   945  	if x[j] != 0 {
   946  		return 1
   947  	}
   948  	if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
   949  		return 1
   950  	}
   951  	return 0
   952  }
   953  
   954  // Ensure that bounds checks with negative indexes are not incorrectly removed.
   955  func negIndex() {
   956  	n := make([]int, 1)
   957  	for i := -1; i <= 0; i++ { // ERROR "Induction variable: limits \[-1,0\], increment 1$"
   958  		n[i] = 1
   959  	}
   960  }
   961  func negIndex2(n int) {
   962  	a := make([]int, 5)
   963  	b := make([]int, 5)
   964  	c := make([]int, 5)
   965  	for i := -1; i <= 0; i-- {
   966  		b[i] = i
   967  		n++
   968  		if n > 10 {
   969  			break
   970  		}
   971  	}
   972  	useSlice(a)
   973  	useSlice(c)
   974  }
   975  
   976  // Check that prove is zeroing these right shifts of positive ints by bit-width - 1.
   977  // e.g (Rsh64x64 <t> n (Const64 <typ.UInt64> [63])) && ft.isNonNegative(n) -> 0
   978  func sh64(n int64) int64 {
   979  	if n < 0 {
   980  		return n
   981  	}
   982  	return n >> 63 // ERROR "Proved Rsh64x64 shifts to zero"
   983  }
   984  
   985  func sh32(n int32) int32 {
   986  	if n < 0 {
   987  		return n
   988  	}
   989  	return n >> 31 // ERROR "Proved Rsh32x64 shifts to zero"
   990  }
   991  
   992  func sh32x64(n int32) int32 {
   993  	if n < 0 {
   994  		return n
   995  	}
   996  	return n >> uint64(31) // ERROR "Proved Rsh32x64 shifts to zero"
   997  }
   998  
   999  func sh16(n int16) int16 {
  1000  	if n < 0 {
  1001  		return n
  1002  	}
  1003  	return n >> 15 // ERROR "Proved Rsh16x64 shifts to zero"
  1004  }
  1005  
  1006  func sh64noopt(n int64) int64 {
  1007  	return n >> 63 // not optimized; n could be negative
  1008  }
  1009  
  1010  // These cases are division of a positive signed integer by a power of 2.
  1011  // The opt pass doesnt have sufficient information to see that n is positive.
  1012  // So, instead, opt rewrites the division with a less-than-optimal replacement.
  1013  // Prove, which can see that n is nonnegative, cannot see the division because
  1014  // opt, an earlier pass, has already replaced it.
  1015  // The fix for this issue allows prove to zero a right shift that was added as
  1016  // part of the less-than-optimal reqwrite. That change by prove then allows
  1017  // lateopt to clean up all the unnecessary parts of the original division
  1018  // replacement. See issue #36159.
  1019  func divShiftClean(n int) int {
  1020  	if n < 0 {
  1021  		return n
  1022  	}
  1023  	return n / int(8) // ERROR "Proved Rsh64x64 shifts to zero"
  1024  }
  1025  
  1026  func divShiftClean64(n int64) int64 {
  1027  	if n < 0 {
  1028  		return n
  1029  	}
  1030  	return n / int64(16) // ERROR "Proved Rsh64x64 shifts to zero"
  1031  }
  1032  
  1033  func divShiftClean32(n int32) int32 {
  1034  	if n < 0 {
  1035  		return n
  1036  	}
  1037  	return n / int32(16) // ERROR "Proved Rsh32x64 shifts to zero"
  1038  }
  1039  
  1040  // Bounds check elimination
  1041  
  1042  func sliceBCE1(p []string, h uint) string {
  1043  	if len(p) == 0 {
  1044  		return ""
  1045  	}
  1046  
  1047  	i := h & uint(len(p)-1)
  1048  	return p[i] // ERROR "Proved IsInBounds$"
  1049  }
  1050  
  1051  func sliceBCE2(p []string, h int) string {
  1052  	if len(p) == 0 {
  1053  		return ""
  1054  	}
  1055  	i := h & (len(p) - 1)
  1056  	return p[i] // ERROR "Proved IsInBounds$"
  1057  }
  1058  
  1059  func and(p []byte) ([]byte, []byte) { // issue #52563
  1060  	const blocksize = 16
  1061  	fullBlocks := len(p) &^ (blocksize - 1)
  1062  	blk := p[:fullBlocks] // ERROR "Proved IsSliceInBounds$"
  1063  	rem := p[fullBlocks:] // ERROR "Proved IsSliceInBounds$"
  1064  	return blk, rem
  1065  }
  1066  
  1067  func rshu(x, y uint) int {
  1068  	z := x >> y
  1069  	if z <= x { // ERROR "Proved Leq64U$"
  1070  		return 1
  1071  	}
  1072  	return 0
  1073  }
  1074  
  1075  func divu(x, y uint) int {
  1076  	z := x / y
  1077  	if z <= x { // ERROR "Proved Leq64U$"
  1078  		return 1
  1079  	}
  1080  	return 0
  1081  }
  1082  
  1083  func modu1(x, y uint) int {
  1084  	z := x % y
  1085  	if z < y { // ERROR "Proved Less64U$"
  1086  		return 1
  1087  	}
  1088  	return 0
  1089  }
  1090  
  1091  func modu2(x, y uint) int {
  1092  	z := x % y
  1093  	if z <= x { // ERROR "Proved Leq64U$"
  1094  		return 1
  1095  	}
  1096  	return 0
  1097  }
  1098  
  1099  func issue57077(s []int) (left, right []int) {
  1100  	middle := len(s) / 2
  1101  	left = s[:middle] // ERROR "Proved IsSliceInBounds$"
  1102  	right = s[middle:] // ERROR "Proved IsSliceInBounds$"
  1103  	return
  1104  }
  1105  
  1106  func issue51622(b []byte) int {
  1107  	if len(b) >= 3 && b[len(b)-3] == '#' { // ERROR "Proved IsInBounds$"
  1108  		return len(b)
  1109  	}
  1110  	return 0
  1111  }
  1112  
  1113  func issue45928(x int) {
  1114  	combinedFrac := x / (x | (1 << 31)) // ERROR "Proved Neq64$"
  1115  	useInt(combinedFrac)
  1116  }
  1117  
  1118  //go:noinline
  1119  func useInt(a int) {
  1120  }
  1121  
  1122  //go:noinline
  1123  func useSlice(a []int) {
  1124  }
  1125  
  1126  func main() {
  1127  }
  1128  

View as plain text