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

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

View as plain text