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 (
    12  	"math"
    13  	"math/bits"
    14  )
    15  
    16  func f0(a []int) int {
    17  	a[0] = 1
    18  	a[0] = 1 // ERROR "Proved IsInBounds$"
    19  	a[6] = 1
    20  	a[6] = 1 // ERROR "Proved IsInBounds$"
    21  	a[5] = 1 // ERROR "Proved IsInBounds$"
    22  	a[5] = 1 // ERROR "Proved IsInBounds$"
    23  	return 13
    24  }
    25  
    26  func f1(a []int) int {
    27  	if len(a) <= 5 {
    28  		return 18
    29  	}
    30  	a[0] = 1 // ERROR "Proved IsInBounds$"
    31  	a[0] = 1 // ERROR "Proved IsInBounds$"
    32  	a[6] = 1
    33  	a[6] = 1 // ERROR "Proved IsInBounds$"
    34  	a[5] = 1 // ERROR "Proved IsInBounds$"
    35  	a[5] = 1 // ERROR "Proved IsInBounds$"
    36  	return 26
    37  }
    38  
    39  func f1b(a []int, i int, j uint) int {
    40  	if i >= 0 && 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] // ERROR "Proved IsInBounds$"
    48  	}
    49  	if i >= 10 && i < len(a) {
    50  		return a[i-10] // ERROR "Proved IsInBounds$"
    51  	}
    52  	if j < uint(len(a)) {
    53  		return a[j] // ERROR "Proved IsInBounds$"
    54  	}
    55  	return 0
    56  }
    57  
    58  func f1c(a []int, i int64) int {
    59  	c := uint64(math.MaxInt64 + 10) // overflows int
    60  	d := int64(c)
    61  	if i >= d && i < int64(len(a)) {
    62  		// d overflows, should not be handled.
    63  		return a[i]
    64  	}
    65  	return 0
    66  }
    67  
    68  func f2(a []int) int {
    69  	for i := range a { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
    70  		a[i+1] = i
    71  		a[i+1] = i // ERROR "Proved IsInBounds$"
    72  	}
    73  	return 34
    74  }
    75  
    76  func f3(a []uint) int {
    77  	for i := uint(0); i < uint(len(a)); i++ {
    78  		a[i] = i // ERROR "Proved IsInBounds$"
    79  	}
    80  	return 41
    81  }
    82  
    83  func f4a(a, b, c int) int {
    84  	if a < b {
    85  		if a == b { // ERROR "Disproved Eq64$"
    86  			return 47
    87  		}
    88  		if a > b { // ERROR "Disproved Less64$"
    89  			return 50
    90  		}
    91  		if a < b { // ERROR "Proved Less64$"
    92  			return 53
    93  		}
    94  		// We can't get to this point and prove knows that, so
    95  		// there's no message for the next (obvious) branch.
    96  		if a != a {
    97  			return 56
    98  		}
    99  		return 61
   100  	}
   101  	return 63
   102  }
   103  
   104  func f4b(a, b, c int) int {
   105  	if a <= b {
   106  		if a >= b {
   107  			if a == b { // ERROR "Proved Eq64$"
   108  				return 70
   109  			}
   110  			return 75
   111  		}
   112  		return 77
   113  	}
   114  	return 79
   115  }
   116  
   117  func f4c(a, b, c int) int {
   118  	if a <= b {
   119  		if a >= b {
   120  			if a != b { // ERROR "Disproved Neq64$"
   121  				return 73
   122  			}
   123  			return 75
   124  		}
   125  		return 77
   126  	}
   127  	return 79
   128  }
   129  
   130  func f4d(a, b, c int) int {
   131  	if a < b {
   132  		if a < c {
   133  			if a < b { // ERROR "Proved Less64$"
   134  				if a < c { // ERROR "Proved Less64$"
   135  					return 87
   136  				}
   137  				return 89
   138  			}
   139  			return 91
   140  		}
   141  		return 93
   142  	}
   143  	return 95
   144  }
   145  
   146  func f4e(a, b, c int) int {
   147  	if a < b {
   148  		if b > a { // ERROR "Proved Less64$"
   149  			return 101
   150  		}
   151  		return 103
   152  	}
   153  	return 105
   154  }
   155  
   156  func f4f(a, b, c int) int {
   157  	if a <= b {
   158  		if b > a {
   159  			if b == a { // ERROR "Disproved Eq64$"
   160  				return 112
   161  			}
   162  			return 114
   163  		}
   164  		if b >= a { // ERROR "Proved Leq64$"
   165  			if b == a { // ERROR "Proved Eq64$"
   166  				return 118
   167  			}
   168  			return 120
   169  		}
   170  		return 122
   171  	}
   172  	return 124
   173  }
   174  
   175  func f5(a, b uint) int {
   176  	if a == b {
   177  		if a <= b { // ERROR "Proved Leq64U$"
   178  			return 130
   179  		}
   180  		return 132
   181  	}
   182  	return 134
   183  }
   184  
   185  // These comparisons are compile time constants.
   186  func f6a(a uint8) int {
   187  	if a < a { // ERROR "Disproved Less8U$"
   188  		return 140
   189  	}
   190  	return 151
   191  }
   192  
   193  func f6b(a uint8) int {
   194  	if a < a { // ERROR "Disproved Less8U$"
   195  		return 140
   196  	}
   197  	return 151
   198  }
   199  
   200  func f6x(a uint8) int {
   201  	if a > a { // ERROR "Disproved Less8U$"
   202  		return 143
   203  	}
   204  	return 151
   205  }
   206  
   207  func f6d(a uint8) int {
   208  	if a <= a { // ERROR "Proved Leq8U$"
   209  		return 146
   210  	}
   211  	return 151
   212  }
   213  
   214  func f6e(a uint8) int {
   215  	if a >= a { // ERROR "Proved Leq8U$"
   216  		return 149
   217  	}
   218  	return 151
   219  }
   220  
   221  func f7(a []int, b int) int {
   222  	if b < len(a) {
   223  		a[b] = 3
   224  		if b < len(a) { // ERROR "Proved Less64$"
   225  			a[b] = 5 // ERROR "Proved IsInBounds$"
   226  		}
   227  	}
   228  	return 161
   229  }
   230  
   231  func f8(a, b uint) int {
   232  	if a == b {
   233  		return 166
   234  	}
   235  	if a > b {
   236  		return 169
   237  	}
   238  	if a < b { // ERROR "Proved Less64U$"
   239  		return 172
   240  	}
   241  	return 174
   242  }
   243  
   244  func f9(a, b bool) int {
   245  	if a {
   246  		return 1
   247  	}
   248  	if a || b { // ERROR "Disproved Arg$"
   249  		return 2
   250  	}
   251  	return 3
   252  }
   253  
   254  func f10(a string) int {
   255  	n := len(a)
   256  	// We optimize comparisons with small constant strings (see cmd/compile/internal/gc/walk.go),
   257  	// so this string literal must be long.
   258  	if a[:n>>1] == "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" {
   259  		return 0
   260  	}
   261  	return 1
   262  }
   263  
   264  func f11a(a []int, i int) {
   265  	useInt(a[i])
   266  	useInt(a[i]) // ERROR "Proved IsInBounds$"
   267  }
   268  
   269  func f11b(a []int, i int) {
   270  	useSlice(a[i:])
   271  	useSlice(a[i:]) // ERROR "Proved IsSliceInBounds$"
   272  }
   273  
   274  func f11c(a []int, i int) {
   275  	useSlice(a[:i])
   276  	useSlice(a[:i]) // ERROR "Proved IsSliceInBounds$"
   277  }
   278  
   279  func f11d(a []int, i int) {
   280  	useInt(a[2*i+7])
   281  	useInt(a[2*i+7]) // ERROR "Proved IsInBounds$"
   282  }
   283  
   284  func f12(a []int, b int) {
   285  	useSlice(a[:b])
   286  }
   287  
   288  func f13a(a, b, c int, x bool) int {
   289  	if a > 12 {
   290  		if x {
   291  			if a < 12 { // ERROR "Disproved Less64$"
   292  				return 1
   293  			}
   294  		}
   295  		if x {
   296  			if a <= 12 { // ERROR "Disproved Leq64$"
   297  				return 2
   298  			}
   299  		}
   300  		if x {
   301  			if a == 12 { // ERROR "Disproved Eq64$"
   302  				return 3
   303  			}
   304  		}
   305  		if x {
   306  			if a >= 12 { // ERROR "Proved Leq64$"
   307  				return 4
   308  			}
   309  		}
   310  		if x {
   311  			if a > 12 { // ERROR "Proved Less64$"
   312  				return 5
   313  			}
   314  		}
   315  		return 6
   316  	}
   317  	return 0
   318  }
   319  
   320  func f13b(a int, x bool) int {
   321  	if a == -9 {
   322  		if x {
   323  			if a < -9 { // ERROR "Disproved Less64$"
   324  				return 7
   325  			}
   326  		}
   327  		if x {
   328  			if a <= -9 { // ERROR "Proved Leq64$"
   329  				return 8
   330  			}
   331  		}
   332  		if x {
   333  			if a == -9 { // ERROR "Proved Eq64$"
   334  				return 9
   335  			}
   336  		}
   337  		if x {
   338  			if a >= -9 { // ERROR "Proved Leq64$"
   339  				return 10
   340  			}
   341  		}
   342  		if x {
   343  			if a > -9 { // ERROR "Disproved Less64$"
   344  				return 11
   345  			}
   346  		}
   347  		return 12
   348  	}
   349  	return 0
   350  }
   351  
   352  func f13c(a int, x bool) int {
   353  	if a < 90 {
   354  		if x {
   355  			if a < 90 { // ERROR "Proved Less64$"
   356  				return 13
   357  			}
   358  		}
   359  		if x {
   360  			if a <= 90 { // ERROR "Proved Leq64$"
   361  				return 14
   362  			}
   363  		}
   364  		if x {
   365  			if a == 90 { // ERROR "Disproved Eq64$"
   366  				return 15
   367  			}
   368  		}
   369  		if x {
   370  			if a >= 90 { // ERROR "Disproved Leq64$"
   371  				return 16
   372  			}
   373  		}
   374  		if x {
   375  			if a > 90 { // ERROR "Disproved Less64$"
   376  				return 17
   377  			}
   378  		}
   379  		return 18
   380  	}
   381  	return 0
   382  }
   383  
   384  func f13d(a int) int {
   385  	if a < 5 {
   386  		if a < 9 { // ERROR "Proved Less64$"
   387  			return 1
   388  		}
   389  	}
   390  	return 0
   391  }
   392  
   393  func f13e(a int) int {
   394  	if a > 9 {
   395  		if a > 5 { // ERROR "Proved Less64$"
   396  			return 1
   397  		}
   398  	}
   399  	return 0
   400  }
   401  
   402  func f13f(a, b int64) int64 {
   403  	if b != math.MaxInt64 {
   404  		return 42
   405  	}
   406  	if a > b { // ERROR "Disproved Less64$"
   407  		if a == 0 {
   408  			return 1
   409  		}
   410  	}
   411  	return 0
   412  }
   413  
   414  func f13g(a int) int {
   415  	if a < 3 {
   416  		return 5
   417  	}
   418  	if a > 3 {
   419  		return 6
   420  	}
   421  	if a == 3 { // ERROR "Proved Eq64$"
   422  		return 7
   423  	}
   424  	return 8
   425  }
   426  
   427  func f13h(a int) int {
   428  	if a < 3 {
   429  		if a > 1 {
   430  			if a == 2 { // ERROR "Proved Eq64$"
   431  				return 5
   432  			}
   433  		}
   434  	}
   435  	return 0
   436  }
   437  
   438  func f13i(a uint) int {
   439  	if a == 0 {
   440  		return 1
   441  	}
   442  	if a > 0 { // ERROR "Proved Less64U$"
   443  		return 2
   444  	}
   445  	return 3
   446  }
   447  
   448  func f14(p, q *int, a []int) {
   449  	// This crazy ordering usually gives i1 the lowest value ID,
   450  	// j the middle value ID, and i2 the highest value ID.
   451  	// That used to confuse CSE because it ordered the args
   452  	// of the two + ops below differently.
   453  	// That in turn foiled bounds check elimination.
   454  	i1 := *p
   455  	j := *q
   456  	i2 := *p
   457  	useInt(a[i1+j])
   458  	useInt(a[i2+j]) // ERROR "Proved IsInBounds$"
   459  }
   460  
   461  func f15(s []int, x int) {
   462  	useSlice(s[x:])
   463  	useSlice(s[:x]) // ERROR "Proved IsSliceInBounds$"
   464  }
   465  
   466  func f16(s []int) []int {
   467  	if len(s) >= 10 {
   468  		return s[:10] // ERROR "Proved IsSliceInBounds$"
   469  	}
   470  	return nil
   471  }
   472  
   473  func f17(b []int) {
   474  	for i := 0; i < len(b); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   475  		// This tests for i <= cap, which we can only prove
   476  		// using the derived relation between len and cap.
   477  		// This depends on finding the contradiction, since we
   478  		// don't query this condition directly.
   479  		useSlice(b[:i]) // ERROR "Proved IsSliceInBounds$"
   480  	}
   481  }
   482  
   483  func f18(b []int, x int, y uint) {
   484  	_ = b[x]
   485  	_ = b[y]
   486  
   487  	if x > len(b) { // ERROR "Disproved Less64$"
   488  		return
   489  	}
   490  	if y > uint(len(b)) { // ERROR "Disproved Less64U$"
   491  		return
   492  	}
   493  	if int(y) > len(b) { // ERROR "Disproved Less64$"
   494  		return
   495  	}
   496  }
   497  
   498  func f19() (e int64, err error) {
   499  	// Issue 29502: slice[:0] is incorrectly disproved.
   500  	var stack []int64
   501  	stack = append(stack, 123)
   502  	if len(stack) > 1 {
   503  		panic("too many elements")
   504  	}
   505  	last := len(stack) - 1
   506  	e = stack[last]
   507  	// Buggy compiler prints "Disproved Leq64" for the next line.
   508  	stack = stack[:last]
   509  	return e, nil
   510  }
   511  
   512  func sm1(b []int, x int) {
   513  	// Test constant argument to slicemask.
   514  	useSlice(b[2:8]) // ERROR "Proved slicemask not needed$"
   515  	// Test non-constant argument with known limits.
   516  	if cap(b) > 10 {
   517  		useSlice(b[2:])
   518  	}
   519  }
   520  
   521  func lim1(x, y, z int) {
   522  	// Test relations between signed and unsigned limits.
   523  	if x > 5 {
   524  		if uint(x) > 5 { // ERROR "Proved Less64U$"
   525  			return
   526  		}
   527  	}
   528  	if y >= 0 && y < 4 {
   529  		if uint(y) > 4 { // ERROR "Disproved Less64U$"
   530  			return
   531  		}
   532  		if uint(y) < 5 { // ERROR "Proved Less64U$"
   533  			return
   534  		}
   535  	}
   536  	if z < 4 {
   537  		if uint(z) > 4 { // Not provable without disjunctions.
   538  			return
   539  		}
   540  	}
   541  }
   542  
   543  // fence1–4 correspond to the four fence-post implications.
   544  
   545  func fence1(b []int, x, y int) {
   546  	// Test proofs that rely on fence-post implications.
   547  	if x+1 > y {
   548  		if x < y { // ERROR "Disproved Less64$"
   549  			return
   550  		}
   551  	}
   552  	if len(b) < cap(b) {
   553  		// This eliminates the growslice path.
   554  		b = append(b, 1) // ERROR "Disproved Less64U$"
   555  	}
   556  }
   557  
   558  func fence2(x, y int) {
   559  	if x-1 < y {
   560  		if x > y { // ERROR "Disproved Less64$"
   561  			return
   562  		}
   563  	}
   564  }
   565  
   566  func fence3(b, c []int, x, y int64) {
   567  	if x-1 >= y {
   568  		if x <= y { // Can't prove because x may have wrapped.
   569  			return
   570  		}
   571  	}
   572  
   573  	if x != math.MinInt64 && x-1 >= y {
   574  		if x <= y { // ERROR "Disproved Leq64$"
   575  			return
   576  		}
   577  	}
   578  
   579  	c[len(c)-1] = 0 // Can't prove because len(c) might be 0
   580  
   581  	if n := len(b); n > 0 {
   582  		b[n-1] = 0 // ERROR "Proved IsInBounds$"
   583  	}
   584  }
   585  
   586  func fence4(x, y int64) {
   587  	if x >= y+1 {
   588  		if x <= y {
   589  			return
   590  		}
   591  	}
   592  	if y != math.MaxInt64 && x >= y+1 {
   593  		if x <= y { // ERROR "Disproved Leq64$"
   594  			return
   595  		}
   596  	}
   597  }
   598  
   599  // Check transitive relations
   600  func trans1(x, y int64) {
   601  	if x > 5 {
   602  		if y > x {
   603  			if y > 2 { // ERROR "Proved Less64$"
   604  				return
   605  			}
   606  		} else if y == x {
   607  			if y > 5 { // ERROR "Proved Less64$"
   608  				return
   609  			}
   610  		}
   611  	}
   612  	if x >= 10 {
   613  		if y > x {
   614  			if y > 10 { // ERROR "Proved Less64$"
   615  				return
   616  			}
   617  		}
   618  	}
   619  }
   620  
   621  func trans2(a, b []int, i int) {
   622  	if len(a) != len(b) {
   623  		return
   624  	}
   625  
   626  	_ = a[i]
   627  	_ = b[i] // ERROR "Proved IsInBounds$"
   628  }
   629  
   630  func trans3(a, b []int, i int) {
   631  	if len(a) > len(b) {
   632  		return
   633  	}
   634  
   635  	_ = a[i]
   636  	_ = b[i] // ERROR "Proved IsInBounds$"
   637  }
   638  
   639  func trans4(b []byte, x int) {
   640  	// Issue #42603: slice len/cap transitive relations.
   641  	switch x {
   642  	case 0:
   643  		if len(b) < 20 {
   644  			return
   645  		}
   646  		_ = b[:2] // ERROR "Proved IsSliceInBounds$"
   647  	case 1:
   648  		if len(b) < 40 {
   649  			return
   650  		}
   651  		_ = b[:2] // ERROR "Proved IsSliceInBounds$"
   652  	}
   653  }
   654  
   655  // Derived from nat.cmp
   656  func natcmp(x, y []uint) (r int) {
   657  	m := len(x)
   658  	n := len(y)
   659  	if m != n || m == 0 {
   660  		return
   661  	}
   662  
   663  	i := m - 1
   664  	for i > 0 && // ERROR "Induction variable: limits \(0,\?\], increment 1$"
   665  		x[i] == // ERROR "Proved IsInBounds$"
   666  			y[i] { // ERROR "Proved IsInBounds$"
   667  		i--
   668  	}
   669  
   670  	switch {
   671  	case x[i] < // todo, cannot prove this because it's dominated by i<=0 || x[i]==y[i]
   672  		y[i]: // ERROR "Proved IsInBounds$"
   673  		r = -1
   674  	case x[i] > // ERROR "Proved IsInBounds$"
   675  		y[i]: // ERROR "Proved IsInBounds$"
   676  		r = 1
   677  	}
   678  	return
   679  }
   680  
   681  func suffix(s, suffix string) bool {
   682  	// todo, we're still not able to drop the bound check here in the general case
   683  	return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix
   684  }
   685  
   686  func constsuffix(s string) bool {
   687  	return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$"
   688  }
   689  
   690  func atexit(foobar []func()) {
   691  	for i := len(foobar) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1"
   692  		f := foobar[i]
   693  		foobar = foobar[:i] // ERROR "IsSliceInBounds"
   694  		f()
   695  	}
   696  }
   697  
   698  func make1(n int) []int {
   699  	s := make([]int, n)
   700  	for i := 0; i < n; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1"
   701  		s[i] = 1 // ERROR "Proved IsInBounds$"
   702  	}
   703  	return s
   704  }
   705  
   706  func make2(n int) []int {
   707  	s := make([]int, n)
   708  	for i := range s { // ERROR "Induction variable: limits \[0,\?\), increment 1"
   709  		s[i] = 1 // ERROR "Proved IsInBounds$"
   710  	}
   711  	return s
   712  }
   713  
   714  // The range tests below test the index variable of range loops.
   715  
   716  // range1 compiles to the "efficiently indexable" form of a range loop.
   717  func range1(b []int) {
   718  	for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   719  		b[i] = v + 1    // ERROR "Proved IsInBounds$"
   720  		if i < len(b) { // ERROR "Proved Less64$"
   721  			println("x")
   722  		}
   723  		if i >= 0 { // ERROR "Proved Leq64$"
   724  			println("x")
   725  		}
   726  	}
   727  }
   728  
   729  // range2 elements are larger, so they use the general form of a range loop.
   730  func range2(b [][32]int) {
   731  	for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   732  		b[i][0] = v[0] + 1 // ERROR "Proved IsInBounds$"
   733  		if i < len(b) {    // ERROR "Proved Less64$"
   734  			println("x")
   735  		}
   736  		if i >= 0 { // ERROR "Proved Leq64$"
   737  			println("x")
   738  		}
   739  	}
   740  }
   741  
   742  // signhint1-2 test whether the hint (int >= 0) is propagated into the loop.
   743  func signHint1(i int, data []byte) {
   744  	if i >= 0 {
   745  		for i < len(data) { // ERROR "Induction variable: limits \[\?,\?\), increment 1$"
   746  			_ = data[i] // ERROR "Proved IsInBounds$"
   747  			i++
   748  		}
   749  	}
   750  }
   751  
   752  func signHint2(b []byte, n int) {
   753  	if n < 0 {
   754  		panic("")
   755  	}
   756  	_ = b[25]
   757  	for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
   758  		b[i] = 123 // ERROR "Proved IsInBounds$"
   759  	}
   760  }
   761  
   762  // indexGT0 tests whether prove learns int index >= 0 from bounds check.
   763  func indexGT0(b []byte, n int) {
   764  	_ = b[n]
   765  	_ = b[25]
   766  
   767  	for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
   768  		b[i] = 123 // ERROR "Proved IsInBounds$"
   769  	}
   770  }
   771  
   772  // Induction variable in unrolled loop.
   773  func unrollUpExcl(a []int) int {
   774  	var i, x int
   775  	for i = 0; i < len(a)-1; i += 2 { // ERROR "Induction variable: limits \[0,\?\), increment 2$"
   776  		x += a[i] // ERROR "Proved IsInBounds$"
   777  		x += a[i+1]
   778  	}
   779  	if i == len(a)-1 {
   780  		x += a[i]
   781  	}
   782  	return x
   783  }
   784  
   785  // Induction variable in unrolled loop.
   786  func unrollUpIncl(a []int) int {
   787  	var i, x int
   788  	for i = 0; i <= len(a)-2; i += 2 { // ERROR "Induction variable: limits \[0,\?\], increment 2$"
   789  		x += a[i] // ERROR "Proved IsInBounds$"
   790  		x += a[i+1]
   791  	}
   792  	if i == len(a)-1 {
   793  		x += a[i]
   794  	}
   795  	return x
   796  }
   797  
   798  // Induction variable in unrolled loop.
   799  func unrollDownExcl0(a []int) int {
   800  	var i, x int
   801  	for i = len(a) - 1; i > 0; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
   802  		x += a[i]   // ERROR "Proved IsInBounds$"
   803  		x += a[i-1] // ERROR "Proved IsInBounds$"
   804  	}
   805  	if i == 0 {
   806  		x += a[i]
   807  	}
   808  	return x
   809  }
   810  
   811  // Induction variable in unrolled loop.
   812  func unrollDownExcl1(a []int) int {
   813  	var i, x int
   814  	for i = len(a) - 1; i >= 1; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
   815  		x += a[i]   // ERROR "Proved IsInBounds$"
   816  		x += a[i-1] // ERROR "Proved IsInBounds$"
   817  	}
   818  	if i == 0 {
   819  		x += a[i]
   820  	}
   821  	return x
   822  }
   823  
   824  // Induction variable in unrolled loop.
   825  func unrollDownInclStep(a []int) int {
   826  	var i, x int
   827  	for i = len(a); i >= 2; i -= 2 { // ERROR "Induction variable: limits \[2,\?\], increment 2$"
   828  		x += a[i-1] // ERROR "Proved IsInBounds$"
   829  		x += a[i-2] // ERROR "Proved IsInBounds$"
   830  	}
   831  	if i == 1 {
   832  		x += a[i-1]
   833  	}
   834  	return x
   835  }
   836  
   837  // Not an induction variable (step too large)
   838  func unrollExclStepTooLarge(a []int) int {
   839  	var i, x int
   840  	for i = 0; i < len(a)-1; i += 3 {
   841  		x += a[i]
   842  		x += a[i+1]
   843  	}
   844  	if i == len(a)-1 {
   845  		x += a[i]
   846  	}
   847  	return x
   848  }
   849  
   850  // Not an induction variable (step too large)
   851  func unrollInclStepTooLarge(a []int) int {
   852  	var i, x int
   853  	for i = 0; i <= len(a)-2; i += 3 {
   854  		x += a[i]
   855  		x += a[i+1]
   856  	}
   857  	if i == len(a)-1 {
   858  		x += a[i]
   859  	}
   860  	return x
   861  }
   862  
   863  // Not an induction variable (min too small, iterating down)
   864  func unrollDecMin(a []int, b int) int {
   865  	if b != math.MinInt64 {
   866  		return 42
   867  	}
   868  	var i, x int
   869  	for i = len(a); i >= b; i -= 2 { // ERROR "Proved Leq64"
   870  		x += a[i-1]
   871  		x += a[i-2]
   872  	}
   873  	if i == 1 {
   874  		x += a[i-1]
   875  	}
   876  	return x
   877  }
   878  
   879  // Not an induction variable (min too small, iterating up -- perhaps could allow, but why bother?)
   880  func unrollIncMin(a []int, b int) int {
   881  	if b != math.MinInt64 {
   882  		return 42
   883  	}
   884  	var i, x int
   885  	for i = len(a); i >= b; i += 2 { // ERROR "Proved Leq64"
   886  		x += a[i-1]
   887  		x += a[i-2]
   888  	}
   889  	if i == 1 {
   890  		x += a[i-1]
   891  	}
   892  	return x
   893  }
   894  
   895  // The 4 xxxxExtNto64 functions below test whether prove is looking
   896  // through value-preserving sign/zero extensions of index values (issue #26292).
   897  
   898  // Look through all extensions
   899  func signExtNto64(x []int, j8 int8, j16 int16, j32 int32) int {
   900  	if len(x) < 22 {
   901  		return 0
   902  	}
   903  	if j8 >= 0 && j8 < 22 {
   904  		return x[j8] // ERROR "Proved IsInBounds$"
   905  	}
   906  	if j16 >= 0 && j16 < 22 {
   907  		return x[j16] // ERROR "Proved IsInBounds$"
   908  	}
   909  	if j32 >= 0 && j32 < 22 {
   910  		return x[j32] // ERROR "Proved IsInBounds$"
   911  	}
   912  	return 0
   913  }
   914  
   915  func zeroExtNto64(x []int, j8 uint8, j16 uint16, j32 uint32) int {
   916  	if len(x) < 22 {
   917  		return 0
   918  	}
   919  	if j8 >= 0 && j8 < 22 {
   920  		return x[j8] // ERROR "Proved IsInBounds$"
   921  	}
   922  	if j16 >= 0 && j16 < 22 {
   923  		return x[j16] // ERROR "Proved IsInBounds$"
   924  	}
   925  	if j32 >= 0 && j32 < 22 {
   926  		return x[j32] // ERROR "Proved IsInBounds$"
   927  	}
   928  	return 0
   929  }
   930  
   931  // Process fence-post implications through 32to64 extensions (issue #29964)
   932  func signExt32to64Fence(x []int, j int32) int {
   933  	if x[j] != 0 {
   934  		return 1
   935  	}
   936  	if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
   937  		return 1
   938  	}
   939  	return 0
   940  }
   941  
   942  func zeroExt32to64Fence(x []int, j uint32) int {
   943  	if x[j] != 0 {
   944  		return 1
   945  	}
   946  	if j > 0 && x[j-1] != 0 { // ERROR "Proved IsInBounds$"
   947  		return 1
   948  	}
   949  	return 0
   950  }
   951  
   952  // Ensure that bounds checks with negative indexes are not incorrectly removed.
   953  func negIndex() {
   954  	n := make([]int, 1)
   955  	for i := -1; i <= 0; i++ { // ERROR "Induction variable: limits \[-1,0\], increment 1$"
   956  		n[i] = 1
   957  	}
   958  }
   959  func negIndex2(n int) {
   960  	a := make([]int, 5)
   961  	b := make([]int, 5)
   962  	c := make([]int, 5)
   963  	for i := -1; i <= 0; i-- {
   964  		b[i] = i
   965  		n++
   966  		if n > 10 {
   967  			break
   968  		}
   969  	}
   970  	useSlice(a)
   971  	useSlice(c)
   972  }
   973  
   974  // Check that prove is zeroing these right shifts of positive ints by bit-width - 1.
   975  // e.g (Rsh64x64 <t> n (Const64 <typ.UInt64> [63])) && ft.isNonNegative(n) -> 0
   976  func sh64(n int64) int64 {
   977  	if n < 0 {
   978  		return n
   979  	}
   980  	return n >> 63 // ERROR "Proved Rsh64x64 shifts to zero"
   981  }
   982  
   983  func sh32(n int32) int32 {
   984  	if n < 0 {
   985  		return n
   986  	}
   987  	return n >> 31 // ERROR "Proved Rsh32x64 shifts to zero"
   988  }
   989  
   990  func sh32x64(n int32) int32 {
   991  	if n < 0 {
   992  		return n
   993  	}
   994  	return n >> uint64(31) // ERROR "Proved Rsh32x64 shifts to zero"
   995  }
   996  
   997  func sh16(n int16) int16 {
   998  	if n < 0 {
   999  		return n
  1000  	}
  1001  	return n >> 15 // ERROR "Proved Rsh16x64 shifts to zero"
  1002  }
  1003  
  1004  func sh64noopt(n int64) int64 {
  1005  	return n >> 63 // not optimized; n could be negative
  1006  }
  1007  
  1008  // These cases are division of a positive signed integer by a power of 2.
  1009  // The opt pass doesnt have sufficient information to see that n is positive.
  1010  // So, instead, opt rewrites the division with a less-than-optimal replacement.
  1011  // Prove, which can see that n is nonnegative, cannot see the division because
  1012  // opt, an earlier pass, has already replaced it.
  1013  // The fix for this issue allows prove to zero a right shift that was added as
  1014  // part of the less-than-optimal reqwrite. That change by prove then allows
  1015  // lateopt to clean up all the unnecessary parts of the original division
  1016  // replacement. See issue #36159.
  1017  func divShiftClean(n int) int {
  1018  	if n < 0 {
  1019  		return n
  1020  	}
  1021  	return n / int(8) // ERROR "Proved Rsh64x64 shifts to zero"
  1022  }
  1023  
  1024  func divShiftClean64(n int64) int64 {
  1025  	if n < 0 {
  1026  		return n
  1027  	}
  1028  	return n / int64(16) // ERROR "Proved Rsh64x64 shifts to zero"
  1029  }
  1030  
  1031  func divShiftClean32(n int32) int32 {
  1032  	if n < 0 {
  1033  		return n
  1034  	}
  1035  	return n / int32(16) // ERROR "Proved Rsh32x64 shifts to zero"
  1036  }
  1037  
  1038  // Bounds check elimination
  1039  
  1040  func sliceBCE1(p []string, h uint) string {
  1041  	if len(p) == 0 {
  1042  		return ""
  1043  	}
  1044  
  1045  	i := h & uint(len(p)-1)
  1046  	return p[i] // ERROR "Proved IsInBounds$"
  1047  }
  1048  
  1049  func sliceBCE2(p []string, h int) string {
  1050  	if len(p) == 0 {
  1051  		return ""
  1052  	}
  1053  	i := h & (len(p) - 1)
  1054  	return p[i] // ERROR "Proved IsInBounds$"
  1055  }
  1056  
  1057  func and(p []byte) ([]byte, []byte) { // issue #52563
  1058  	const blocksize = 16
  1059  	fullBlocks := len(p) &^ (blocksize - 1)
  1060  	blk := p[:fullBlocks] // ERROR "Proved IsSliceInBounds$"
  1061  	rem := p[fullBlocks:] // ERROR "Proved IsSliceInBounds$"
  1062  	return blk, rem
  1063  }
  1064  
  1065  func rshu(x, y uint) int {
  1066  	z := x >> y
  1067  	if z <= x { // ERROR "Proved Leq64U$"
  1068  		return 1
  1069  	}
  1070  	return 0
  1071  }
  1072  
  1073  func divu(x, y uint) int {
  1074  	z := x / y
  1075  	if z <= x { // ERROR "Proved Leq64U$"
  1076  		return 1
  1077  	}
  1078  	return 0
  1079  }
  1080  
  1081  func modu1(x, y uint) int {
  1082  	z := x % y
  1083  	if z < y { // ERROR "Proved Less64U$"
  1084  		return 1
  1085  	}
  1086  	return 0
  1087  }
  1088  
  1089  func modu2(x, y uint) int {
  1090  	z := x % y
  1091  	if z <= x { // ERROR "Proved Leq64U$"
  1092  		return 1
  1093  	}
  1094  	return 0
  1095  }
  1096  
  1097  func issue57077(s []int) (left, right []int) {
  1098  	middle := len(s) / 2
  1099  	left = s[:middle]  // ERROR "Proved IsSliceInBounds$"
  1100  	right = s[middle:] // ERROR "Proved IsSliceInBounds$"
  1101  	return
  1102  }
  1103  
  1104  func issue51622(b []byte) int {
  1105  	if len(b) >= 3 && b[len(b)-3] == '#' { // ERROR "Proved IsInBounds$"
  1106  		return len(b)
  1107  	}
  1108  	return 0
  1109  }
  1110  
  1111  func issue45928(x int) {
  1112  	combinedFrac := x / (x | (1 << 31)) // ERROR "Proved Neq64$"
  1113  	useInt(combinedFrac)
  1114  }
  1115  
  1116  func constantBounds1(i, j uint) int {
  1117  	var a [10]int
  1118  	if j < 11 && i < j {
  1119  		return a[i] // ERROR "Proved IsInBounds$"
  1120  	}
  1121  	return 0
  1122  }
  1123  
  1124  func constantBounds2(i, j uint) int {
  1125  	var a [10]int
  1126  	if i < j && j < 11 {
  1127  		return a[i] // ERROR "Proved IsInBounds"
  1128  	}
  1129  	return 0
  1130  }
  1131  
  1132  func constantBounds3(i, j, k, l uint) int {
  1133  	var a [8]int
  1134  	if i < j && j < k && k < l && l < 11 {
  1135  		return a[i] // ERROR "Proved IsInBounds"
  1136  	}
  1137  	return 0
  1138  }
  1139  
  1140  func equalityPropagation(a [1]int, i, j uint) int {
  1141  	if i == j && i == 5 {
  1142  		return a[j-5] // ERROR "Proved IsInBounds"
  1143  	}
  1144  	return 0
  1145  }
  1146  func inequalityPropagation(a [1]int, i, j uint) int {
  1147  	if i != j && j >= 5 && j <= 6 && i == 5 {
  1148  		return a[j-6] // ERROR "Proved IsInBounds"
  1149  	}
  1150  	return 0
  1151  }
  1152  
  1153  func issue66826a(a [21]byte) {
  1154  	for i := 0; i <= 10; i++ { // ERROR "Induction variable: limits \[0,10\], increment 1$"
  1155  		_ = a[2*i] // ERROR "Proved IsInBounds"
  1156  	}
  1157  }
  1158  func issue66826b(a [31]byte, i int) {
  1159  	if i < 0 || i > 10 {
  1160  		return
  1161  	}
  1162  	_ = a[3*i] // ERROR "Proved IsInBounds"
  1163  }
  1164  
  1165  func f20(a, b bool) int {
  1166  	if a == b {
  1167  		if a {
  1168  			if b { // ERROR "Proved Arg"
  1169  				return 1
  1170  			}
  1171  		}
  1172  	}
  1173  	return 0
  1174  }
  1175  
  1176  func f21(a, b *int) int {
  1177  	if a == b {
  1178  		if a != nil {
  1179  			if b != nil { // ERROR "Proved IsNonNil"
  1180  				return 1
  1181  			}
  1182  		}
  1183  	}
  1184  	return 0
  1185  }
  1186  
  1187  func f22(b bool, x, y int) int {
  1188  	b2 := x < y
  1189  	if b == b2 {
  1190  		if b {
  1191  			if x >= y { // ERROR "Disproved Leq64$"
  1192  				return 1
  1193  			}
  1194  		}
  1195  	}
  1196  	return 0
  1197  }
  1198  
  1199  func ctz64(x uint64, ensureBothBranchesCouldHappen bool) int {
  1200  	const max = math.MaxUint64
  1201  	sz := bits.Len64(max)
  1202  
  1203  	log2half := uint64(max) >> (sz / 2)
  1204  	if x >= log2half || x == 0 {
  1205  		return 42
  1206  	}
  1207  
  1208  	y := bits.TrailingZeros64(x) // ERROR "Proved Ctz64 non-zero$""
  1209  
  1210  	z := sz / 2
  1211  	if ensureBothBranchesCouldHappen {
  1212  		if y < z { // ERROR "Proved Less64$"
  1213  			return -42
  1214  		}
  1215  	} else {
  1216  		if y >= z { // ERROR "Disproved Leq64$"
  1217  			return 1337
  1218  		}
  1219  	}
  1220  
  1221  	return y
  1222  }
  1223  func ctz32(x uint32, ensureBothBranchesCouldHappen bool) int {
  1224  	const max = math.MaxUint32
  1225  	sz := bits.Len32(max)
  1226  
  1227  	log2half := uint32(max) >> (sz / 2)
  1228  	if x >= log2half || x == 0 {
  1229  		return 42
  1230  	}
  1231  
  1232  	y := bits.TrailingZeros32(x) // ERROR "Proved Ctz32 non-zero$""
  1233  
  1234  	z := sz / 2
  1235  	if ensureBothBranchesCouldHappen {
  1236  		if y < z { // ERROR "Proved Less64$"
  1237  			return -42
  1238  		}
  1239  	} else {
  1240  		if y >= z { // ERROR "Disproved Leq64$"
  1241  			return 1337
  1242  		}
  1243  	}
  1244  
  1245  	return y
  1246  }
  1247  func ctz16(x uint16, ensureBothBranchesCouldHappen bool) int {
  1248  	const max = math.MaxUint16
  1249  	sz := bits.Len16(max)
  1250  
  1251  	log2half := uint16(max) >> (sz / 2)
  1252  	if x >= log2half || x == 0 {
  1253  		return 42
  1254  	}
  1255  
  1256  	y := bits.TrailingZeros16(x) // ERROR "Proved Ctz16 non-zero$""
  1257  
  1258  	z := sz / 2
  1259  	if ensureBothBranchesCouldHappen {
  1260  		if y < z { // ERROR "Proved Less64$"
  1261  			return -42
  1262  		}
  1263  	} else {
  1264  		if y >= z { // ERROR "Disproved Leq64$"
  1265  			return 1337
  1266  		}
  1267  	}
  1268  
  1269  	return y
  1270  }
  1271  func ctz8(x uint8, ensureBothBranchesCouldHappen bool) int {
  1272  	const max = math.MaxUint8
  1273  	sz := bits.Len8(max)
  1274  
  1275  	log2half := uint8(max) >> (sz / 2)
  1276  	if x >= log2half || x == 0 {
  1277  		return 42
  1278  	}
  1279  
  1280  	y := bits.TrailingZeros8(x) // ERROR "Proved Ctz8 non-zero$""
  1281  
  1282  	z := sz / 2
  1283  	if ensureBothBranchesCouldHappen {
  1284  		if y < z { // ERROR "Proved Less64$"
  1285  			return -42
  1286  		}
  1287  	} else {
  1288  		if y >= z { // ERROR "Disproved Leq64$"
  1289  			return 1337
  1290  		}
  1291  	}
  1292  
  1293  	return y
  1294  }
  1295  
  1296  func bitLen64(x uint64, ensureBothBranchesCouldHappen bool) int {
  1297  	const max = math.MaxUint64
  1298  	sz := bits.Len64(max)
  1299  
  1300  	if x >= max>>3 {
  1301  		return 42
  1302  	}
  1303  	if x <= max>>6 {
  1304  		return 42
  1305  	}
  1306  
  1307  	y := bits.Len64(x)
  1308  
  1309  	if ensureBothBranchesCouldHappen {
  1310  		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
  1311  			return -42
  1312  		}
  1313  	} else {
  1314  		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
  1315  			return 1337
  1316  		}
  1317  	}
  1318  	return y
  1319  }
  1320  func bitLen32(x uint32, ensureBothBranchesCouldHappen bool) int {
  1321  	const max = math.MaxUint32
  1322  	sz := bits.Len32(max)
  1323  
  1324  	if x >= max>>3 {
  1325  		return 42
  1326  	}
  1327  	if x <= max>>6 {
  1328  		return 42
  1329  	}
  1330  
  1331  	y := bits.Len32(x)
  1332  
  1333  	if ensureBothBranchesCouldHappen {
  1334  		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
  1335  			return -42
  1336  		}
  1337  	} else {
  1338  		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
  1339  			return 1337
  1340  		}
  1341  	}
  1342  	return y
  1343  }
  1344  func bitLen16(x uint16, ensureBothBranchesCouldHappen bool) int {
  1345  	const max = math.MaxUint16
  1346  	sz := bits.Len16(max)
  1347  
  1348  	if x >= max>>3 {
  1349  		return 42
  1350  	}
  1351  	if x <= max>>6 {
  1352  		return 42
  1353  	}
  1354  
  1355  	y := bits.Len16(x)
  1356  
  1357  	if ensureBothBranchesCouldHappen {
  1358  		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
  1359  			return -42
  1360  		}
  1361  	} else {
  1362  		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
  1363  			return 1337
  1364  		}
  1365  	}
  1366  	return y
  1367  }
  1368  func bitLen8(x uint8, ensureBothBranchesCouldHappen bool) int {
  1369  	const max = math.MaxUint8
  1370  	sz := bits.Len8(max)
  1371  
  1372  	if x >= max>>3 {
  1373  		return 42
  1374  	}
  1375  	if x <= max>>6 {
  1376  		return 42
  1377  	}
  1378  
  1379  	y := bits.Len8(x)
  1380  
  1381  	if ensureBothBranchesCouldHappen {
  1382  		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
  1383  			return -42
  1384  		}
  1385  	} else {
  1386  		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
  1387  			return 1337
  1388  		}
  1389  	}
  1390  	return y
  1391  }
  1392  
  1393  func xor64(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1394  	a &= 0xff
  1395  	b &= 0xfff
  1396  
  1397  	z := a ^ b
  1398  
  1399  	if ensureBothBranchesCouldHappen {
  1400  		if z > 0xfff { // ERROR "Disproved Less64U$"
  1401  			return 42
  1402  		}
  1403  	} else {
  1404  		if z <= 0xfff { // ERROR "Proved Leq64U$"
  1405  			return 1337
  1406  		}
  1407  	}
  1408  	return int(z)
  1409  }
  1410  
  1411  func or64(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1412  	a &= 0xff
  1413  	b &= 0xfff
  1414  
  1415  	z := a | b
  1416  
  1417  	if ensureBothBranchesCouldHappen {
  1418  		if z > 0xfff { // ERROR "Disproved Less64U$"
  1419  			return 42
  1420  		}
  1421  	} else {
  1422  		if z <= 0xfff { // ERROR "Proved Leq64U$"
  1423  			return 1337
  1424  		}
  1425  	}
  1426  	return int(z)
  1427  }
  1428  
  1429  func mod64uWithSmallerDividendMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1430  	a &= 0xff
  1431  	b &= 0xfff
  1432  
  1433  	z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
  1434  
  1435  	if ensureBothBranchesCouldHappen {
  1436  		if z > bits.Len64(0xff) { // ERROR "Disproved Less64$"
  1437  			return 42
  1438  		}
  1439  	} else {
  1440  		if z <= bits.Len64(0xff) { // ERROR "Proved Leq64$"
  1441  			return 1337
  1442  		}
  1443  	}
  1444  	return z
  1445  }
  1446  func mod64uWithSmallerDivisorMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1447  	a &= 0xfff
  1448  	b &= 0x10 // we need bits.Len64(b.umax) != bits.Len64(b.umax-1)
  1449  
  1450  	z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
  1451  
  1452  	if ensureBothBranchesCouldHappen {
  1453  		if z > bits.Len64(0x10-1) { // ERROR "Disproved Less64$"
  1454  			return 42
  1455  		}
  1456  	} else {
  1457  		if z <= bits.Len64(0x10-1) { // ERROR "Proved Leq64$"
  1458  			return 1337
  1459  		}
  1460  	}
  1461  	return z
  1462  }
  1463  func mod64uWithIdenticalMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1464  	a &= 0x10
  1465  	b &= 0x10 // we need bits.Len64(b.umax) != bits.Len64(b.umax-1)
  1466  
  1467  	z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
  1468  
  1469  	if ensureBothBranchesCouldHappen {
  1470  		if z > bits.Len64(0x10-1) { // ERROR "Disproved Less64$"
  1471  			return 42
  1472  		}
  1473  	} else {
  1474  		if z <= bits.Len64(0x10-1) { // ERROR "Proved Leq64$"
  1475  			return 1337
  1476  		}
  1477  	}
  1478  	return z
  1479  }
  1480  func mod64sPositiveWithSmallerDividendMax(a, b int64, ensureBothBranchesCouldHappen bool) int64 {
  1481  	if a < 0 || b < 0 {
  1482  		return 42
  1483  	}
  1484  	a &= 0xff
  1485  	b &= 0xfff
  1486  
  1487  	z := a % b // ERROR "Proved Mod64 does not need fix-up$"
  1488  
  1489  	if ensureBothBranchesCouldHappen {
  1490  		if z > 0xff { // ERROR "Disproved Less64$"
  1491  			return 42
  1492  		}
  1493  	} else {
  1494  		if z <= 0xff { // ERROR "Proved Leq64$"
  1495  			return 1337
  1496  		}
  1497  	}
  1498  	return z
  1499  }
  1500  func mod64sPositiveWithSmallerDivisorMax(a, b int64, ensureBothBranchesCouldHappen bool) int64 {
  1501  	if a < 0 || b < 0 {
  1502  		return 42
  1503  	}
  1504  	a &= 0xfff
  1505  	b &= 0xff
  1506  
  1507  	z := a % b // ERROR "Proved Mod64 does not need fix-up$"
  1508  
  1509  	if ensureBothBranchesCouldHappen {
  1510  		if z > 0xff-1 { // ERROR "Disproved Less64$"
  1511  			return 42
  1512  		}
  1513  	} else {
  1514  		if z <= 0xff-1 { // ERROR "Proved Leq64$"
  1515  			return 1337
  1516  		}
  1517  	}
  1518  	return z
  1519  }
  1520  func mod64sPositiveWithIdenticalMax(a, b int64, ensureBothBranchesCouldHappen bool) int64 {
  1521  	if a < 0 || b < 0 {
  1522  		return 42
  1523  	}
  1524  	a &= 0xfff
  1525  	b &= 0xfff
  1526  
  1527  	z := a % b // ERROR "Proved Mod64 does not need fix-up$"
  1528  
  1529  	if ensureBothBranchesCouldHappen {
  1530  		if z > 0xfff-1 { // ERROR "Disproved Less64$"
  1531  			return 42
  1532  		}
  1533  	} else {
  1534  		if z <= 0xfff-1 { // ERROR "Proved Leq64$"
  1535  			return 1337
  1536  		}
  1537  	}
  1538  	return z
  1539  }
  1540  
  1541  func div64u(a, b uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
  1542  	a &= 0xffff
  1543  	a |= 0xfff
  1544  	b &= 0xff
  1545  	b |= 0xf
  1546  
  1547  	z := a / b // ERROR "Proved Neq64$"
  1548  
  1549  	if ensureAllBranchesCouldHappen() && z > 0xffff/0xf { // ERROR "Disproved Less64U$"
  1550  		return 42
  1551  	}
  1552  	if ensureAllBranchesCouldHappen() && z <= 0xffff/0xf { // ERROR "Proved Leq64U$"
  1553  		return 1337
  1554  	}
  1555  	if ensureAllBranchesCouldHappen() && z < 0xfff/0xff { // ERROR "Disproved Less64U$"
  1556  		return 42
  1557  	}
  1558  	if ensureAllBranchesCouldHappen() && z >= 0xfff/0xff { // ERROR "Proved Leq64U$"
  1559  		return 42
  1560  	}
  1561  	return z
  1562  }
  1563  func div64s(a, b int64, ensureAllBranchesCouldHappen func() bool) int64 {
  1564  	if a < 0 || b < 0 {
  1565  		return 42
  1566  	}
  1567  	a &= 0xffff
  1568  	a |= 0xfff
  1569  	b &= 0xff
  1570  	b |= 0xf
  1571  
  1572  	z := a / b // ERROR "(Proved Div64 does not need fix-up|Proved Neq64)$"
  1573  
  1574  	if ensureAllBranchesCouldHappen() && z > 0xffff/0xf { // ERROR "Disproved Less64$"
  1575  		return 42
  1576  	}
  1577  	if ensureAllBranchesCouldHappen() && z <= 0xffff/0xf { // ERROR "Proved Leq64$"
  1578  		return 1337
  1579  	}
  1580  	if ensureAllBranchesCouldHappen() && z < 0xfff/0xff { // ERROR "Disproved Less64$"
  1581  		return 42
  1582  	}
  1583  	if ensureAllBranchesCouldHappen() && z >= 0xfff/0xff { // ERROR "Proved Leq64$"
  1584  		return 42
  1585  	}
  1586  	return z
  1587  }
  1588  
  1589  func trunc64to16(a uint64, ensureAllBranchesCouldHappen func() bool) uint16 {
  1590  	a &= 0xfff
  1591  	a |= 0xff
  1592  
  1593  	z := uint16(a)
  1594  	if ensureAllBranchesCouldHappen() && z > 0xfff { // ERROR "Disproved Less16U$"
  1595  		return 42
  1596  	}
  1597  	if ensureAllBranchesCouldHappen() && z <= 0xfff { // ERROR "Proved Leq16U$"
  1598  		return 1337
  1599  	}
  1600  	if ensureAllBranchesCouldHappen() && z < 0xff { // ERROR "Disproved Less16U$"
  1601  		return 42
  1602  	}
  1603  	if ensureAllBranchesCouldHappen() && z >= 0xff { // ERROR "Proved Leq16U$"
  1604  		return 1337
  1605  	}
  1606  	return z
  1607  }
  1608  
  1609  func com64(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
  1610  	a &= 0xffff
  1611  	a |= 0xff
  1612  
  1613  	z := ^a
  1614  
  1615  	if ensureAllBranchesCouldHappen() && z > ^uint64(0xff) { // ERROR "Disproved Less64U$"
  1616  		return 42
  1617  	}
  1618  	if ensureAllBranchesCouldHappen() && z <= ^uint64(0xff) { // ERROR "Proved Leq64U$"
  1619  		return 1337
  1620  	}
  1621  	if ensureAllBranchesCouldHappen() && z < ^uint64(0xffff) { // ERROR "Disproved Less64U$"
  1622  		return 42
  1623  	}
  1624  	if ensureAllBranchesCouldHappen() && z >= ^uint64(0xffff) { // ERROR "Proved Leq64U$"
  1625  		return 1337
  1626  	}
  1627  	return z
  1628  }
  1629  
  1630  func neg64(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
  1631  	var lo, hi uint64 = 0xff, 0xfff
  1632  	a &= hi
  1633  	a |= lo
  1634  
  1635  	z := -a
  1636  
  1637  	if ensureAllBranchesCouldHappen() && z > -lo { // ERROR "Disproved Less64U$"
  1638  		return 42
  1639  	}
  1640  	if ensureAllBranchesCouldHappen() && z <= -lo { // ERROR "Proved Leq64U$"
  1641  		return 1337
  1642  	}
  1643  	if ensureAllBranchesCouldHappen() && z < -hi { // ERROR "Disproved Less64U$"
  1644  		return 42
  1645  	}
  1646  	if ensureAllBranchesCouldHappen() && z >= -hi { // ERROR "Proved Leq64U$"
  1647  		return 1337
  1648  	}
  1649  	return z
  1650  }
  1651  func neg64mightOverflowDuringNeg(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
  1652  	var lo, hi uint64 = 0, 0xfff
  1653  	a &= hi
  1654  	a |= lo
  1655  
  1656  	z := -a
  1657  
  1658  	if ensureAllBranchesCouldHappen() && z > -lo {
  1659  		return 42
  1660  	}
  1661  	if ensureAllBranchesCouldHappen() && z <= -lo {
  1662  		return 1337
  1663  	}
  1664  	if ensureAllBranchesCouldHappen() && z < -hi {
  1665  		return 42
  1666  	}
  1667  	if ensureAllBranchesCouldHappen() && z >= -hi {
  1668  		return 1337
  1669  	}
  1670  	return z
  1671  }
  1672  
  1673  func phiMin(a, b []byte) {
  1674  	_ = a[:min(len(a), len(b))] // ERROR "Proved IsSliceInBounds"
  1675  	_ = b[:min(len(a), len(b))] // ERROR "Proved IsSliceInBounds"
  1676  	_ = a[:max(len(a), len(b))]
  1677  	_ = b[:max(len(a), len(b))]
  1678  	x := len(a)
  1679  	if x > len(b) {
  1680  		x = len(b)
  1681  		useInt(0)
  1682  	}
  1683  	_ = a[:x] // ERROR "Proved IsSliceInBounds"
  1684  	y := len(a)
  1685  	if y > len(b) {
  1686  		y = len(b)
  1687  		useInt(0)
  1688  	} else {
  1689  		useInt(1)
  1690  	}
  1691  	_ = b[:y] // ERROR "Proved IsSliceInBounds"
  1692  }
  1693  
  1694  func issue16833(a, b []byte) {
  1695  	n := copy(a, b)
  1696  	_ = a[n:] // ERROR "Proved IsSliceInBounds"
  1697  	_ = b[n:] // ERROR "Proved IsSliceInBounds"
  1698  	_ = a[:n] // ERROR "Proved IsSliceInBounds"
  1699  	_ = b[:n] // ERROR "Proved IsSliceInBounds"
  1700  }
  1701  
  1702  func clampedIdx1(x []int, i int) int {
  1703  	if len(x) == 0 {
  1704  		return 0
  1705  	}
  1706  	return x[min(max(0, i), len(x)-1)] // ERROR "Proved IsInBounds"
  1707  }
  1708  func clampedIdx2(x []int, i int) int {
  1709  	if len(x) == 0 {
  1710  		return 0
  1711  	}
  1712  	return x[max(min(i, len(x)-1), 0)] // TODO: can't get rid of this bounds check yet
  1713  }
  1714  
  1715  //go:noinline
  1716  func useInt(a int) {
  1717  }
  1718  
  1719  //go:noinline
  1720  func useSlice(a []int) {
  1721  }
  1722  
  1723  func main() {
  1724  }
  1725  

View as plain text