Source file test/prove.go

     1  // errorcheck -0 -d=ssa/prove/debug=1
     2  
     3  //go:build amd64 || arm64
     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  	b := a[:n>>1] // ERROR "(Proved IsSliceInBounds|Proved Rsh64x64 is unsigned)$"
   257  	// We optimize comparisons with small constant strings (see cmd/compile/internal/gc/walk.go),
   258  	// so this string literal must be long.
   259  	if b == "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" {
   260  		return 0
   261  	}
   262  	return 1
   263  }
   264  
   265  func f11a(a []int, i int) {
   266  	useInt(a[i])
   267  	useInt(a[i]) // ERROR "Proved IsInBounds$"
   268  }
   269  
   270  func f11b(a []int, i int) {
   271  	useSlice(a[i:])
   272  	useSlice(a[i:]) // ERROR "Proved IsSliceInBounds$"
   273  }
   274  
   275  func f11c(a []int, i int) {
   276  	useSlice(a[:i])
   277  	useSlice(a[:i]) // ERROR "Proved IsSliceInBounds$"
   278  }
   279  
   280  func f11d(a []int, i int) {
   281  	useInt(a[2*i+7])
   282  	useInt(a[2*i+7]) // ERROR "Proved IsInBounds$"
   283  }
   284  
   285  func f12(a []int, b int) {
   286  	useSlice(a[:b])
   287  }
   288  
   289  func f13a(a, b, c int, x bool) int {
   290  	if a > 12 {
   291  		if x {
   292  			if a < 12 { // ERROR "Disproved Less64$"
   293  				return 1
   294  			}
   295  		}
   296  		if x {
   297  			if a <= 12 { // ERROR "Disproved Leq64$"
   298  				return 2
   299  			}
   300  		}
   301  		if x {
   302  			if a == 12 { // ERROR "Disproved Eq64$"
   303  				return 3
   304  			}
   305  		}
   306  		if x {
   307  			if a >= 12 { // ERROR "Proved Leq64$"
   308  				return 4
   309  			}
   310  		}
   311  		if x {
   312  			if a > 12 { // ERROR "Proved Less64$"
   313  				return 5
   314  			}
   315  		}
   316  		return 6
   317  	}
   318  	return 0
   319  }
   320  
   321  func f13b(a int, x bool) int {
   322  	if a == -9 {
   323  		if x {
   324  			if a < -9 { // ERROR "Disproved Less64$"
   325  				return 7
   326  			}
   327  		}
   328  		if x {
   329  			if a <= -9 { // ERROR "Proved Leq64$"
   330  				return 8
   331  			}
   332  		}
   333  		if x {
   334  			if a == -9 { // ERROR "Proved Eq64$"
   335  				return 9
   336  			}
   337  		}
   338  		if x {
   339  			if a >= -9 { // ERROR "Proved Leq64$"
   340  				return 10
   341  			}
   342  		}
   343  		if x {
   344  			if a > -9 { // ERROR "Disproved Less64$"
   345  				return 11
   346  			}
   347  		}
   348  		return 12
   349  	}
   350  	return 0
   351  }
   352  
   353  func f13c(a int, x bool) int {
   354  	if a < 90 {
   355  		if x {
   356  			if a < 90 { // ERROR "Proved Less64$"
   357  				return 13
   358  			}
   359  		}
   360  		if x {
   361  			if a <= 90 { // ERROR "Proved Leq64$"
   362  				return 14
   363  			}
   364  		}
   365  		if x {
   366  			if a == 90 { // ERROR "Disproved Eq64$"
   367  				return 15
   368  			}
   369  		}
   370  		if x {
   371  			if a >= 90 { // ERROR "Disproved Leq64$"
   372  				return 16
   373  			}
   374  		}
   375  		if x {
   376  			if a > 90 { // ERROR "Disproved Less64$"
   377  				return 17
   378  			}
   379  		}
   380  		return 18
   381  	}
   382  	return 0
   383  }
   384  
   385  func f13d(a int) int {
   386  	if a < 5 {
   387  		if a < 9 { // ERROR "Proved Less64$"
   388  			return 1
   389  		}
   390  	}
   391  	return 0
   392  }
   393  
   394  func f13e(a int) int {
   395  	if a > 9 {
   396  		if a > 5 { // ERROR "Proved Less64$"
   397  			return 1
   398  		}
   399  	}
   400  	return 0
   401  }
   402  
   403  func f13f(a, b int64) int64 {
   404  	if b != math.MaxInt64 {
   405  		return 42
   406  	}
   407  	if a > b { // ERROR "Disproved Less64$"
   408  		if a == 0 {
   409  			return 1
   410  		}
   411  	}
   412  	return 0
   413  }
   414  
   415  func f13g(a int) int {
   416  	if a < 3 {
   417  		return 5
   418  	}
   419  	if a > 3 {
   420  		return 6
   421  	}
   422  	if a == 3 { // ERROR "Proved Eq64$"
   423  		return 7
   424  	}
   425  	return 8
   426  }
   427  
   428  func f13h(a int) int {
   429  	if a < 3 {
   430  		if a > 1 {
   431  			if a == 2 { // ERROR "Proved Eq64$"
   432  				return 5
   433  			}
   434  		}
   435  	}
   436  	return 0
   437  }
   438  
   439  func f13i(a uint) int {
   440  	if a == 0 {
   441  		return 1
   442  	}
   443  	if a > 0 { // ERROR "Proved Less64U$"
   444  		return 2
   445  	}
   446  	return 3
   447  }
   448  
   449  func f14(p, q *int, a []int) {
   450  	// This crazy ordering usually gives i1 the lowest value ID,
   451  	// j the middle value ID, and i2 the highest value ID.
   452  	// That used to confuse CSE because it ordered the args
   453  	// of the two + ops below differently.
   454  	// That in turn foiled bounds check elimination.
   455  	i1 := *p
   456  	j := *q
   457  	i2 := *p
   458  	useInt(a[i1+j])
   459  	useInt(a[i2+j]) // ERROR "Proved IsInBounds$"
   460  }
   461  
   462  func f15(s []int, x int) {
   463  	useSlice(s[x:])
   464  	useSlice(s[:x]) // ERROR "Proved IsSliceInBounds$"
   465  }
   466  
   467  func f16(s []int) []int {
   468  	if len(s) >= 10 {
   469  		return s[:10] // ERROR "Proved IsSliceInBounds$"
   470  	}
   471  	return nil
   472  }
   473  
   474  func f17(b []int) {
   475  	for i := 0; i < len(b); i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   476  		// This tests for i <= cap, which we can only prove
   477  		// using the derived relation between len and cap.
   478  		// This depends on finding the contradiction, since we
   479  		// don't query this condition directly.
   480  		useSlice(b[:i]) // ERROR "Proved IsSliceInBounds$"
   481  	}
   482  }
   483  
   484  func f18(b []int, x int, y uint) {
   485  	_ = b[x]
   486  	_ = b[y]
   487  
   488  	if x > len(b) { // ERROR "Disproved Less64$"
   489  		return
   490  	}
   491  	if y > uint(len(b)) { // ERROR "Disproved Less64U$"
   492  		return
   493  	}
   494  	if int(y) > len(b) { // ERROR "Disproved Less64$"
   495  		return
   496  	}
   497  }
   498  
   499  func f19() (e int64, err error) {
   500  	// Issue 29502: slice[:0] is incorrectly disproved.
   501  	var stack []int64
   502  	stack = append(stack, 123)
   503  	if len(stack) > 1 {
   504  		panic("too many elements")
   505  	}
   506  	last := len(stack) - 1
   507  	e = stack[last]
   508  	// Buggy compiler prints "Disproved Leq64" for the next line.
   509  	stack = stack[:last]
   510  	return e, nil
   511  }
   512  
   513  func sm1(b []int, x int) {
   514  	// Test constant argument to slicemask.
   515  	useSlice(b[2:8]) // optimized away earlier by rewrite
   516  	// Test non-constant argument with known limits.
   517  	if cap(b) > 10 {
   518  		useSlice(b[2:]) // ERROR "Proved slicemask not needed$"
   519  	}
   520  }
   521  
   522  func lim1(x, y, z int) {
   523  	// Test relations between signed and unsigned limits.
   524  	if x > 5 {
   525  		if uint(x) > 5 { // ERROR "Proved Less64U$"
   526  			return
   527  		}
   528  	}
   529  	if y >= 0 && y < 4 {
   530  		if uint(y) > 4 { // ERROR "Disproved Less64U$"
   531  			return
   532  		}
   533  		if uint(y) < 5 { // ERROR "Proved Less64U$"
   534  			return
   535  		}
   536  	}
   537  	if z < 4 {
   538  		if uint(z) > 4 { // Not provable without disjunctions.
   539  			return
   540  		}
   541  	}
   542  }
   543  
   544  // fence1–4 correspond to the four fence-post implications.
   545  
   546  func fence1(b []int, x, y int) {
   547  	// Test proofs that rely on fence-post implications.
   548  	if x+1 > y {
   549  		if x < y { // ERROR "Disproved Less64$"
   550  			return
   551  		}
   552  	}
   553  	if len(b) < cap(b) {
   554  		// This eliminates the growslice path.
   555  		b = append(b, 1) // ERROR "Disproved Less64U$"
   556  	}
   557  }
   558  
   559  func fence2(x, y int) {
   560  	if x-1 < y {
   561  		if x > y { // ERROR "Disproved Less64$"
   562  			return
   563  		}
   564  	}
   565  }
   566  
   567  func fence3(b, c []int, x, y int64) {
   568  	if x-1 >= y {
   569  		if x <= y { // Can't prove because x may have wrapped.
   570  			return
   571  		}
   572  	}
   573  
   574  	if x != math.MinInt64 && x-1 >= y {
   575  		if x <= y { // ERROR "Disproved Leq64$"
   576  			return
   577  		}
   578  	}
   579  
   580  	c[len(c)-1] = 0 // Can't prove because len(c) might be 0
   581  
   582  	if n := len(b); n > 0 {
   583  		b[n-1] = 0 // ERROR "Proved IsInBounds$"
   584  	}
   585  }
   586  
   587  func fence4(x, y int64) {
   588  	if x >= y+1 {
   589  		if x <= y {
   590  			return
   591  		}
   592  	}
   593  	if y != math.MaxInt64 && x >= y+1 {
   594  		if x <= y { // ERROR "Disproved Leq64$"
   595  			return
   596  		}
   597  	}
   598  }
   599  
   600  // Check transitive relations
   601  func trans1(x, y int64) {
   602  	if x > 5 {
   603  		if y > x {
   604  			if y > 2 { // ERROR "Proved Less64$"
   605  				return
   606  			}
   607  		} else if y == x {
   608  			if y > 5 { // ERROR "Proved Less64$"
   609  				return
   610  			}
   611  		}
   612  	}
   613  	if x >= 10 {
   614  		if y > x {
   615  			if y > 10 { // ERROR "Proved Less64$"
   616  				return
   617  			}
   618  		}
   619  	}
   620  }
   621  
   622  func trans2(a, b []int, i int) {
   623  	if len(a) != len(b) {
   624  		return
   625  	}
   626  
   627  	_ = a[i]
   628  	_ = b[i] // ERROR "Proved IsInBounds$"
   629  }
   630  
   631  func trans3(a, b []int, i int) {
   632  	if len(a) > len(b) {
   633  		return
   634  	}
   635  
   636  	_ = a[i]
   637  	_ = b[i] // ERROR "Proved IsInBounds$"
   638  }
   639  
   640  func trans4(b []byte, x int) {
   641  	// Issue #42603: slice len/cap transitive relations.
   642  	switch x {
   643  	case 0:
   644  		if len(b) < 20 {
   645  			return
   646  		}
   647  		_ = b[:2] // ERROR "Proved IsSliceInBounds$"
   648  	case 1:
   649  		if len(b) < 40 {
   650  			return
   651  		}
   652  		_ = b[:2] // ERROR "Proved IsSliceInBounds$"
   653  	}
   654  }
   655  
   656  // Derived from nat.cmp
   657  func natcmp(x, y []uint) (r int) {
   658  	m := len(x)
   659  	n := len(y)
   660  	if m != n || m == 0 {
   661  		return
   662  	}
   663  
   664  	i := m - 1
   665  	for i > 0 && // ERROR "Induction variable: limits \(0,\?\], increment 1$"
   666  		x[i] == // ERROR "Proved IsInBounds$"
   667  			y[i] { // ERROR "Proved IsInBounds$"
   668  		i--
   669  	}
   670  
   671  	switch {
   672  	case x[i] < // todo, cannot prove this because it's dominated by i<=0 || x[i]==y[i]
   673  		y[i]: // ERROR "Proved IsInBounds$"
   674  		r = -1
   675  	case x[i] > // ERROR "Proved IsInBounds$"
   676  		y[i]: // ERROR "Proved IsInBounds$"
   677  		r = 1
   678  	}
   679  	return
   680  }
   681  
   682  func suffix(s, suffix string) bool {
   683  	// Note: issue 76304
   684  	return len(s) >= len(suffix) && s[len(s)-len(suffix):] == suffix // ERROR "Proved IsSliceInBounds"
   685  }
   686  
   687  func constsuffix(s string) bool {
   688  	return suffix(s, "abc") // ERROR "Proved IsSliceInBounds$" "Proved slicemask not needed$" "Proved Eq64$"
   689  }
   690  
   691  func atexit(foobar []func()) {
   692  	for i := len(foobar) - 1; i >= 0; i-- { // ERROR "Induction variable: limits \[0,\?\], increment 1"
   693  		f := foobar[i]
   694  		foobar = foobar[:i] // ERROR "IsSliceInBounds"
   695  		f()
   696  	}
   697  }
   698  
   699  func make1(n int) []int {
   700  	s := make([]int, n)
   701  	for i := 0; i < n; i++ { // ERROR "Induction variable: limits \[0,\?\), increment 1"
   702  		s[i] = 1 // ERROR "Proved IsInBounds$"
   703  	}
   704  	return s
   705  }
   706  
   707  func make2(n int) []int {
   708  	s := make([]int, n)
   709  	for i := range s { // ERROR "Induction variable: limits \[0,\?\), increment 1"
   710  		s[i] = 1 // ERROR "Proved IsInBounds$"
   711  	}
   712  	return s
   713  }
   714  
   715  // The range tests below test the index variable of range loops.
   716  
   717  // range1 compiles to the "efficiently indexable" form of a range loop.
   718  func range1(b []int) {
   719  	for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   720  		b[i] = v + 1    // ERROR "Proved IsInBounds$"
   721  		if i < len(b) { // ERROR "Proved Less64$"
   722  			println("x")
   723  		}
   724  		if i >= 0 { // ERROR "Proved Leq64$"
   725  			println("x")
   726  		}
   727  	}
   728  }
   729  
   730  // range2 elements are larger, so they use the general form of a range loop.
   731  func range2(b [][32]int) {
   732  	for i, v := range b { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
   733  		b[i][0] = v[0] + 1 // ERROR "Proved IsInBounds$"
   734  		if i < len(b) {    // ERROR "Proved Less64$"
   735  			println("x")
   736  		}
   737  		if i >= 0 { // ERROR "Proved Leq64$"
   738  			println("x")
   739  		}
   740  	}
   741  }
   742  
   743  // signhint1-2 test whether the hint (int >= 0) is propagated into the loop.
   744  func signHint1(i int, data []byte) {
   745  	if i >= 0 {
   746  		for i < len(data) { // ERROR "Induction variable: limits \[\?,\?\), increment 1$"
   747  			_ = data[i] // ERROR "Proved IsInBounds$"
   748  			i++
   749  		}
   750  	}
   751  }
   752  
   753  func signHint2(b []byte, n int) {
   754  	if n < 0 {
   755  		panic("")
   756  	}
   757  	_ = b[25]
   758  	for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
   759  		b[i] = 123 // ERROR "Proved IsInBounds$"
   760  	}
   761  }
   762  
   763  // indexGT0 tests whether prove learns int index >= 0 from bounds check.
   764  func indexGT0(b []byte, n int) {
   765  	_ = b[n]
   766  	_ = b[25]
   767  
   768  	for i := n; i <= 25; i++ { // ERROR "Induction variable: limits \[\?,25\], increment 1$"
   769  		b[i] = 123 // ERROR "Proved IsInBounds$"
   770  	}
   771  }
   772  
   773  // Induction variable in unrolled loop.
   774  func unrollUpExcl(a []int) int {
   775  	var i, x int
   776  	for i = 0; i < len(a)-1; i += 2 { // ERROR "Induction variable: limits \[0,\?\), increment 2$"
   777  		x += a[i]   // ERROR "Proved IsInBounds$"
   778  		x += a[i+1] // ERROR "Proved IsInBounds( for blocked indexing)?$"
   779  	}
   780  	if i == len(a)-1 {
   781  		x += a[i]
   782  	}
   783  	return x
   784  }
   785  
   786  // Induction variable in unrolled loop.
   787  func unrollUpIncl(a []int) int {
   788  	var i, x int
   789  	for i = 0; i <= len(a)-2; i += 2 { // ERROR "Induction variable: limits \[0,\?\], increment 2$"
   790  		x += a[i]   // ERROR "Proved IsInBounds$"
   791  		x += a[i+1] // ERROR "Proved IsInBounds( for blocked indexing)?$"
   792  	}
   793  	if i == len(a)-1 {
   794  		x += a[i]
   795  	}
   796  	return x
   797  }
   798  
   799  // Induction variable in unrolled loop.
   800  func unrollDownExcl0(a []int) int {
   801  	var i, x int
   802  	for i = len(a) - 1; i > 0; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
   803  		x += a[i]   // ERROR "Proved IsInBounds$"
   804  		x += a[i-1] // ERROR "Proved IsInBounds$"
   805  	}
   806  	if i == 0 {
   807  		x += a[i]
   808  	}
   809  	return x
   810  }
   811  
   812  // Induction variable in unrolled loop.
   813  func unrollDownExcl1(a []int) int {
   814  	var i, x int
   815  	for i = len(a) - 1; i >= 1; i -= 2 { // ERROR "Induction variable: limits \(0,\?\], increment 2$"
   816  		x += a[i]   // ERROR "Proved IsInBounds$"
   817  		x += a[i-1] // ERROR "Proved IsInBounds$"
   818  	}
   819  	if i == 0 {
   820  		x += a[i]
   821  	}
   822  	return x
   823  }
   824  
   825  // Induction variable in unrolled loop.
   826  func unrollDownInclStep(a []int) int {
   827  	var i, x int
   828  	for i = len(a); i >= 2; i -= 2 { // ERROR "Induction variable: limits \[2,\?\], increment 2$"
   829  		x += a[i-1] // ERROR "Proved IsInBounds$"
   830  		x += a[i-2] // ERROR "Proved IsInBounds$"
   831  	}
   832  	if i == 1 {
   833  		x += a[i-1]
   834  	}
   835  	return x
   836  }
   837  
   838  // Not an induction variable (step too large)
   839  func unrollExclStepTooLarge(a []int) int {
   840  	var i, x int
   841  	for i = 0; i < len(a)-1; i += 3 {
   842  		x += a[i]
   843  		x += a[i+1] // ERROR "Proved IsInBounds( for blocked indexing)?$"
   844  	}
   845  	if i == len(a)-1 {
   846  		x += a[i]
   847  	}
   848  	return x
   849  }
   850  
   851  // Not an induction variable (step too large)
   852  func unrollInclStepTooLarge(a []int) int {
   853  	var i, x int
   854  	for i = 0; i <= len(a)-2; i += 3 {
   855  		x += a[i]
   856  		x += a[i+1] // ERROR "Proved IsInBounds( for blocked indexing)?$"
   857  	}
   858  	if i == len(a)-1 {
   859  		x += a[i]
   860  	}
   861  	return x
   862  }
   863  
   864  // Not an induction variable (min too small, iterating down)
   865  func unrollDecMin(a []int, b int) int {
   866  	if b != math.MinInt64 {
   867  		return 42
   868  	}
   869  	var i, x int
   870  	for i = len(a); i >= b; i -= 2 { // ERROR "Proved Leq64"
   871  		x += a[i-1]
   872  		x += a[i-2]
   873  	}
   874  	if i == 1 {
   875  		x += a[i-1]
   876  	}
   877  	return x
   878  }
   879  
   880  // Not an induction variable (min too small, iterating up -- perhaps could allow, but why bother?)
   881  func unrollIncMin(a []int, b int) int {
   882  	if b != math.MinInt64 {
   883  		return 42
   884  	}
   885  	var i, x int
   886  	for i = len(a); i >= b; i += 2 { // ERROR "Proved Leq64"
   887  		x += a[i-1]
   888  		x += a[i-2]
   889  	}
   890  	if i == 1 {
   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  // These cases are division of a positive signed integer by a power of 2.
   976  // The opt pass doesnt have sufficient information to see that n is positive.
   977  // So, instead, opt rewrites the division with a less-than-optimal replacement.
   978  // Prove, which can see that n is nonnegative, cannot see the division because
   979  // opt, an earlier pass, has already replaced it.
   980  // The fix for this issue allows prove to zero a right shift that was added as
   981  // part of the less-than-optimal reqwrite. That change by prove then allows
   982  // lateopt to clean up all the unnecessary parts of the original division
   983  // replacement. See issue #36159.
   984  func divShiftClean(n int) int {
   985  	if n < 0 {
   986  		return n
   987  	}
   988  	return n / int(8) // ERROR "Proved Div64 is unsigned$"
   989  }
   990  
   991  func divShiftClean64(n int64) int64 {
   992  	if n < 0 {
   993  		return n
   994  	}
   995  	return n / int64(16) // ERROR "Proved Div64 is unsigned$"
   996  }
   997  
   998  func divShiftClean32(n int32) int32 {
   999  	if n < 0 {
  1000  		return n
  1001  	}
  1002  	return n / int32(16) // ERROR "Proved Div32 is unsigned$"
  1003  }
  1004  
  1005  // Bounds check elimination
  1006  
  1007  func sliceBCE1(p []string, h uint) string {
  1008  	if len(p) == 0 {
  1009  		return ""
  1010  	}
  1011  
  1012  	i := h & uint(len(p)-1)
  1013  	return p[i] // ERROR "Proved IsInBounds$"
  1014  }
  1015  
  1016  func sliceBCE2(p []string, h int) string {
  1017  	if len(p) == 0 {
  1018  		return ""
  1019  	}
  1020  	i := h & (len(p) - 1)
  1021  	return p[i] // ERROR "Proved IsInBounds$"
  1022  }
  1023  
  1024  func and(p []byte) ([]byte, []byte) { // issue #52563
  1025  	const blocksize = 16
  1026  	fullBlocks := len(p) &^ (blocksize - 1)
  1027  	blk := p[:fullBlocks] // ERROR "Proved IsSliceInBounds$"
  1028  	rem := p[fullBlocks:] // ERROR "Proved IsSliceInBounds$"
  1029  	return blk, rem
  1030  }
  1031  
  1032  func rshu(x, y uint) int {
  1033  	z := x >> y
  1034  	if z <= x { // ERROR "Proved Leq64U$"
  1035  		return 1
  1036  	}
  1037  	return 0
  1038  }
  1039  
  1040  func divu(x, y uint) int {
  1041  	z := x / y
  1042  	if z <= x { // ERROR "Proved Leq64U$"
  1043  		return 1
  1044  	}
  1045  	return 0
  1046  }
  1047  
  1048  func divuRoundUp(x, y, z uint) int {
  1049  	x &= ^uint(0) >> 8 // can't overflow in add
  1050  	y = min(y, 0xff-1)
  1051  	z = max(z, 0xff)
  1052  	r := (x + y) / z // ERROR "Proved Neq64$"
  1053  	if r <= x {      // ERROR "Proved Leq64U$"
  1054  		return 1
  1055  	}
  1056  	return 0
  1057  }
  1058  
  1059  func divuRoundUpSlice(x []string) {
  1060  	halfRoundedUp := uint(len(x)+1) / 2
  1061  	_ = x[:halfRoundedUp] // ERROR "Proved IsSliceInBounds$"
  1062  	_ = x[halfRoundedUp:] // ERROR "Proved IsSliceInBounds$"
  1063  }
  1064  
  1065  func modu1(x, y uint) int {
  1066  	z := x % y
  1067  	if z < y { // ERROR "Proved Less64U$"
  1068  		return 1
  1069  	}
  1070  	return 0
  1071  }
  1072  
  1073  func modu2(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 issue57077(s []int) (left, right []int) {
  1082  	middle := len(s) / 2 // ERROR "Proved Div64 is unsigned$"
  1083  	left = s[:middle]    // ERROR "Proved IsSliceInBounds$"
  1084  	right = s[middle:]   // ERROR "Proved IsSliceInBounds$"
  1085  	return
  1086  }
  1087  
  1088  func issue76332(s []int) (left, right []int) {
  1089  	middle := len(s) >> 1 // ERROR "Proved Rsh64x64 is unsigned$"
  1090  	left = s[:middle]     // ERROR "Proved IsSliceInBounds$"
  1091  	right = s[middle:]    // ERROR "Proved IsSliceInBounds$"
  1092  	return
  1093  }
  1094  
  1095  func issue51622(b []byte) int {
  1096  	if len(b) >= 3 && b[len(b)-3] == '#' { // ERROR "Proved IsInBounds$"
  1097  		return len(b)
  1098  	}
  1099  	return 0
  1100  }
  1101  
  1102  func issue45928(x int) {
  1103  	combinedFrac := x / (x | (1 << 31)) // ERROR "Proved Neq64$"
  1104  	useInt(combinedFrac)
  1105  }
  1106  
  1107  func constantBounds1(i, j uint) int {
  1108  	var a [10]int
  1109  	if j < 11 && i < j {
  1110  		return a[i] // ERROR "Proved IsInBounds$"
  1111  	}
  1112  	return 0
  1113  }
  1114  
  1115  func constantBounds2(i, j uint) int {
  1116  	var a [10]int
  1117  	if i < j && j < 11 {
  1118  		return a[i] // ERROR "Proved IsInBounds"
  1119  	}
  1120  	return 0
  1121  }
  1122  
  1123  func constantBounds3(i, j, k, l uint) int {
  1124  	var a [8]int
  1125  	if i < j && j < k && k < l && l < 11 {
  1126  		return a[i] // ERROR "Proved IsInBounds"
  1127  	}
  1128  	return 0
  1129  }
  1130  
  1131  func equalityPropagation(a [1]int, i, j uint) int {
  1132  	if i == j && i == 5 {
  1133  		return a[j-5] // ERROR "Proved IsInBounds"
  1134  	}
  1135  	return 0
  1136  }
  1137  func inequalityPropagation(a [1]int, i, j uint) int {
  1138  	if i != j && j >= 5 && j <= 6 && i == 5 {
  1139  		return a[j-6] // ERROR "Proved IsInBounds"
  1140  	}
  1141  	return 0
  1142  }
  1143  
  1144  func issue66826a(a [21]byte) {
  1145  	for i := 0; i <= 10; i++ { // ERROR "Induction variable: limits \[0,10\], increment 1$"
  1146  		_ = a[2*i] // ERROR "Proved IsInBounds"
  1147  	}
  1148  }
  1149  func issue66826b(a [31]byte, i int) {
  1150  	if i < 0 || i > 10 {
  1151  		return
  1152  	}
  1153  	_ = a[3*i] // ERROR "Proved IsInBounds"
  1154  }
  1155  
  1156  func f20(a, b bool) int {
  1157  	if a == b {
  1158  		if a {
  1159  			if b { // ERROR "Proved Arg"
  1160  				return 1
  1161  			}
  1162  		}
  1163  	}
  1164  	return 0
  1165  }
  1166  
  1167  func f21(a, b *int) int {
  1168  	if a == b {
  1169  		if a != nil {
  1170  			if b != nil { // ERROR "Proved IsNonNil"
  1171  				return 1
  1172  			}
  1173  		}
  1174  	}
  1175  	return 0
  1176  }
  1177  
  1178  func f22(b bool, x, y int) int {
  1179  	b2 := x < y
  1180  	if b == b2 {
  1181  		if b {
  1182  			if x >= y { // ERROR "Disproved Leq64$"
  1183  				return 1
  1184  			}
  1185  		}
  1186  	}
  1187  	return 0
  1188  }
  1189  
  1190  func ctz64(x uint64, ensureBothBranchesCouldHappen bool) int {
  1191  	const max = math.MaxUint64
  1192  	sz := bits.Len64(max)
  1193  
  1194  	log2half := uint64(max) >> (sz / 2)
  1195  	if x >= log2half || x == 0 {
  1196  		return 42
  1197  	}
  1198  
  1199  	y := bits.TrailingZeros64(x) // ERROR "Proved Ctz64 non-zero$""
  1200  
  1201  	z := sz / 2
  1202  	if ensureBothBranchesCouldHappen {
  1203  		if y < z { // ERROR "Proved Less64$"
  1204  			return -42
  1205  		}
  1206  	} else {
  1207  		if y >= z { // ERROR "Disproved Leq64$"
  1208  			return 1337
  1209  		}
  1210  	}
  1211  
  1212  	return y
  1213  }
  1214  func ctz32(x uint32, ensureBothBranchesCouldHappen bool) int {
  1215  	const max = math.MaxUint32
  1216  	sz := bits.Len32(max)
  1217  
  1218  	log2half := uint32(max) >> (sz / 2)
  1219  	if x >= log2half || x == 0 {
  1220  		return 42
  1221  	}
  1222  
  1223  	y := bits.TrailingZeros32(x) // ERROR "Proved Ctz32 non-zero$""
  1224  
  1225  	z := sz / 2
  1226  	if ensureBothBranchesCouldHappen {
  1227  		if y < z { // ERROR "Proved Less64$"
  1228  			return -42
  1229  		}
  1230  	} else {
  1231  		if y >= z { // ERROR "Disproved Leq64$"
  1232  			return 1337
  1233  		}
  1234  	}
  1235  
  1236  	return y
  1237  }
  1238  func ctz16(x uint16, ensureBothBranchesCouldHappen bool) int {
  1239  	const max = math.MaxUint16
  1240  	sz := bits.Len16(max)
  1241  
  1242  	log2half := uint16(max) >> (sz / 2)
  1243  	if x >= log2half || x == 0 {
  1244  		return 42
  1245  	}
  1246  
  1247  	y := bits.TrailingZeros16(x) // ERROR "Proved Ctz16 non-zero$""
  1248  
  1249  	z := sz / 2
  1250  	if ensureBothBranchesCouldHappen {
  1251  		if y < z { // ERROR "Proved Less64$"
  1252  			return -42
  1253  		}
  1254  	} else {
  1255  		if y >= z { // ERROR "Disproved Leq64$"
  1256  			return 1337
  1257  		}
  1258  	}
  1259  
  1260  	return y
  1261  }
  1262  func ctz8(x uint8, ensureBothBranchesCouldHappen bool) int {
  1263  	const max = math.MaxUint8
  1264  	sz := bits.Len8(max)
  1265  
  1266  	log2half := uint8(max) >> (sz / 2)
  1267  	if x >= log2half || x == 0 {
  1268  		return 42
  1269  	}
  1270  
  1271  	y := bits.TrailingZeros8(x) // ERROR "Proved Ctz8 non-zero$""
  1272  
  1273  	z := sz / 2
  1274  	if ensureBothBranchesCouldHappen {
  1275  		if y < z { // ERROR "Proved Less64$"
  1276  			return -42
  1277  		}
  1278  	} else {
  1279  		if y >= z { // ERROR "Disproved Leq64$"
  1280  			return 1337
  1281  		}
  1282  	}
  1283  
  1284  	return y
  1285  }
  1286  
  1287  func bitLen64(x uint64, ensureBothBranchesCouldHappen bool) int {
  1288  	const max = math.MaxUint64
  1289  	sz := bits.Len64(max)
  1290  
  1291  	if x >= max>>3 {
  1292  		return 42
  1293  	}
  1294  	if x <= max>>6 {
  1295  		return 42
  1296  	}
  1297  
  1298  	y := bits.Len64(x)
  1299  
  1300  	if ensureBothBranchesCouldHappen {
  1301  		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
  1302  			return -42
  1303  		}
  1304  	} else {
  1305  		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
  1306  			return 1337
  1307  		}
  1308  	}
  1309  	return y
  1310  }
  1311  func bitLen32(x uint32, ensureBothBranchesCouldHappen bool) int {
  1312  	const max = math.MaxUint32
  1313  	sz := bits.Len32(max)
  1314  
  1315  	if x >= max>>3 {
  1316  		return 42
  1317  	}
  1318  	if x <= max>>6 {
  1319  		return 42
  1320  	}
  1321  
  1322  	y := bits.Len32(x)
  1323  
  1324  	if ensureBothBranchesCouldHappen {
  1325  		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
  1326  			return -42
  1327  		}
  1328  	} else {
  1329  		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
  1330  			return 1337
  1331  		}
  1332  	}
  1333  	return y
  1334  }
  1335  func bitLen16(x uint16, ensureBothBranchesCouldHappen bool) int {
  1336  	const max = math.MaxUint16
  1337  	sz := bits.Len16(max)
  1338  
  1339  	if x >= max>>3 {
  1340  		return 42
  1341  	}
  1342  	if x <= max>>6 {
  1343  		return 42
  1344  	}
  1345  
  1346  	y := bits.Len16(x)
  1347  
  1348  	if ensureBothBranchesCouldHappen {
  1349  		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
  1350  			return -42
  1351  		}
  1352  	} else {
  1353  		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
  1354  			return 1337
  1355  		}
  1356  	}
  1357  	return y
  1358  }
  1359  func bitLen8(x uint8, ensureBothBranchesCouldHappen bool) int {
  1360  	const max = math.MaxUint8
  1361  	sz := bits.Len8(max)
  1362  
  1363  	if x >= max>>3 {
  1364  		return 42
  1365  	}
  1366  	if x <= max>>6 {
  1367  		return 42
  1368  	}
  1369  
  1370  	y := bits.Len8(x)
  1371  
  1372  	if ensureBothBranchesCouldHappen {
  1373  		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
  1374  			return -42
  1375  		}
  1376  	} else {
  1377  		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
  1378  			return 1337
  1379  		}
  1380  	}
  1381  	return y
  1382  }
  1383  
  1384  func xor64(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1385  	a = min(a, 0xff)
  1386  	b = min(b, 0xfff)
  1387  
  1388  	z := a ^ b
  1389  
  1390  	if ensureBothBranchesCouldHappen {
  1391  		if z > 0xfff { // ERROR "Disproved Less64U$"
  1392  			return 42
  1393  		}
  1394  	} else {
  1395  		if z <= 0xfff { // ERROR "Proved Leq64U$"
  1396  			return 1337
  1397  		}
  1398  	}
  1399  	return int(z)
  1400  }
  1401  
  1402  func or64(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1403  	a = min(a, 0xff)
  1404  	b = min(b, 0xfff)
  1405  
  1406  	z := a | b
  1407  
  1408  	if ensureBothBranchesCouldHappen {
  1409  		if z > 0xfff { // ERROR "Disproved Less64U$"
  1410  			return 42
  1411  		}
  1412  	} else {
  1413  		if z <= 0xfff { // ERROR "Proved Leq64U$"
  1414  			return 1337
  1415  		}
  1416  	}
  1417  	return int(z)
  1418  }
  1419  
  1420  func mod64uWithSmallerDividendMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1421  	a = min(a, 0xff)
  1422  	b = min(b, 0xfff)
  1423  
  1424  	z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
  1425  
  1426  	if ensureBothBranchesCouldHappen {
  1427  		if z > bits.Len64(0xff) { // ERROR "Disproved Less64$"
  1428  			return 42
  1429  		}
  1430  	} else {
  1431  		if z <= bits.Len64(0xff) { // ERROR "Proved Leq64$"
  1432  			return 1337
  1433  		}
  1434  	}
  1435  	return z
  1436  }
  1437  func mod64uWithSmallerDivisorMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1438  	a = min(a, 0xfff)
  1439  	b = min(b, 0x10) // we need bits.Len64(b.umax) != bits.Len64(b.umax-1)
  1440  
  1441  	z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
  1442  
  1443  	if ensureBothBranchesCouldHappen {
  1444  		if z > bits.Len64(0x10-1) { // ERROR "Disproved Less64$"
  1445  			return 42
  1446  		}
  1447  	} else {
  1448  		if z <= bits.Len64(0x10-1) { // ERROR "Proved Leq64$"
  1449  			return 1337
  1450  		}
  1451  	}
  1452  	return z
  1453  }
  1454  func mod64uWithIdenticalMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1455  	a = min(a, 0x10)
  1456  	b = min(b, 0x10) // we need bits.Len64(b.umax) != bits.Len64(b.umax-1)
  1457  
  1458  	z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
  1459  
  1460  	if ensureBothBranchesCouldHappen {
  1461  		if z > bits.Len64(0x10-1) { // ERROR "Disproved Less64$"
  1462  			return 42
  1463  		}
  1464  	} else {
  1465  		if z <= bits.Len64(0x10-1) { // ERROR "Proved Leq64$"
  1466  			return 1337
  1467  		}
  1468  	}
  1469  	return z
  1470  }
  1471  func mod64sPositiveWithSmallerDividendMax(a, b int64, ensureBothBranchesCouldHappen bool) int64 {
  1472  	if a < 0 || b < 0 {
  1473  		return 42
  1474  	}
  1475  	a = min(a, 0xff)
  1476  	b = min(b, 0xfff)
  1477  
  1478  	z := a % b // ERROR "Proved Mod64 is unsigned$"
  1479  
  1480  	if ensureBothBranchesCouldHappen {
  1481  		if z > 0xff { // ERROR "Disproved Less64$"
  1482  			return 42
  1483  		}
  1484  	} else {
  1485  		if z <= 0xff { // ERROR "Proved Leq64$"
  1486  			return 1337
  1487  		}
  1488  	}
  1489  	return z
  1490  }
  1491  func mod64sPositiveWithSmallerDivisorMax(a, b int64, ensureBothBranchesCouldHappen bool) int64 {
  1492  	if a < 0 || b < 0 {
  1493  		return 42
  1494  	}
  1495  	a = min(a, 0xfff)
  1496  	b = min(b, 0xff)
  1497  
  1498  	z := a % b // ERROR "Proved Mod64 is unsigned$"
  1499  
  1500  	if ensureBothBranchesCouldHappen {
  1501  		if z > 0xff-1 { // ERROR "Disproved Less64$"
  1502  			return 42
  1503  		}
  1504  	} else {
  1505  		if z <= 0xff-1 { // ERROR "Proved Leq64$"
  1506  			return 1337
  1507  		}
  1508  	}
  1509  	return z
  1510  }
  1511  func mod64sPositiveWithIdenticalMax(a, b int64, ensureBothBranchesCouldHappen bool) int64 {
  1512  	if a < 0 || b < 0 {
  1513  		return 42
  1514  	}
  1515  	a = min(a, 0xfff)
  1516  	b = min(b, 0xfff)
  1517  
  1518  	z := a % b // ERROR "Proved Mod64 is unsigned$"
  1519  
  1520  	if ensureBothBranchesCouldHappen {
  1521  		if z > 0xfff-1 { // ERROR "Disproved Less64$"
  1522  			return 42
  1523  		}
  1524  	} else {
  1525  		if z <= 0xfff-1 { // ERROR "Proved Leq64$"
  1526  			return 1337
  1527  		}
  1528  	}
  1529  	return z
  1530  }
  1531  
  1532  func div64u(a, b uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
  1533  	a = min(a, 0xffff)
  1534  	a = max(a, 0xfff)
  1535  	b = min(b, 0xff)
  1536  	b = max(b, 0xf)
  1537  
  1538  	z := a / b // ERROR "Proved Neq64$"
  1539  
  1540  	if ensureAllBranchesCouldHappen() && z > 0xffff/0xf { // ERROR "Disproved Less64U$"
  1541  		return 42
  1542  	}
  1543  	if ensureAllBranchesCouldHappen() && z <= 0xffff/0xf { // ERROR "Proved Leq64U$"
  1544  		return 1337
  1545  	}
  1546  	if ensureAllBranchesCouldHappen() && z < 0xfff/0xff { // ERROR "Disproved Less64U$"
  1547  		return 42
  1548  	}
  1549  	if ensureAllBranchesCouldHappen() && z >= 0xfff/0xff { // ERROR "Proved Leq64U$"
  1550  		return 42
  1551  	}
  1552  	return z
  1553  }
  1554  func div64s(a, b int64, ensureAllBranchesCouldHappen func() bool) int64 {
  1555  	if a < 0 || b < 0 {
  1556  		return 42
  1557  	}
  1558  	a = min(a, 0xffff)
  1559  	a = max(a, 0xfff)
  1560  	b = min(b, 0xff)
  1561  	b = max(b, 0xf)
  1562  
  1563  	z := a / b // ERROR "Proved Div64 is unsigned|Proved Neq64"
  1564  
  1565  	if ensureAllBranchesCouldHappen() && z > 0xffff/0xf { // ERROR "Disproved Less64$"
  1566  		return 42
  1567  	}
  1568  	if ensureAllBranchesCouldHappen() && z <= 0xffff/0xf { // ERROR "Proved Leq64$"
  1569  		return 1337
  1570  	}
  1571  	if ensureAllBranchesCouldHappen() && z < 0xfff/0xff { // ERROR "Disproved Less64$"
  1572  		return 42
  1573  	}
  1574  	if ensureAllBranchesCouldHappen() && z >= 0xfff/0xff { // ERROR "Proved Leq64$"
  1575  		return 42
  1576  	}
  1577  	return z
  1578  }
  1579  
  1580  func trunc64to16(a uint64, ensureAllBranchesCouldHappen func() bool) uint16 {
  1581  	a = min(a, 0xfff)
  1582  	a = max(a, 0xff)
  1583  
  1584  	z := uint16(a)
  1585  	if ensureAllBranchesCouldHappen() && z > 0xfff { // ERROR "Disproved Less16U$"
  1586  		return 42
  1587  	}
  1588  	if ensureAllBranchesCouldHappen() && z <= 0xfff { // ERROR "Proved Leq16U$"
  1589  		return 1337
  1590  	}
  1591  	if ensureAllBranchesCouldHappen() && z < 0xff { // ERROR "Disproved Less16U$"
  1592  		return 42
  1593  	}
  1594  	if ensureAllBranchesCouldHappen() && z >= 0xff { // ERROR "Proved Leq16U$"
  1595  		return 1337
  1596  	}
  1597  	return z
  1598  }
  1599  
  1600  func com64(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
  1601  	a = min(a, 0xffff)
  1602  	a = max(a, 0xff)
  1603  
  1604  	z := ^a
  1605  
  1606  	if ensureAllBranchesCouldHappen() && z > ^uint64(0xff) { // ERROR "Disproved Less64U$"
  1607  		return 42
  1608  	}
  1609  	if ensureAllBranchesCouldHappen() && z <= ^uint64(0xff) { // ERROR "Proved Leq64U$"
  1610  		return 1337
  1611  	}
  1612  	if ensureAllBranchesCouldHappen() && z < ^uint64(0xffff) { // ERROR "Disproved Less64U$"
  1613  		return 42
  1614  	}
  1615  	if ensureAllBranchesCouldHappen() && z >= ^uint64(0xffff) { // ERROR "Proved Leq64U$"
  1616  		return 1337
  1617  	}
  1618  	return z
  1619  }
  1620  
  1621  func neg64(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
  1622  	var lo, hi uint64 = 0xff, 0xfff
  1623  	a = min(a, hi)
  1624  	a = max(a, lo)
  1625  
  1626  	z := -a
  1627  
  1628  	if ensureAllBranchesCouldHappen() && z > -lo { // ERROR "Disproved Less64U$"
  1629  		return 42
  1630  	}
  1631  	if ensureAllBranchesCouldHappen() && z <= -lo { // ERROR "Proved Leq64U$"
  1632  		return 1337
  1633  	}
  1634  	if ensureAllBranchesCouldHappen() && z < -hi { // ERROR "Disproved Less64U$"
  1635  		return 42
  1636  	}
  1637  	if ensureAllBranchesCouldHappen() && z >= -hi { // ERROR "Proved Leq64U$"
  1638  		return 1337
  1639  	}
  1640  	return z
  1641  }
  1642  func neg64mightOverflowDuringNeg(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
  1643  	var lo, hi uint64 = 0, 0xfff
  1644  	a = min(a, hi)
  1645  	a = max(a, lo)
  1646  
  1647  	z := -a
  1648  
  1649  	if ensureAllBranchesCouldHappen() && z > -lo {
  1650  		return 42
  1651  	}
  1652  	if ensureAllBranchesCouldHappen() && z <= -lo {
  1653  		return 1337
  1654  	}
  1655  	if ensureAllBranchesCouldHappen() && z < -hi {
  1656  		return 42
  1657  	}
  1658  	if ensureAllBranchesCouldHappen() && z >= -hi {
  1659  		return 1337
  1660  	}
  1661  	return z
  1662  }
  1663  
  1664  func phiMin(a, b []byte) {
  1665  	_ = a[:min(len(a), len(b))] // ERROR "Proved IsSliceInBounds"
  1666  	_ = b[:min(len(a), len(b))] // ERROR "Proved IsSliceInBounds"
  1667  	_ = a[:max(len(a), len(b))]
  1668  	_ = b[:max(len(a), len(b))]
  1669  	x := len(a)
  1670  	if x > len(b) {
  1671  		x = len(b)
  1672  		useInt(0)
  1673  	}
  1674  	_ = a[:x] // ERROR "Proved IsSliceInBounds"
  1675  	y := len(a)
  1676  	if y > len(b) {
  1677  		y = len(b)
  1678  		useInt(0)
  1679  	} else {
  1680  		useInt(1)
  1681  	}
  1682  	_ = b[:y] // ERROR "Proved IsSliceInBounds"
  1683  }
  1684  
  1685  func minPhiLeq[T uint | int](x, y T) (z T) {
  1686  	if x <= y {
  1687  		z = x
  1688  	} else {
  1689  		z = y
  1690  	}
  1691  	return z
  1692  }
  1693  func maxPhiLeq[T uint | int](x, y T) (z T) {
  1694  	if y <= x {
  1695  		z = x
  1696  	} else {
  1697  		z = y
  1698  	}
  1699  	return z
  1700  }
  1701  func mathBasedOnPhiLosangeMinUFirstLeq(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1702  	const maxc = 0xf2a
  1703  	const minc = 0xf0a
  1704  	x = minPhiLeq(x, maxc)
  1705  	x = maxPhiLeq(x, minc)
  1706  
  1707  	const k = 1
  1708  	x += k
  1709  
  1710  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1711  		return 42
  1712  	}
  1713  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1714  		return 4242
  1715  	}
  1716  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1717  		return 424242
  1718  	}
  1719  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1720  		return 42424242
  1721  	}
  1722  	return x
  1723  }
  1724  func mathBasedOnPhiLosangeMinUSecondLeq(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1725  	const maxc = 0xf2a
  1726  	const minc = 0xf0a
  1727  	x = maxPhiLeq(x, minc)
  1728  	x = minPhiLeq(x, maxc)
  1729  
  1730  	const k = 1
  1731  	x += k
  1732  
  1733  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1734  		return 42
  1735  	}
  1736  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1737  		return 4242
  1738  	}
  1739  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1740  		return 424242
  1741  	}
  1742  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1743  		return 42424242
  1744  	}
  1745  	return x
  1746  }
  1747  func mathBasedOnPhiLosangeMinFirstLeq(x int, ensureAllBranchesCouldHappen func() bool) int {
  1748  	const maxc = 0xf2a
  1749  	const minc = 0xf0a
  1750  	x = minPhiLeq(x, maxc)
  1751  	x = maxPhiLeq(x, minc)
  1752  
  1753  	const k = 1
  1754  	x += k
  1755  
  1756  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1757  		return 42
  1758  	}
  1759  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1760  		return 4242
  1761  	}
  1762  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1763  		return 424242
  1764  	}
  1765  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1766  		return 42424242
  1767  	}
  1768  	return x
  1769  }
  1770  func mathBasedOnPhiLosangeMinSecondLeq(x int, ensureAllBranchesCouldHappen func() bool) int {
  1771  	const maxc = 0xf2a
  1772  	const minc = 0xf0a
  1773  	x = maxPhiLeq(x, minc)
  1774  	x = minPhiLeq(x, maxc)
  1775  
  1776  	const k = 1
  1777  	x += k
  1778  
  1779  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1780  		return 42
  1781  	}
  1782  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1783  		return 4242
  1784  	}
  1785  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1786  		return 424242
  1787  	}
  1788  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1789  		return 42424242
  1790  	}
  1791  	return x
  1792  }
  1793  
  1794  func minPhiLess[T uint | int](x, y T) (z T) {
  1795  	if x < y {
  1796  		z = x
  1797  	} else {
  1798  		z = y
  1799  	}
  1800  	return z
  1801  }
  1802  func maxPhiLess[T uint | int](x, y T) (z T) {
  1803  	if y < x {
  1804  		z = x
  1805  	} else {
  1806  		z = y
  1807  	}
  1808  	return z
  1809  }
  1810  func mathBasedOnPhiLosangeMinUFirstLess(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1811  	const maxc = 0xf2a
  1812  	const minc = 0xf0a
  1813  	x = minPhiLess(x, maxc)
  1814  	x = maxPhiLess(x, minc)
  1815  
  1816  	const k = 1
  1817  	x += k
  1818  
  1819  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1820  		return 42
  1821  	}
  1822  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1823  		return 4242
  1824  	}
  1825  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1826  		return 424242
  1827  	}
  1828  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1829  		return 42424242
  1830  	}
  1831  	return x
  1832  }
  1833  func mathBasedOnPhiLosangeMinUSecondLess(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1834  	const maxc = 0xf2a
  1835  	const minc = 0xf0a
  1836  	x = maxPhiLess(x, minc)
  1837  	x = minPhiLess(x, maxc)
  1838  
  1839  	const k = 1
  1840  	x += k
  1841  
  1842  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1843  		return 42
  1844  	}
  1845  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1846  		return 4242
  1847  	}
  1848  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1849  		return 424242
  1850  	}
  1851  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1852  		return 42424242
  1853  	}
  1854  	return x
  1855  }
  1856  func mathBasedOnPhiLosangeMinFirstLess(x int, ensureAllBranchesCouldHappen func() bool) int {
  1857  	const maxc = 0xf2a
  1858  	const minc = 0xf0a
  1859  	x = minPhiLess(x, maxc)
  1860  	x = maxPhiLess(x, minc)
  1861  
  1862  	const k = 1
  1863  	x += k
  1864  
  1865  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1866  		return 42
  1867  	}
  1868  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1869  		return 4242
  1870  	}
  1871  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1872  		return 424242
  1873  	}
  1874  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1875  		return 42424242
  1876  	}
  1877  	return x
  1878  }
  1879  func mathBasedOnPhiLosangeMinSecondLess(x int, ensureAllBranchesCouldHappen func() bool) int {
  1880  	const maxc = 0xf2a
  1881  	const minc = 0xf0a
  1882  	x = maxPhiLess(x, minc)
  1883  	x = minPhiLess(x, maxc)
  1884  
  1885  	const k = 1
  1886  	x += k
  1887  
  1888  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1889  		return 42
  1890  	}
  1891  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1892  		return 4242
  1893  	}
  1894  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1895  		return 424242
  1896  	}
  1897  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1898  		return 42424242
  1899  	}
  1900  	return x
  1901  }
  1902  
  1903  func mathBasedOnPhiBuiltinMinUFirst(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1904  	const maxc = 0xf2a
  1905  	const minc = 0xf0a
  1906  	x = min(x, maxc)
  1907  	x = max(x, minc)
  1908  
  1909  	const k = 1
  1910  	x += k
  1911  
  1912  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1913  		return 42
  1914  	}
  1915  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1916  		return 4242
  1917  	}
  1918  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1919  		return 424242
  1920  	}
  1921  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1922  		return 42424242
  1923  	}
  1924  	return x
  1925  }
  1926  func mathBasedOnPhiBuiltinMinUSecond(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1927  	const maxc = 0xf2a
  1928  	const minc = 0xf0a
  1929  	x = max(x, minc)
  1930  	x = min(x, maxc)
  1931  
  1932  	const k = 1
  1933  	x += k
  1934  
  1935  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1936  		return 42
  1937  	}
  1938  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1939  		return 4242
  1940  	}
  1941  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1942  		return 424242
  1943  	}
  1944  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1945  		return 42424242
  1946  	}
  1947  	return x
  1948  }
  1949  func mathBasedOnPhiBuiltinMinFirst(x int, ensureAllBranchesCouldHappen func() bool) int {
  1950  	const maxc = 0xf2a
  1951  	const minc = 0xf0a
  1952  	x = min(x, maxc)
  1953  	x = max(x, minc)
  1954  
  1955  	const k = 1
  1956  	x += k
  1957  
  1958  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1959  		return 42
  1960  	}
  1961  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1962  		return 4242
  1963  	}
  1964  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1965  		return 424242
  1966  	}
  1967  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1968  		return 42424242
  1969  	}
  1970  	return x
  1971  }
  1972  func mathBasedOnPhiBuiltinMinSecond(x int, ensureAllBranchesCouldHappen func() bool) int {
  1973  	const maxc = 0xf2a
  1974  	const minc = 0xf0a
  1975  	x = max(x, minc)
  1976  	x = min(x, maxc)
  1977  
  1978  	const k = 1
  1979  	x += k
  1980  
  1981  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1982  		return 42
  1983  	}
  1984  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1985  		return 4242
  1986  	}
  1987  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1988  		return 424242
  1989  	}
  1990  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1991  		return 42424242
  1992  	}
  1993  	return x
  1994  }
  1995  
  1996  func issue16833(a, b []byte) {
  1997  	n := copy(a, b)
  1998  	_ = a[n:] // ERROR "Proved IsSliceInBounds"
  1999  	_ = b[n:] // ERROR "Proved IsSliceInBounds"
  2000  	_ = a[:n] // ERROR "Proved IsSliceInBounds"
  2001  	_ = b[:n] // ERROR "Proved IsSliceInBounds"
  2002  }
  2003  
  2004  func clampedIdx1(x []int, i int) int {
  2005  	if len(x) == 0 {
  2006  		return 0
  2007  	}
  2008  	return x[min(max(0, i), len(x)-1)] // ERROR "Proved IsInBounds"
  2009  }
  2010  func clampedIdx2(x []int, i int) int {
  2011  	if len(x) == 0 {
  2012  		return 0
  2013  	}
  2014  	return x[max(min(i, len(x)-1), 0)] // TODO: can't get rid of this bounds check yet
  2015  }
  2016  
  2017  func cvtBoolToUint8Disprove(b bool) byte {
  2018  	var c byte
  2019  	if b {
  2020  		c = 1
  2021  	}
  2022  	if c == 2 { // ERROR "Disproved Eq8"
  2023  		c = 3
  2024  	}
  2025  	return c
  2026  }
  2027  func cvtBoolToUint8BCE(b bool, a [2]int64) int64 {
  2028  	c := byte(0)
  2029  	if b {
  2030  		c = 1
  2031  	}
  2032  	return a[c] // ERROR "Proved IsInBounds$"
  2033  }
  2034  
  2035  func transitiveProofsThroughNonOverflowingUnsignedAdd(x, y, z uint64) {
  2036  	x &= 1<<63 - 1
  2037  	y &= 1<<63 - 1
  2038  
  2039  	a := x + y
  2040  	if a > z {
  2041  		return
  2042  	}
  2043  
  2044  	if x > z { // ERROR "Disproved Less64U$"
  2045  		return
  2046  	}
  2047  	if y > z { // ERROR "Disproved Less64U$"
  2048  		return
  2049  	}
  2050  	if a == x {
  2051  		return
  2052  	}
  2053  	if a == y {
  2054  		return
  2055  	}
  2056  
  2057  	x |= 1
  2058  	y |= 1
  2059  	a = x + y
  2060  	if a == x { // ERROR "Disproved Eq64$"
  2061  		return
  2062  	}
  2063  	if a == y { // ERROR "Disproved Eq64$"
  2064  		return
  2065  	}
  2066  }
  2067  
  2068  func transitiveProofsThroughOverflowingUnsignedAdd(x, y, z uint64) {
  2069  	a := x + y
  2070  	if a > z {
  2071  		return
  2072  	}
  2073  
  2074  	if x > z {
  2075  		return
  2076  	}
  2077  	if y > z {
  2078  		return
  2079  	}
  2080  	if a == x {
  2081  		return
  2082  	}
  2083  	if a == y {
  2084  		return
  2085  	}
  2086  
  2087  	x |= 1
  2088  	y |= 1
  2089  	a = x + y
  2090  	if a == x {
  2091  		return
  2092  	}
  2093  	if a == y {
  2094  		return
  2095  	}
  2096  }
  2097  
  2098  func transitiveProofsThroughNonOverflowingSignedAddPositive(x, y, z int64) {
  2099  	x &= 1<<62 - 1
  2100  	y &= 1<<62 - 1
  2101  
  2102  	a := x + y
  2103  	if a > z {
  2104  		return
  2105  	}
  2106  
  2107  	if x > z { // ERROR "Disproved Less64$"
  2108  		return
  2109  	}
  2110  	if y > z { // ERROR "Disproved Less64$"
  2111  		return
  2112  	}
  2113  	if a == x {
  2114  		return
  2115  	}
  2116  	if a == y {
  2117  		return
  2118  	}
  2119  
  2120  	x |= 1
  2121  	y |= 1
  2122  	a = x + y
  2123  	if a == x { // ERROR "Disproved Eq64$"
  2124  		return
  2125  	}
  2126  	if a == y { // ERROR "Disproved Eq64$"
  2127  		return
  2128  	}
  2129  }
  2130  
  2131  func transitiveProofsThroughOverflowingSignedAddPositive(x, y, z int64) {
  2132  	if x < 0 || y < 0 {
  2133  		return
  2134  	}
  2135  
  2136  	a := x + y
  2137  	if a > z {
  2138  		return
  2139  	}
  2140  
  2141  	if x > z {
  2142  		return
  2143  	}
  2144  	if y > z {
  2145  		return
  2146  	}
  2147  	if a == x {
  2148  		return
  2149  	}
  2150  	if a == y {
  2151  		return
  2152  	}
  2153  
  2154  	x |= 1
  2155  	y |= 1
  2156  	a = x + y
  2157  	if a == x { // ERROR "Disproved Eq64$"
  2158  		return
  2159  	}
  2160  	if a == y { // ERROR "Disproved Eq64$"
  2161  		return
  2162  	}
  2163  }
  2164  
  2165  func transitiveProofsThroughNonOverflowingSignedAddNegative(x, y, z int64) {
  2166  	if x < math.MinInt64>>1 || x > 0 ||
  2167  		y < math.MinInt64>>1 || y > 0 {
  2168  		return
  2169  	}
  2170  
  2171  	a := x + y
  2172  	if a < z {
  2173  		return
  2174  	}
  2175  
  2176  	if x < z { // ERROR "Disproved Less64$"
  2177  		return
  2178  	}
  2179  	if y < z { // ERROR "Disproved Less64$"
  2180  		return
  2181  	}
  2182  	if a == x {
  2183  		return
  2184  	}
  2185  	if a == y {
  2186  		return
  2187  	}
  2188  
  2189  	if x == 0 && y == 0 {
  2190  		return
  2191  	}
  2192  	a = x + y
  2193  	if a == x { // ERROR "Disproved Eq64$"
  2194  		return
  2195  	}
  2196  	if a == y { // ERROR "Disproved Eq64$"
  2197  		return
  2198  	}
  2199  }
  2200  
  2201  func transitiveProofsThroughOverflowingSignedAddNegative(x, y, z int64) {
  2202  	if x >= 0 || y >= 0 {
  2203  		return
  2204  	}
  2205  
  2206  	a := x + y
  2207  	if a < z {
  2208  		return
  2209  	}
  2210  
  2211  	if x < z {
  2212  		return
  2213  	}
  2214  	if y < z {
  2215  		return
  2216  	}
  2217  	if a == x {
  2218  		return
  2219  	}
  2220  	if a == y {
  2221  		return
  2222  	}
  2223  
  2224  	x |= 1
  2225  	y |= 1
  2226  	a = x + y
  2227  	if a == x {
  2228  		return
  2229  	}
  2230  	if a == y {
  2231  		return
  2232  	}
  2233  }
  2234  
  2235  func transitiveProofsThroughNonOverflowingUnsignedSub(x, y, z uint64) {
  2236  	x |= 0xfff
  2237  	y &= 0xfff
  2238  
  2239  	a := x - y
  2240  	if a < z {
  2241  		return
  2242  	}
  2243  
  2244  	if x < z { // ERROR "Disproved Less64U$"
  2245  		return
  2246  	}
  2247  	if y < z {
  2248  		return
  2249  	}
  2250  	if a == x {
  2251  		return
  2252  	}
  2253  	if a == y {
  2254  		return
  2255  	}
  2256  
  2257  	y |= 1
  2258  	a = x - y
  2259  	if a == x { // ERROR "Disproved Eq64$"
  2260  		return
  2261  	}
  2262  	if a == y {
  2263  		return
  2264  	}
  2265  }
  2266  
  2267  func transitiveProofsThroughOverflowingUnsignedSub(x, y, z uint64) {
  2268  	a := x - y
  2269  	if a < z {
  2270  		return
  2271  	}
  2272  
  2273  	if x < z {
  2274  		return
  2275  	}
  2276  	if y < z {
  2277  		return
  2278  	}
  2279  	if a == x {
  2280  		return
  2281  	}
  2282  	if a == y {
  2283  		return
  2284  	}
  2285  
  2286  	y |= 1
  2287  	a = x - y
  2288  	if a == x {
  2289  		return
  2290  	}
  2291  	if a == y {
  2292  		return
  2293  	}
  2294  }
  2295  
  2296  func resliceString(s string) byte {
  2297  	if len(s) >= 4 {
  2298  		s = s[2:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
  2299  		s = s[1:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
  2300  		return s[0] // ERROR "Proved IsInBounds"
  2301  	}
  2302  	return 0
  2303  }
  2304  func resliceBytes(b []byte) byte {
  2305  	if len(b) >= 4 {
  2306  		b = b[2:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
  2307  		b = b[1:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
  2308  		return b[0] // ERROR "Proved IsInBounds"
  2309  	}
  2310  	return 0
  2311  }
  2312  
  2313  func issue74473(s []uint) {
  2314  	i := 0
  2315  	for {
  2316  		if i >= len(s) { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
  2317  			break
  2318  		}
  2319  		_ = s[i] // ERROR "Proved IsInBounds$"
  2320  		i++
  2321  	}
  2322  }
  2323  
  2324  func setCapMaxBasedOnElementSize(x []uint64) int {
  2325  	c := uintptr(cap(x))
  2326  	max := ^uintptr(0) >> 3
  2327  	if c > max { // ERROR "Disproved Less"
  2328  		return 42
  2329  	}
  2330  	if c <= max { // ERROR "Proved Leq"
  2331  		return 1337
  2332  	}
  2333  	return 0
  2334  }
  2335  
  2336  func issue75144for(a, b []uint64) bool {
  2337  	if len(a) == len(b) {
  2338  		for len(a) > 4 {
  2339  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2340  			b = b[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2341  		}
  2342  		if len(a) == len(b) { // ERROR "Proved Eq64$"
  2343  			return true
  2344  		}
  2345  	}
  2346  	return false
  2347  }
  2348  
  2349  func issue75144if(a, b []uint64) bool {
  2350  	if len(a) == len(b) {
  2351  		if len(a) > 4 {
  2352  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2353  			b = b[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2354  		}
  2355  		if len(a) == len(b) { // ERROR "Proved Eq64$"
  2356  			return true
  2357  		}
  2358  	}
  2359  	return false
  2360  }
  2361  
  2362  func issue75144if2(a, b, c, d []uint64) (r bool) {
  2363  	if len(a) != len(b) || len(c) != len(d) {
  2364  		return
  2365  	}
  2366  	if len(a) <= 4 || len(c) <= 4 {
  2367  		return
  2368  	}
  2369  	if len(a) < len(c) {
  2370  		c = c[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2371  		d = d[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2372  	} else {
  2373  		a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2374  		b = b[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2375  	}
  2376  	if len(a) == len(c) {
  2377  		return
  2378  	}
  2379  	if len(a) == len(b) { // ERROR "Proved Eq64$"
  2380  		r = true
  2381  	}
  2382  	if len(c) == len(d) { // ERROR "Proved Eq64$"
  2383  		r = true
  2384  	}
  2385  	return
  2386  }
  2387  
  2388  func issue75144forCannot(a, b []uint64) bool {
  2389  	if len(a) == len(b) {
  2390  		for len(a) > 4 {
  2391  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2392  			b = b[4:]
  2393  			for len(a) > 2 {
  2394  				a = a[2:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2395  				b = b[2:]
  2396  			}
  2397  		}
  2398  		if len(a) == len(b) {
  2399  			return true
  2400  		}
  2401  	}
  2402  	return false
  2403  }
  2404  
  2405  func issue75144ifCannot(a, b []uint64) bool {
  2406  	if len(a) == len(b) {
  2407  		if len(a) > 4 {
  2408  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2409  			b = b[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2410  			if len(a) > 2 {
  2411  				a = a[2:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2412  				b = b[2:]
  2413  			}
  2414  		}
  2415  		if len(a) == len(b) {
  2416  			return true
  2417  		}
  2418  	}
  2419  	return false
  2420  }
  2421  
  2422  func issue75144ifCannot2(a, b []uint64) bool {
  2423  	if len(a) == len(b) {
  2424  		if len(a) > 4 {
  2425  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2426  			b = b[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2427  		} else if len(a) > 2 {
  2428  			a = a[2:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2429  			b = b[2:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2430  		}
  2431  		if len(a) == len(b) {
  2432  			return true
  2433  		}
  2434  	}
  2435  	return false
  2436  }
  2437  
  2438  func issue75144forNot(a, b []uint64) bool {
  2439  	if len(a) == len(b) {
  2440  		for len(a) > 4 {
  2441  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2442  			b = b[3:]
  2443  		}
  2444  		if len(a) == len(b) {
  2445  			return true
  2446  		}
  2447  	}
  2448  	return false
  2449  }
  2450  
  2451  func issue75144forNot2(a, b, c []uint64) bool {
  2452  	if len(a) == len(b) {
  2453  		for len(a) > 4 {
  2454  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2455  			b = c[4:]
  2456  		}
  2457  		if len(a) == len(b) {
  2458  			return true
  2459  		}
  2460  	}
  2461  	return false
  2462  }
  2463  
  2464  func issue75144ifNot(a, b []uint64) bool {
  2465  	if len(a) == len(b) {
  2466  		if len(a) > 4 {
  2467  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2468  		} else {
  2469  			b = b[4:]
  2470  		}
  2471  		if len(a) == len(b) {
  2472  			return true
  2473  		}
  2474  	}
  2475  	return false
  2476  }
  2477  
  2478  func mulIntoAnd(a, b uint) uint {
  2479  	if a > 1 || b > 1 {
  2480  		return 0
  2481  	}
  2482  	return a * b // ERROR "Rewrote Mul v[0-9]+ into And$"
  2483  }
  2484  
  2485  func mulIntoCondSelect(a, b uint) uint {
  2486  	if a > 1 {
  2487  		return 0
  2488  	}
  2489  	return a * b // ERROR "Rewrote Mul v[0-9]+ into CondSelect"
  2490  }
  2491  
  2492  func div7pos(x int32) bool {
  2493  	if x > 0 {
  2494  		return x%7 == 0 // ERROR "Proved Div32 is unsigned"
  2495  	}
  2496  	return false
  2497  }
  2498  
  2499  func div2pos(x []int) int {
  2500  	return len(x) / 2 // ERROR "Proved Div64 is unsigned"
  2501  }
  2502  
  2503  func div3pos(x []int) int {
  2504  	return len(x) / 3 // ERROR "Proved Div64 is unsigned"
  2505  }
  2506  
  2507  var len200 [200]int
  2508  
  2509  func modbound1(u uint64) int {
  2510  	s := 0
  2511  	for u > 0 {
  2512  		var d uint64
  2513  		u, d = u/100, u%100
  2514  		s += len200[d*2+1] // ERROR "Proved IsInBounds"
  2515  	}
  2516  	return s
  2517  }
  2518  
  2519  func modbound2(p *[10]int, x uint) int {
  2520  	return p[x%9+1] // ERROR "Proved IsInBounds"
  2521  }
  2522  
  2523  func shiftbound(x int) int {
  2524  	return 1 << (x % 11) // ERROR "Proved Lsh(32x32|64x64) bounded" "Proved Div64 does not need fix-up"
  2525  }
  2526  
  2527  func shiftbound2(x int) int {
  2528  	return 1 << (x % 8) // ERROR "Proved Lsh(32x32|64x64) bounded" "Proved Div64 does not need fix-up"
  2529  }
  2530  
  2531  func rangebound1(x []int) int {
  2532  	s := 0
  2533  	for i := range 1000 { // ERROR "Induction variable"
  2534  		if i < len(x) {
  2535  			s += x[i] // ERROR "Proved IsInBounds"
  2536  		}
  2537  	}
  2538  	return s
  2539  }
  2540  
  2541  func rangebound2(x []int) int {
  2542  	s := 0
  2543  	if len(x) > 0 {
  2544  		for i := range 1000 { // ERROR "Induction variable"
  2545  			s += x[i%len(x)] // ERROR "Proved Mod64 is unsigned" "Proved Neq64" "Proved IsInBounds"
  2546  		}
  2547  	}
  2548  	return s
  2549  }
  2550  
  2551  func swapbound(v []int) {
  2552  	for i := 0; i < len(v)/2; i++ { // ERROR "Proved Div64 is unsigned|Induction variable"
  2553  		v[i], // ERROR "Proved IsInBounds"
  2554  			v[len(v)-1-i] = // ERROR "Proved IsInBounds"
  2555  			v[len(v)-1-i],
  2556  			v[i] // ERROR "Proved IsInBounds"
  2557  	}
  2558  }
  2559  
  2560  func rightshift(v *[256]int) int {
  2561  	for i := range 1024 { // ERROR "Induction"
  2562  		if v[i/32] == 0 { // ERROR "Proved Div64 is unsigned" "Proved IsInBounds"
  2563  			return i
  2564  		}
  2565  	}
  2566  	for i := range 1024 { // ERROR "Induction"
  2567  		if v[i>>2] == 0 { // ERROR "(Proved IsInBounds|Proved Rsh64x64 is unsigned)"
  2568  			return i
  2569  		}
  2570  	}
  2571  	return -1
  2572  }
  2573  
  2574  func rightShiftBounds(v, s int) {
  2575  	// The ignored "Proved" messages on the shift itself are about whether s >= 0 or s < 32 or 64.
  2576  	// We care about the bounds for x printed on the prove(x) lines.
  2577  
  2578  	if -8 <= v && v <= -2 && 1 <= s && s <= 3 {
  2579  		x := v >> s // ERROR "Proved"
  2580  		prove(x)    // ERROR "Proved sm,SM=-4,-1 "
  2581  	}
  2582  	if -80 <= v && v <= -20 && 1 <= s && s <= 3 {
  2583  		x := v >> s // ERROR "Proved"
  2584  		prove(x)    // ERROR "Proved sm,SM=-40,-3 "
  2585  	}
  2586  	if -8 <= v && v <= 10 && 1 <= s && s <= 3 {
  2587  		x := v >> s // ERROR "Proved"
  2588  		prove(x)    // ERROR "Proved sm,SM=-4,5 "
  2589  	}
  2590  	if 2 <= v && v <= 10 && 1 <= s && s <= 3 {
  2591  		x := v >> s // ERROR "Proved"
  2592  		prove(x)    // ERROR "Proved sm,SM=0,5 "
  2593  	}
  2594  
  2595  	if -8 <= v && v <= -2 && 0 <= s && s <= 3 {
  2596  		x := v >> s // ERROR "Proved"
  2597  		prove(x)    // ERROR "Proved sm,SM=-8,-1 "
  2598  	}
  2599  	if -80 <= v && v <= -20 && 0 <= s && s <= 3 {
  2600  		x := v >> s // ERROR "Proved"
  2601  		prove(x)    // ERROR "Proved sm,SM=-80,-3 "
  2602  	}
  2603  	if -8 <= v && v <= 10 && 0 <= s && s <= 3 {
  2604  		x := v >> s // ERROR "Proved"
  2605  		prove(x)    // ERROR "Proved sm,SM=-8,10 "
  2606  	}
  2607  	if 2 <= v && v <= 10 && 0 <= s && s <= 3 {
  2608  		x := v >> s // ERROR "Proved"
  2609  		prove(x)    // ERROR "Proved sm,SM=0,10 "
  2610  	}
  2611  
  2612  	if -8 <= v && v <= -2 && -1 <= s && s <= 3 {
  2613  		x := v >> s // ERROR "Proved"
  2614  		prove(x)    // ERROR "Proved sm,SM=-8,-1 "
  2615  	}
  2616  	if -80 <= v && v <= -20 && -1 <= s && s <= 3 {
  2617  		x := v >> s // ERROR "Proved"
  2618  		prove(x)    // ERROR "Proved sm,SM=-80,-3 "
  2619  	}
  2620  	if -8 <= v && v <= 10 && -1 <= s && s <= 3 {
  2621  		x := v >> s // ERROR "Proved"
  2622  		prove(x)    // ERROR "Proved sm,SM=-8,10 "
  2623  	}
  2624  	if 2 <= v && v <= 10 && -1 <= s && s <= 3 {
  2625  		x := v >> s // ERROR "Proved"
  2626  		prove(x)    // ERROR "Proved sm,SM=0,10 "
  2627  	}
  2628  }
  2629  
  2630  func unsignedRightShiftBounds(v uint, s int) {
  2631  	if 2 <= v && v <= 10 && -1 <= s && s <= 3 {
  2632  		x := v >> s // ERROR "Proved"
  2633  		proveu(x)   // ERROR "Proved sm,SM=0,10 "
  2634  	}
  2635  	if 2 <= v && v <= 10 && 0 <= s && s <= 3 {
  2636  		x := v >> s // ERROR "Proved"
  2637  		proveu(x)   // ERROR "Proved sm,SM=0,10 "
  2638  	}
  2639  	if 2 <= v && v <= 10 && 1 <= s && s <= 3 {
  2640  		x := v >> s // ERROR "Proved"
  2641  		proveu(x)   // ERROR "Proved sm,SM=0,5 "
  2642  	}
  2643  	if 20 <= v && v <= 100 && 1 <= s && s <= 3 {
  2644  		x := v >> s // ERROR "Proved"
  2645  		proveu(x)   // ERROR "Proved sm,SM=2,50 "
  2646  	}
  2647  }
  2648  
  2649  func subLengths1(b []byte, i int) {
  2650  	if i >= 0 && i <= len(b) {
  2651  		_ = b[len(b)-i:] // ERROR "Proved IsSliceInBounds"
  2652  	}
  2653  }
  2654  
  2655  func subLengths2(b []byte, i int) {
  2656  	if i >= 0 && i <= len(b) {
  2657  		_ = b[:len(b)-i] // ERROR "Proved IsSliceInBounds"
  2658  	}
  2659  }
  2660  
  2661  func issue76355(s []int, i int) int {
  2662  	var a [10]int
  2663  	if i <= len(s)-1 {
  2664  		v := len(s) - i
  2665  		if v < 10 {
  2666  			return a[v]
  2667  		}
  2668  	}
  2669  	return 0
  2670  }
  2671  
  2672  func stringDotDotDot(s string) bool {
  2673  	for i := 0; i < len(s)-2; i++ { // ERROR "Induction variable: limits \[0,[?][)], increment 1"
  2674  		if s[i] == '.' && // ERROR "Proved IsInBounds"
  2675  			s[i+1] == '.' && // ERROR "Proved IsInBounds"
  2676  			s[i+2] == '.' { // ERROR "Proved IsInBounds"
  2677  			return true
  2678  		}
  2679  	}
  2680  	return false
  2681  }
  2682  
  2683  func bytesDotDotDot(s []byte) bool {
  2684  	for i := 0; i < len(s)-2; i++ { // ERROR "Induction variable"
  2685  		if s[i] == '.' && // ERROR "Proved IsInBounds"
  2686  			s[i+1] == '.' && // ERROR "Proved IsInBounds"
  2687  			s[i+2] == '.' { // ERROR "Proved IsInBounds"
  2688  			return true
  2689  		}
  2690  	}
  2691  	return false
  2692  }
  2693  
  2694  // detectSliceLenRelation matches the pattern where
  2695  //  1. v := slicelen - index, OR v := slicecap - index
  2696  //     AND
  2697  //  2. index <= slicelen - K
  2698  //     THEN
  2699  //
  2700  // slicecap - index >= slicelen - index >= K
  2701  func detectSliceLenRelation(s []byte) bool {
  2702  	for i := 0; i <= len(s)-3; i++ { // ERROR "Induction variable"
  2703  		v := len(s) - i
  2704  		if v >= 3 { // ERROR "Proved Leq"
  2705  			return true
  2706  		}
  2707  	}
  2708  	return false
  2709  }
  2710  
  2711  func detectStringLenRelation(s string) bool {
  2712  	for i := 0; i <= len(s)-3; i++ { // ERROR "Induction variable"
  2713  		v := len(s) - i
  2714  		if v >= 3 { // ERROR "Proved Leq"
  2715  			return true
  2716  		}
  2717  	}
  2718  	return false
  2719  }
  2720  
  2721  func issue76688(x, y uint64) uint64 {
  2722  	if x > 1 || y != 1<<63 {
  2723  		return 42
  2724  	}
  2725  	// We do not want to rewrite the multiply to a condselect here since opt can do a better job with a left shift.
  2726  	return x * y
  2727  }
  2728  
  2729  //go:noinline
  2730  func prove(x int) {
  2731  }
  2732  
  2733  //go:noinline
  2734  func proveu(x uint) {
  2735  }
  2736  
  2737  //go:noinline
  2738  func useInt(a int) {
  2739  }
  2740  
  2741  //go:noinline
  2742  func useSlice(a []int) {
  2743  }
  2744  
  2745  func main() {
  2746  }
  2747  

View as plain text