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  	// 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]) // optimized away earlier by rewrite
   515  	// Test non-constant argument with known limits.
   516  	if cap(b) > 10 {
   517  		useSlice(b[2:]) // ERROR "Proved slicemask not needed$"
   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] // ERROR "Proved IsInBounds( for blocked indexing)?$"
   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] // ERROR "Proved IsInBounds( for blocked indexing)?$"
   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] // ERROR "Proved IsInBounds( for blocked indexing)?$"
   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] // ERROR "Proved IsInBounds( for blocked indexing)?$"
   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  // These cases are division of a positive signed integer by a power of 2.
   975  // The opt pass doesnt have sufficient information to see that n is positive.
   976  // So, instead, opt rewrites the division with a less-than-optimal replacement.
   977  // Prove, which can see that n is nonnegative, cannot see the division because
   978  // opt, an earlier pass, has already replaced it.
   979  // The fix for this issue allows prove to zero a right shift that was added as
   980  // part of the less-than-optimal reqwrite. That change by prove then allows
   981  // lateopt to clean up all the unnecessary parts of the original division
   982  // replacement. See issue #36159.
   983  func divShiftClean(n int) int {
   984  	if n < 0 {
   985  		return n
   986  	}
   987  	return n / int(8) // ERROR "Proved Div64 is unsigned$"
   988  }
   989  
   990  func divShiftClean64(n int64) int64 {
   991  	if n < 0 {
   992  		return n
   993  	}
   994  	return n / int64(16)  // ERROR "Proved Div64 is unsigned$"
   995  }
   996  
   997  func divShiftClean32(n int32) int32 {
   998  	if n < 0 {
   999  		return n
  1000  	}
  1001  	return n / int32(16)  // ERROR "Proved Div32 is unsigned$"
  1002  }
  1003  
  1004  // Bounds check elimination
  1005  
  1006  func sliceBCE1(p []string, h uint) string {
  1007  	if len(p) == 0 {
  1008  		return ""
  1009  	}
  1010  
  1011  	i := h & uint(len(p)-1)
  1012  	return p[i] // ERROR "Proved IsInBounds$"
  1013  }
  1014  
  1015  func sliceBCE2(p []string, h int) string {
  1016  	if len(p) == 0 {
  1017  		return ""
  1018  	}
  1019  	i := h & (len(p) - 1)
  1020  	return p[i] // ERROR "Proved IsInBounds$"
  1021  }
  1022  
  1023  func and(p []byte) ([]byte, []byte) { // issue #52563
  1024  	const blocksize = 16
  1025  	fullBlocks := len(p) &^ (blocksize - 1)
  1026  	blk := p[:fullBlocks] // ERROR "Proved IsSliceInBounds$"
  1027  	rem := p[fullBlocks:] // ERROR "Proved IsSliceInBounds$"
  1028  	return blk, rem
  1029  }
  1030  
  1031  func rshu(x, y uint) int {
  1032  	z := x >> y
  1033  	if z <= x { // ERROR "Proved Leq64U$"
  1034  		return 1
  1035  	}
  1036  	return 0
  1037  }
  1038  
  1039  func divu(x, y uint) int {
  1040  	z := x / y
  1041  	if z <= x { // ERROR "Proved Leq64U$"
  1042  		return 1
  1043  	}
  1044  	return 0
  1045  }
  1046  
  1047  func divuRoundUp(x, y, z uint) int {
  1048  	x &= ^uint(0) >> 8 // can't overflow in add
  1049  	y = min(y, 0xff-1)
  1050  	z = max(z, 0xff)
  1051  	r := (x + y) / z // ERROR "Proved Neq64$"
  1052  	if r <= x {      // ERROR "Proved Leq64U$"
  1053  		return 1
  1054  	}
  1055  	return 0
  1056  }
  1057  
  1058  func divuRoundUpSlice(x []string) {
  1059  	halfRoundedUp := uint(len(x)+1) / 2
  1060  	_ = x[:halfRoundedUp] // ERROR "Proved IsSliceInBounds$"
  1061  	_ = x[halfRoundedUp:] // ERROR "Proved IsSliceInBounds$"
  1062  }
  1063  
  1064  func modu1(x, y uint) int {
  1065  	z := x % y
  1066  	if z < y { // ERROR "Proved Less64U$"
  1067  		return 1
  1068  	}
  1069  	return 0
  1070  }
  1071  
  1072  func modu2(x, y uint) int {
  1073  	z := x % y
  1074  	if z <= x { // ERROR "Proved Leq64U$"
  1075  		return 1
  1076  	}
  1077  	return 0
  1078  }
  1079  
  1080  func issue57077(s []int) (left, right []int) {
  1081  	middle := len(s) / 2 // ERROR "Proved Div64 is unsigned$"
  1082  	left = s[:middle]  // ERROR "Proved IsSliceInBounds$"
  1083  	right = s[middle:] // ERROR "Proved IsSliceInBounds$"
  1084  	return
  1085  }
  1086  
  1087  func issue51622(b []byte) int {
  1088  	if len(b) >= 3 && b[len(b)-3] == '#' { // ERROR "Proved IsInBounds$"
  1089  		return len(b)
  1090  	}
  1091  	return 0
  1092  }
  1093  
  1094  func issue45928(x int) {
  1095  	combinedFrac := x / (x | (1 << 31)) // ERROR "Proved Neq64$"
  1096  	useInt(combinedFrac)
  1097  }
  1098  
  1099  func constantBounds1(i, j uint) int {
  1100  	var a [10]int
  1101  	if j < 11 && i < j {
  1102  		return a[i] // ERROR "Proved IsInBounds$"
  1103  	}
  1104  	return 0
  1105  }
  1106  
  1107  func constantBounds2(i, j uint) int {
  1108  	var a [10]int
  1109  	if i < j && j < 11 {
  1110  		return a[i] // ERROR "Proved IsInBounds"
  1111  	}
  1112  	return 0
  1113  }
  1114  
  1115  func constantBounds3(i, j, k, l uint) int {
  1116  	var a [8]int
  1117  	if i < j && j < k && k < l && l < 11 {
  1118  		return a[i] // ERROR "Proved IsInBounds"
  1119  	}
  1120  	return 0
  1121  }
  1122  
  1123  func equalityPropagation(a [1]int, i, j uint) int {
  1124  	if i == j && i == 5 {
  1125  		return a[j-5] // ERROR "Proved IsInBounds"
  1126  	}
  1127  	return 0
  1128  }
  1129  func inequalityPropagation(a [1]int, i, j uint) int {
  1130  	if i != j && j >= 5 && j <= 6 && i == 5 {
  1131  		return a[j-6] // ERROR "Proved IsInBounds"
  1132  	}
  1133  	return 0
  1134  }
  1135  
  1136  func issue66826a(a [21]byte) {
  1137  	for i := 0; i <= 10; i++ { // ERROR "Induction variable: limits \[0,10\], increment 1$"
  1138  		_ = a[2*i] // ERROR "Proved IsInBounds"
  1139  	}
  1140  }
  1141  func issue66826b(a [31]byte, i int) {
  1142  	if i < 0 || i > 10 {
  1143  		return
  1144  	}
  1145  	_ = a[3*i] // ERROR "Proved IsInBounds"
  1146  }
  1147  
  1148  func f20(a, b bool) int {
  1149  	if a == b {
  1150  		if a {
  1151  			if b { // ERROR "Proved Arg"
  1152  				return 1
  1153  			}
  1154  		}
  1155  	}
  1156  	return 0
  1157  }
  1158  
  1159  func f21(a, b *int) int {
  1160  	if a == b {
  1161  		if a != nil {
  1162  			if b != nil { // ERROR "Proved IsNonNil"
  1163  				return 1
  1164  			}
  1165  		}
  1166  	}
  1167  	return 0
  1168  }
  1169  
  1170  func f22(b bool, x, y int) int {
  1171  	b2 := x < y
  1172  	if b == b2 {
  1173  		if b {
  1174  			if x >= y { // ERROR "Disproved Leq64$"
  1175  				return 1
  1176  			}
  1177  		}
  1178  	}
  1179  	return 0
  1180  }
  1181  
  1182  func ctz64(x uint64, ensureBothBranchesCouldHappen bool) int {
  1183  	const max = math.MaxUint64
  1184  	sz := bits.Len64(max)
  1185  
  1186  	log2half := uint64(max) >> (sz / 2)
  1187  	if x >= log2half || x == 0 {
  1188  		return 42
  1189  	}
  1190  
  1191  	y := bits.TrailingZeros64(x) // ERROR "Proved Ctz64 non-zero$""
  1192  
  1193  	z := sz / 2
  1194  	if ensureBothBranchesCouldHappen {
  1195  		if y < z { // ERROR "Proved Less64$"
  1196  			return -42
  1197  		}
  1198  	} else {
  1199  		if y >= z { // ERROR "Disproved Leq64$"
  1200  			return 1337
  1201  		}
  1202  	}
  1203  
  1204  	return y
  1205  }
  1206  func ctz32(x uint32, ensureBothBranchesCouldHappen bool) int {
  1207  	const max = math.MaxUint32
  1208  	sz := bits.Len32(max)
  1209  
  1210  	log2half := uint32(max) >> (sz / 2)
  1211  	if x >= log2half || x == 0 {
  1212  		return 42
  1213  	}
  1214  
  1215  	y := bits.TrailingZeros32(x) // ERROR "Proved Ctz32 non-zero$""
  1216  
  1217  	z := sz / 2
  1218  	if ensureBothBranchesCouldHappen {
  1219  		if y < z { // ERROR "Proved Less64$"
  1220  			return -42
  1221  		}
  1222  	} else {
  1223  		if y >= z { // ERROR "Disproved Leq64$"
  1224  			return 1337
  1225  		}
  1226  	}
  1227  
  1228  	return y
  1229  }
  1230  func ctz16(x uint16, ensureBothBranchesCouldHappen bool) int {
  1231  	const max = math.MaxUint16
  1232  	sz := bits.Len16(max)
  1233  
  1234  	log2half := uint16(max) >> (sz / 2)
  1235  	if x >= log2half || x == 0 {
  1236  		return 42
  1237  	}
  1238  
  1239  	y := bits.TrailingZeros16(x) // ERROR "Proved Ctz16 non-zero$""
  1240  
  1241  	z := sz / 2
  1242  	if ensureBothBranchesCouldHappen {
  1243  		if y < z { // ERROR "Proved Less64$"
  1244  			return -42
  1245  		}
  1246  	} else {
  1247  		if y >= z { // ERROR "Disproved Leq64$"
  1248  			return 1337
  1249  		}
  1250  	}
  1251  
  1252  	return y
  1253  }
  1254  func ctz8(x uint8, ensureBothBranchesCouldHappen bool) int {
  1255  	const max = math.MaxUint8
  1256  	sz := bits.Len8(max)
  1257  
  1258  	log2half := uint8(max) >> (sz / 2)
  1259  	if x >= log2half || x == 0 {
  1260  		return 42
  1261  	}
  1262  
  1263  	y := bits.TrailingZeros8(x) // ERROR "Proved Ctz8 non-zero$""
  1264  
  1265  	z := sz / 2
  1266  	if ensureBothBranchesCouldHappen {
  1267  		if y < z { // ERROR "Proved Less64$"
  1268  			return -42
  1269  		}
  1270  	} else {
  1271  		if y >= z { // ERROR "Disproved Leq64$"
  1272  			return 1337
  1273  		}
  1274  	}
  1275  
  1276  	return y
  1277  }
  1278  
  1279  func bitLen64(x uint64, ensureBothBranchesCouldHappen bool) int {
  1280  	const max = math.MaxUint64
  1281  	sz := bits.Len64(max)
  1282  
  1283  	if x >= max>>3 {
  1284  		return 42
  1285  	}
  1286  	if x <= max>>6 {
  1287  		return 42
  1288  	}
  1289  
  1290  	y := bits.Len64(x)
  1291  
  1292  	if ensureBothBranchesCouldHappen {
  1293  		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
  1294  			return -42
  1295  		}
  1296  	} else {
  1297  		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
  1298  			return 1337
  1299  		}
  1300  	}
  1301  	return y
  1302  }
  1303  func bitLen32(x uint32, ensureBothBranchesCouldHappen bool) int {
  1304  	const max = math.MaxUint32
  1305  	sz := bits.Len32(max)
  1306  
  1307  	if x >= max>>3 {
  1308  		return 42
  1309  	}
  1310  	if x <= max>>6 {
  1311  		return 42
  1312  	}
  1313  
  1314  	y := bits.Len32(x)
  1315  
  1316  	if ensureBothBranchesCouldHappen {
  1317  		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
  1318  			return -42
  1319  		}
  1320  	} else {
  1321  		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
  1322  			return 1337
  1323  		}
  1324  	}
  1325  	return y
  1326  }
  1327  func bitLen16(x uint16, ensureBothBranchesCouldHappen bool) int {
  1328  	const max = math.MaxUint16
  1329  	sz := bits.Len16(max)
  1330  
  1331  	if x >= max>>3 {
  1332  		return 42
  1333  	}
  1334  	if x <= max>>6 {
  1335  		return 42
  1336  	}
  1337  
  1338  	y := bits.Len16(x)
  1339  
  1340  	if ensureBothBranchesCouldHappen {
  1341  		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
  1342  			return -42
  1343  		}
  1344  	} else {
  1345  		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
  1346  			return 1337
  1347  		}
  1348  	}
  1349  	return y
  1350  }
  1351  func bitLen8(x uint8, ensureBothBranchesCouldHappen bool) int {
  1352  	const max = math.MaxUint8
  1353  	sz := bits.Len8(max)
  1354  
  1355  	if x >= max>>3 {
  1356  		return 42
  1357  	}
  1358  	if x <= max>>6 {
  1359  		return 42
  1360  	}
  1361  
  1362  	y := bits.Len8(x)
  1363  
  1364  	if ensureBothBranchesCouldHappen {
  1365  		if sz-6 <= y && y <= sz-3 { // ERROR "Proved Leq64$"
  1366  			return -42
  1367  		}
  1368  	} else {
  1369  		if y < sz-6 || sz-3 < y { // ERROR "Disproved Less64$"
  1370  			return 1337
  1371  		}
  1372  	}
  1373  	return y
  1374  }
  1375  
  1376  func xor64(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1377  	a = min(a, 0xff)
  1378  	b = min(b, 0xfff)
  1379  
  1380  	z := a ^ b
  1381  
  1382  	if ensureBothBranchesCouldHappen {
  1383  		if z > 0xfff { // ERROR "Disproved Less64U$"
  1384  			return 42
  1385  		}
  1386  	} else {
  1387  		if z <= 0xfff { // ERROR "Proved Leq64U$"
  1388  			return 1337
  1389  		}
  1390  	}
  1391  	return int(z)
  1392  }
  1393  
  1394  func or64(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1395  	a = min(a, 0xff)
  1396  	b = min(b, 0xfff)
  1397  
  1398  	z := a | b
  1399  
  1400  	if ensureBothBranchesCouldHappen {
  1401  		if z > 0xfff { // ERROR "Disproved Less64U$"
  1402  			return 42
  1403  		}
  1404  	} else {
  1405  		if z <= 0xfff { // ERROR "Proved Leq64U$"
  1406  			return 1337
  1407  		}
  1408  	}
  1409  	return int(z)
  1410  }
  1411  
  1412  func mod64uWithSmallerDividendMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1413  	a = min(a, 0xff)
  1414  	b = min(b, 0xfff)
  1415  
  1416  	z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
  1417  
  1418  	if ensureBothBranchesCouldHappen {
  1419  		if z > bits.Len64(0xff) { // ERROR "Disproved Less64$"
  1420  			return 42
  1421  		}
  1422  	} else {
  1423  		if z <= bits.Len64(0xff) { // ERROR "Proved Leq64$"
  1424  			return 1337
  1425  		}
  1426  	}
  1427  	return z
  1428  }
  1429  func mod64uWithSmallerDivisorMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1430  	a = min(a, 0xfff)
  1431  	b = min(b, 0x10) // we need bits.Len64(b.umax) != bits.Len64(b.umax-1)
  1432  
  1433  	z := bits.Len64(a % b) // see go.dev/issue/68857 for bits.Len64
  1434  
  1435  	if ensureBothBranchesCouldHappen {
  1436  		if z > bits.Len64(0x10-1) { // ERROR "Disproved Less64$"
  1437  			return 42
  1438  		}
  1439  	} else {
  1440  		if z <= bits.Len64(0x10-1) { // ERROR "Proved Leq64$"
  1441  			return 1337
  1442  		}
  1443  	}
  1444  	return z
  1445  }
  1446  func mod64uWithIdenticalMax(a, b uint64, ensureBothBranchesCouldHappen bool) int {
  1447  	a = min(a, 0x10)
  1448  	b = min(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 mod64sPositiveWithSmallerDividendMax(a, b int64, ensureBothBranchesCouldHappen bool) int64 {
  1464  	if a < 0 || b < 0 {
  1465  		return 42
  1466  	}
  1467  	a = min(a, 0xff)
  1468  	b = min(b, 0xfff)
  1469  
  1470  	z := a % b // ERROR "Proved Mod64 is unsigned$"
  1471  
  1472  	if ensureBothBranchesCouldHappen {
  1473  		if z > 0xff { // ERROR "Disproved Less64$"
  1474  			return 42
  1475  		}
  1476  	} else {
  1477  		if z <= 0xff { // ERROR "Proved Leq64$"
  1478  			return 1337
  1479  		}
  1480  	}
  1481  	return z
  1482  }
  1483  func mod64sPositiveWithSmallerDivisorMax(a, b int64, ensureBothBranchesCouldHappen bool) int64 {
  1484  	if a < 0 || b < 0 {
  1485  		return 42
  1486  	}
  1487  	a = min(a, 0xfff)
  1488  	b = min(b, 0xff)
  1489  
  1490  	z := a % b // ERROR "Proved Mod64 is unsigned$"
  1491  
  1492  	if ensureBothBranchesCouldHappen {
  1493  		if z > 0xff-1 { // ERROR "Disproved Less64$"
  1494  			return 42
  1495  		}
  1496  	} else {
  1497  		if z <= 0xff-1 { // ERROR "Proved Leq64$"
  1498  			return 1337
  1499  		}
  1500  	}
  1501  	return z
  1502  }
  1503  func mod64sPositiveWithIdenticalMax(a, b int64, ensureBothBranchesCouldHappen bool) int64 {
  1504  	if a < 0 || b < 0 {
  1505  		return 42
  1506  	}
  1507  	a = min(a, 0xfff)
  1508  	b = min(b, 0xfff)
  1509  
  1510  	z := a % b // ERROR "Proved Mod64 is unsigned$"
  1511  
  1512  	if ensureBothBranchesCouldHappen {
  1513  		if z > 0xfff-1 { // ERROR "Disproved Less64$"
  1514  			return 42
  1515  		}
  1516  	} else {
  1517  		if z <= 0xfff-1 { // ERROR "Proved Leq64$"
  1518  			return 1337
  1519  		}
  1520  	}
  1521  	return z
  1522  }
  1523  
  1524  func div64u(a, b uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
  1525  	a = min(a, 0xffff)
  1526  	a = max(a, 0xfff)
  1527  	b = min(b, 0xff)
  1528  	b = max(b, 0xf)
  1529  
  1530  	z := a / b // ERROR "Proved Neq64$"
  1531  
  1532  	if ensureAllBranchesCouldHappen() && z > 0xffff/0xf { // ERROR "Disproved Less64U$"
  1533  		return 42
  1534  	}
  1535  	if ensureAllBranchesCouldHappen() && z <= 0xffff/0xf { // ERROR "Proved Leq64U$"
  1536  		return 1337
  1537  	}
  1538  	if ensureAllBranchesCouldHappen() && z < 0xfff/0xff { // ERROR "Disproved Less64U$"
  1539  		return 42
  1540  	}
  1541  	if ensureAllBranchesCouldHappen() && z >= 0xfff/0xff { // ERROR "Proved Leq64U$"
  1542  		return 42
  1543  	}
  1544  	return z
  1545  }
  1546  func div64s(a, b int64, ensureAllBranchesCouldHappen func() bool) int64 {
  1547  	if a < 0 || b < 0 {
  1548  		return 42
  1549  	}
  1550  	a = min(a, 0xffff)
  1551  	a = max(a, 0xfff)
  1552  	b = min(b, 0xff)
  1553  	b = max(b, 0xf)
  1554  
  1555  	z := a / b // ERROR "Proved Div64 is unsigned|Proved Neq64"
  1556  
  1557  	if ensureAllBranchesCouldHappen() && z > 0xffff/0xf { // ERROR "Disproved Less64$"
  1558  		return 42
  1559  	}
  1560  	if ensureAllBranchesCouldHappen() && z <= 0xffff/0xf { // ERROR "Proved Leq64$"
  1561  		return 1337
  1562  	}
  1563  	if ensureAllBranchesCouldHappen() && z < 0xfff/0xff { // ERROR "Disproved Less64$"
  1564  		return 42
  1565  	}
  1566  	if ensureAllBranchesCouldHappen() && z >= 0xfff/0xff { // ERROR "Proved Leq64$"
  1567  		return 42
  1568  	}
  1569  	return z
  1570  }
  1571  
  1572  func trunc64to16(a uint64, ensureAllBranchesCouldHappen func() bool) uint16 {
  1573  	a = min(a, 0xfff)
  1574  	a = max(a, 0xff)
  1575  
  1576  	z := uint16(a)
  1577  	if ensureAllBranchesCouldHappen() && z > 0xfff { // ERROR "Disproved Less16U$"
  1578  		return 42
  1579  	}
  1580  	if ensureAllBranchesCouldHappen() && z <= 0xfff { // ERROR "Proved Leq16U$"
  1581  		return 1337
  1582  	}
  1583  	if ensureAllBranchesCouldHappen() && z < 0xff { // ERROR "Disproved Less16U$"
  1584  		return 42
  1585  	}
  1586  	if ensureAllBranchesCouldHappen() && z >= 0xff { // ERROR "Proved Leq16U$"
  1587  		return 1337
  1588  	}
  1589  	return z
  1590  }
  1591  
  1592  func com64(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
  1593  	a = min(a, 0xffff)
  1594  	a = max(a, 0xff)
  1595  
  1596  	z := ^a
  1597  
  1598  	if ensureAllBranchesCouldHappen() && z > ^uint64(0xff) { // ERROR "Disproved Less64U$"
  1599  		return 42
  1600  	}
  1601  	if ensureAllBranchesCouldHappen() && z <= ^uint64(0xff) { // ERROR "Proved Leq64U$"
  1602  		return 1337
  1603  	}
  1604  	if ensureAllBranchesCouldHappen() && z < ^uint64(0xffff) { // ERROR "Disproved Less64U$"
  1605  		return 42
  1606  	}
  1607  	if ensureAllBranchesCouldHappen() && z >= ^uint64(0xffff) { // ERROR "Proved Leq64U$"
  1608  		return 1337
  1609  	}
  1610  	return z
  1611  }
  1612  
  1613  func neg64(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
  1614  	var lo, hi uint64 = 0xff, 0xfff
  1615  	a = min(a, hi)
  1616  	a = max(a, lo)
  1617  
  1618  	z := -a
  1619  
  1620  	if ensureAllBranchesCouldHappen() && z > -lo { // ERROR "Disproved Less64U$"
  1621  		return 42
  1622  	}
  1623  	if ensureAllBranchesCouldHappen() && z <= -lo { // ERROR "Proved Leq64U$"
  1624  		return 1337
  1625  	}
  1626  	if ensureAllBranchesCouldHappen() && z < -hi { // ERROR "Disproved Less64U$"
  1627  		return 42
  1628  	}
  1629  	if ensureAllBranchesCouldHappen() && z >= -hi { // ERROR "Proved Leq64U$"
  1630  		return 1337
  1631  	}
  1632  	return z
  1633  }
  1634  func neg64mightOverflowDuringNeg(a uint64, ensureAllBranchesCouldHappen func() bool) uint64 {
  1635  	var lo, hi uint64 = 0, 0xfff
  1636  	a = min(a, hi)
  1637  	a = max(a, lo)
  1638  
  1639  	z := -a
  1640  
  1641  	if ensureAllBranchesCouldHappen() && z > -lo {
  1642  		return 42
  1643  	}
  1644  	if ensureAllBranchesCouldHappen() && z <= -lo {
  1645  		return 1337
  1646  	}
  1647  	if ensureAllBranchesCouldHappen() && z < -hi {
  1648  		return 42
  1649  	}
  1650  	if ensureAllBranchesCouldHappen() && z >= -hi {
  1651  		return 1337
  1652  	}
  1653  	return z
  1654  }
  1655  
  1656  func phiMin(a, b []byte) {
  1657  	_ = a[:min(len(a), len(b))] // ERROR "Proved IsSliceInBounds"
  1658  	_ = b[:min(len(a), len(b))] // ERROR "Proved IsSliceInBounds"
  1659  	_ = a[:max(len(a), len(b))]
  1660  	_ = b[:max(len(a), len(b))]
  1661  	x := len(a)
  1662  	if x > len(b) {
  1663  		x = len(b)
  1664  		useInt(0)
  1665  	}
  1666  	_ = a[:x] // ERROR "Proved IsSliceInBounds"
  1667  	y := len(a)
  1668  	if y > len(b) {
  1669  		y = len(b)
  1670  		useInt(0)
  1671  	} else {
  1672  		useInt(1)
  1673  	}
  1674  	_ = b[:y] // ERROR "Proved IsSliceInBounds"
  1675  }
  1676  
  1677  func minPhiLeq[T uint | int](x, y T) (z T) {
  1678  	if x <= y {
  1679  		z = x
  1680  	} else {
  1681  		z = y
  1682  	}
  1683  	return z
  1684  }
  1685  func maxPhiLeq[T uint | int](x, y T) (z T) {
  1686  	if y <= x {
  1687  		z = x
  1688  	} else {
  1689  		z = y
  1690  	}
  1691  	return z
  1692  }
  1693  func mathBasedOnPhiLosangeMinUFirstLeq(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1694  	const maxc = 0xf2a
  1695  	const minc = 0xf0a
  1696  	x = minPhiLeq(x, maxc)
  1697  	x = maxPhiLeq(x, minc)
  1698  
  1699  	const k = 1
  1700  	x += k
  1701  
  1702  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1703  		return 42
  1704  	}
  1705  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1706  		return 4242
  1707  	}
  1708  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1709  		return 424242
  1710  	}
  1711  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1712  		return 42424242
  1713  	}
  1714  	return x
  1715  }
  1716  func mathBasedOnPhiLosangeMinUSecondLeq(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1717  	const maxc = 0xf2a
  1718  	const minc = 0xf0a
  1719  	x = maxPhiLeq(x, minc)
  1720  	x = minPhiLeq(x, maxc)
  1721  
  1722  	const k = 1
  1723  	x += k
  1724  
  1725  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1726  		return 42
  1727  	}
  1728  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1729  		return 4242
  1730  	}
  1731  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1732  		return 424242
  1733  	}
  1734  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1735  		return 42424242
  1736  	}
  1737  	return x
  1738  }
  1739  func mathBasedOnPhiLosangeMinFirstLeq(x int, ensureAllBranchesCouldHappen func() bool) int {
  1740  	const maxc = 0xf2a
  1741  	const minc = 0xf0a
  1742  	x = minPhiLeq(x, maxc)
  1743  	x = maxPhiLeq(x, minc)
  1744  
  1745  	const k = 1
  1746  	x += k
  1747  
  1748  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1749  		return 42
  1750  	}
  1751  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1752  		return 4242
  1753  	}
  1754  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1755  		return 424242
  1756  	}
  1757  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1758  		return 42424242
  1759  	}
  1760  	return x
  1761  }
  1762  func mathBasedOnPhiLosangeMinSecondLeq(x int, ensureAllBranchesCouldHappen func() bool) int {
  1763  	const maxc = 0xf2a
  1764  	const minc = 0xf0a
  1765  	x = maxPhiLeq(x, minc)
  1766  	x = minPhiLeq(x, maxc)
  1767  
  1768  	const k = 1
  1769  	x += k
  1770  
  1771  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1772  		return 42
  1773  	}
  1774  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1775  		return 4242
  1776  	}
  1777  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1778  		return 424242
  1779  	}
  1780  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1781  		return 42424242
  1782  	}
  1783  	return x
  1784  }
  1785  
  1786  func minPhiLess[T uint | int](x, y T) (z T) {
  1787  	if x < y {
  1788  		z = x
  1789  	} else {
  1790  		z = y
  1791  	}
  1792  	return z
  1793  }
  1794  func maxPhiLess[T uint | int](x, y T) (z T) {
  1795  	if y < x {
  1796  		z = x
  1797  	} else {
  1798  		z = y
  1799  	}
  1800  	return z
  1801  }
  1802  func mathBasedOnPhiLosangeMinUFirstLess(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1803  	const maxc = 0xf2a
  1804  	const minc = 0xf0a
  1805  	x = minPhiLess(x, maxc)
  1806  	x = maxPhiLess(x, minc)
  1807  
  1808  	const k = 1
  1809  	x += k
  1810  
  1811  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1812  		return 42
  1813  	}
  1814  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1815  		return 4242
  1816  	}
  1817  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1818  		return 424242
  1819  	}
  1820  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1821  		return 42424242
  1822  	}
  1823  	return x
  1824  }
  1825  func mathBasedOnPhiLosangeMinUSecondLess(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1826  	const maxc = 0xf2a
  1827  	const minc = 0xf0a
  1828  	x = maxPhiLess(x, minc)
  1829  	x = minPhiLess(x, maxc)
  1830  
  1831  	const k = 1
  1832  	x += k
  1833  
  1834  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1835  		return 42
  1836  	}
  1837  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1838  		return 4242
  1839  	}
  1840  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1841  		return 424242
  1842  	}
  1843  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1844  		return 42424242
  1845  	}
  1846  	return x
  1847  }
  1848  func mathBasedOnPhiLosangeMinFirstLess(x int, ensureAllBranchesCouldHappen func() bool) int {
  1849  	const maxc = 0xf2a
  1850  	const minc = 0xf0a
  1851  	x = minPhiLess(x, maxc)
  1852  	x = maxPhiLess(x, minc)
  1853  
  1854  	const k = 1
  1855  	x += k
  1856  
  1857  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1858  		return 42
  1859  	}
  1860  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1861  		return 4242
  1862  	}
  1863  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1864  		return 424242
  1865  	}
  1866  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1867  		return 42424242
  1868  	}
  1869  	return x
  1870  }
  1871  func mathBasedOnPhiLosangeMinSecondLess(x int, ensureAllBranchesCouldHappen func() bool) int {
  1872  	const maxc = 0xf2a
  1873  	const minc = 0xf0a
  1874  	x = maxPhiLess(x, minc)
  1875  	x = minPhiLess(x, maxc)
  1876  
  1877  	const k = 1
  1878  	x += k
  1879  
  1880  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1881  		return 42
  1882  	}
  1883  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1884  		return 4242
  1885  	}
  1886  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1887  		return 424242
  1888  	}
  1889  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1890  		return 42424242
  1891  	}
  1892  	return x
  1893  }
  1894  
  1895  func mathBasedOnPhiBuiltinMinUFirst(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1896  	const maxc = 0xf2a
  1897  	const minc = 0xf0a
  1898  	x = min(x, maxc)
  1899  	x = max(x, minc)
  1900  
  1901  	const k = 1
  1902  	x += k
  1903  
  1904  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1905  		return 42
  1906  	}
  1907  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1908  		return 4242
  1909  	}
  1910  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1911  		return 424242
  1912  	}
  1913  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1914  		return 42424242
  1915  	}
  1916  	return x
  1917  }
  1918  func mathBasedOnPhiBuiltinMinUSecond(x uint, ensureAllBranchesCouldHappen func() bool) uint {
  1919  	const maxc = 0xf2a
  1920  	const minc = 0xf0a
  1921  	x = max(x, minc)
  1922  	x = min(x, maxc)
  1923  
  1924  	const k = 1
  1925  	x += k
  1926  
  1927  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64U$"
  1928  		return 42
  1929  	}
  1930  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64U$"
  1931  		return 4242
  1932  	}
  1933  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64U$"
  1934  		return 424242
  1935  	}
  1936  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64U$"
  1937  		return 42424242
  1938  	}
  1939  	return x
  1940  }
  1941  func mathBasedOnPhiBuiltinMinFirst(x int, ensureAllBranchesCouldHappen func() bool) int {
  1942  	const maxc = 0xf2a
  1943  	const minc = 0xf0a
  1944  	x = min(x, maxc)
  1945  	x = max(x, minc)
  1946  
  1947  	const k = 1
  1948  	x += k
  1949  
  1950  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1951  		return 42
  1952  	}
  1953  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1954  		return 4242
  1955  	}
  1956  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1957  		return 424242
  1958  	}
  1959  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1960  		return 42424242
  1961  	}
  1962  	return x
  1963  }
  1964  func mathBasedOnPhiBuiltinMinSecond(x int, ensureAllBranchesCouldHappen func() bool) int {
  1965  	const maxc = 0xf2a
  1966  	const minc = 0xf0a
  1967  	x = max(x, minc)
  1968  	x = min(x, maxc)
  1969  
  1970  	const k = 1
  1971  	x += k
  1972  
  1973  	if ensureAllBranchesCouldHappen() && x > maxc+k { // ERROR "Disproved Less64$"
  1974  		return 42
  1975  	}
  1976  	if ensureAllBranchesCouldHappen() && x <= maxc+k { // ERROR "Proved Leq64$"
  1977  		return 4242
  1978  	}
  1979  	if ensureAllBranchesCouldHappen() && x < minc+k { // ERROR "Disproved Less64$"
  1980  		return 424242
  1981  	}
  1982  	if ensureAllBranchesCouldHappen() && x >= minc+k { // ERROR "Proved Leq64$"
  1983  		return 42424242
  1984  	}
  1985  	return x
  1986  }
  1987  
  1988  func issue16833(a, b []byte) {
  1989  	n := copy(a, b)
  1990  	_ = a[n:] // ERROR "Proved IsSliceInBounds"
  1991  	_ = b[n:] // ERROR "Proved IsSliceInBounds"
  1992  	_ = a[:n] // ERROR "Proved IsSliceInBounds"
  1993  	_ = b[:n] // ERROR "Proved IsSliceInBounds"
  1994  }
  1995  
  1996  func clampedIdx1(x []int, i int) int {
  1997  	if len(x) == 0 {
  1998  		return 0
  1999  	}
  2000  	return x[min(max(0, i), len(x)-1)] // ERROR "Proved IsInBounds"
  2001  }
  2002  func clampedIdx2(x []int, i int) int {
  2003  	if len(x) == 0 {
  2004  		return 0
  2005  	}
  2006  	return x[max(min(i, len(x)-1), 0)] // TODO: can't get rid of this bounds check yet
  2007  }
  2008  
  2009  func cvtBoolToUint8Disprove(b bool) byte {
  2010  	var c byte
  2011  	if b {
  2012  		c = 1
  2013  	}
  2014  	if c == 2 { // ERROR "Disproved Eq8"
  2015  		c = 3
  2016  	}
  2017  	return c
  2018  }
  2019  func cvtBoolToUint8BCE(b bool, a [2]int64) int64 {
  2020  	c := byte(0)
  2021  	if b {
  2022  		c = 1
  2023  	}
  2024  	return a[c] // ERROR "Proved IsInBounds$"
  2025  }
  2026  
  2027  func transitiveProofsThroughNonOverflowingUnsignedAdd(x, y, z uint64) {
  2028  	x &= 1<<63 - 1
  2029  	y &= 1<<63 - 1
  2030  
  2031  	a := x + y
  2032  	if a > z {
  2033  		return
  2034  	}
  2035  
  2036  	if x > z { // ERROR "Disproved Less64U$"
  2037  		return
  2038  	}
  2039  	if y > z { // ERROR "Disproved Less64U$"
  2040  		return
  2041  	}
  2042  	if a == x {
  2043  		return
  2044  	}
  2045  	if a == y {
  2046  		return
  2047  	}
  2048  
  2049  	x |= 1
  2050  	y |= 1
  2051  	a = x + y
  2052  	if a == x { // ERROR "Disproved Eq64$"
  2053  		return
  2054  	}
  2055  	if a == y { // ERROR "Disproved Eq64$"
  2056  		return
  2057  	}
  2058  }
  2059  
  2060  func transitiveProofsThroughOverflowingUnsignedAdd(x, y, z uint64) {
  2061  	a := x + y
  2062  	if a > z {
  2063  		return
  2064  	}
  2065  
  2066  	if x > z {
  2067  		return
  2068  	}
  2069  	if y > z {
  2070  		return
  2071  	}
  2072  	if a == x {
  2073  		return
  2074  	}
  2075  	if a == y {
  2076  		return
  2077  	}
  2078  
  2079  	x |= 1
  2080  	y |= 1
  2081  	a = x + y
  2082  	if a == x {
  2083  		return
  2084  	}
  2085  	if a == y {
  2086  		return
  2087  	}
  2088  }
  2089  
  2090  func transitiveProofsThroughNonOverflowingSignedAddPositive(x, y, z int64) {
  2091  	x &= 1<<62 - 1
  2092  	y &= 1<<62 - 1
  2093  
  2094  	a := x + y
  2095  	if a > z {
  2096  		return
  2097  	}
  2098  
  2099  	if x > z { // ERROR "Disproved Less64$"
  2100  		return
  2101  	}
  2102  	if y > z { // ERROR "Disproved Less64$"
  2103  		return
  2104  	}
  2105  	if a == x {
  2106  		return
  2107  	}
  2108  	if a == y {
  2109  		return
  2110  	}
  2111  
  2112  	x |= 1
  2113  	y |= 1
  2114  	a = x + y
  2115  	if a == x { // ERROR "Disproved Eq64$"
  2116  		return
  2117  	}
  2118  	if a == y { // ERROR "Disproved Eq64$"
  2119  		return
  2120  	}
  2121  }
  2122  
  2123  func transitiveProofsThroughOverflowingSignedAddPositive(x, y, z int64) {
  2124  	if x < 0 || y < 0 {
  2125  		return
  2126  	}
  2127  
  2128  	a := x + y
  2129  	if a > z {
  2130  		return
  2131  	}
  2132  
  2133  	if x > z {
  2134  		return
  2135  	}
  2136  	if y > z {
  2137  		return
  2138  	}
  2139  	if a == x {
  2140  		return
  2141  	}
  2142  	if a == y {
  2143  		return
  2144  	}
  2145  
  2146  	x |= 1
  2147  	y |= 1
  2148  	a = x + y
  2149  	if a == x { // ERROR "Disproved Eq64$"
  2150  		return
  2151  	}
  2152  	if a == y { // ERROR "Disproved Eq64$"
  2153  		return
  2154  	}
  2155  }
  2156  
  2157  func transitiveProofsThroughNonOverflowingSignedAddNegative(x, y, z int64) {
  2158  	if x < math.MinInt64>>1 || x > 0 ||
  2159  		y < math.MinInt64>>1 || y > 0 {
  2160  		return
  2161  	}
  2162  
  2163  	a := x + y
  2164  	if a < z {
  2165  		return
  2166  	}
  2167  
  2168  	if x < z { // ERROR "Disproved Less64$"
  2169  		return
  2170  	}
  2171  	if y < z { // ERROR "Disproved Less64$"
  2172  		return
  2173  	}
  2174  	if a == x {
  2175  		return
  2176  	}
  2177  	if a == y {
  2178  		return
  2179  	}
  2180  
  2181  	if x == 0 && y == 0 {
  2182  		return
  2183  	}
  2184  	a = x + y
  2185  	if a == x { // ERROR "Disproved Eq64$"
  2186  		return
  2187  	}
  2188  	if a == y { // ERROR "Disproved Eq64$"
  2189  		return
  2190  	}
  2191  }
  2192  
  2193  func transitiveProofsThroughOverflowingSignedAddNegative(x, y, z int64) {
  2194  	if x >= 0 || y >= 0 {
  2195  		return
  2196  	}
  2197  
  2198  	a := x + y
  2199  	if a < z {
  2200  		return
  2201  	}
  2202  
  2203  	if x < z {
  2204  		return
  2205  	}
  2206  	if y < z {
  2207  		return
  2208  	}
  2209  	if a == x {
  2210  		return
  2211  	}
  2212  	if a == y {
  2213  		return
  2214  	}
  2215  
  2216  	x |= 1
  2217  	y |= 1
  2218  	a = x + y
  2219  	if a == x {
  2220  		return
  2221  	}
  2222  	if a == y {
  2223  		return
  2224  	}
  2225  }
  2226  
  2227  func transitiveProofsThroughNonOverflowingUnsignedSub(x, y, z uint64) {
  2228  	x |= 0xfff
  2229  	y &= 0xfff
  2230  
  2231  	a := x - y
  2232  	if a < z {
  2233  		return
  2234  	}
  2235  
  2236  	if x < z { // ERROR "Disproved Less64U$"
  2237  		return
  2238  	}
  2239  	if y < z {
  2240  		return
  2241  	}
  2242  	if a == x {
  2243  		return
  2244  	}
  2245  	if a == y {
  2246  		return
  2247  	}
  2248  
  2249  	y |= 1
  2250  	a = x - y
  2251  	if a == x { // ERROR "Disproved Eq64$"
  2252  		return
  2253  	}
  2254  	if a == y {
  2255  		return
  2256  	}
  2257  }
  2258  
  2259  func transitiveProofsThroughOverflowingUnsignedSub(x, y, z uint64) {
  2260  	a := x - y
  2261  	if a < z {
  2262  		return
  2263  	}
  2264  
  2265  	if x < z {
  2266  		return
  2267  	}
  2268  	if y < z {
  2269  		return
  2270  	}
  2271  	if a == x {
  2272  		return
  2273  	}
  2274  	if a == y {
  2275  		return
  2276  	}
  2277  
  2278  	y |= 1
  2279  	a = x - y
  2280  	if a == x {
  2281  		return
  2282  	}
  2283  	if a == y {
  2284  		return
  2285  	}
  2286  }
  2287  
  2288  func resliceString(s string) byte {
  2289  	if len(s) >= 4 {
  2290  		s = s[2:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
  2291  		s = s[1:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
  2292  		return s[0] // ERROR "Proved IsInBounds"
  2293  	}
  2294  	return 0
  2295  }
  2296  func resliceBytes(b []byte) byte {
  2297  	if len(b) >= 4 {
  2298  		b = b[2:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
  2299  		b = b[1:]   // ERROR "Proved IsSliceInBounds" "Proved slicemask not needed"
  2300  		return b[0] // ERROR "Proved IsInBounds"
  2301  	}
  2302  	return 0
  2303  }
  2304  
  2305  func issue74473(s []uint) {
  2306  	i := 0
  2307  	for {
  2308  		if i >= len(s) { // ERROR "Induction variable: limits \[0,\?\), increment 1$"
  2309  			break
  2310  		}
  2311  		_ = s[i] // ERROR "Proved IsInBounds$"
  2312  		i++
  2313  	}
  2314  }
  2315  
  2316  func setCapMaxBasedOnElementSize(x []uint64) int {
  2317  	c := uintptr(cap(x))
  2318  	max := ^uintptr(0) >> 3
  2319  	if c > max { // ERROR "Disproved Less"
  2320  		return 42
  2321  	}
  2322  	if c <= max { // ERROR "Proved Leq"
  2323  		return 1337
  2324  	}
  2325  	return 0
  2326  }
  2327  
  2328  func issue75144for(a, b []uint64) bool {
  2329  	if len(a) == len(b) {
  2330  		for len(a) > 4 {
  2331  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2332  			b = b[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2333  		}
  2334  		if len(a) == len(b) { // ERROR "Proved Eq64$"
  2335  			return true
  2336  		}
  2337  	}
  2338  	return false
  2339  }
  2340  
  2341  func issue75144if(a, b []uint64) bool {
  2342  	if len(a) == len(b) {
  2343  		if len(a) > 4 {
  2344  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2345  			b = b[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2346  		}
  2347  		if len(a) == len(b) { // ERROR "Proved Eq64$"
  2348  			return true
  2349  		}
  2350  	}
  2351  	return false
  2352  }
  2353  
  2354  func issue75144if2(a, b, c, d []uint64) (r bool) {
  2355  	if len(a) != len(b) || len(c) != len(d) {
  2356  		return
  2357  	}
  2358  	if len(a) <= 4 || len(c) <= 4 {
  2359  		return
  2360  	}
  2361  	if len(a) < len(c) {
  2362  		c = c[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2363  		d = d[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2364  	} else {
  2365  		a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2366  		b = b[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2367  	}
  2368  	if len(a) == len(c) {
  2369  		return
  2370  	}
  2371  	if len(a) == len(b) { // ERROR "Proved Eq64$"
  2372  		r = true
  2373  	}
  2374  	if len(c) == len(d) { // ERROR "Proved Eq64$"
  2375  		r = true
  2376  	}
  2377  	return
  2378  }
  2379  
  2380  func issue75144forCannot(a, b []uint64) bool {
  2381  	if len(a) == len(b) {
  2382  		for len(a) > 4 {
  2383  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2384  			b = b[4:]
  2385  			for len(a) > 2 {
  2386  				a = a[2:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2387  				b = b[2:]
  2388  			}
  2389  		}
  2390  		if len(a) == len(b) {
  2391  			return true
  2392  		}
  2393  	}
  2394  	return false
  2395  }
  2396  
  2397  func issue75144ifCannot(a, b []uint64) bool {
  2398  	if len(a) == len(b) {
  2399  		if len(a) > 4 {
  2400  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2401  			b = b[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2402  			if len(a) > 2 {
  2403  				a = a[2:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2404  				b = b[2:]
  2405  			}
  2406  		}
  2407  		if len(a) == len(b) {
  2408  			return true
  2409  		}
  2410  	}
  2411  	return false
  2412  }
  2413  
  2414  func issue75144ifCannot2(a, b []uint64) bool {
  2415  	if len(a) == len(b) {
  2416  		if len(a) > 4 {
  2417  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2418  			b = b[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2419  		} else if len(a) > 2 {
  2420  			a = a[2:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2421  			b = b[2:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2422  		}
  2423  		if len(a) == len(b) {
  2424  			return true
  2425  		}
  2426  	}
  2427  	return false
  2428  }
  2429  
  2430  func issue75144forNot(a, b []uint64) bool {
  2431  	if len(a) == len(b) {
  2432  		for len(a) > 4 {
  2433  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2434  			b = b[3:]
  2435  		}
  2436  		if len(a) == len(b) {
  2437  			return true
  2438  		}
  2439  	}
  2440  	return false
  2441  }
  2442  
  2443  func issue75144forNot2(a, b, c []uint64) bool {
  2444  	if len(a) == len(b) {
  2445  		for len(a) > 4 {
  2446  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2447  			b = c[4:]
  2448  		}
  2449  		if len(a) == len(b) {
  2450  			return true
  2451  		}
  2452  	}
  2453  	return false
  2454  }
  2455  
  2456  func issue75144ifNot(a, b []uint64) bool {
  2457  	if len(a) == len(b) {
  2458  		if len(a) > 4 {
  2459  			a = a[4:] // ERROR "Proved slicemask not needed$" "Proved IsSliceInBounds$"
  2460  		} else {
  2461  			b = b[4:]
  2462  		}
  2463  		if len(a) == len(b) {
  2464  			return true
  2465  		}
  2466  	}
  2467  	return false
  2468  }
  2469  
  2470  func mulIntoAnd(a, b uint) uint {
  2471  	if a > 1 || b > 1 {
  2472  		return 0
  2473  	}
  2474  	return a * b // ERROR "Rewrote Mul v[0-9]+ into And$"
  2475  }
  2476  
  2477  func mulIntoCondSelect(a, b uint) uint {
  2478  	if a > 1 {
  2479  		return 0
  2480  	}
  2481  	return a * b // ERROR "Rewrote Mul v[0-9]+ into CondSelect"
  2482  }
  2483  
  2484  func div7pos(x int32) bool {
  2485  	if x > 0 {
  2486  		return x%7 == 0 // ERROR "Proved Div32 is unsigned"
  2487  	}
  2488  	return false
  2489  }
  2490  
  2491  func div2pos(x []int) int {
  2492  	return len(x) / 2 // ERROR "Proved Div64 is unsigned"
  2493  }
  2494  
  2495  func div3pos(x []int) int {
  2496  	return len(x) / 3 // ERROR "Proved Div64 is unsigned"
  2497  }
  2498  
  2499  
  2500  var len200 [200]int
  2501  
  2502  func modbound1(u uint64) int {
  2503  	s := 0
  2504  	for u > 0 {
  2505  		var d uint64
  2506  		u, d = u/100, u%100
  2507  		s += len200[d*2+1] // ERROR "Proved IsInBounds"
  2508  	}
  2509  	return s
  2510  }
  2511  
  2512  func modbound2(p *[10]int, x uint) int {
  2513  	return p[x%9+1] // ERROR "Proved IsInBounds"
  2514  }
  2515  
  2516  func shiftbound(x int) int {
  2517  	return 1 << (x % 11) // ERROR "Proved Lsh(32x32|64x64) bounded" "Proved Div64 does not need fix-up"
  2518  }
  2519  
  2520  func shiftbound2(x int) int {
  2521  	return 1 << (x % 8) // ERROR "Proved Lsh(32x32|64x64) bounded" "Proved Div64 does not need fix-up"
  2522  }
  2523  
  2524  func rangebound1(x []int) int {
  2525  	s := 0
  2526  	for i := range 1000 { // ERROR "Induction variable"
  2527  		if i < len(x) {
  2528  			s += x[i] // ERROR "Proved IsInBounds"
  2529  		}
  2530  	}
  2531  	return s
  2532  }
  2533  
  2534  func rangebound2(x []int) int {
  2535  	s := 0
  2536  	if len(x) > 0 {
  2537  		for i := range 1000 { // ERROR "Induction variable"
  2538  			s += x[i%len(x)] // ERROR "Proved Mod64 is unsigned" "Proved Neq64" "Proved IsInBounds"
  2539  		}
  2540  	}
  2541  	return s
  2542  }
  2543  
  2544  func swapbound(v []int) {
  2545  	for i := 0; i < len(v)/2; i++ { // ERROR "Proved Div64 is unsigned|Induction variable"
  2546  		v[i], // ERROR "Proved IsInBounds"
  2547  		v[len(v)-1-i] = // ERROR "Proved IsInBounds"
  2548  		v[len(v)-1-i],
  2549  		v[i] // ERROR "Proved IsInBounds"
  2550  	}
  2551  }
  2552  
  2553  func rightshift(v *[256]int) int {
  2554  	for i := range 1024 { // ERROR "Induction"
  2555  		if v[i/32] == 0 { // ERROR "Proved Div64 is unsigned" "Proved IsInBounds"
  2556  			return i
  2557  		}
  2558  	}
  2559  	for i := range 1024 { // ERROR "Induction"
  2560  		if v[i>>2] == 0 { // ERROR "Proved IsInBounds"
  2561  			return i
  2562  		}
  2563  	}
  2564  	return -1
  2565  }
  2566  
  2567  func rightShiftBounds(v, s int) {
  2568  	// The ignored "Proved" messages on the shift itself are about whether s >= 0 or s < 32 or 64.
  2569  	// We care about the bounds for x printed on the prove(x) lines.
  2570  
  2571  	if -8 <= v && v <= -2 && 1 <= s && s <= 3 {
  2572  		x := v>>s // ERROR "Proved"
  2573  		prove(x) // ERROR "Proved sm,SM=-4,-1 "
  2574  	}
  2575  	if -80 <= v && v <= -20 && 1 <= s && s <= 3 {
  2576  		x := v>>s // ERROR "Proved"
  2577  		prove(x) // ERROR "Proved sm,SM=-40,-3 "
  2578  	}
  2579  	if -8 <= v && v <= 10 && 1 <= s && s <= 3 {
  2580  		x := v>>s // ERROR "Proved"
  2581  		prove(x) // ERROR "Proved sm,SM=-4,5 "
  2582  	}
  2583  	if 2 <= v && v <= 10 && 1 <= s && s <= 3 {
  2584  		x := v>>s // ERROR "Proved"
  2585  		prove(x) // ERROR "Proved sm,SM=0,5 "
  2586  	}
  2587  
  2588  	if -8 <= v && v <= -2 && 0 <= s && s <= 3 {
  2589  		x := v>>s // ERROR "Proved"
  2590  		prove(x) // ERROR "Proved sm,SM=-8,-1 "
  2591  	}
  2592  	if -80 <= v && v <= -20 && 0 <= s && s <= 3 {
  2593  		x := v>>s // ERROR "Proved"
  2594  		prove(x) // ERROR "Proved sm,SM=-80,-3 "
  2595  	}
  2596  	if -8 <= v && v <= 10 && 0 <= s && s <= 3 {
  2597  		x := v>>s // ERROR "Proved"
  2598  		prove(x) // ERROR "Proved sm,SM=-8,10 "
  2599  	}
  2600  	if 2 <= v && v <= 10 && 0 <= s && s <= 3 {
  2601  		x := v>>s // ERROR "Proved"
  2602  		prove(x) // ERROR "Proved sm,SM=0,10 "
  2603  	}
  2604  
  2605  	if -8 <= v && v <= -2 && -1 <= s && s <= 3 {
  2606  		x := v>>s // ERROR "Proved"
  2607  		prove(x) // ERROR "Proved sm,SM=-8,-1 "
  2608  	}
  2609  	if -80 <= v && v <= -20 && -1 <= s && s <= 3 {
  2610  		x := v>>s // ERROR "Proved"
  2611  		prove(x) // ERROR "Proved sm,SM=-80,-3 "
  2612  	}
  2613  	if -8 <= v && v <= 10 && -1 <= s && s <= 3 {
  2614  		x := v>>s // ERROR "Proved"
  2615  		prove(x) // ERROR "Proved sm,SM=-8,10 "
  2616  	}
  2617  	if 2 <= v && v <= 10 && -1 <= s && s <= 3 {
  2618  		x := v>>s // ERROR "Proved"
  2619  		prove(x) // ERROR "Proved sm,SM=0,10 "
  2620  	}
  2621  }
  2622  
  2623  func unsignedRightShiftBounds(v uint, s int) {
  2624  	if 2 <= v && v <= 10 && -1 <= s && s <= 3 {
  2625  		x := v>>s // ERROR "Proved"
  2626  		proveu(x) // ERROR "Proved sm,SM=0,10 "
  2627  	}
  2628  	if 2 <= v && v <= 10 && 0 <= s && s <= 3 {
  2629  		x := v>>s // ERROR "Proved"
  2630  		proveu(x) // ERROR "Proved sm,SM=0,10 "
  2631  	}
  2632  	if 2 <= v && v <= 10 && 1 <= s && s <= 3 {
  2633  		x := v>>s // ERROR "Proved"
  2634  		proveu(x) // ERROR "Proved sm,SM=0,5 "
  2635  	}
  2636  	if 20 <= v && v <= 100 && 1 <= s && s <= 3 {
  2637  		x := v>>s // ERROR "Proved"
  2638  		proveu(x) // ERROR "Proved sm,SM=2,50 "
  2639  	}
  2640  }
  2641  
  2642  //go:noinline
  2643  func prove(x int) {
  2644  }
  2645  
  2646  //go:noinline
  2647  func proveu(x uint) {
  2648  }
  2649  
  2650  //go:noinline
  2651  func useInt(a int) {
  2652  }
  2653  
  2654  //go:noinline
  2655  func useSlice(a []int) {
  2656  }
  2657  
  2658  func main() {
  2659  }
  2660  

View as plain text