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

View as plain text