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

View as plain text