Source file test/prove.go

Documentation: test

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

View as plain text