Source file src/cmd/compile/internal/ssa/prove.go

     1  // Copyright 2016 The Go Authors. All rights reserved.
     2  // Use of this source code is governed by a BSD-style
     3  // license that can be found in the LICENSE file.
     4  
     5  package ssa
     6  
     7  import (
     8  	"cmd/internal/src"
     9  	"fmt"
    10  	"math"
    11  	"math/bits"
    12  )
    13  
    14  type branch int
    15  
    16  const (
    17  	unknown branch = iota
    18  	positive
    19  	negative
    20  	// The outedges from a jump table are jumpTable0,
    21  	// jumpTable0+1, jumpTable0+2, etc. There could be an
    22  	// arbitrary number so we can't list them all here.
    23  	jumpTable0
    24  )
    25  
    26  func (b branch) String() string {
    27  	switch b {
    28  	case unknown:
    29  		return "unk"
    30  	case positive:
    31  		return "pos"
    32  	case negative:
    33  		return "neg"
    34  	default:
    35  		return fmt.Sprintf("jmp%d", b-jumpTable0)
    36  	}
    37  }
    38  
    39  // relation represents the set of possible relations between
    40  // pairs of variables (v, w). Without a priori knowledge the
    41  // mask is lt | eq | gt meaning v can be less than, equal to or
    42  // greater than w. When the execution path branches on the condition
    43  // `v op w` the set of relations is updated to exclude any
    44  // relation not possible due to `v op w` being true (or false).
    45  //
    46  // E.g.
    47  //
    48  //	r := relation(...)
    49  //
    50  //	if v < w {
    51  //	  newR := r & lt
    52  //	}
    53  //	if v >= w {
    54  //	  newR := r & (eq|gt)
    55  //	}
    56  //	if v != w {
    57  //	  newR := r & (lt|gt)
    58  //	}
    59  type relation uint
    60  
    61  const (
    62  	lt relation = 1 << iota
    63  	eq
    64  	gt
    65  )
    66  
    67  var relationStrings = [...]string{
    68  	0: "none", lt: "<", eq: "==", lt | eq: "<=",
    69  	gt: ">", gt | lt: "!=", gt | eq: ">=", gt | eq | lt: "any",
    70  }
    71  
    72  func (r relation) String() string {
    73  	if r < relation(len(relationStrings)) {
    74  		return relationStrings[r]
    75  	}
    76  	return fmt.Sprintf("relation(%d)", uint(r))
    77  }
    78  
    79  // domain represents the domain of a variable pair in which a set
    80  // of relations is known. For example, relations learned for unsigned
    81  // pairs cannot be transferred to signed pairs because the same bit
    82  // representation can mean something else.
    83  type domain uint
    84  
    85  const (
    86  	signed domain = 1 << iota
    87  	unsigned
    88  	pointer
    89  	boolean
    90  )
    91  
    92  var domainStrings = [...]string{
    93  	"signed", "unsigned", "pointer", "boolean",
    94  }
    95  
    96  func (d domain) String() string {
    97  	s := ""
    98  	for i, ds := range domainStrings {
    99  		if d&(1<<uint(i)) != 0 {
   100  			if len(s) != 0 {
   101  				s += "|"
   102  			}
   103  			s += ds
   104  			d &^= 1 << uint(i)
   105  		}
   106  	}
   107  	if d != 0 {
   108  		if len(s) != 0 {
   109  			s += "|"
   110  		}
   111  		s += fmt.Sprintf("0x%x", uint(d))
   112  	}
   113  	return s
   114  }
   115  
   116  // a limit records known upper and lower bounds for a value.
   117  //
   118  // If we have min>max or umin>umax, then this limit is
   119  // called "unsatisfiable". When we encounter such a limit, we
   120  // know that any code for which that limit applies is unreachable.
   121  // We don't particularly care how unsatisfiable limits propagate,
   122  // including becoming satisfiable, because any optimization
   123  // decisions based on those limits only apply to unreachable code.
   124  type limit struct {
   125  	min, max   int64  // min <= value <= max, signed
   126  	umin, umax uint64 // umin <= value <= umax, unsigned
   127  	// For booleans, we use 0==false, 1==true for both ranges
   128  	// For pointers, we use 0,0,0,0 for nil and minInt64,maxInt64,1,maxUint64 for nonnil
   129  }
   130  
   131  func (l limit) String() string {
   132  	return fmt.Sprintf("sm,SM,um,UM=%d,%d,%d,%d", l.min, l.max, l.umin, l.umax)
   133  }
   134  
   135  func (l limit) intersect(l2 limit) limit {
   136  	l.min = max(l.min, l2.min)
   137  	l.umin = max(l.umin, l2.umin)
   138  	l.max = min(l.max, l2.max)
   139  	l.umax = min(l.umax, l2.umax)
   140  	return l
   141  }
   142  
   143  func (l limit) signedMin(m int64) limit {
   144  	l.min = max(l.min, m)
   145  	return l
   146  }
   147  func (l limit) signedMax(m int64) limit {
   148  	l.max = min(l.max, m)
   149  	return l
   150  }
   151  func (l limit) signedMinMax(minimum, maximum int64) limit {
   152  	l.min = max(l.min, minimum)
   153  	l.max = min(l.max, maximum)
   154  	return l
   155  }
   156  
   157  func (l limit) unsignedMin(m uint64) limit {
   158  	l.umin = max(l.umin, m)
   159  	return l
   160  }
   161  func (l limit) unsignedMax(m uint64) limit {
   162  	l.umax = min(l.umax, m)
   163  	return l
   164  }
   165  func (l limit) unsignedMinMax(minimum, maximum uint64) limit {
   166  	l.umin = max(l.umin, minimum)
   167  	l.umax = min(l.umax, maximum)
   168  	return l
   169  }
   170  
   171  func (l limit) nonzero() bool {
   172  	return l.min > 0 || l.umin > 0 || l.max < 0
   173  }
   174  func (l limit) nonnegative() bool {
   175  	return l.min >= 0
   176  }
   177  func (l limit) unsat() bool {
   178  	return l.min > l.max || l.umin > l.umax
   179  }
   180  
   181  // If x and y can add without overflow or underflow
   182  // (using b bits), safeAdd returns x+y, true.
   183  // Otherwise, returns 0, false.
   184  func safeAdd(x, y int64, b uint) (int64, bool) {
   185  	s := x + y
   186  	if x >= 0 && y >= 0 && s < 0 {
   187  		return 0, false // 64-bit overflow
   188  	}
   189  	if x < 0 && y < 0 && s >= 0 {
   190  		return 0, false // 64-bit underflow
   191  	}
   192  	if !fitsInBits(s, b) {
   193  		return 0, false
   194  	}
   195  	return s, true
   196  }
   197  
   198  // same as safeAdd for unsigned arithmetic.
   199  func safeAddU(x, y uint64, b uint) (uint64, bool) {
   200  	s := x + y
   201  	if s < x || s < y {
   202  		return 0, false // 64-bit overflow
   203  	}
   204  	if !fitsInBitsU(s, b) {
   205  		return 0, false
   206  	}
   207  	return s, true
   208  }
   209  
   210  // same as safeAdd but for subtraction.
   211  func safeSub(x, y int64, b uint) (int64, bool) {
   212  	if y == math.MinInt64 {
   213  		if x == math.MaxInt64 {
   214  			return 0, false // 64-bit overflow
   215  		}
   216  		x++
   217  		y++
   218  	}
   219  	return safeAdd(x, -y, b)
   220  }
   221  
   222  // same as safeAddU but for subtraction.
   223  func safeSubU(x, y uint64, b uint) (uint64, bool) {
   224  	if x < y {
   225  		return 0, false // 64-bit underflow
   226  	}
   227  	s := x - y
   228  	if !fitsInBitsU(s, b) {
   229  		return 0, false
   230  	}
   231  	return s, true
   232  }
   233  
   234  // fitsInBits reports whether x fits in b bits (signed).
   235  func fitsInBits(x int64, b uint) bool {
   236  	if b == 64 {
   237  		return true
   238  	}
   239  	m := int64(-1) << (b - 1)
   240  	M := -m - 1
   241  	return x >= m && x <= M
   242  }
   243  
   244  // fitsInBitsU reports whether x fits in b bits (unsigned).
   245  func fitsInBitsU(x uint64, b uint) bool {
   246  	return x>>b == 0
   247  }
   248  
   249  // add returns the limit obtained by adding a value with limit l
   250  // to a value with limit l2. The result must fit in b bits.
   251  func (l limit) add(l2 limit, b uint) limit {
   252  	r := noLimit
   253  	min, minOk := safeAdd(l.min, l2.min, b)
   254  	max, maxOk := safeAdd(l.max, l2.max, b)
   255  	if minOk && maxOk {
   256  		r.min = min
   257  		r.max = max
   258  	}
   259  	umin, uminOk := safeAddU(l.umin, l2.umin, b)
   260  	umax, umaxOk := safeAddU(l.umax, l2.umax, b)
   261  	if uminOk && umaxOk {
   262  		r.umin = umin
   263  		r.umax = umax
   264  	}
   265  	return r
   266  }
   267  
   268  // same as add but for subtraction.
   269  func (l limit) sub(l2 limit, b uint) limit {
   270  	r := noLimit
   271  	min, minOk := safeSub(l.min, l2.max, b)
   272  	max, maxOk := safeSub(l.max, l2.min, b)
   273  	if minOk && maxOk {
   274  		r.min = min
   275  		r.max = max
   276  	}
   277  	umin, uminOk := safeSubU(l.umin, l2.umax, b)
   278  	umax, umaxOk := safeSubU(l.umax, l2.umin, b)
   279  	if uminOk && umaxOk {
   280  		r.umin = umin
   281  		r.umax = umax
   282  	}
   283  	return r
   284  }
   285  
   286  // same as add but for multiplication.
   287  func (l limit) mul(l2 limit, b uint) limit {
   288  	r := noLimit
   289  	umaxhi, umaxlo := bits.Mul64(l.umax, l2.umax)
   290  	if umaxhi == 0 && fitsInBitsU(umaxlo, b) {
   291  		r.umax = umaxlo
   292  		r.umin = l.umin * l2.umin
   293  		// Note: if the code containing this multiply is
   294  		// unreachable, then we may have umin>umax, and this
   295  		// multiply may overflow.  But that's ok for
   296  		// unreachable code. If this code is reachable, we
   297  		// know umin<=umax, so this multiply will not overflow
   298  		// because the max multiply didn't.
   299  	}
   300  	// Signed is harder, so don't bother. The only useful
   301  	// case is when we know both multiplicands are nonnegative,
   302  	// but that case is handled above because we would have then
   303  	// previously propagated signed info to the unsigned domain,
   304  	// and will propagate it back after the multiply.
   305  	return r
   306  }
   307  
   308  // Similar to add, but compute 1 << l if it fits without overflow in b bits.
   309  func (l limit) exp2(b uint) limit {
   310  	r := noLimit
   311  	if l.umax < uint64(b) {
   312  		r.umin = 1 << l.umin
   313  		r.umax = 1 << l.umax
   314  		// Same as above in mul, signed<->unsigned propagation
   315  		// will handle the signed case for us.
   316  	}
   317  	return r
   318  }
   319  
   320  // Similar to add, but computes the complement of the limit for bitsize b.
   321  func (l limit) com(b uint) limit {
   322  	switch b {
   323  	case 64:
   324  		return limit{
   325  			min:  ^l.max,
   326  			max:  ^l.min,
   327  			umin: ^l.umax,
   328  			umax: ^l.umin,
   329  		}
   330  	case 32:
   331  		return limit{
   332  			min:  int64(^int32(l.max)),
   333  			max:  int64(^int32(l.min)),
   334  			umin: uint64(^uint32(l.umax)),
   335  			umax: uint64(^uint32(l.umin)),
   336  		}
   337  	case 16:
   338  		return limit{
   339  			min:  int64(^int16(l.max)),
   340  			max:  int64(^int16(l.min)),
   341  			umin: uint64(^uint16(l.umax)),
   342  			umax: uint64(^uint16(l.umin)),
   343  		}
   344  	case 8:
   345  		return limit{
   346  			min:  int64(^int8(l.max)),
   347  			max:  int64(^int8(l.min)),
   348  			umin: uint64(^uint8(l.umax)),
   349  			umax: uint64(^uint8(l.umin)),
   350  		}
   351  	default:
   352  		panic("unreachable")
   353  	}
   354  }
   355  
   356  var noLimit = limit{math.MinInt64, math.MaxInt64, 0, math.MaxUint64}
   357  
   358  // a limitFact is a limit known for a particular value.
   359  type limitFact struct {
   360  	vid   ID
   361  	limit limit
   362  }
   363  
   364  // An ordering encodes facts like v < w.
   365  type ordering struct {
   366  	next *ordering // linked list of all known orderings for v.
   367  	// Note: v is implicit here, determined by which linked list it is in.
   368  	w *Value
   369  	d domain
   370  	r relation // one of ==,!=,<,<=,>,>=
   371  	// if d is boolean or pointer, r can only be ==, !=
   372  }
   373  
   374  // factsTable keeps track of relations between pairs of values.
   375  //
   376  // The fact table logic is sound, but incomplete. Outside of a few
   377  // special cases, it performs no deduction or arithmetic. While there
   378  // are known decision procedures for this, the ad hoc approach taken
   379  // by the facts table is effective for real code while remaining very
   380  // efficient.
   381  type factsTable struct {
   382  	// unsat is true if facts contains a contradiction.
   383  	//
   384  	// Note that the factsTable logic is incomplete, so if unsat
   385  	// is false, the assertions in factsTable could be satisfiable
   386  	// *or* unsatisfiable.
   387  	unsat      bool // true if facts contains a contradiction
   388  	unsatDepth int  // number of unsat checkpoints
   389  
   390  	// order* is a couple of partial order sets that record information
   391  	// about relations between SSA values in the signed and unsigned
   392  	// domain.
   393  	orderS *poset
   394  	orderU *poset
   395  
   396  	// orderings contains a list of known orderings between values.
   397  	// These lists are indexed by v.ID.
   398  	// We do not record transitive orderings. Only explicitly learned
   399  	// orderings are recorded. Transitive orderings can be obtained
   400  	// by walking along the individual orderings.
   401  	orderings map[ID]*ordering
   402  	// stack of IDs which have had an entry added in orderings.
   403  	// In addition, ID==0 are checkpoint markers.
   404  	orderingsStack []ID
   405  	orderingCache  *ordering // unused ordering records
   406  
   407  	// known lower and upper constant bounds on individual values.
   408  	limits       []limit     // indexed by value ID
   409  	limitStack   []limitFact // previous entries
   410  	recurseCheck []bool      // recursion detector for limit propagation
   411  
   412  	// For each slice s, a map from s to a len(s)/cap(s) value (if any)
   413  	// TODO: check if there are cases that matter where we have
   414  	// more than one len(s) for a slice. We could keep a list if necessary.
   415  	lens map[ID]*Value
   416  	caps map[ID]*Value
   417  }
   418  
   419  // checkpointBound is an invalid value used for checkpointing
   420  // and restoring factsTable.
   421  var checkpointBound = limitFact{}
   422  
   423  func newFactsTable(f *Func) *factsTable {
   424  	ft := &factsTable{}
   425  	ft.orderS = f.newPoset()
   426  	ft.orderU = f.newPoset()
   427  	ft.orderS.SetUnsigned(false)
   428  	ft.orderU.SetUnsigned(true)
   429  	ft.orderings = make(map[ID]*ordering)
   430  	ft.limits = f.Cache.allocLimitSlice(f.NumValues())
   431  	for _, b := range f.Blocks {
   432  		for _, v := range b.Values {
   433  			ft.limits[v.ID] = initLimit(v)
   434  		}
   435  	}
   436  	ft.limitStack = make([]limitFact, 4)
   437  	ft.recurseCheck = f.Cache.allocBoolSlice(f.NumValues())
   438  	return ft
   439  }
   440  
   441  // initLimitForNewValue initializes the limits for newly created values,
   442  // possibly needing to expand the limits slice. Currently used by
   443  // simplifyBlock when certain provably constant results are folded.
   444  func (ft *factsTable) initLimitForNewValue(v *Value) {
   445  	if int(v.ID) >= len(ft.limits) {
   446  		f := v.Block.Func
   447  		n := f.NumValues()
   448  		if cap(ft.limits) >= n {
   449  			ft.limits = ft.limits[:n]
   450  		} else {
   451  			old := ft.limits
   452  			ft.limits = f.Cache.allocLimitSlice(n)
   453  			copy(ft.limits, old)
   454  			f.Cache.freeLimitSlice(old)
   455  		}
   456  	}
   457  	ft.limits[v.ID] = initLimit(v)
   458  }
   459  
   460  // signedMin records the fact that we know v is at least
   461  // min in the signed domain.
   462  func (ft *factsTable) signedMin(v *Value, min int64) bool {
   463  	return ft.newLimit(v, limit{min: min, max: math.MaxInt64, umin: 0, umax: math.MaxUint64})
   464  }
   465  
   466  // signedMax records the fact that we know v is at most
   467  // max in the signed domain.
   468  func (ft *factsTable) signedMax(v *Value, max int64) bool {
   469  	return ft.newLimit(v, limit{min: math.MinInt64, max: max, umin: 0, umax: math.MaxUint64})
   470  }
   471  func (ft *factsTable) signedMinMax(v *Value, min, max int64) bool {
   472  	return ft.newLimit(v, limit{min: min, max: max, umin: 0, umax: math.MaxUint64})
   473  }
   474  
   475  // setNonNegative records the fact that v is known to be non-negative.
   476  func (ft *factsTable) setNonNegative(v *Value) bool {
   477  	return ft.signedMin(v, 0)
   478  }
   479  
   480  // unsignedMin records the fact that we know v is at least
   481  // min in the unsigned domain.
   482  func (ft *factsTable) unsignedMin(v *Value, min uint64) bool {
   483  	return ft.newLimit(v, limit{min: math.MinInt64, max: math.MaxInt64, umin: min, umax: math.MaxUint64})
   484  }
   485  
   486  // unsignedMax records the fact that we know v is at most
   487  // max in the unsigned domain.
   488  func (ft *factsTable) unsignedMax(v *Value, max uint64) bool {
   489  	return ft.newLimit(v, limit{min: math.MinInt64, max: math.MaxInt64, umin: 0, umax: max})
   490  }
   491  func (ft *factsTable) unsignedMinMax(v *Value, min, max uint64) bool {
   492  	return ft.newLimit(v, limit{min: math.MinInt64, max: math.MaxInt64, umin: min, umax: max})
   493  }
   494  
   495  func (ft *factsTable) booleanFalse(v *Value) bool {
   496  	return ft.newLimit(v, limit{min: 0, max: 0, umin: 0, umax: 0})
   497  }
   498  func (ft *factsTable) booleanTrue(v *Value) bool {
   499  	return ft.newLimit(v, limit{min: 1, max: 1, umin: 1, umax: 1})
   500  }
   501  func (ft *factsTable) pointerNil(v *Value) bool {
   502  	return ft.newLimit(v, limit{min: 0, max: 0, umin: 0, umax: 0})
   503  }
   504  func (ft *factsTable) pointerNonNil(v *Value) bool {
   505  	l := noLimit
   506  	l.umin = 1
   507  	return ft.newLimit(v, l)
   508  }
   509  
   510  // newLimit adds new limiting information for v.
   511  // Returns true if the new limit added any new information.
   512  func (ft *factsTable) newLimit(v *Value, newLim limit) bool {
   513  	oldLim := ft.limits[v.ID]
   514  
   515  	// Merge old and new information.
   516  	lim := oldLim.intersect(newLim)
   517  
   518  	// signed <-> unsigned propagation
   519  	if lim.min >= 0 {
   520  		lim = lim.unsignedMinMax(uint64(lim.min), uint64(lim.max))
   521  	}
   522  	if fitsInBitsU(lim.umax, uint(8*v.Type.Size()-1)) {
   523  		lim = lim.signedMinMax(int64(lim.umin), int64(lim.umax))
   524  	}
   525  
   526  	if lim == oldLim {
   527  		return false // nothing new to record
   528  	}
   529  
   530  	if lim.unsat() {
   531  		r := !ft.unsat
   532  		ft.unsat = true
   533  		return r
   534  	}
   535  
   536  	// Check for recursion. This normally happens because in unsatisfiable
   537  	// cases we have a < b < a, and every update to a's limits returns
   538  	// here again with the limit increased by 2.
   539  	// Normally this is caught early by the orderS/orderU posets, but in
   540  	// cases where the comparisons jump between signed and unsigned domains,
   541  	// the posets will not notice.
   542  	if ft.recurseCheck[v.ID] {
   543  		// This should only happen for unsatisfiable cases. TODO: check
   544  		return false
   545  	}
   546  	ft.recurseCheck[v.ID] = true
   547  	defer func() {
   548  		ft.recurseCheck[v.ID] = false
   549  	}()
   550  
   551  	// Record undo information.
   552  	ft.limitStack = append(ft.limitStack, limitFact{v.ID, oldLim})
   553  	// Record new information.
   554  	ft.limits[v.ID] = lim
   555  	if v.Block.Func.pass.debug > 2 {
   556  		// TODO: pos is probably wrong. This is the position where v is defined,
   557  		// not the position where we learned the fact about it (which was
   558  		// probably some subsequent compare+branch).
   559  		v.Block.Func.Warnl(v.Pos, "new limit %s %s unsat=%v", v, lim.String(), ft.unsat)
   560  	}
   561  
   562  	// Propagate this new constant range to other values
   563  	// that we know are ordered with respect to this one.
   564  	// Note overflow/underflow in the arithmetic below is ok,
   565  	// it will just lead to imprecision (undetected unsatisfiability).
   566  	for o := ft.orderings[v.ID]; o != nil; o = o.next {
   567  		switch o.d {
   568  		case signed:
   569  			switch o.r {
   570  			case eq: // v == w
   571  				ft.signedMinMax(o.w, lim.min, lim.max)
   572  			case lt | eq: // v <= w
   573  				ft.signedMin(o.w, lim.min)
   574  			case lt: // v < w
   575  				ft.signedMin(o.w, lim.min+1)
   576  			case gt | eq: // v >= w
   577  				ft.signedMax(o.w, lim.max)
   578  			case gt: // v > w
   579  				ft.signedMax(o.w, lim.max-1)
   580  			case lt | gt: // v != w
   581  				if lim.min == lim.max { // v is a constant
   582  					c := lim.min
   583  					if ft.limits[o.w.ID].min == c {
   584  						ft.signedMin(o.w, c+1)
   585  					}
   586  					if ft.limits[o.w.ID].max == c {
   587  						ft.signedMax(o.w, c-1)
   588  					}
   589  				}
   590  			}
   591  		case unsigned:
   592  			switch o.r {
   593  			case eq: // v == w
   594  				ft.unsignedMinMax(o.w, lim.umin, lim.umax)
   595  			case lt | eq: // v <= w
   596  				ft.unsignedMin(o.w, lim.umin)
   597  			case lt: // v < w
   598  				ft.unsignedMin(o.w, lim.umin+1)
   599  			case gt | eq: // v >= w
   600  				ft.unsignedMax(o.w, lim.umax)
   601  			case gt: // v > w
   602  				ft.unsignedMax(o.w, lim.umax-1)
   603  			case lt | gt: // v != w
   604  				if lim.umin == lim.umax { // v is a constant
   605  					c := lim.umin
   606  					if ft.limits[o.w.ID].umin == c {
   607  						ft.unsignedMin(o.w, c+1)
   608  					}
   609  					if ft.limits[o.w.ID].umax == c {
   610  						ft.unsignedMax(o.w, c-1)
   611  					}
   612  				}
   613  			}
   614  		case boolean:
   615  			switch o.r {
   616  			case eq:
   617  				if lim.min == 0 && lim.max == 0 { // constant false
   618  					ft.booleanFalse(o.w)
   619  				}
   620  				if lim.min == 1 && lim.max == 1 { // constant true
   621  					ft.booleanTrue(o.w)
   622  				}
   623  			case lt | gt:
   624  				if lim.min == 0 && lim.max == 0 { // constant false
   625  					ft.booleanTrue(o.w)
   626  				}
   627  				if lim.min == 1 && lim.max == 1 { // constant true
   628  					ft.booleanFalse(o.w)
   629  				}
   630  			}
   631  		case pointer:
   632  			switch o.r {
   633  			case eq:
   634  				if lim.umax == 0 { // nil
   635  					ft.pointerNil(o.w)
   636  				}
   637  				if lim.umin > 0 { // non-nil
   638  					ft.pointerNonNil(o.w)
   639  				}
   640  			case lt | gt:
   641  				if lim.umax == 0 { // nil
   642  					ft.pointerNonNil(o.w)
   643  				}
   644  				// note: not equal to non-nil doesn't tell us anything.
   645  			}
   646  		}
   647  	}
   648  
   649  	// If this is new known constant for a boolean value,
   650  	// extract relation between its args. For example, if
   651  	// We learn v is false, and v is defined as a<b, then we learn a>=b.
   652  	if v.Type.IsBoolean() {
   653  		// If we reach here, it is because we have a more restrictive
   654  		// value for v than the default. The only two such values
   655  		// are constant true or constant false.
   656  		if lim.min != lim.max {
   657  			v.Block.Func.Fatalf("boolean not constant %v", v)
   658  		}
   659  		isTrue := lim.min == 1
   660  		if dr, ok := domainRelationTable[v.Op]; ok && v.Op != OpIsInBounds && v.Op != OpIsSliceInBounds {
   661  			d := dr.d
   662  			r := dr.r
   663  			if d == signed && ft.isNonNegative(v.Args[0]) && ft.isNonNegative(v.Args[1]) {
   664  				d |= unsigned
   665  			}
   666  			if !isTrue {
   667  				r ^= lt | gt | eq
   668  			}
   669  			// TODO: v.Block is wrong?
   670  			addRestrictions(v.Block, ft, d, v.Args[0], v.Args[1], r)
   671  		}
   672  		switch v.Op {
   673  		case OpIsNonNil:
   674  			if isTrue {
   675  				ft.pointerNonNil(v.Args[0])
   676  			} else {
   677  				ft.pointerNil(v.Args[0])
   678  			}
   679  		case OpIsInBounds, OpIsSliceInBounds:
   680  			// 0 <= a0 < a1 (or 0 <= a0 <= a1)
   681  			r := lt
   682  			if v.Op == OpIsSliceInBounds {
   683  				r |= eq
   684  			}
   685  			if isTrue {
   686  				// On the positive branch, we learn:
   687  				//   signed: 0 <= a0 < a1 (or 0 <= a0 <= a1)
   688  				//   unsigned:    a0 < a1 (or a0 <= a1)
   689  				ft.setNonNegative(v.Args[0])
   690  				ft.update(v.Block, v.Args[0], v.Args[1], signed, r)
   691  				ft.update(v.Block, v.Args[0], v.Args[1], unsigned, r)
   692  			} else {
   693  				// On the negative branch, we learn (0 > a0 ||
   694  				// a0 >= a1). In the unsigned domain, this is
   695  				// simply a0 >= a1 (which is the reverse of the
   696  				// positive branch, so nothing surprising).
   697  				// But in the signed domain, we can't express the ||
   698  				// condition, so check if a0 is non-negative instead,
   699  				// to be able to learn something.
   700  				r ^= lt | gt | eq // >= (index) or > (slice)
   701  				if ft.isNonNegative(v.Args[0]) {
   702  					ft.update(v.Block, v.Args[0], v.Args[1], signed, r)
   703  				}
   704  				ft.update(v.Block, v.Args[0], v.Args[1], unsigned, r)
   705  				// TODO: v.Block is wrong here
   706  			}
   707  		}
   708  	}
   709  
   710  	return true
   711  }
   712  
   713  func (ft *factsTable) addOrdering(v, w *Value, d domain, r relation) {
   714  	o := ft.orderingCache
   715  	if o == nil {
   716  		o = &ordering{}
   717  	} else {
   718  		ft.orderingCache = o.next
   719  	}
   720  	o.w = w
   721  	o.d = d
   722  	o.r = r
   723  	o.next = ft.orderings[v.ID]
   724  	ft.orderings[v.ID] = o
   725  	ft.orderingsStack = append(ft.orderingsStack, v.ID)
   726  }
   727  
   728  // update updates the set of relations between v and w in domain d
   729  // restricting it to r.
   730  func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
   731  	if parent.Func.pass.debug > 2 {
   732  		parent.Func.Warnl(parent.Pos, "parent=%s, update %s %s %s", parent, v, w, r)
   733  	}
   734  	// No need to do anything else if we already found unsat.
   735  	if ft.unsat {
   736  		return
   737  	}
   738  
   739  	// Self-fact. It's wasteful to register it into the facts
   740  	// table, so just note whether it's satisfiable
   741  	if v == w {
   742  		if r&eq == 0 {
   743  			ft.unsat = true
   744  		}
   745  		return
   746  	}
   747  
   748  	if d == signed || d == unsigned {
   749  		var ok bool
   750  		order := ft.orderS
   751  		if d == unsigned {
   752  			order = ft.orderU
   753  		}
   754  		switch r {
   755  		case lt:
   756  			ok = order.SetOrder(v, w)
   757  		case gt:
   758  			ok = order.SetOrder(w, v)
   759  		case lt | eq:
   760  			ok = order.SetOrderOrEqual(v, w)
   761  		case gt | eq:
   762  			ok = order.SetOrderOrEqual(w, v)
   763  		case eq:
   764  			ok = order.SetEqual(v, w)
   765  		case lt | gt:
   766  			ok = order.SetNonEqual(v, w)
   767  		default:
   768  			panic("unknown relation")
   769  		}
   770  		ft.addOrdering(v, w, d, r)
   771  		ft.addOrdering(w, v, d, reverseBits[r])
   772  
   773  		if !ok {
   774  			if parent.Func.pass.debug > 2 {
   775  				parent.Func.Warnl(parent.Pos, "unsat %s %s %s", v, w, r)
   776  			}
   777  			ft.unsat = true
   778  			return
   779  		}
   780  	}
   781  	if d == boolean || d == pointer {
   782  		for o := ft.orderings[v.ID]; o != nil; o = o.next {
   783  			if o.d == d && o.w == w {
   784  				// We already know a relationship between v and w.
   785  				// Either it is a duplicate, or it is a contradiction,
   786  				// as we only allow eq and lt|gt for these domains,
   787  				if o.r != r {
   788  					ft.unsat = true
   789  				}
   790  				return
   791  			}
   792  		}
   793  		// TODO: this does not do transitive equality.
   794  		// We could use a poset like above, but somewhat degenerate (==,!= only).
   795  		ft.addOrdering(v, w, d, r)
   796  		ft.addOrdering(w, v, d, r) // note: reverseBits unnecessary for eq and lt|gt.
   797  	}
   798  
   799  	// Extract new constant limits based on the comparison.
   800  	vLimit := ft.limits[v.ID]
   801  	wLimit := ft.limits[w.ID]
   802  	// Note: all the +1/-1 below could overflow/underflow. Either will
   803  	// still generate correct results, it will just lead to imprecision.
   804  	// In fact if there is overflow/underflow, the corresponding
   805  	// code is unreachable because the known range is outside the range
   806  	// of the value's type.
   807  	switch d {
   808  	case signed:
   809  		switch r {
   810  		case eq: // v == w
   811  			ft.signedMinMax(v, wLimit.min, wLimit.max)
   812  			ft.signedMinMax(w, vLimit.min, vLimit.max)
   813  		case lt: // v < w
   814  			ft.signedMax(v, wLimit.max-1)
   815  			ft.signedMin(w, vLimit.min+1)
   816  		case lt | eq: // v <= w
   817  			ft.signedMax(v, wLimit.max)
   818  			ft.signedMin(w, vLimit.min)
   819  		case gt: // v > w
   820  			ft.signedMin(v, wLimit.min+1)
   821  			ft.signedMax(w, vLimit.max-1)
   822  		case gt | eq: // v >= w
   823  			ft.signedMin(v, wLimit.min)
   824  			ft.signedMax(w, vLimit.max)
   825  		case lt | gt: // v != w
   826  			if vLimit.min == vLimit.max { // v is a constant
   827  				c := vLimit.min
   828  				if wLimit.min == c {
   829  					ft.signedMin(w, c+1)
   830  				}
   831  				if wLimit.max == c {
   832  					ft.signedMax(w, c-1)
   833  				}
   834  			}
   835  			if wLimit.min == wLimit.max { // w is a constant
   836  				c := wLimit.min
   837  				if vLimit.min == c {
   838  					ft.signedMin(v, c+1)
   839  				}
   840  				if vLimit.max == c {
   841  					ft.signedMax(v, c-1)
   842  				}
   843  			}
   844  		}
   845  	case unsigned:
   846  		switch r {
   847  		case eq: // v == w
   848  			ft.unsignedMinMax(v, wLimit.umin, wLimit.umax)
   849  			ft.unsignedMinMax(w, vLimit.umin, vLimit.umax)
   850  		case lt: // v < w
   851  			ft.unsignedMax(v, wLimit.umax-1)
   852  			ft.unsignedMin(w, vLimit.umin+1)
   853  		case lt | eq: // v <= w
   854  			ft.unsignedMax(v, wLimit.umax)
   855  			ft.unsignedMin(w, vLimit.umin)
   856  		case gt: // v > w
   857  			ft.unsignedMin(v, wLimit.umin+1)
   858  			ft.unsignedMax(w, vLimit.umax-1)
   859  		case gt | eq: // v >= w
   860  			ft.unsignedMin(v, wLimit.umin)
   861  			ft.unsignedMax(w, vLimit.umax)
   862  		case lt | gt: // v != w
   863  			if vLimit.umin == vLimit.umax { // v is a constant
   864  				c := vLimit.umin
   865  				if wLimit.umin == c {
   866  					ft.unsignedMin(w, c+1)
   867  				}
   868  				if wLimit.umax == c {
   869  					ft.unsignedMax(w, c-1)
   870  				}
   871  			}
   872  			if wLimit.umin == wLimit.umax { // w is a constant
   873  				c := wLimit.umin
   874  				if vLimit.umin == c {
   875  					ft.unsignedMin(v, c+1)
   876  				}
   877  				if vLimit.umax == c {
   878  					ft.unsignedMax(v, c-1)
   879  				}
   880  			}
   881  		}
   882  	case boolean:
   883  		switch r {
   884  		case eq: // v == w
   885  			if vLimit.min == 1 { // v is true
   886  				ft.booleanTrue(w)
   887  			}
   888  			if vLimit.max == 0 { // v is false
   889  				ft.booleanFalse(w)
   890  			}
   891  			if wLimit.min == 1 { // w is true
   892  				ft.booleanTrue(v)
   893  			}
   894  			if wLimit.max == 0 { // w is false
   895  				ft.booleanFalse(v)
   896  			}
   897  		case lt | gt: // v != w
   898  			if vLimit.min == 1 { // v is true
   899  				ft.booleanFalse(w)
   900  			}
   901  			if vLimit.max == 0 { // v is false
   902  				ft.booleanTrue(w)
   903  			}
   904  			if wLimit.min == 1 { // w is true
   905  				ft.booleanFalse(v)
   906  			}
   907  			if wLimit.max == 0 { // w is false
   908  				ft.booleanTrue(v)
   909  			}
   910  		}
   911  	case pointer:
   912  		switch r {
   913  		case eq: // v == w
   914  			if vLimit.umax == 0 { // v is nil
   915  				ft.pointerNil(w)
   916  			}
   917  			if vLimit.umin > 0 { // v is non-nil
   918  				ft.pointerNonNil(w)
   919  			}
   920  			if wLimit.umax == 0 { // w is nil
   921  				ft.pointerNil(v)
   922  			}
   923  			if wLimit.umin > 0 { // w is non-nil
   924  				ft.pointerNonNil(v)
   925  			}
   926  		case lt | gt: // v != w
   927  			if vLimit.umax == 0 { // v is nil
   928  				ft.pointerNonNil(w)
   929  			}
   930  			if wLimit.umax == 0 { // w is nil
   931  				ft.pointerNonNil(v)
   932  			}
   933  			// Note: the other direction doesn't work.
   934  			// Being not equal to a non-nil pointer doesn't
   935  			// make you (necessarily) a nil pointer.
   936  		}
   937  	}
   938  
   939  	// Derived facts below here are only about numbers.
   940  	if d != signed && d != unsigned {
   941  		return
   942  	}
   943  
   944  	// Additional facts we know given the relationship between len and cap.
   945  	//
   946  	// TODO: Since prove now derives transitive relations, it
   947  	// should be sufficient to learn that len(w) <= cap(w) at the
   948  	// beginning of prove where we look for all len/cap ops.
   949  	if v.Op == OpSliceLen && r&lt == 0 && ft.caps[v.Args[0].ID] != nil {
   950  		// len(s) > w implies cap(s) > w
   951  		// len(s) >= w implies cap(s) >= w
   952  		// len(s) == w implies cap(s) >= w
   953  		ft.update(parent, ft.caps[v.Args[0].ID], w, d, r|gt)
   954  	}
   955  	if w.Op == OpSliceLen && r&gt == 0 && ft.caps[w.Args[0].ID] != nil {
   956  		// same, length on the RHS.
   957  		ft.update(parent, v, ft.caps[w.Args[0].ID], d, r|lt)
   958  	}
   959  	if v.Op == OpSliceCap && r&gt == 0 && ft.lens[v.Args[0].ID] != nil {
   960  		// cap(s) < w implies len(s) < w
   961  		// cap(s) <= w implies len(s) <= w
   962  		// cap(s) == w implies len(s) <= w
   963  		ft.update(parent, ft.lens[v.Args[0].ID], w, d, r|lt)
   964  	}
   965  	if w.Op == OpSliceCap && r&lt == 0 && ft.lens[w.Args[0].ID] != nil {
   966  		// same, capacity on the RHS.
   967  		ft.update(parent, v, ft.lens[w.Args[0].ID], d, r|gt)
   968  	}
   969  
   970  	// Process fence-post implications.
   971  	//
   972  	// First, make the condition > or >=.
   973  	if r == lt || r == lt|eq {
   974  		v, w = w, v
   975  		r = reverseBits[r]
   976  	}
   977  	switch r {
   978  	case gt:
   979  		if x, delta := isConstDelta(v); x != nil && delta == 1 {
   980  			// x+1 > w  ⇒  x >= w
   981  			//
   982  			// This is useful for eliminating the
   983  			// growslice branch of append.
   984  			ft.update(parent, x, w, d, gt|eq)
   985  		} else if x, delta := isConstDelta(w); x != nil && delta == -1 {
   986  			// v > x-1  ⇒  v >= x
   987  			ft.update(parent, v, x, d, gt|eq)
   988  		}
   989  	case gt | eq:
   990  		if x, delta := isConstDelta(v); x != nil && delta == -1 {
   991  			// x-1 >= w && x > min  ⇒  x > w
   992  			//
   993  			// Useful for i > 0; s[i-1].
   994  			lim := ft.limits[x.ID]
   995  			if (d == signed && lim.min > opMin[v.Op]) || (d == unsigned && lim.umin > 0) {
   996  				ft.update(parent, x, w, d, gt)
   997  			}
   998  		} else if x, delta := isConstDelta(w); x != nil && delta == 1 {
   999  			// v >= x+1 && x < max  ⇒  v > x
  1000  			lim := ft.limits[x.ID]
  1001  			if (d == signed && lim.max < opMax[w.Op]) || (d == unsigned && lim.umax < opUMax[w.Op]) {
  1002  				ft.update(parent, v, x, d, gt)
  1003  			}
  1004  		}
  1005  	}
  1006  
  1007  	// Process: x+delta > w (with delta constant)
  1008  	// Only signed domain for now (useful for accesses to slices in loops).
  1009  	if r == gt || r == gt|eq {
  1010  		if x, delta := isConstDelta(v); x != nil && d == signed {
  1011  			if parent.Func.pass.debug > 1 {
  1012  				parent.Func.Warnl(parent.Pos, "x+d %s w; x:%v %v delta:%v w:%v d:%v", r, x, parent.String(), delta, w.AuxInt, d)
  1013  			}
  1014  			underflow := true
  1015  			if delta < 0 {
  1016  				l := ft.limits[x.ID]
  1017  				if (x.Type.Size() == 8 && l.min >= math.MinInt64-delta) ||
  1018  					(x.Type.Size() == 4 && l.min >= math.MinInt32-delta) {
  1019  					underflow = false
  1020  				}
  1021  			}
  1022  			if delta < 0 && !underflow {
  1023  				// If delta < 0 and x+delta cannot underflow then x > x+delta (that is, x > v)
  1024  				ft.update(parent, x, v, signed, gt)
  1025  			}
  1026  			if !w.isGenericIntConst() {
  1027  				// If we know that x+delta > w but w is not constant, we can derive:
  1028  				//    if delta < 0 and x+delta cannot underflow, then x > w
  1029  				// This is useful for loops with bounds "len(slice)-K" (delta = -K)
  1030  				if delta < 0 && !underflow {
  1031  					ft.update(parent, x, w, signed, r)
  1032  				}
  1033  			} else {
  1034  				// With w,delta constants, we want to derive: x+delta > w  ⇒  x > w-delta
  1035  				//
  1036  				// We compute (using integers of the correct size):
  1037  				//    min = w - delta
  1038  				//    max = MaxInt - delta
  1039  				//
  1040  				// And we prove that:
  1041  				//    if min<max: min < x AND x <= max
  1042  				//    if min>max: min < x OR  x <= max
  1043  				//
  1044  				// This is always correct, even in case of overflow.
  1045  				//
  1046  				// If the initial fact is x+delta >= w instead, the derived conditions are:
  1047  				//    if min<max: min <= x AND x <= max
  1048  				//    if min>max: min <= x OR  x <= max
  1049  				//
  1050  				// Notice the conditions for max are still <=, as they handle overflows.
  1051  				var min, max int64
  1052  				switch x.Type.Size() {
  1053  				case 8:
  1054  					min = w.AuxInt - delta
  1055  					max = int64(^uint64(0)>>1) - delta
  1056  				case 4:
  1057  					min = int64(int32(w.AuxInt) - int32(delta))
  1058  					max = int64(int32(^uint32(0)>>1) - int32(delta))
  1059  				case 2:
  1060  					min = int64(int16(w.AuxInt) - int16(delta))
  1061  					max = int64(int16(^uint16(0)>>1) - int16(delta))
  1062  				case 1:
  1063  					min = int64(int8(w.AuxInt) - int8(delta))
  1064  					max = int64(int8(^uint8(0)>>1) - int8(delta))
  1065  				default:
  1066  					panic("unimplemented")
  1067  				}
  1068  
  1069  				if min < max {
  1070  					// Record that x > min and max >= x
  1071  					if r == gt {
  1072  						min++
  1073  					}
  1074  					ft.signedMinMax(x, min, max)
  1075  				} else {
  1076  					// We know that either x>min OR x<=max. factsTable cannot record OR conditions,
  1077  					// so let's see if we can already prove that one of them is false, in which case
  1078  					// the other must be true
  1079  					l := ft.limits[x.ID]
  1080  					if l.max <= min {
  1081  						if r&eq == 0 || l.max < min {
  1082  							// x>min (x>=min) is impossible, so it must be x<=max
  1083  							ft.signedMax(x, max)
  1084  						}
  1085  					} else if l.min > max {
  1086  						// x<=max is impossible, so it must be x>min
  1087  						if r == gt {
  1088  							min++
  1089  						}
  1090  						ft.signedMin(x, min)
  1091  					}
  1092  				}
  1093  			}
  1094  		}
  1095  	}
  1096  
  1097  	// Look through value-preserving extensions.
  1098  	// If the domain is appropriate for the pre-extension Type,
  1099  	// repeat the update with the pre-extension Value.
  1100  	if isCleanExt(v) {
  1101  		switch {
  1102  		case d == signed && v.Args[0].Type.IsSigned():
  1103  			fallthrough
  1104  		case d == unsigned && !v.Args[0].Type.IsSigned():
  1105  			ft.update(parent, v.Args[0], w, d, r)
  1106  		}
  1107  	}
  1108  	if isCleanExt(w) {
  1109  		switch {
  1110  		case d == signed && w.Args[0].Type.IsSigned():
  1111  			fallthrough
  1112  		case d == unsigned && !w.Args[0].Type.IsSigned():
  1113  			ft.update(parent, v, w.Args[0], d, r)
  1114  		}
  1115  	}
  1116  }
  1117  
  1118  var opMin = map[Op]int64{
  1119  	OpAdd64: math.MinInt64, OpSub64: math.MinInt64,
  1120  	OpAdd32: math.MinInt32, OpSub32: math.MinInt32,
  1121  }
  1122  
  1123  var opMax = map[Op]int64{
  1124  	OpAdd64: math.MaxInt64, OpSub64: math.MaxInt64,
  1125  	OpAdd32: math.MaxInt32, OpSub32: math.MaxInt32,
  1126  }
  1127  
  1128  var opUMax = map[Op]uint64{
  1129  	OpAdd64: math.MaxUint64, OpSub64: math.MaxUint64,
  1130  	OpAdd32: math.MaxUint32, OpSub32: math.MaxUint32,
  1131  }
  1132  
  1133  // isNonNegative reports whether v is known to be non-negative.
  1134  func (ft *factsTable) isNonNegative(v *Value) bool {
  1135  	return ft.limits[v.ID].min >= 0
  1136  }
  1137  
  1138  // checkpoint saves the current state of known relations.
  1139  // Called when descending on a branch.
  1140  func (ft *factsTable) checkpoint() {
  1141  	if ft.unsat {
  1142  		ft.unsatDepth++
  1143  	}
  1144  	ft.limitStack = append(ft.limitStack, checkpointBound)
  1145  	ft.orderS.Checkpoint()
  1146  	ft.orderU.Checkpoint()
  1147  	ft.orderingsStack = append(ft.orderingsStack, 0)
  1148  }
  1149  
  1150  // restore restores known relation to the state just
  1151  // before the previous checkpoint.
  1152  // Called when backing up on a branch.
  1153  func (ft *factsTable) restore() {
  1154  	if ft.unsatDepth > 0 {
  1155  		ft.unsatDepth--
  1156  	} else {
  1157  		ft.unsat = false
  1158  	}
  1159  	for {
  1160  		old := ft.limitStack[len(ft.limitStack)-1]
  1161  		ft.limitStack = ft.limitStack[:len(ft.limitStack)-1]
  1162  		if old.vid == 0 { // checkpointBound
  1163  			break
  1164  		}
  1165  		ft.limits[old.vid] = old.limit
  1166  	}
  1167  	ft.orderS.Undo()
  1168  	ft.orderU.Undo()
  1169  	for {
  1170  		id := ft.orderingsStack[len(ft.orderingsStack)-1]
  1171  		ft.orderingsStack = ft.orderingsStack[:len(ft.orderingsStack)-1]
  1172  		if id == 0 { // checkpoint marker
  1173  			break
  1174  		}
  1175  		o := ft.orderings[id]
  1176  		ft.orderings[id] = o.next
  1177  		o.next = ft.orderingCache
  1178  		ft.orderingCache = o
  1179  	}
  1180  }
  1181  
  1182  var (
  1183  	reverseBits = [...]relation{0, 4, 2, 6, 1, 5, 3, 7}
  1184  
  1185  	// maps what we learn when the positive branch is taken.
  1186  	// For example:
  1187  	//      OpLess8:   {signed, lt},
  1188  	//	v1 = (OpLess8 v2 v3).
  1189  	// If we learn that v1 is true, then we can deduce that v2<v3
  1190  	// in the signed domain.
  1191  	domainRelationTable = map[Op]struct {
  1192  		d domain
  1193  		r relation
  1194  	}{
  1195  		OpEq8:   {signed | unsigned, eq},
  1196  		OpEq16:  {signed | unsigned, eq},
  1197  		OpEq32:  {signed | unsigned, eq},
  1198  		OpEq64:  {signed | unsigned, eq},
  1199  		OpEqPtr: {pointer, eq},
  1200  		OpEqB:   {boolean, eq},
  1201  
  1202  		OpNeq8:   {signed | unsigned, lt | gt},
  1203  		OpNeq16:  {signed | unsigned, lt | gt},
  1204  		OpNeq32:  {signed | unsigned, lt | gt},
  1205  		OpNeq64:  {signed | unsigned, lt | gt},
  1206  		OpNeqPtr: {pointer, lt | gt},
  1207  		OpNeqB:   {boolean, lt | gt},
  1208  
  1209  		OpLess8:   {signed, lt},
  1210  		OpLess8U:  {unsigned, lt},
  1211  		OpLess16:  {signed, lt},
  1212  		OpLess16U: {unsigned, lt},
  1213  		OpLess32:  {signed, lt},
  1214  		OpLess32U: {unsigned, lt},
  1215  		OpLess64:  {signed, lt},
  1216  		OpLess64U: {unsigned, lt},
  1217  
  1218  		OpLeq8:   {signed, lt | eq},
  1219  		OpLeq8U:  {unsigned, lt | eq},
  1220  		OpLeq16:  {signed, lt | eq},
  1221  		OpLeq16U: {unsigned, lt | eq},
  1222  		OpLeq32:  {signed, lt | eq},
  1223  		OpLeq32U: {unsigned, lt | eq},
  1224  		OpLeq64:  {signed, lt | eq},
  1225  		OpLeq64U: {unsigned, lt | eq},
  1226  	}
  1227  )
  1228  
  1229  // cleanup returns the posets to the free list
  1230  func (ft *factsTable) cleanup(f *Func) {
  1231  	for _, po := range []*poset{ft.orderS, ft.orderU} {
  1232  		// Make sure it's empty as it should be. A non-empty poset
  1233  		// might cause errors and miscompilations if reused.
  1234  		if checkEnabled {
  1235  			if err := po.CheckEmpty(); err != nil {
  1236  				f.Fatalf("poset not empty after function %s: %v", f.Name, err)
  1237  			}
  1238  		}
  1239  		f.retPoset(po)
  1240  	}
  1241  	f.Cache.freeLimitSlice(ft.limits)
  1242  	f.Cache.freeBoolSlice(ft.recurseCheck)
  1243  }
  1244  
  1245  // prove removes redundant BlockIf branches that can be inferred
  1246  // from previous dominating comparisons.
  1247  //
  1248  // By far, the most common redundant pair are generated by bounds checking.
  1249  // For example for the code:
  1250  //
  1251  //	a[i] = 4
  1252  //	foo(a[i])
  1253  //
  1254  // The compiler will generate the following code:
  1255  //
  1256  //	if i >= len(a) {
  1257  //	    panic("not in bounds")
  1258  //	}
  1259  //	a[i] = 4
  1260  //	if i >= len(a) {
  1261  //	    panic("not in bounds")
  1262  //	}
  1263  //	foo(a[i])
  1264  //
  1265  // The second comparison i >= len(a) is clearly redundant because if the
  1266  // else branch of the first comparison is executed, we already know that i < len(a).
  1267  // The code for the second panic can be removed.
  1268  //
  1269  // prove works by finding contradictions and trimming branches whose
  1270  // conditions are unsatisfiable given the branches leading up to them.
  1271  // It tracks a "fact table" of branch conditions. For each branching
  1272  // block, it asserts the branch conditions that uniquely dominate that
  1273  // block, and then separately asserts the block's branch condition and
  1274  // its negation. If either leads to a contradiction, it can trim that
  1275  // successor.
  1276  func prove(f *Func) {
  1277  	// Find induction variables. Currently, findIndVars
  1278  	// is limited to one induction variable per block.
  1279  	var indVars map[*Block]indVar
  1280  	for _, v := range findIndVar(f) {
  1281  		ind := v.ind
  1282  		if len(ind.Args) != 2 {
  1283  			// the rewrite code assumes there is only ever two parents to loops
  1284  			panic("unexpected induction with too many parents")
  1285  		}
  1286  
  1287  		nxt := v.nxt
  1288  		if !(ind.Uses == 2 && // 2 used by comparison and next
  1289  			nxt.Uses == 1) { // 1 used by induction
  1290  			// ind or nxt is used inside the loop, add it for the facts table
  1291  			if indVars == nil {
  1292  				indVars = make(map[*Block]indVar)
  1293  			}
  1294  			indVars[v.entry] = v
  1295  			continue
  1296  		} else {
  1297  			// Since this induction variable is not used for anything but counting the iterations,
  1298  			// no point in putting it into the facts table.
  1299  		}
  1300  
  1301  		// try to rewrite to a downward counting loop checking against start if the
  1302  		// loop body does not depend on ind or nxt and end is known before the loop.
  1303  		// This reduces pressure on the register allocator because this does not need
  1304  		// to use end on each iteration anymore. We compare against the start constant instead.
  1305  		// That means this code:
  1306  		//
  1307  		//	loop:
  1308  		//		ind = (Phi (Const [x]) nxt),
  1309  		//		if ind < end
  1310  		//		then goto enter_loop
  1311  		//		else goto exit_loop
  1312  		//
  1313  		//	enter_loop:
  1314  		//		do something without using ind nor nxt
  1315  		//		nxt = inc + ind
  1316  		//		goto loop
  1317  		//
  1318  		//	exit_loop:
  1319  		//
  1320  		// is rewritten to:
  1321  		//
  1322  		//	loop:
  1323  		//		ind = (Phi end nxt)
  1324  		//		if (Const [x]) < ind
  1325  		//		then goto enter_loop
  1326  		//		else goto exit_loop
  1327  		//
  1328  		//	enter_loop:
  1329  		//		do something without using ind nor nxt
  1330  		//		nxt = ind - inc
  1331  		//		goto loop
  1332  		//
  1333  		//	exit_loop:
  1334  		//
  1335  		// this is better because it only requires to keep ind then nxt alive while looping,
  1336  		// while the original form keeps ind then nxt and end alive
  1337  		start, end := v.min, v.max
  1338  		if v.flags&indVarCountDown != 0 {
  1339  			start, end = end, start
  1340  		}
  1341  
  1342  		if !start.isGenericIntConst() {
  1343  			// if start is not a constant we would be winning nothing from inverting the loop
  1344  			continue
  1345  		}
  1346  		if end.isGenericIntConst() {
  1347  			// TODO: if both start and end are constants we should rewrite such that the comparison
  1348  			// is against zero and nxt is ++ or -- operation
  1349  			// That means:
  1350  			//	for i := 2; i < 11; i += 2 {
  1351  			// should be rewritten to:
  1352  			//	for i := 5; 0 < i; i-- {
  1353  			continue
  1354  		}
  1355  
  1356  		if end.Block == ind.Block {
  1357  			// we can't rewrite loops where the condition depends on the loop body
  1358  			// this simple check is forced to work because if this is true a Phi in ind.Block must exist
  1359  			continue
  1360  		}
  1361  
  1362  		check := ind.Block.Controls[0]
  1363  		// invert the check
  1364  		check.Args[0], check.Args[1] = check.Args[1], check.Args[0]
  1365  
  1366  		// swap start and end in the loop
  1367  		for i, v := range check.Args {
  1368  			if v != end {
  1369  				continue
  1370  			}
  1371  
  1372  			check.SetArg(i, start)
  1373  			goto replacedEnd
  1374  		}
  1375  		panic(fmt.Sprintf("unreachable, ind: %v, start: %v, end: %v", ind, start, end))
  1376  	replacedEnd:
  1377  
  1378  		for i, v := range ind.Args {
  1379  			if v != start {
  1380  				continue
  1381  			}
  1382  
  1383  			ind.SetArg(i, end)
  1384  			goto replacedStart
  1385  		}
  1386  		panic(fmt.Sprintf("unreachable, ind: %v, start: %v, end: %v", ind, start, end))
  1387  	replacedStart:
  1388  
  1389  		if nxt.Args[0] != ind {
  1390  			// unlike additions subtractions are not commutative so be sure we get it right
  1391  			nxt.Args[0], nxt.Args[1] = nxt.Args[1], nxt.Args[0]
  1392  		}
  1393  
  1394  		switch nxt.Op {
  1395  		case OpAdd8:
  1396  			nxt.Op = OpSub8
  1397  		case OpAdd16:
  1398  			nxt.Op = OpSub16
  1399  		case OpAdd32:
  1400  			nxt.Op = OpSub32
  1401  		case OpAdd64:
  1402  			nxt.Op = OpSub64
  1403  		case OpSub8:
  1404  			nxt.Op = OpAdd8
  1405  		case OpSub16:
  1406  			nxt.Op = OpAdd16
  1407  		case OpSub32:
  1408  			nxt.Op = OpAdd32
  1409  		case OpSub64:
  1410  			nxt.Op = OpAdd64
  1411  		default:
  1412  			panic("unreachable")
  1413  		}
  1414  
  1415  		if f.pass.debug > 0 {
  1416  			f.Warnl(ind.Pos, "Inverted loop iteration")
  1417  		}
  1418  	}
  1419  
  1420  	ft := newFactsTable(f)
  1421  	ft.checkpoint()
  1422  
  1423  	// Find length and capacity ops.
  1424  	for _, b := range f.Blocks {
  1425  		for _, v := range b.Values {
  1426  			if v.Uses == 0 {
  1427  				// We don't care about dead values.
  1428  				// (There can be some that are CSEd but not removed yet.)
  1429  				continue
  1430  			}
  1431  			switch v.Op {
  1432  			case OpSliceLen:
  1433  				if ft.lens == nil {
  1434  					ft.lens = map[ID]*Value{}
  1435  				}
  1436  				// Set all len Values for the same slice as equal in the poset.
  1437  				// The poset handles transitive relations, so Values related to
  1438  				// any OpSliceLen for this slice will be correctly related to others.
  1439  				if l, ok := ft.lens[v.Args[0].ID]; ok {
  1440  					ft.update(b, v, l, signed, eq)
  1441  				} else {
  1442  					ft.lens[v.Args[0].ID] = v
  1443  				}
  1444  			case OpSliceCap:
  1445  				if ft.caps == nil {
  1446  					ft.caps = map[ID]*Value{}
  1447  				}
  1448  				// Same as case OpSliceLen above, but for slice cap.
  1449  				if c, ok := ft.caps[v.Args[0].ID]; ok {
  1450  					ft.update(b, v, c, signed, eq)
  1451  				} else {
  1452  					ft.caps[v.Args[0].ID] = v
  1453  				}
  1454  			}
  1455  		}
  1456  	}
  1457  
  1458  	// current node state
  1459  	type walkState int
  1460  	const (
  1461  		descend walkState = iota
  1462  		simplify
  1463  	)
  1464  	// work maintains the DFS stack.
  1465  	type bp struct {
  1466  		block *Block    // current handled block
  1467  		state walkState // what's to do
  1468  	}
  1469  	work := make([]bp, 0, 256)
  1470  	work = append(work, bp{
  1471  		block: f.Entry,
  1472  		state: descend,
  1473  	})
  1474  
  1475  	idom := f.Idom()
  1476  	sdom := f.Sdom()
  1477  
  1478  	// DFS on the dominator tree.
  1479  	//
  1480  	// For efficiency, we consider only the dominator tree rather
  1481  	// than the entire flow graph. On the way down, we consider
  1482  	// incoming branches and accumulate conditions that uniquely
  1483  	// dominate the current block. If we discover a contradiction,
  1484  	// we can eliminate the entire block and all of its children.
  1485  	// On the way back up, we consider outgoing branches that
  1486  	// haven't already been considered. This way we consider each
  1487  	// branch condition only once.
  1488  	for len(work) > 0 {
  1489  		node := work[len(work)-1]
  1490  		work = work[:len(work)-1]
  1491  		parent := idom[node.block.ID]
  1492  		branch := getBranch(sdom, parent, node.block)
  1493  
  1494  		switch node.state {
  1495  		case descend:
  1496  			ft.checkpoint()
  1497  
  1498  			// Entering the block, add facts about the induction variable
  1499  			// that is bound to this block.
  1500  			if iv, ok := indVars[node.block]; ok {
  1501  				addIndVarRestrictions(ft, parent, iv)
  1502  			}
  1503  
  1504  			// Add results of reaching this block via a branch from
  1505  			// its immediate dominator (if any).
  1506  			if branch != unknown {
  1507  				addBranchRestrictions(ft, parent, branch)
  1508  			}
  1509  
  1510  			if ft.unsat {
  1511  				// node.block is unreachable.
  1512  				// Remove it and don't visit
  1513  				// its children.
  1514  				removeBranch(parent, branch)
  1515  				ft.restore()
  1516  				break
  1517  			}
  1518  			// Otherwise, we can now commit to
  1519  			// taking this branch. We'll restore
  1520  			// ft when we unwind.
  1521  
  1522  			// Add facts about the values in the current block.
  1523  			addLocalFacts(ft, node.block)
  1524  
  1525  			work = append(work, bp{
  1526  				block: node.block,
  1527  				state: simplify,
  1528  			})
  1529  			for s := sdom.Child(node.block); s != nil; s = sdom.Sibling(s) {
  1530  				work = append(work, bp{
  1531  					block: s,
  1532  					state: descend,
  1533  				})
  1534  			}
  1535  
  1536  		case simplify:
  1537  			simplifyBlock(sdom, ft, node.block)
  1538  			ft.restore()
  1539  		}
  1540  	}
  1541  
  1542  	ft.restore()
  1543  
  1544  	ft.cleanup(f)
  1545  }
  1546  
  1547  // initLimit sets initial constant limit for v.  This limit is based
  1548  // only on the operation itself, not any of its input arguments. This
  1549  // method is only used in two places, once when the prove pass startup
  1550  // and the other when a new ssa value is created, both for init. (unlike
  1551  // flowLimit, below, which computes additional constraints based on
  1552  // ranges of opcode arguments).
  1553  func initLimit(v *Value) limit {
  1554  	if v.Type.IsBoolean() {
  1555  		switch v.Op {
  1556  		case OpConstBool:
  1557  			b := v.AuxInt
  1558  			return limit{min: b, max: b, umin: uint64(b), umax: uint64(b)}
  1559  		default:
  1560  			return limit{min: 0, max: 1, umin: 0, umax: 1}
  1561  		}
  1562  	}
  1563  	if v.Type.IsPtrShaped() { // These are the types that EqPtr/NeqPtr operate on, except uintptr.
  1564  		switch v.Op {
  1565  		case OpConstNil:
  1566  			return limit{min: 0, max: 0, umin: 0, umax: 0}
  1567  		case OpAddr, OpLocalAddr: // TODO: others?
  1568  			l := noLimit
  1569  			l.umin = 1
  1570  			return l
  1571  		default:
  1572  			return noLimit
  1573  		}
  1574  	}
  1575  	if !v.Type.IsInteger() {
  1576  		return noLimit
  1577  	}
  1578  
  1579  	// Default limits based on type.
  1580  	bitsize := v.Type.Size() * 8
  1581  	lim := limit{min: -(1 << (bitsize - 1)), max: 1<<(bitsize-1) - 1, umin: 0, umax: 1<<bitsize - 1}
  1582  
  1583  	// Tighter limits on some opcodes.
  1584  	switch v.Op {
  1585  	// constants
  1586  	case OpConst64:
  1587  		lim = limit{min: v.AuxInt, max: v.AuxInt, umin: uint64(v.AuxInt), umax: uint64(v.AuxInt)}
  1588  	case OpConst32:
  1589  		lim = limit{min: v.AuxInt, max: v.AuxInt, umin: uint64(uint32(v.AuxInt)), umax: uint64(uint32(v.AuxInt))}
  1590  	case OpConst16:
  1591  		lim = limit{min: v.AuxInt, max: v.AuxInt, umin: uint64(uint16(v.AuxInt)), umax: uint64(uint16(v.AuxInt))}
  1592  	case OpConst8:
  1593  		lim = limit{min: v.AuxInt, max: v.AuxInt, umin: uint64(uint8(v.AuxInt)), umax: uint64(uint8(v.AuxInt))}
  1594  
  1595  	// extensions
  1596  	case OpZeroExt8to64, OpZeroExt8to32, OpZeroExt8to16:
  1597  		lim = lim.signedMinMax(0, 1<<8-1)
  1598  		lim = lim.unsignedMax(1<<8 - 1)
  1599  	case OpZeroExt16to64, OpZeroExt16to32:
  1600  		lim = lim.signedMinMax(0, 1<<16-1)
  1601  		lim = lim.unsignedMax(1<<16 - 1)
  1602  	case OpZeroExt32to64:
  1603  		lim = lim.signedMinMax(0, 1<<32-1)
  1604  		lim = lim.unsignedMax(1<<32 - 1)
  1605  	case OpSignExt8to64, OpSignExt8to32, OpSignExt8to16:
  1606  		lim = lim.signedMinMax(math.MinInt8, math.MaxInt8)
  1607  	case OpSignExt16to64, OpSignExt16to32:
  1608  		lim = lim.signedMinMax(math.MinInt16, math.MaxInt16)
  1609  	case OpSignExt32to64:
  1610  		lim = lim.signedMinMax(math.MinInt32, math.MaxInt32)
  1611  
  1612  	// math/bits intrinsics
  1613  	case OpCtz64, OpBitLen64, OpPopCount64,
  1614  		OpCtz32, OpBitLen32, OpPopCount32,
  1615  		OpCtz16, OpBitLen16, OpPopCount16,
  1616  		OpCtz8, OpBitLen8, OpPopCount8:
  1617  		lim = lim.unsignedMax(uint64(v.Args[0].Type.Size() * 8))
  1618  
  1619  	// bool to uint8 conversion
  1620  	case OpCvtBoolToUint8:
  1621  		lim = lim.unsignedMax(1)
  1622  
  1623  	// length operations
  1624  	case OpStringLen, OpSliceLen, OpSliceCap:
  1625  		lim = lim.signedMin(0)
  1626  	}
  1627  
  1628  	// signed <-> unsigned propagation
  1629  	if lim.min >= 0 {
  1630  		lim = lim.unsignedMinMax(uint64(lim.min), uint64(lim.max))
  1631  	}
  1632  	if fitsInBitsU(lim.umax, uint(8*v.Type.Size()-1)) {
  1633  		lim = lim.signedMinMax(int64(lim.umin), int64(lim.umax))
  1634  	}
  1635  
  1636  	return lim
  1637  }
  1638  
  1639  // flowLimit updates the known limits of v in ft. Returns true if anything changed.
  1640  // flowLimit can use the ranges of input arguments.
  1641  //
  1642  // Note: this calculation only happens at the point the value is defined. We do not reevaluate
  1643  // it later. So for example:
  1644  //
  1645  //	v := x + y
  1646  //	if 0 <= x && x < 5 && 0 <= y && y < 5 { ... use v ... }
  1647  //
  1648  // we don't discover that the range of v is bounded in the conditioned
  1649  // block. We could recompute the range of v once we enter the block so
  1650  // we know that it is 0 <= v <= 8, but we don't have a mechanism to do
  1651  // that right now.
  1652  func (ft *factsTable) flowLimit(v *Value) bool {
  1653  	if !v.Type.IsInteger() {
  1654  		// TODO: boolean?
  1655  		return false
  1656  	}
  1657  
  1658  	// Additional limits based on opcode and argument.
  1659  	// No need to repeat things here already done in initLimit.
  1660  	switch v.Op {
  1661  
  1662  	// extensions
  1663  	case OpZeroExt8to64, OpZeroExt8to32, OpZeroExt8to16, OpZeroExt16to64, OpZeroExt16to32, OpZeroExt32to64:
  1664  		a := ft.limits[v.Args[0].ID]
  1665  		return ft.unsignedMinMax(v, a.umin, a.umax)
  1666  	case OpSignExt8to64, OpSignExt8to32, OpSignExt8to16, OpSignExt16to64, OpSignExt16to32, OpSignExt32to64:
  1667  		a := ft.limits[v.Args[0].ID]
  1668  		return ft.signedMinMax(v, a.min, a.max)
  1669  	case OpTrunc64to8, OpTrunc64to16, OpTrunc64to32, OpTrunc32to8, OpTrunc32to16, OpTrunc16to8:
  1670  		a := ft.limits[v.Args[0].ID]
  1671  		if a.umax <= 1<<(uint64(v.Type.Size())*8)-1 {
  1672  			return ft.unsignedMinMax(v, a.umin, a.umax)
  1673  		}
  1674  
  1675  	// math/bits
  1676  	case OpCtz64:
  1677  		a := ft.limits[v.Args[0].ID]
  1678  		if a.nonzero() {
  1679  			return ft.unsignedMax(v, uint64(bits.Len64(a.umax)-1))
  1680  		}
  1681  	case OpCtz32:
  1682  		a := ft.limits[v.Args[0].ID]
  1683  		if a.nonzero() {
  1684  			return ft.unsignedMax(v, uint64(bits.Len32(uint32(a.umax))-1))
  1685  		}
  1686  	case OpCtz16:
  1687  		a := ft.limits[v.Args[0].ID]
  1688  		if a.nonzero() {
  1689  			return ft.unsignedMax(v, uint64(bits.Len16(uint16(a.umax))-1))
  1690  		}
  1691  	case OpCtz8:
  1692  		a := ft.limits[v.Args[0].ID]
  1693  		if a.nonzero() {
  1694  			return ft.unsignedMax(v, uint64(bits.Len8(uint8(a.umax))-1))
  1695  		}
  1696  
  1697  	case OpPopCount64, OpPopCount32, OpPopCount16, OpPopCount8:
  1698  		a := ft.limits[v.Args[0].ID]
  1699  		changingBitsCount := uint64(bits.Len64(a.umax ^ a.umin))
  1700  		sharedLeadingMask := ^(uint64(1)<<changingBitsCount - 1)
  1701  		fixedBits := a.umax & sharedLeadingMask
  1702  		min := uint64(bits.OnesCount64(fixedBits))
  1703  		return ft.unsignedMinMax(v, min, min+changingBitsCount)
  1704  
  1705  	case OpBitLen64:
  1706  		a := ft.limits[v.Args[0].ID]
  1707  		return ft.unsignedMinMax(v,
  1708  			uint64(bits.Len64(a.umin)),
  1709  			uint64(bits.Len64(a.umax)))
  1710  	case OpBitLen32:
  1711  		a := ft.limits[v.Args[0].ID]
  1712  		return ft.unsignedMinMax(v,
  1713  			uint64(bits.Len32(uint32(a.umin))),
  1714  			uint64(bits.Len32(uint32(a.umax))))
  1715  	case OpBitLen16:
  1716  		a := ft.limits[v.Args[0].ID]
  1717  		return ft.unsignedMinMax(v,
  1718  			uint64(bits.Len16(uint16(a.umin))),
  1719  			uint64(bits.Len16(uint16(a.umax))))
  1720  	case OpBitLen8:
  1721  		a := ft.limits[v.Args[0].ID]
  1722  		return ft.unsignedMinMax(v,
  1723  			uint64(bits.Len8(uint8(a.umin))),
  1724  			uint64(bits.Len8(uint8(a.umax))))
  1725  
  1726  	// Masks.
  1727  
  1728  	// TODO: if y.umax and y.umin share a leading bit pattern, y also has that leading bit pattern.
  1729  	// we could compare the patterns of always set bits in a and b and learn more about minimum and maximum.
  1730  	// But I doubt this help any real world code.
  1731  	case OpAnd64, OpAnd32, OpAnd16, OpAnd8:
  1732  		// AND can only make the value smaller.
  1733  		a := ft.limits[v.Args[0].ID]
  1734  		b := ft.limits[v.Args[1].ID]
  1735  		return ft.unsignedMax(v, min(a.umax, b.umax))
  1736  	case OpOr64, OpOr32, OpOr16, OpOr8:
  1737  		// OR can only make the value bigger and can't flip bits proved to be zero in both inputs.
  1738  		a := ft.limits[v.Args[0].ID]
  1739  		b := ft.limits[v.Args[1].ID]
  1740  		return ft.unsignedMinMax(v,
  1741  			max(a.umin, b.umin),
  1742  			1<<bits.Len64(a.umax|b.umax)-1)
  1743  	case OpXor64, OpXor32, OpXor16, OpXor8:
  1744  		// XOR can't flip bits that are proved to be zero in both inputs.
  1745  		a := ft.limits[v.Args[0].ID]
  1746  		b := ft.limits[v.Args[1].ID]
  1747  		return ft.unsignedMax(v, 1<<bits.Len64(a.umax|b.umax)-1)
  1748  	case OpCom64, OpCom32, OpCom16, OpCom8:
  1749  		a := ft.limits[v.Args[0].ID]
  1750  		return ft.newLimit(v, a.com(uint(v.Type.Size())*8))
  1751  
  1752  	// Arithmetic.
  1753  	case OpAdd64, OpAdd32, OpAdd16, OpAdd8:
  1754  		a := ft.limits[v.Args[0].ID]
  1755  		b := ft.limits[v.Args[1].ID]
  1756  		return ft.newLimit(v, a.add(b, uint(v.Type.Size())*8))
  1757  	case OpSub64, OpSub32, OpSub16, OpSub8:
  1758  		a := ft.limits[v.Args[0].ID]
  1759  		b := ft.limits[v.Args[1].ID]
  1760  		sub := ft.newLimit(v, a.sub(b, uint(v.Type.Size())*8))
  1761  		mod := ft.detectSignedMod(v)
  1762  		return sub || mod
  1763  	case OpNeg64, OpNeg32, OpNeg16, OpNeg8:
  1764  		a := ft.limits[v.Args[0].ID]
  1765  		bitsize := uint(v.Type.Size()) * 8
  1766  		return ft.newLimit(v, a.com(bitsize).add(limit{min: 1, max: 1, umin: 1, umax: 1}, bitsize))
  1767  	case OpMul64, OpMul32, OpMul16, OpMul8:
  1768  		a := ft.limits[v.Args[0].ID]
  1769  		b := ft.limits[v.Args[1].ID]
  1770  		return ft.newLimit(v, a.mul(b, uint(v.Type.Size())*8))
  1771  	case OpLsh64x64, OpLsh64x32, OpLsh64x16, OpLsh64x8,
  1772  		OpLsh32x64, OpLsh32x32, OpLsh32x16, OpLsh32x8,
  1773  		OpLsh16x64, OpLsh16x32, OpLsh16x16, OpLsh16x8,
  1774  		OpLsh8x64, OpLsh8x32, OpLsh8x16, OpLsh8x8:
  1775  		a := ft.limits[v.Args[0].ID]
  1776  		b := ft.limits[v.Args[1].ID]
  1777  		bitsize := uint(v.Type.Size()) * 8
  1778  		return ft.newLimit(v, a.mul(b.exp2(bitsize), bitsize))
  1779  	case OpMod64, OpMod32, OpMod16, OpMod8:
  1780  		a := ft.limits[v.Args[0].ID]
  1781  		b := ft.limits[v.Args[1].ID]
  1782  		if !(a.nonnegative() && b.nonnegative()) {
  1783  			// TODO: we could handle signed limits but I didn't bother.
  1784  			break
  1785  		}
  1786  		fallthrough
  1787  	case OpMod64u, OpMod32u, OpMod16u, OpMod8u:
  1788  		a := ft.limits[v.Args[0].ID]
  1789  		b := ft.limits[v.Args[1].ID]
  1790  		// Underflow in the arithmetic below is ok, it gives to MaxUint64 which does nothing to the limit.
  1791  		return ft.unsignedMax(v, min(a.umax, b.umax-1))
  1792  	case OpDiv64, OpDiv32, OpDiv16, OpDiv8:
  1793  		a := ft.limits[v.Args[0].ID]
  1794  		b := ft.limits[v.Args[1].ID]
  1795  		if !(a.nonnegative() && b.nonnegative()) {
  1796  			// TODO: we could handle signed limits but I didn't bother.
  1797  			break
  1798  		}
  1799  		fallthrough
  1800  	case OpDiv64u, OpDiv32u, OpDiv16u, OpDiv8u:
  1801  		a := ft.limits[v.Args[0].ID]
  1802  		b := ft.limits[v.Args[1].ID]
  1803  		lim := noLimit
  1804  		if b.umax > 0 {
  1805  			lim = lim.unsignedMin(a.umin / b.umax)
  1806  		}
  1807  		if b.umin > 0 {
  1808  			lim = lim.unsignedMax(a.umax / b.umin)
  1809  		}
  1810  		return ft.newLimit(v, lim)
  1811  
  1812  	case OpPhi:
  1813  		{
  1814  			// Work around for go.dev/issue/68857, look for min(x, y) and max(x, y).
  1815  			b := v.Block
  1816  			if len(b.Preds) != 2 {
  1817  				goto notMinNorMax
  1818  			}
  1819  			// FIXME: this code searches for the following losange pattern
  1820  			// because that what ssagen produce for min and max builtins:
  1821  			// conditionBlock → (firstBlock, secondBlock) → v.Block
  1822  			// there are three non losange equivalent constructions
  1823  			// we could match for, but I didn't bother:
  1824  			// conditionBlock → (v.Block, secondBlock → v.Block)
  1825  			// conditionBlock → (firstBlock → v.Block, v.Block)
  1826  			// conditionBlock → (v.Block, v.Block)
  1827  			firstBlock, secondBlock := b.Preds[0].b, b.Preds[1].b
  1828  			if firstBlock.Kind != BlockPlain || secondBlock.Kind != BlockPlain {
  1829  				goto notMinNorMax
  1830  			}
  1831  			if len(firstBlock.Preds) != 1 || len(secondBlock.Preds) != 1 {
  1832  				goto notMinNorMax
  1833  			}
  1834  			conditionBlock := firstBlock.Preds[0].b
  1835  			if conditionBlock != secondBlock.Preds[0].b {
  1836  				goto notMinNorMax
  1837  			}
  1838  			if conditionBlock.Kind != BlockIf {
  1839  				goto notMinNorMax
  1840  			}
  1841  
  1842  			less := conditionBlock.Controls[0]
  1843  			var unsigned bool
  1844  			switch less.Op {
  1845  			case OpLess64U, OpLess32U, OpLess16U, OpLess8U,
  1846  				OpLeq64U, OpLeq32U, OpLeq16U, OpLeq8U:
  1847  				unsigned = true
  1848  			case OpLess64, OpLess32, OpLess16, OpLess8,
  1849  				OpLeq64, OpLeq32, OpLeq16, OpLeq8:
  1850  			default:
  1851  				goto notMinNorMax
  1852  			}
  1853  			small, big := less.Args[0], less.Args[1]
  1854  			truev, falsev := v.Args[0], v.Args[1]
  1855  			if conditionBlock.Succs[0].b == secondBlock {
  1856  				truev, falsev = falsev, truev
  1857  			}
  1858  
  1859  			bigl, smalll := ft.limits[big.ID], ft.limits[small.ID]
  1860  			if truev == big {
  1861  				if falsev == small {
  1862  					// v := big if small <¿=? big else small
  1863  					if unsigned {
  1864  						maximum := max(bigl.umax, smalll.umax)
  1865  						minimum := max(bigl.umin, smalll.umin)
  1866  						return ft.unsignedMinMax(v, minimum, maximum)
  1867  					} else {
  1868  						maximum := max(bigl.max, smalll.max)
  1869  						minimum := max(bigl.min, smalll.min)
  1870  						return ft.signedMinMax(v, minimum, maximum)
  1871  					}
  1872  				} else {
  1873  					goto notMinNorMax
  1874  				}
  1875  			} else if truev == small {
  1876  				if falsev == big {
  1877  					// v := small if small <¿=? big else big
  1878  					if unsigned {
  1879  						maximum := min(bigl.umax, smalll.umax)
  1880  						minimum := min(bigl.umin, smalll.umin)
  1881  						return ft.unsignedMinMax(v, minimum, maximum)
  1882  					} else {
  1883  						maximum := min(bigl.max, smalll.max)
  1884  						minimum := min(bigl.min, smalll.min)
  1885  						return ft.signedMinMax(v, minimum, maximum)
  1886  					}
  1887  				} else {
  1888  					goto notMinNorMax
  1889  				}
  1890  			} else {
  1891  				goto notMinNorMax
  1892  			}
  1893  		}
  1894  	notMinNorMax:
  1895  
  1896  		// Compute the union of all the input phis.
  1897  		// Often this will convey no information, because the block
  1898  		// is not dominated by its predecessors and hence the
  1899  		// phi arguments might not have been processed yet. But if
  1900  		// the values are declared earlier, it may help. e.g., for
  1901  		//    v = phi(c3, c5)
  1902  		// where c3 = OpConst [3] and c5 = OpConst [5] are
  1903  		// defined in the entry block, we can derive [3,5]
  1904  		// as the limit for v.
  1905  		l := ft.limits[v.Args[0].ID]
  1906  		for _, a := range v.Args[1:] {
  1907  			l2 := ft.limits[a.ID]
  1908  			l.min = min(l.min, l2.min)
  1909  			l.max = max(l.max, l2.max)
  1910  			l.umin = min(l.umin, l2.umin)
  1911  			l.umax = max(l.umax, l2.umax)
  1912  		}
  1913  		return ft.newLimit(v, l)
  1914  	}
  1915  	return false
  1916  }
  1917  
  1918  // See if we can get any facts because v is the result of signed mod by a constant.
  1919  // The mod operation has already been rewritten, so we have to try and reconstruct it.
  1920  //   x % d
  1921  // is rewritten as
  1922  //   x - (x / d) * d
  1923  // furthermore, the divide itself gets rewritten. If d is a power of 2 (d == 1<<k), we do
  1924  //   (x / d) * d = ((x + adj) >> k) << k
  1925  //               = (x + adj) & (-1<<k)
  1926  // with adj being an adjustment in case x is negative (see below).
  1927  // if d is not a power of 2, we do
  1928  //   x / d = ... TODO ...
  1929  func (ft *factsTable) detectSignedMod(v *Value) bool {
  1930  	if ft.detectSignedModByPowerOfTwo(v) {
  1931  		return true
  1932  	}
  1933  	// TODO: non-powers-of-2
  1934  	return false
  1935  }
  1936  func (ft *factsTable) detectSignedModByPowerOfTwo(v *Value) bool {
  1937  	// We're looking for:
  1938  	//
  1939  	//   x % d ==
  1940  	//   x - (x / d) * d
  1941  	//
  1942  	// which for d a power of 2, d == 1<<k, is done as
  1943  	//
  1944  	//   x - ((x + (x>>(w-1))>>>(w-k)) & (-1<<k))
  1945  	//
  1946  	// w = bit width of x.
  1947  	// (>> = signed shift, >>> = unsigned shift).
  1948  	// See ./_gen/generic.rules, search for "Signed divide by power of 2".
  1949  
  1950  	var w int64
  1951  	var addOp, andOp, constOp, sshiftOp, ushiftOp Op
  1952  	switch v.Op {
  1953  	case OpSub64:
  1954  		w = 64
  1955  		addOp = OpAdd64
  1956  		andOp = OpAnd64
  1957  		constOp = OpConst64
  1958  		sshiftOp = OpRsh64x64
  1959  		ushiftOp = OpRsh64Ux64
  1960  	case OpSub32:
  1961  		w = 32
  1962  		addOp = OpAdd32
  1963  		andOp = OpAnd32
  1964  		constOp = OpConst32
  1965  		sshiftOp = OpRsh32x64
  1966  		ushiftOp = OpRsh32Ux64
  1967  	case OpSub16:
  1968  		w = 16
  1969  		addOp = OpAdd16
  1970  		andOp = OpAnd16
  1971  		constOp = OpConst16
  1972  		sshiftOp = OpRsh16x64
  1973  		ushiftOp = OpRsh16Ux64
  1974  	case OpSub8:
  1975  		w = 8
  1976  		addOp = OpAdd8
  1977  		andOp = OpAnd8
  1978  		constOp = OpConst8
  1979  		sshiftOp = OpRsh8x64
  1980  		ushiftOp = OpRsh8Ux64
  1981  	default:
  1982  		return false
  1983  	}
  1984  
  1985  	x := v.Args[0]
  1986  	and := v.Args[1]
  1987  	if and.Op != andOp {
  1988  		return false
  1989  	}
  1990  	var add, mask *Value
  1991  	if and.Args[0].Op == addOp && and.Args[1].Op == constOp {
  1992  		add = and.Args[0]
  1993  		mask = and.Args[1]
  1994  	} else if and.Args[1].Op == addOp && and.Args[0].Op == constOp {
  1995  		add = and.Args[1]
  1996  		mask = and.Args[0]
  1997  	} else {
  1998  		return false
  1999  	}
  2000  	var ushift *Value
  2001  	if add.Args[0] == x {
  2002  		ushift = add.Args[1]
  2003  	} else if add.Args[1] == x {
  2004  		ushift = add.Args[0]
  2005  	} else {
  2006  		return false
  2007  	}
  2008  	if ushift.Op != ushiftOp {
  2009  		return false
  2010  	}
  2011  	if ushift.Args[1].Op != OpConst64 {
  2012  		return false
  2013  	}
  2014  	k := w - ushift.Args[1].AuxInt // Now we know k!
  2015  	d := int64(1) << k             // divisor
  2016  	sshift := ushift.Args[0]
  2017  	if sshift.Op != sshiftOp {
  2018  		return false
  2019  	}
  2020  	if sshift.Args[0] != x {
  2021  		return false
  2022  	}
  2023  	if sshift.Args[1].Op != OpConst64 || sshift.Args[1].AuxInt != w-1 {
  2024  		return false
  2025  	}
  2026  	if mask.AuxInt != -d {
  2027  		return false
  2028  	}
  2029  
  2030  	// All looks ok. x % d is at most +/- d-1.
  2031  	return ft.signedMinMax(v, -d+1, d-1)
  2032  }
  2033  
  2034  // getBranch returns the range restrictions added by p
  2035  // when reaching b. p is the immediate dominator of b.
  2036  func getBranch(sdom SparseTree, p *Block, b *Block) branch {
  2037  	if p == nil {
  2038  		return unknown
  2039  	}
  2040  	switch p.Kind {
  2041  	case BlockIf:
  2042  		// If p and p.Succs[0] are dominators it means that every path
  2043  		// from entry to b passes through p and p.Succs[0]. We care that
  2044  		// no path from entry to b passes through p.Succs[1]. If p.Succs[0]
  2045  		// has one predecessor then (apart from the degenerate case),
  2046  		// there is no path from entry that can reach b through p.Succs[1].
  2047  		// TODO: how about p->yes->b->yes, i.e. a loop in yes.
  2048  		if sdom.IsAncestorEq(p.Succs[0].b, b) && len(p.Succs[0].b.Preds) == 1 {
  2049  			return positive
  2050  		}
  2051  		if sdom.IsAncestorEq(p.Succs[1].b, b) && len(p.Succs[1].b.Preds) == 1 {
  2052  			return negative
  2053  		}
  2054  	case BlockJumpTable:
  2055  		// TODO: this loop can lead to quadratic behavior, as
  2056  		// getBranch can be called len(p.Succs) times.
  2057  		for i, e := range p.Succs {
  2058  			if sdom.IsAncestorEq(e.b, b) && len(e.b.Preds) == 1 {
  2059  				return jumpTable0 + branch(i)
  2060  			}
  2061  		}
  2062  	}
  2063  	return unknown
  2064  }
  2065  
  2066  // addIndVarRestrictions updates the factsTables ft with the facts
  2067  // learned from the induction variable indVar which drives the loop
  2068  // starting in Block b.
  2069  func addIndVarRestrictions(ft *factsTable, b *Block, iv indVar) {
  2070  	d := signed
  2071  	if ft.isNonNegative(iv.min) && ft.isNonNegative(iv.max) {
  2072  		d |= unsigned
  2073  	}
  2074  
  2075  	if iv.flags&indVarMinExc == 0 {
  2076  		addRestrictions(b, ft, d, iv.min, iv.ind, lt|eq)
  2077  	} else {
  2078  		addRestrictions(b, ft, d, iv.min, iv.ind, lt)
  2079  	}
  2080  
  2081  	if iv.flags&indVarMaxInc == 0 {
  2082  		addRestrictions(b, ft, d, iv.ind, iv.max, lt)
  2083  	} else {
  2084  		addRestrictions(b, ft, d, iv.ind, iv.max, lt|eq)
  2085  	}
  2086  }
  2087  
  2088  // addBranchRestrictions updates the factsTables ft with the facts learned when
  2089  // branching from Block b in direction br.
  2090  func addBranchRestrictions(ft *factsTable, b *Block, br branch) {
  2091  	c := b.Controls[0]
  2092  	switch {
  2093  	case br == negative:
  2094  		ft.booleanFalse(c)
  2095  	case br == positive:
  2096  		ft.booleanTrue(c)
  2097  	case br >= jumpTable0:
  2098  		idx := br - jumpTable0
  2099  		val := int64(idx)
  2100  		if v, off := isConstDelta(c); v != nil {
  2101  			// Establish the bound on the underlying value we're switching on,
  2102  			// not on the offset-ed value used as the jump table index.
  2103  			c = v
  2104  			val -= off
  2105  		}
  2106  		ft.newLimit(c, limit{min: val, max: val, umin: uint64(val), umax: uint64(val)})
  2107  	default:
  2108  		panic("unknown branch")
  2109  	}
  2110  }
  2111  
  2112  // addRestrictions updates restrictions from the immediate
  2113  // dominating block (p) using r.
  2114  func addRestrictions(parent *Block, ft *factsTable, t domain, v, w *Value, r relation) {
  2115  	if t == 0 {
  2116  		// Trivial case: nothing to do.
  2117  		// Should not happen, but just in case.
  2118  		return
  2119  	}
  2120  	for i := domain(1); i <= t; i <<= 1 {
  2121  		if t&i == 0 {
  2122  			continue
  2123  		}
  2124  		ft.update(parent, v, w, i, r)
  2125  	}
  2126  }
  2127  
  2128  func addLocalFacts(ft *factsTable, b *Block) {
  2129  	// Propagate constant ranges among values in this block.
  2130  	// We do this before the second loop so that we have the
  2131  	// most up-to-date constant bounds for isNonNegative calls.
  2132  	for {
  2133  		changed := false
  2134  		for _, v := range b.Values {
  2135  			changed = ft.flowLimit(v) || changed
  2136  		}
  2137  		if !changed {
  2138  			break
  2139  		}
  2140  	}
  2141  
  2142  	// Add facts about individual operations.
  2143  	for _, v := range b.Values {
  2144  		// FIXME(go.dev/issue/68857): this loop only set up limits properly when b.Values is in topological order.
  2145  		// flowLimit can also depend on limits given by this loop which right now is not handled.
  2146  		switch v.Op {
  2147  		case OpAnd64, OpAnd32, OpAnd16, OpAnd8:
  2148  			ft.update(b, v, v.Args[0], unsigned, lt|eq)
  2149  			ft.update(b, v, v.Args[1], unsigned, lt|eq)
  2150  			if ft.isNonNegative(v.Args[0]) {
  2151  				ft.update(b, v, v.Args[0], signed, lt|eq)
  2152  			}
  2153  			if ft.isNonNegative(v.Args[1]) {
  2154  				ft.update(b, v, v.Args[1], signed, lt|eq)
  2155  			}
  2156  		case OpOr64, OpOr32, OpOr16, OpOr8:
  2157  			// TODO: investigate how to always add facts without much slowdown, see issue #57959
  2158  			//ft.update(b, v, v.Args[0], unsigned, gt|eq)
  2159  			//ft.update(b, v, v.Args[1], unsigned, gt|eq)
  2160  		case OpDiv64u, OpDiv32u, OpDiv16u, OpDiv8u,
  2161  			OpRsh8Ux64, OpRsh8Ux32, OpRsh8Ux16, OpRsh8Ux8,
  2162  			OpRsh16Ux64, OpRsh16Ux32, OpRsh16Ux16, OpRsh16Ux8,
  2163  			OpRsh32Ux64, OpRsh32Ux32, OpRsh32Ux16, OpRsh32Ux8,
  2164  			OpRsh64Ux64, OpRsh64Ux32, OpRsh64Ux16, OpRsh64Ux8:
  2165  			ft.update(b, v, v.Args[0], unsigned, lt|eq)
  2166  		case OpMod64u, OpMod32u, OpMod16u, OpMod8u:
  2167  			ft.update(b, v, v.Args[0], unsigned, lt|eq)
  2168  			// Note: we have to be careful that this doesn't imply
  2169  			// that the modulus is >0, which isn't true until *after*
  2170  			// the mod instruction executes (and thus panics if the
  2171  			// modulus is 0). See issue 67625.
  2172  			ft.update(b, v, v.Args[1], unsigned, lt)
  2173  		case OpSliceLen:
  2174  			if v.Args[0].Op == OpSliceMake {
  2175  				ft.update(b, v, v.Args[0].Args[1], signed, eq)
  2176  			}
  2177  		case OpSliceCap:
  2178  			if v.Args[0].Op == OpSliceMake {
  2179  				ft.update(b, v, v.Args[0].Args[2], signed, eq)
  2180  			}
  2181  		case OpPhi:
  2182  			addLocalFactsPhi(ft, v)
  2183  		}
  2184  	}
  2185  }
  2186  
  2187  func addLocalFactsPhi(ft *factsTable, v *Value) {
  2188  	// Look for phis that implement min/max.
  2189  	//   z:
  2190  	//      c = Less64 x y (or other Less/Leq operation)
  2191  	//      If c -> bx by
  2192  	//   bx: <- z
  2193  	//       -> b ...
  2194  	//   by: <- z
  2195  	//      -> b ...
  2196  	//   b: <- bx by
  2197  	//      v = Phi x y
  2198  	// Then v is either min or max of x,y.
  2199  	// If it is the min, then we deduce v <= x && v <= y.
  2200  	// If it is the max, then we deduce v >= x && v >= y.
  2201  	// The min case is useful for the copy builtin, see issue 16833.
  2202  	if len(v.Args) != 2 {
  2203  		return
  2204  	}
  2205  	b := v.Block
  2206  	x := v.Args[0]
  2207  	y := v.Args[1]
  2208  	bx := b.Preds[0].b
  2209  	by := b.Preds[1].b
  2210  	var z *Block // branch point
  2211  	switch {
  2212  	case bx == by: // bx == by == z case
  2213  		z = bx
  2214  	case by.uniquePred() == bx: // bx == z case
  2215  		z = bx
  2216  	case bx.uniquePred() == by: // by == z case
  2217  		z = by
  2218  	case bx.uniquePred() == by.uniquePred():
  2219  		z = bx.uniquePred()
  2220  	}
  2221  	if z == nil || z.Kind != BlockIf {
  2222  		return
  2223  	}
  2224  	c := z.Controls[0]
  2225  	if len(c.Args) != 2 {
  2226  		return
  2227  	}
  2228  	var isMin bool // if c, a less-than comparison, is true, phi chooses x.
  2229  	if bx == z {
  2230  		isMin = b.Preds[0].i == 0
  2231  	} else {
  2232  		isMin = bx.Preds[0].i == 0
  2233  	}
  2234  	if c.Args[0] == x && c.Args[1] == y {
  2235  		// ok
  2236  	} else if c.Args[0] == y && c.Args[1] == x {
  2237  		// Comparison is reversed from how the values are listed in the Phi.
  2238  		isMin = !isMin
  2239  	} else {
  2240  		// Not comparing x and y.
  2241  		return
  2242  	}
  2243  	var dom domain
  2244  	switch c.Op {
  2245  	case OpLess64, OpLess32, OpLess16, OpLess8, OpLeq64, OpLeq32, OpLeq16, OpLeq8:
  2246  		dom = signed
  2247  	case OpLess64U, OpLess32U, OpLess16U, OpLess8U, OpLeq64U, OpLeq32U, OpLeq16U, OpLeq8U:
  2248  		dom = unsigned
  2249  	default:
  2250  		return
  2251  	}
  2252  	var rel relation
  2253  	if isMin {
  2254  		rel = lt | eq
  2255  	} else {
  2256  		rel = gt | eq
  2257  	}
  2258  	ft.update(b, v, x, dom, rel)
  2259  	ft.update(b, v, y, dom, rel)
  2260  }
  2261  
  2262  var ctzNonZeroOp = map[Op]Op{OpCtz8: OpCtz8NonZero, OpCtz16: OpCtz16NonZero, OpCtz32: OpCtz32NonZero, OpCtz64: OpCtz64NonZero}
  2263  var mostNegativeDividend = map[Op]int64{
  2264  	OpDiv16: -1 << 15,
  2265  	OpMod16: -1 << 15,
  2266  	OpDiv32: -1 << 31,
  2267  	OpMod32: -1 << 31,
  2268  	OpDiv64: -1 << 63,
  2269  	OpMod64: -1 << 63}
  2270  
  2271  // simplifyBlock simplifies some constant values in b and evaluates
  2272  // branches to non-uniquely dominated successors of b.
  2273  func simplifyBlock(sdom SparseTree, ft *factsTable, b *Block) {
  2274  	for _, v := range b.Values {
  2275  		switch v.Op {
  2276  		case OpSlicemask:
  2277  			// Replace OpSlicemask operations in b with constants where possible.
  2278  			x, delta := isConstDelta(v.Args[0])
  2279  			if x == nil {
  2280  				break
  2281  			}
  2282  			// slicemask(x + y)
  2283  			// if x is larger than -y (y is negative), then slicemask is -1.
  2284  			lim := ft.limits[x.ID]
  2285  			if lim.umin > uint64(-delta) {
  2286  				if v.Args[0].Op == OpAdd64 {
  2287  					v.reset(OpConst64)
  2288  				} else {
  2289  					v.reset(OpConst32)
  2290  				}
  2291  				if b.Func.pass.debug > 0 {
  2292  					b.Func.Warnl(v.Pos, "Proved slicemask not needed")
  2293  				}
  2294  				v.AuxInt = -1
  2295  			}
  2296  		case OpCtz8, OpCtz16, OpCtz32, OpCtz64:
  2297  			// On some architectures, notably amd64, we can generate much better
  2298  			// code for CtzNN if we know that the argument is non-zero.
  2299  			// Capture that information here for use in arch-specific optimizations.
  2300  			x := v.Args[0]
  2301  			lim := ft.limits[x.ID]
  2302  			if lim.umin > 0 || lim.min > 0 || lim.max < 0 {
  2303  				if b.Func.pass.debug > 0 {
  2304  					b.Func.Warnl(v.Pos, "Proved %v non-zero", v.Op)
  2305  				}
  2306  				v.Op = ctzNonZeroOp[v.Op]
  2307  			}
  2308  		case OpRsh8x8, OpRsh8x16, OpRsh8x32, OpRsh8x64,
  2309  			OpRsh16x8, OpRsh16x16, OpRsh16x32, OpRsh16x64,
  2310  			OpRsh32x8, OpRsh32x16, OpRsh32x32, OpRsh32x64,
  2311  			OpRsh64x8, OpRsh64x16, OpRsh64x32, OpRsh64x64:
  2312  			// Check whether, for a >> b, we know that a is non-negative
  2313  			// and b is all of a's bits except the MSB. If so, a is shifted to zero.
  2314  			bits := 8 * v.Args[0].Type.Size()
  2315  			if v.Args[1].isGenericIntConst() && v.Args[1].AuxInt >= bits-1 && ft.isNonNegative(v.Args[0]) {
  2316  				if b.Func.pass.debug > 0 {
  2317  					b.Func.Warnl(v.Pos, "Proved %v shifts to zero", v.Op)
  2318  				}
  2319  				switch bits {
  2320  				case 64:
  2321  					v.reset(OpConst64)
  2322  				case 32:
  2323  					v.reset(OpConst32)
  2324  				case 16:
  2325  					v.reset(OpConst16)
  2326  				case 8:
  2327  					v.reset(OpConst8)
  2328  				default:
  2329  					panic("unexpected integer size")
  2330  				}
  2331  				v.AuxInt = 0
  2332  				break // Be sure not to fallthrough - this is no longer OpRsh.
  2333  			}
  2334  			// If the Rsh hasn't been replaced with 0, still check if it is bounded.
  2335  			fallthrough
  2336  		case OpLsh8x8, OpLsh8x16, OpLsh8x32, OpLsh8x64,
  2337  			OpLsh16x8, OpLsh16x16, OpLsh16x32, OpLsh16x64,
  2338  			OpLsh32x8, OpLsh32x16, OpLsh32x32, OpLsh32x64,
  2339  			OpLsh64x8, OpLsh64x16, OpLsh64x32, OpLsh64x64,
  2340  			OpRsh8Ux8, OpRsh8Ux16, OpRsh8Ux32, OpRsh8Ux64,
  2341  			OpRsh16Ux8, OpRsh16Ux16, OpRsh16Ux32, OpRsh16Ux64,
  2342  			OpRsh32Ux8, OpRsh32Ux16, OpRsh32Ux32, OpRsh32Ux64,
  2343  			OpRsh64Ux8, OpRsh64Ux16, OpRsh64Ux32, OpRsh64Ux64:
  2344  			// Check whether, for a << b, we know that b
  2345  			// is strictly less than the number of bits in a.
  2346  			by := v.Args[1]
  2347  			lim := ft.limits[by.ID]
  2348  			bits := 8 * v.Args[0].Type.Size()
  2349  			if lim.umax < uint64(bits) || (lim.max < bits && ft.isNonNegative(by)) {
  2350  				v.AuxInt = 1 // see shiftIsBounded
  2351  				if b.Func.pass.debug > 0 && !by.isGenericIntConst() {
  2352  					b.Func.Warnl(v.Pos, "Proved %v bounded", v.Op)
  2353  				}
  2354  			}
  2355  		case OpDiv16, OpDiv32, OpDiv64, OpMod16, OpMod32, OpMod64:
  2356  			// On amd64 and 386 fix-up code can be avoided if we know
  2357  			//  the divisor is not -1 or the dividend > MinIntNN.
  2358  			// Don't modify AuxInt on other architectures,
  2359  			// as that can interfere with CSE.
  2360  			// TODO: add other architectures?
  2361  			if b.Func.Config.arch != "386" && b.Func.Config.arch != "amd64" {
  2362  				break
  2363  			}
  2364  			divr := v.Args[1]
  2365  			divrLim := ft.limits[divr.ID]
  2366  			divd := v.Args[0]
  2367  			divdLim := ft.limits[divd.ID]
  2368  			if divrLim.max < -1 || divrLim.min > -1 || divdLim.min > mostNegativeDividend[v.Op] {
  2369  				// See DivisionNeedsFixUp in rewrite.go.
  2370  				// v.AuxInt = 1 means we have proved both that the divisor is not -1
  2371  				// and that the dividend is not the most negative integer,
  2372  				// so we do not need to add fix-up code.
  2373  				v.AuxInt = 1
  2374  				if b.Func.pass.debug > 0 {
  2375  					b.Func.Warnl(v.Pos, "Proved %v does not need fix-up", v.Op)
  2376  				}
  2377  			}
  2378  		}
  2379  		// Fold provable constant results.
  2380  		// Helps in cases where we reuse a value after branching on its equality.
  2381  		for i, arg := range v.Args {
  2382  			lim := ft.limits[arg.ID]
  2383  			var constValue int64
  2384  			switch {
  2385  			case lim.min == lim.max:
  2386  				constValue = lim.min
  2387  			case lim.umin == lim.umax:
  2388  				constValue = int64(lim.umin)
  2389  			default:
  2390  				continue
  2391  			}
  2392  			switch arg.Op {
  2393  			case OpConst64, OpConst32, OpConst16, OpConst8, OpConstBool, OpConstNil:
  2394  				continue
  2395  			}
  2396  			typ := arg.Type
  2397  			f := b.Func
  2398  			var c *Value
  2399  			switch {
  2400  			case typ.IsBoolean():
  2401  				c = f.ConstBool(typ, constValue != 0)
  2402  			case typ.IsInteger() && typ.Size() == 1:
  2403  				c = f.ConstInt8(typ, int8(constValue))
  2404  			case typ.IsInteger() && typ.Size() == 2:
  2405  				c = f.ConstInt16(typ, int16(constValue))
  2406  			case typ.IsInteger() && typ.Size() == 4:
  2407  				c = f.ConstInt32(typ, int32(constValue))
  2408  			case typ.IsInteger() && typ.Size() == 8:
  2409  				c = f.ConstInt64(typ, constValue)
  2410  			case typ.IsPtrShaped():
  2411  				if constValue == 0 {
  2412  					c = f.ConstNil(typ)
  2413  				} else {
  2414  					// Not sure how this might happen, but if it
  2415  					// does, just skip it.
  2416  					continue
  2417  				}
  2418  			default:
  2419  				// Not sure how this might happen, but if it
  2420  				// does, just skip it.
  2421  				continue
  2422  			}
  2423  			v.SetArg(i, c)
  2424  			ft.initLimitForNewValue(c)
  2425  			if b.Func.pass.debug > 1 {
  2426  				b.Func.Warnl(v.Pos, "Proved %v's arg %d (%v) is constant %d", v, i, arg, constValue)
  2427  			}
  2428  		}
  2429  	}
  2430  
  2431  	if b.Kind != BlockIf {
  2432  		return
  2433  	}
  2434  
  2435  	// Consider outgoing edges from this block.
  2436  	parent := b
  2437  	for i, branch := range [...]branch{positive, negative} {
  2438  		child := parent.Succs[i].b
  2439  		if getBranch(sdom, parent, child) != unknown {
  2440  			// For edges to uniquely dominated blocks, we
  2441  			// already did this when we visited the child.
  2442  			continue
  2443  		}
  2444  		// For edges to other blocks, this can trim a branch
  2445  		// even if we couldn't get rid of the child itself.
  2446  		ft.checkpoint()
  2447  		addBranchRestrictions(ft, parent, branch)
  2448  		unsat := ft.unsat
  2449  		ft.restore()
  2450  		if unsat {
  2451  			// This branch is impossible, so remove it
  2452  			// from the block.
  2453  			removeBranch(parent, branch)
  2454  			// No point in considering the other branch.
  2455  			// (It *is* possible for both to be
  2456  			// unsatisfiable since the fact table is
  2457  			// incomplete. We could turn this into a
  2458  			// BlockExit, but it doesn't seem worth it.)
  2459  			break
  2460  		}
  2461  	}
  2462  }
  2463  
  2464  func removeBranch(b *Block, branch branch) {
  2465  	c := b.Controls[0]
  2466  	if b.Func.pass.debug > 0 {
  2467  		verb := "Proved"
  2468  		if branch == positive {
  2469  			verb = "Disproved"
  2470  		}
  2471  		if b.Func.pass.debug > 1 {
  2472  			b.Func.Warnl(b.Pos, "%s %s (%s)", verb, c.Op, c)
  2473  		} else {
  2474  			b.Func.Warnl(b.Pos, "%s %s", verb, c.Op)
  2475  		}
  2476  	}
  2477  	if c != nil && c.Pos.IsStmt() == src.PosIsStmt && c.Pos.SameFileAndLine(b.Pos) {
  2478  		// attempt to preserve statement marker.
  2479  		b.Pos = b.Pos.WithIsStmt()
  2480  	}
  2481  	if branch == positive || branch == negative {
  2482  		b.Kind = BlockFirst
  2483  		b.ResetControls()
  2484  		if branch == positive {
  2485  			b.swapSuccessors()
  2486  		}
  2487  	} else {
  2488  		// TODO: figure out how to remove an entry from a jump table
  2489  	}
  2490  }
  2491  
  2492  // isConstDelta returns non-nil if v is equivalent to w+delta (signed).
  2493  func isConstDelta(v *Value) (w *Value, delta int64) {
  2494  	cop := OpConst64
  2495  	switch v.Op {
  2496  	case OpAdd32, OpSub32:
  2497  		cop = OpConst32
  2498  	case OpAdd16, OpSub16:
  2499  		cop = OpConst16
  2500  	case OpAdd8, OpSub8:
  2501  		cop = OpConst8
  2502  	}
  2503  	switch v.Op {
  2504  	case OpAdd64, OpAdd32, OpAdd16, OpAdd8:
  2505  		if v.Args[0].Op == cop {
  2506  			return v.Args[1], v.Args[0].AuxInt
  2507  		}
  2508  		if v.Args[1].Op == cop {
  2509  			return v.Args[0], v.Args[1].AuxInt
  2510  		}
  2511  	case OpSub64, OpSub32, OpSub16, OpSub8:
  2512  		if v.Args[1].Op == cop {
  2513  			aux := v.Args[1].AuxInt
  2514  			if aux != -aux { // Overflow; too bad
  2515  				return v.Args[0], -aux
  2516  			}
  2517  		}
  2518  	}
  2519  	return nil, 0
  2520  }
  2521  
  2522  // isCleanExt reports whether v is the result of a value-preserving
  2523  // sign or zero extension.
  2524  func isCleanExt(v *Value) bool {
  2525  	switch v.Op {
  2526  	case OpSignExt8to16, OpSignExt8to32, OpSignExt8to64,
  2527  		OpSignExt16to32, OpSignExt16to64, OpSignExt32to64:
  2528  		// signed -> signed is the only value-preserving sign extension
  2529  		return v.Args[0].Type.IsSigned() && v.Type.IsSigned()
  2530  
  2531  	case OpZeroExt8to16, OpZeroExt8to32, OpZeroExt8to64,
  2532  		OpZeroExt16to32, OpZeroExt16to64, OpZeroExt32to64:
  2533  		// unsigned -> signed/unsigned are value-preserving zero extensions
  2534  		return !v.Args[0].Type.IsSigned()
  2535  	}
  2536  	return false
  2537  }
  2538  

View as plain text