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  
  1302  	ft := newFactsTable(f)
  1303  	ft.checkpoint()
  1304  
  1305  	// Find length and capacity ops.
  1306  	for _, b := range f.Blocks {
  1307  		for _, v := range b.Values {
  1308  			if v.Uses == 0 {
  1309  				// We don't care about dead values.
  1310  				// (There can be some that are CSEd but not removed yet.)
  1311  				continue
  1312  			}
  1313  			switch v.Op {
  1314  			case OpSliceLen:
  1315  				if ft.lens == nil {
  1316  					ft.lens = map[ID]*Value{}
  1317  				}
  1318  				// Set all len Values for the same slice as equal in the poset.
  1319  				// The poset handles transitive relations, so Values related to
  1320  				// any OpSliceLen for this slice will be correctly related to others.
  1321  				if l, ok := ft.lens[v.Args[0].ID]; ok {
  1322  					ft.update(b, v, l, signed, eq)
  1323  				} else {
  1324  					ft.lens[v.Args[0].ID] = v
  1325  				}
  1326  			case OpSliceCap:
  1327  				if ft.caps == nil {
  1328  					ft.caps = map[ID]*Value{}
  1329  				}
  1330  				// Same as case OpSliceLen above, but for slice cap.
  1331  				if c, ok := ft.caps[v.Args[0].ID]; ok {
  1332  					ft.update(b, v, c, signed, eq)
  1333  				} else {
  1334  					ft.caps[v.Args[0].ID] = v
  1335  				}
  1336  			}
  1337  		}
  1338  	}
  1339  
  1340  	// current node state
  1341  	type walkState int
  1342  	const (
  1343  		descend walkState = iota
  1344  		simplify
  1345  	)
  1346  	// work maintains the DFS stack.
  1347  	type bp struct {
  1348  		block *Block    // current handled block
  1349  		state walkState // what's to do
  1350  	}
  1351  	work := make([]bp, 0, 256)
  1352  	work = append(work, bp{
  1353  		block: f.Entry,
  1354  		state: descend,
  1355  	})
  1356  
  1357  	idom := f.Idom()
  1358  	sdom := f.Sdom()
  1359  
  1360  	// DFS on the dominator tree.
  1361  	//
  1362  	// For efficiency, we consider only the dominator tree rather
  1363  	// than the entire flow graph. On the way down, we consider
  1364  	// incoming branches and accumulate conditions that uniquely
  1365  	// dominate the current block. If we discover a contradiction,
  1366  	// we can eliminate the entire block and all of its children.
  1367  	// On the way back up, we consider outgoing branches that
  1368  	// haven't already been considered. This way we consider each
  1369  	// branch condition only once.
  1370  	for len(work) > 0 {
  1371  		node := work[len(work)-1]
  1372  		work = work[:len(work)-1]
  1373  		parent := idom[node.block.ID]
  1374  		branch := getBranch(sdom, parent, node.block)
  1375  
  1376  		switch node.state {
  1377  		case descend:
  1378  			ft.checkpoint()
  1379  
  1380  			// Entering the block, add facts about the induction variable
  1381  			// that is bound to this block.
  1382  			if iv, ok := indVars[node.block]; ok {
  1383  				addIndVarRestrictions(ft, parent, iv)
  1384  			}
  1385  
  1386  			// Add results of reaching this block via a branch from
  1387  			// its immediate dominator (if any).
  1388  			if branch != unknown {
  1389  				addBranchRestrictions(ft, parent, branch)
  1390  			}
  1391  
  1392  			if ft.unsat {
  1393  				// node.block is unreachable.
  1394  				// Remove it and don't visit
  1395  				// its children.
  1396  				removeBranch(parent, branch)
  1397  				ft.restore()
  1398  				break
  1399  			}
  1400  			// Otherwise, we can now commit to
  1401  			// taking this branch. We'll restore
  1402  			// ft when we unwind.
  1403  
  1404  			// Add facts about the values in the current block.
  1405  			addLocalFacts(ft, node.block)
  1406  
  1407  			work = append(work, bp{
  1408  				block: node.block,
  1409  				state: simplify,
  1410  			})
  1411  			for s := sdom.Child(node.block); s != nil; s = sdom.Sibling(s) {
  1412  				work = append(work, bp{
  1413  					block: s,
  1414  					state: descend,
  1415  				})
  1416  			}
  1417  
  1418  		case simplify:
  1419  			simplifyBlock(sdom, ft, node.block)
  1420  			ft.restore()
  1421  		}
  1422  	}
  1423  
  1424  	ft.restore()
  1425  
  1426  	ft.cleanup(f)
  1427  }
  1428  
  1429  // initLimit sets initial constant limit for v.  This limit is based
  1430  // only on the operation itself, not any of its input arguments. This
  1431  // method is only used in two places, once when the prove pass startup
  1432  // and the other when a new ssa value is created, both for init. (unlike
  1433  // flowLimit, below, which computes additional constraints based on
  1434  // ranges of opcode arguments).
  1435  func initLimit(v *Value) limit {
  1436  	if v.Type.IsBoolean() {
  1437  		switch v.Op {
  1438  		case OpConstBool:
  1439  			b := v.AuxInt
  1440  			return limit{min: b, max: b, umin: uint64(b), umax: uint64(b)}
  1441  		default:
  1442  			return limit{min: 0, max: 1, umin: 0, umax: 1}
  1443  		}
  1444  	}
  1445  	if v.Type.IsPtrShaped() { // These are the types that EqPtr/NeqPtr operate on, except uintptr.
  1446  		switch v.Op {
  1447  		case OpConstNil:
  1448  			return limit{min: 0, max: 0, umin: 0, umax: 0}
  1449  		case OpAddr, OpLocalAddr: // TODO: others?
  1450  			l := noLimit
  1451  			l.umin = 1
  1452  			return l
  1453  		default:
  1454  			return noLimit
  1455  		}
  1456  	}
  1457  	if !v.Type.IsInteger() {
  1458  		return noLimit
  1459  	}
  1460  
  1461  	// Default limits based on type.
  1462  	bitsize := v.Type.Size() * 8
  1463  	lim := limit{min: -(1 << (bitsize - 1)), max: 1<<(bitsize-1) - 1, umin: 0, umax: 1<<bitsize - 1}
  1464  
  1465  	// Tighter limits on some opcodes.
  1466  	switch v.Op {
  1467  	// constants
  1468  	case OpConst64:
  1469  		lim = limit{min: v.AuxInt, max: v.AuxInt, umin: uint64(v.AuxInt), umax: uint64(v.AuxInt)}
  1470  	case OpConst32:
  1471  		lim = limit{min: v.AuxInt, max: v.AuxInt, umin: uint64(uint32(v.AuxInt)), umax: uint64(uint32(v.AuxInt))}
  1472  	case OpConst16:
  1473  		lim = limit{min: v.AuxInt, max: v.AuxInt, umin: uint64(uint16(v.AuxInt)), umax: uint64(uint16(v.AuxInt))}
  1474  	case OpConst8:
  1475  		lim = limit{min: v.AuxInt, max: v.AuxInt, umin: uint64(uint8(v.AuxInt)), umax: uint64(uint8(v.AuxInt))}
  1476  
  1477  	// extensions
  1478  	case OpZeroExt8to64, OpZeroExt8to32, OpZeroExt8to16:
  1479  		lim = lim.signedMinMax(0, 1<<8-1)
  1480  		lim = lim.unsignedMax(1<<8 - 1)
  1481  	case OpZeroExt16to64, OpZeroExt16to32:
  1482  		lim = lim.signedMinMax(0, 1<<16-1)
  1483  		lim = lim.unsignedMax(1<<16 - 1)
  1484  	case OpZeroExt32to64:
  1485  		lim = lim.signedMinMax(0, 1<<32-1)
  1486  		lim = lim.unsignedMax(1<<32 - 1)
  1487  	case OpSignExt8to64, OpSignExt8to32, OpSignExt8to16:
  1488  		lim = lim.signedMinMax(math.MinInt8, math.MaxInt8)
  1489  	case OpSignExt16to64, OpSignExt16to32:
  1490  		lim = lim.signedMinMax(math.MinInt16, math.MaxInt16)
  1491  	case OpSignExt32to64:
  1492  		lim = lim.signedMinMax(math.MinInt32, math.MaxInt32)
  1493  
  1494  	// math/bits intrinsics
  1495  	case OpCtz64, OpBitLen64, OpPopCount64,
  1496  		OpCtz32, OpBitLen32, OpPopCount32,
  1497  		OpCtz16, OpBitLen16, OpPopCount16,
  1498  		OpCtz8, OpBitLen8, OpPopCount8:
  1499  		lim = lim.unsignedMax(uint64(v.Args[0].Type.Size() * 8))
  1500  
  1501  	// bool to uint8 conversion
  1502  	case OpCvtBoolToUint8:
  1503  		lim = lim.unsignedMax(1)
  1504  
  1505  	// length operations
  1506  	case OpStringLen, OpSliceLen, OpSliceCap:
  1507  		lim = lim.signedMin(0)
  1508  	}
  1509  
  1510  	// signed <-> unsigned propagation
  1511  	if lim.min >= 0 {
  1512  		lim = lim.unsignedMinMax(uint64(lim.min), uint64(lim.max))
  1513  	}
  1514  	if fitsInBitsU(lim.umax, uint(8*v.Type.Size()-1)) {
  1515  		lim = lim.signedMinMax(int64(lim.umin), int64(lim.umax))
  1516  	}
  1517  
  1518  	return lim
  1519  }
  1520  
  1521  // flowLimit updates the known limits of v in ft. Returns true if anything changed.
  1522  // flowLimit can use the ranges of input arguments.
  1523  //
  1524  // Note: this calculation only happens at the point the value is defined. We do not reevaluate
  1525  // it later. So for example:
  1526  //
  1527  //	v := x + y
  1528  //	if 0 <= x && x < 5 && 0 <= y && y < 5 { ... use v ... }
  1529  //
  1530  // we don't discover that the range of v is bounded in the conditioned
  1531  // block. We could recompute the range of v once we enter the block so
  1532  // we know that it is 0 <= v <= 8, but we don't have a mechanism to do
  1533  // that right now.
  1534  func (ft *factsTable) flowLimit(v *Value) bool {
  1535  	if !v.Type.IsInteger() {
  1536  		// TODO: boolean?
  1537  		return false
  1538  	}
  1539  
  1540  	// Additional limits based on opcode and argument.
  1541  	// No need to repeat things here already done in initLimit.
  1542  	switch v.Op {
  1543  
  1544  	// extensions
  1545  	case OpZeroExt8to64, OpZeroExt8to32, OpZeroExt8to16, OpZeroExt16to64, OpZeroExt16to32, OpZeroExt32to64:
  1546  		a := ft.limits[v.Args[0].ID]
  1547  		return ft.unsignedMinMax(v, a.umin, a.umax)
  1548  	case OpSignExt8to64, OpSignExt8to32, OpSignExt8to16, OpSignExt16to64, OpSignExt16to32, OpSignExt32to64:
  1549  		a := ft.limits[v.Args[0].ID]
  1550  		return ft.signedMinMax(v, a.min, a.max)
  1551  	case OpTrunc64to8, OpTrunc64to16, OpTrunc64to32, OpTrunc32to8, OpTrunc32to16, OpTrunc16to8:
  1552  		a := ft.limits[v.Args[0].ID]
  1553  		if a.umax <= 1<<(uint64(v.Type.Size())*8)-1 {
  1554  			return ft.unsignedMinMax(v, a.umin, a.umax)
  1555  		}
  1556  
  1557  	// math/bits
  1558  	case OpCtz64:
  1559  		a := ft.limits[v.Args[0].ID]
  1560  		if a.nonzero() {
  1561  			return ft.unsignedMax(v, uint64(bits.Len64(a.umax)-1))
  1562  		}
  1563  	case OpCtz32:
  1564  		a := ft.limits[v.Args[0].ID]
  1565  		if a.nonzero() {
  1566  			return ft.unsignedMax(v, uint64(bits.Len32(uint32(a.umax))-1))
  1567  		}
  1568  	case OpCtz16:
  1569  		a := ft.limits[v.Args[0].ID]
  1570  		if a.nonzero() {
  1571  			return ft.unsignedMax(v, uint64(bits.Len16(uint16(a.umax))-1))
  1572  		}
  1573  	case OpCtz8:
  1574  		a := ft.limits[v.Args[0].ID]
  1575  		if a.nonzero() {
  1576  			return ft.unsignedMax(v, uint64(bits.Len8(uint8(a.umax))-1))
  1577  		}
  1578  
  1579  	case OpPopCount64, OpPopCount32, OpPopCount16, OpPopCount8:
  1580  		a := ft.limits[v.Args[0].ID]
  1581  		changingBitsCount := uint64(bits.Len64(a.umax ^ a.umin))
  1582  		sharedLeadingMask := ^(uint64(1)<<changingBitsCount - 1)
  1583  		fixedBits := a.umax & sharedLeadingMask
  1584  		min := uint64(bits.OnesCount64(fixedBits))
  1585  		return ft.unsignedMinMax(v, min, min+changingBitsCount)
  1586  
  1587  	case OpBitLen64:
  1588  		a := ft.limits[v.Args[0].ID]
  1589  		return ft.unsignedMinMax(v,
  1590  			uint64(bits.Len64(a.umin)),
  1591  			uint64(bits.Len64(a.umax)))
  1592  	case OpBitLen32:
  1593  		a := ft.limits[v.Args[0].ID]
  1594  		return ft.unsignedMinMax(v,
  1595  			uint64(bits.Len32(uint32(a.umin))),
  1596  			uint64(bits.Len32(uint32(a.umax))))
  1597  	case OpBitLen16:
  1598  		a := ft.limits[v.Args[0].ID]
  1599  		return ft.unsignedMinMax(v,
  1600  			uint64(bits.Len16(uint16(a.umin))),
  1601  			uint64(bits.Len16(uint16(a.umax))))
  1602  	case OpBitLen8:
  1603  		a := ft.limits[v.Args[0].ID]
  1604  		return ft.unsignedMinMax(v,
  1605  			uint64(bits.Len8(uint8(a.umin))),
  1606  			uint64(bits.Len8(uint8(a.umax))))
  1607  
  1608  	// Masks.
  1609  
  1610  	// TODO: if y.umax and y.umin share a leading bit pattern, y also has that leading bit pattern.
  1611  	// we could compare the patterns of always set bits in a and b and learn more about minimum and maximum.
  1612  	// But I doubt this help any real world code.
  1613  	case OpAnd64, OpAnd32, OpAnd16, OpAnd8:
  1614  		// AND can only make the value smaller.
  1615  		a := ft.limits[v.Args[0].ID]
  1616  		b := ft.limits[v.Args[1].ID]
  1617  		return ft.unsignedMax(v, min(a.umax, b.umax))
  1618  	case OpOr64, OpOr32, OpOr16, OpOr8:
  1619  		// OR can only make the value bigger and can't flip bits proved to be zero in both inputs.
  1620  		a := ft.limits[v.Args[0].ID]
  1621  		b := ft.limits[v.Args[1].ID]
  1622  		return ft.unsignedMinMax(v,
  1623  			max(a.umin, b.umin),
  1624  			1<<bits.Len64(a.umax|b.umax)-1)
  1625  	case OpXor64, OpXor32, OpXor16, OpXor8:
  1626  		// XOR can't flip bits that are proved to be zero in both inputs.
  1627  		a := ft.limits[v.Args[0].ID]
  1628  		b := ft.limits[v.Args[1].ID]
  1629  		return ft.unsignedMax(v, 1<<bits.Len64(a.umax|b.umax)-1)
  1630  	case OpCom64, OpCom32, OpCom16, OpCom8:
  1631  		a := ft.limits[v.Args[0].ID]
  1632  		return ft.newLimit(v, a.com(uint(v.Type.Size())*8))
  1633  
  1634  	// Arithmetic.
  1635  	case OpAdd64, OpAdd32, OpAdd16, OpAdd8:
  1636  		a := ft.limits[v.Args[0].ID]
  1637  		b := ft.limits[v.Args[1].ID]
  1638  		return ft.newLimit(v, a.add(b, uint(v.Type.Size())*8))
  1639  	case OpSub64, OpSub32, OpSub16, OpSub8:
  1640  		a := ft.limits[v.Args[0].ID]
  1641  		b := ft.limits[v.Args[1].ID]
  1642  		sub := ft.newLimit(v, a.sub(b, uint(v.Type.Size())*8))
  1643  		mod := ft.detectSignedMod(v)
  1644  		return sub || mod
  1645  	case OpNeg64, OpNeg32, OpNeg16, OpNeg8:
  1646  		a := ft.limits[v.Args[0].ID]
  1647  		bitsize := uint(v.Type.Size()) * 8
  1648  		return ft.newLimit(v, a.com(bitsize).add(limit{min: 1, max: 1, umin: 1, umax: 1}, bitsize))
  1649  	case OpMul64, OpMul32, OpMul16, OpMul8:
  1650  		a := ft.limits[v.Args[0].ID]
  1651  		b := ft.limits[v.Args[1].ID]
  1652  		return ft.newLimit(v, a.mul(b, uint(v.Type.Size())*8))
  1653  	case OpLsh64x64, OpLsh64x32, OpLsh64x16, OpLsh64x8,
  1654  		OpLsh32x64, OpLsh32x32, OpLsh32x16, OpLsh32x8,
  1655  		OpLsh16x64, OpLsh16x32, OpLsh16x16, OpLsh16x8,
  1656  		OpLsh8x64, OpLsh8x32, OpLsh8x16, OpLsh8x8:
  1657  		a := ft.limits[v.Args[0].ID]
  1658  		b := ft.limits[v.Args[1].ID]
  1659  		bitsize := uint(v.Type.Size()) * 8
  1660  		return ft.newLimit(v, a.mul(b.exp2(bitsize), bitsize))
  1661  	case OpMod64, OpMod32, OpMod16, OpMod8:
  1662  		a := ft.limits[v.Args[0].ID]
  1663  		b := ft.limits[v.Args[1].ID]
  1664  		if !(a.nonnegative() && b.nonnegative()) {
  1665  			// TODO: we could handle signed limits but I didn't bother.
  1666  			break
  1667  		}
  1668  		fallthrough
  1669  	case OpMod64u, OpMod32u, OpMod16u, OpMod8u:
  1670  		a := ft.limits[v.Args[0].ID]
  1671  		b := ft.limits[v.Args[1].ID]
  1672  		// Underflow in the arithmetic below is ok, it gives to MaxUint64 which does nothing to the limit.
  1673  		return ft.unsignedMax(v, min(a.umax, b.umax-1))
  1674  	case OpDiv64, OpDiv32, OpDiv16, OpDiv8:
  1675  		a := ft.limits[v.Args[0].ID]
  1676  		b := ft.limits[v.Args[1].ID]
  1677  		if !(a.nonnegative() && b.nonnegative()) {
  1678  			// TODO: we could handle signed limits but I didn't bother.
  1679  			break
  1680  		}
  1681  		fallthrough
  1682  	case OpDiv64u, OpDiv32u, OpDiv16u, OpDiv8u:
  1683  		a := ft.limits[v.Args[0].ID]
  1684  		b := ft.limits[v.Args[1].ID]
  1685  		lim := noLimit
  1686  		if b.umax > 0 {
  1687  			lim = lim.unsignedMin(a.umin / b.umax)
  1688  		}
  1689  		if b.umin > 0 {
  1690  			lim = lim.unsignedMax(a.umax / b.umin)
  1691  		}
  1692  		return ft.newLimit(v, lim)
  1693  
  1694  	case OpPhi:
  1695  		{
  1696  			// Work around for go.dev/issue/68857, look for min(x, y) and max(x, y).
  1697  			b := v.Block
  1698  			if len(b.Preds) != 2 {
  1699  				goto notMinNorMax
  1700  			}
  1701  			// FIXME: this code searches for the following losange pattern
  1702  			// because that what ssagen produce for min and max builtins:
  1703  			// conditionBlock → (firstBlock, secondBlock) → v.Block
  1704  			// there are three non losange equivalent constructions
  1705  			// we could match for, but I didn't bother:
  1706  			// conditionBlock → (v.Block, secondBlock → v.Block)
  1707  			// conditionBlock → (firstBlock → v.Block, v.Block)
  1708  			// conditionBlock → (v.Block, v.Block)
  1709  			firstBlock, secondBlock := b.Preds[0].b, b.Preds[1].b
  1710  			if firstBlock.Kind != BlockPlain || secondBlock.Kind != BlockPlain {
  1711  				goto notMinNorMax
  1712  			}
  1713  			if len(firstBlock.Preds) != 1 || len(secondBlock.Preds) != 1 {
  1714  				goto notMinNorMax
  1715  			}
  1716  			conditionBlock := firstBlock.Preds[0].b
  1717  			if conditionBlock != secondBlock.Preds[0].b {
  1718  				goto notMinNorMax
  1719  			}
  1720  			if conditionBlock.Kind != BlockIf {
  1721  				goto notMinNorMax
  1722  			}
  1723  
  1724  			less := conditionBlock.Controls[0]
  1725  			var unsigned bool
  1726  			switch less.Op {
  1727  			case OpLess64U, OpLess32U, OpLess16U, OpLess8U,
  1728  				OpLeq64U, OpLeq32U, OpLeq16U, OpLeq8U:
  1729  				unsigned = true
  1730  			case OpLess64, OpLess32, OpLess16, OpLess8,
  1731  				OpLeq64, OpLeq32, OpLeq16, OpLeq8:
  1732  			default:
  1733  				goto notMinNorMax
  1734  			}
  1735  			small, big := less.Args[0], less.Args[1]
  1736  			truev, falsev := v.Args[0], v.Args[1]
  1737  			if conditionBlock.Succs[0].b == secondBlock {
  1738  				truev, falsev = falsev, truev
  1739  			}
  1740  
  1741  			bigl, smalll := ft.limits[big.ID], ft.limits[small.ID]
  1742  			if truev == big {
  1743  				if falsev == small {
  1744  					// v := big if small <¿=? big else small
  1745  					if unsigned {
  1746  						maximum := max(bigl.umax, smalll.umax)
  1747  						minimum := max(bigl.umin, smalll.umin)
  1748  						return ft.unsignedMinMax(v, minimum, maximum)
  1749  					} else {
  1750  						maximum := max(bigl.max, smalll.max)
  1751  						minimum := max(bigl.min, smalll.min)
  1752  						return ft.signedMinMax(v, minimum, maximum)
  1753  					}
  1754  				} else {
  1755  					goto notMinNorMax
  1756  				}
  1757  			} else if truev == small {
  1758  				if falsev == big {
  1759  					// v := small if small <¿=? big else big
  1760  					if unsigned {
  1761  						maximum := min(bigl.umax, smalll.umax)
  1762  						minimum := min(bigl.umin, smalll.umin)
  1763  						return ft.unsignedMinMax(v, minimum, maximum)
  1764  					} else {
  1765  						maximum := min(bigl.max, smalll.max)
  1766  						minimum := min(bigl.min, smalll.min)
  1767  						return ft.signedMinMax(v, minimum, maximum)
  1768  					}
  1769  				} else {
  1770  					goto notMinNorMax
  1771  				}
  1772  			} else {
  1773  				goto notMinNorMax
  1774  			}
  1775  		}
  1776  	notMinNorMax:
  1777  
  1778  		// Compute the union of all the input phis.
  1779  		// Often this will convey no information, because the block
  1780  		// is not dominated by its predecessors and hence the
  1781  		// phi arguments might not have been processed yet. But if
  1782  		// the values are declared earlier, it may help. e.g., for
  1783  		//    v = phi(c3, c5)
  1784  		// where c3 = OpConst [3] and c5 = OpConst [5] are
  1785  		// defined in the entry block, we can derive [3,5]
  1786  		// as the limit for v.
  1787  		l := ft.limits[v.Args[0].ID]
  1788  		for _, a := range v.Args[1:] {
  1789  			l2 := ft.limits[a.ID]
  1790  			l.min = min(l.min, l2.min)
  1791  			l.max = max(l.max, l2.max)
  1792  			l.umin = min(l.umin, l2.umin)
  1793  			l.umax = max(l.umax, l2.umax)
  1794  		}
  1795  		return ft.newLimit(v, l)
  1796  	}
  1797  	return false
  1798  }
  1799  
  1800  // See if we can get any facts because v is the result of signed mod by a constant.
  1801  // The mod operation has already been rewritten, so we have to try and reconstruct it.
  1802  //
  1803  //	x % d
  1804  //
  1805  // is rewritten as
  1806  //
  1807  //	x - (x / d) * d
  1808  //
  1809  // furthermore, the divide itself gets rewritten. If d is a power of 2 (d == 1<<k), we do
  1810  //
  1811  //	(x / d) * d = ((x + adj) >> k) << k
  1812  //	            = (x + adj) & (-1<<k)
  1813  //
  1814  // with adj being an adjustment in case x is negative (see below).
  1815  // if d is not a power of 2, we do
  1816  //
  1817  //	x / d = ... TODO ...
  1818  func (ft *factsTable) detectSignedMod(v *Value) bool {
  1819  	if ft.detectSignedModByPowerOfTwo(v) {
  1820  		return true
  1821  	}
  1822  	// TODO: non-powers-of-2
  1823  	return false
  1824  }
  1825  func (ft *factsTable) detectSignedModByPowerOfTwo(v *Value) bool {
  1826  	// We're looking for:
  1827  	//
  1828  	//   x % d ==
  1829  	//   x - (x / d) * d
  1830  	//
  1831  	// which for d a power of 2, d == 1<<k, is done as
  1832  	//
  1833  	//   x - ((x + (x>>(w-1))>>>(w-k)) & (-1<<k))
  1834  	//
  1835  	// w = bit width of x.
  1836  	// (>> = signed shift, >>> = unsigned shift).
  1837  	// See ./_gen/generic.rules, search for "Signed divide by power of 2".
  1838  
  1839  	var w int64
  1840  	var addOp, andOp, constOp, sshiftOp, ushiftOp Op
  1841  	switch v.Op {
  1842  	case OpSub64:
  1843  		w = 64
  1844  		addOp = OpAdd64
  1845  		andOp = OpAnd64
  1846  		constOp = OpConst64
  1847  		sshiftOp = OpRsh64x64
  1848  		ushiftOp = OpRsh64Ux64
  1849  	case OpSub32:
  1850  		w = 32
  1851  		addOp = OpAdd32
  1852  		andOp = OpAnd32
  1853  		constOp = OpConst32
  1854  		sshiftOp = OpRsh32x64
  1855  		ushiftOp = OpRsh32Ux64
  1856  	case OpSub16:
  1857  		w = 16
  1858  		addOp = OpAdd16
  1859  		andOp = OpAnd16
  1860  		constOp = OpConst16
  1861  		sshiftOp = OpRsh16x64
  1862  		ushiftOp = OpRsh16Ux64
  1863  	case OpSub8:
  1864  		w = 8
  1865  		addOp = OpAdd8
  1866  		andOp = OpAnd8
  1867  		constOp = OpConst8
  1868  		sshiftOp = OpRsh8x64
  1869  		ushiftOp = OpRsh8Ux64
  1870  	default:
  1871  		return false
  1872  	}
  1873  
  1874  	x := v.Args[0]
  1875  	and := v.Args[1]
  1876  	if and.Op != andOp {
  1877  		return false
  1878  	}
  1879  	var add, mask *Value
  1880  	if and.Args[0].Op == addOp && and.Args[1].Op == constOp {
  1881  		add = and.Args[0]
  1882  		mask = and.Args[1]
  1883  	} else if and.Args[1].Op == addOp && and.Args[0].Op == constOp {
  1884  		add = and.Args[1]
  1885  		mask = and.Args[0]
  1886  	} else {
  1887  		return false
  1888  	}
  1889  	var ushift *Value
  1890  	if add.Args[0] == x {
  1891  		ushift = add.Args[1]
  1892  	} else if add.Args[1] == x {
  1893  		ushift = add.Args[0]
  1894  	} else {
  1895  		return false
  1896  	}
  1897  	if ushift.Op != ushiftOp {
  1898  		return false
  1899  	}
  1900  	if ushift.Args[1].Op != OpConst64 {
  1901  		return false
  1902  	}
  1903  	k := w - ushift.Args[1].AuxInt // Now we know k!
  1904  	d := int64(1) << k             // divisor
  1905  	sshift := ushift.Args[0]
  1906  	if sshift.Op != sshiftOp {
  1907  		return false
  1908  	}
  1909  	if sshift.Args[0] != x {
  1910  		return false
  1911  	}
  1912  	if sshift.Args[1].Op != OpConst64 || sshift.Args[1].AuxInt != w-1 {
  1913  		return false
  1914  	}
  1915  	if mask.AuxInt != -d {
  1916  		return false
  1917  	}
  1918  
  1919  	// All looks ok. x % d is at most +/- d-1.
  1920  	return ft.signedMinMax(v, -d+1, d-1)
  1921  }
  1922  
  1923  // getBranch returns the range restrictions added by p
  1924  // when reaching b. p is the immediate dominator of b.
  1925  func getBranch(sdom SparseTree, p *Block, b *Block) branch {
  1926  	if p == nil {
  1927  		return unknown
  1928  	}
  1929  	switch p.Kind {
  1930  	case BlockIf:
  1931  		// If p and p.Succs[0] are dominators it means that every path
  1932  		// from entry to b passes through p and p.Succs[0]. We care that
  1933  		// no path from entry to b passes through p.Succs[1]. If p.Succs[0]
  1934  		// has one predecessor then (apart from the degenerate case),
  1935  		// there is no path from entry that can reach b through p.Succs[1].
  1936  		// TODO: how about p->yes->b->yes, i.e. a loop in yes.
  1937  		if sdom.IsAncestorEq(p.Succs[0].b, b) && len(p.Succs[0].b.Preds) == 1 {
  1938  			return positive
  1939  		}
  1940  		if sdom.IsAncestorEq(p.Succs[1].b, b) && len(p.Succs[1].b.Preds) == 1 {
  1941  			return negative
  1942  		}
  1943  	case BlockJumpTable:
  1944  		// TODO: this loop can lead to quadratic behavior, as
  1945  		// getBranch can be called len(p.Succs) times.
  1946  		for i, e := range p.Succs {
  1947  			if sdom.IsAncestorEq(e.b, b) && len(e.b.Preds) == 1 {
  1948  				return jumpTable0 + branch(i)
  1949  			}
  1950  		}
  1951  	}
  1952  	return unknown
  1953  }
  1954  
  1955  // addIndVarRestrictions updates the factsTables ft with the facts
  1956  // learned from the induction variable indVar which drives the loop
  1957  // starting in Block b.
  1958  func addIndVarRestrictions(ft *factsTable, b *Block, iv indVar) {
  1959  	d := signed
  1960  	if ft.isNonNegative(iv.min) && ft.isNonNegative(iv.max) {
  1961  		d |= unsigned
  1962  	}
  1963  
  1964  	if iv.flags&indVarMinExc == 0 {
  1965  		addRestrictions(b, ft, d, iv.min, iv.ind, lt|eq)
  1966  	} else {
  1967  		addRestrictions(b, ft, d, iv.min, iv.ind, lt)
  1968  	}
  1969  
  1970  	if iv.flags&indVarMaxInc == 0 {
  1971  		addRestrictions(b, ft, d, iv.ind, iv.max, lt)
  1972  	} else {
  1973  		addRestrictions(b, ft, d, iv.ind, iv.max, lt|eq)
  1974  	}
  1975  }
  1976  
  1977  // addBranchRestrictions updates the factsTables ft with the facts learned when
  1978  // branching from Block b in direction br.
  1979  func addBranchRestrictions(ft *factsTable, b *Block, br branch) {
  1980  	c := b.Controls[0]
  1981  	switch {
  1982  	case br == negative:
  1983  		ft.booleanFalse(c)
  1984  	case br == positive:
  1985  		ft.booleanTrue(c)
  1986  	case br >= jumpTable0:
  1987  		idx := br - jumpTable0
  1988  		val := int64(idx)
  1989  		if v, off := isConstDelta(c); v != nil {
  1990  			// Establish the bound on the underlying value we're switching on,
  1991  			// not on the offset-ed value used as the jump table index.
  1992  			c = v
  1993  			val -= off
  1994  		}
  1995  		ft.newLimit(c, limit{min: val, max: val, umin: uint64(val), umax: uint64(val)})
  1996  	default:
  1997  		panic("unknown branch")
  1998  	}
  1999  }
  2000  
  2001  // addRestrictions updates restrictions from the immediate
  2002  // dominating block (p) using r.
  2003  func addRestrictions(parent *Block, ft *factsTable, t domain, v, w *Value, r relation) {
  2004  	if t == 0 {
  2005  		// Trivial case: nothing to do.
  2006  		// Should not happen, but just in case.
  2007  		return
  2008  	}
  2009  	for i := domain(1); i <= t; i <<= 1 {
  2010  		if t&i == 0 {
  2011  			continue
  2012  		}
  2013  		ft.update(parent, v, w, i, r)
  2014  	}
  2015  }
  2016  
  2017  func addLocalFacts(ft *factsTable, b *Block) {
  2018  	// Propagate constant ranges among values in this block.
  2019  	// We do this before the second loop so that we have the
  2020  	// most up-to-date constant bounds for isNonNegative calls.
  2021  	for {
  2022  		changed := false
  2023  		for _, v := range b.Values {
  2024  			changed = ft.flowLimit(v) || changed
  2025  		}
  2026  		if !changed {
  2027  			break
  2028  		}
  2029  	}
  2030  
  2031  	// Add facts about individual operations.
  2032  	for _, v := range b.Values {
  2033  		// FIXME(go.dev/issue/68857): this loop only set up limits properly when b.Values is in topological order.
  2034  		// flowLimit can also depend on limits given by this loop which right now is not handled.
  2035  		switch v.Op {
  2036  		case OpAnd64, OpAnd32, OpAnd16, OpAnd8:
  2037  			ft.update(b, v, v.Args[0], unsigned, lt|eq)
  2038  			ft.update(b, v, v.Args[1], unsigned, lt|eq)
  2039  			if ft.isNonNegative(v.Args[0]) {
  2040  				ft.update(b, v, v.Args[0], signed, lt|eq)
  2041  			}
  2042  			if ft.isNonNegative(v.Args[1]) {
  2043  				ft.update(b, v, v.Args[1], signed, lt|eq)
  2044  			}
  2045  		case OpOr64, OpOr32, OpOr16, OpOr8:
  2046  			// TODO: investigate how to always add facts without much slowdown, see issue #57959
  2047  			//ft.update(b, v, v.Args[0], unsigned, gt|eq)
  2048  			//ft.update(b, v, v.Args[1], unsigned, gt|eq)
  2049  		case OpDiv64u, OpDiv32u, OpDiv16u, OpDiv8u,
  2050  			OpRsh8Ux64, OpRsh8Ux32, OpRsh8Ux16, OpRsh8Ux8,
  2051  			OpRsh16Ux64, OpRsh16Ux32, OpRsh16Ux16, OpRsh16Ux8,
  2052  			OpRsh32Ux64, OpRsh32Ux32, OpRsh32Ux16, OpRsh32Ux8,
  2053  			OpRsh64Ux64, OpRsh64Ux32, OpRsh64Ux16, OpRsh64Ux8:
  2054  			ft.update(b, v, v.Args[0], unsigned, lt|eq)
  2055  		case OpMod64u, OpMod32u, OpMod16u, OpMod8u:
  2056  			ft.update(b, v, v.Args[0], unsigned, lt|eq)
  2057  			// Note: we have to be careful that this doesn't imply
  2058  			// that the modulus is >0, which isn't true until *after*
  2059  			// the mod instruction executes (and thus panics if the
  2060  			// modulus is 0). See issue 67625.
  2061  			ft.update(b, v, v.Args[1], unsigned, lt)
  2062  		case OpSliceLen:
  2063  			if v.Args[0].Op == OpSliceMake {
  2064  				ft.update(b, v, v.Args[0].Args[1], signed, eq)
  2065  			}
  2066  		case OpSliceCap:
  2067  			if v.Args[0].Op == OpSliceMake {
  2068  				ft.update(b, v, v.Args[0].Args[2], signed, eq)
  2069  			}
  2070  		case OpPhi:
  2071  			addLocalFactsPhi(ft, v)
  2072  		}
  2073  	}
  2074  }
  2075  
  2076  func addLocalFactsPhi(ft *factsTable, v *Value) {
  2077  	// Look for phis that implement min/max.
  2078  	//   z:
  2079  	//      c = Less64 x y (or other Less/Leq operation)
  2080  	//      If c -> bx by
  2081  	//   bx: <- z
  2082  	//       -> b ...
  2083  	//   by: <- z
  2084  	//      -> b ...
  2085  	//   b: <- bx by
  2086  	//      v = Phi x y
  2087  	// Then v is either min or max of x,y.
  2088  	// If it is the min, then we deduce v <= x && v <= y.
  2089  	// If it is the max, then we deduce v >= x && v >= y.
  2090  	// The min case is useful for the copy builtin, see issue 16833.
  2091  	if len(v.Args) != 2 {
  2092  		return
  2093  	}
  2094  	b := v.Block
  2095  	x := v.Args[0]
  2096  	y := v.Args[1]
  2097  	bx := b.Preds[0].b
  2098  	by := b.Preds[1].b
  2099  	var z *Block // branch point
  2100  	switch {
  2101  	case bx == by: // bx == by == z case
  2102  		z = bx
  2103  	case by.uniquePred() == bx: // bx == z case
  2104  		z = bx
  2105  	case bx.uniquePred() == by: // by == z case
  2106  		z = by
  2107  	case bx.uniquePred() == by.uniquePred():
  2108  		z = bx.uniquePred()
  2109  	}
  2110  	if z == nil || z.Kind != BlockIf {
  2111  		return
  2112  	}
  2113  	c := z.Controls[0]
  2114  	if len(c.Args) != 2 {
  2115  		return
  2116  	}
  2117  	var isMin bool // if c, a less-than comparison, is true, phi chooses x.
  2118  	if bx == z {
  2119  		isMin = b.Preds[0].i == 0
  2120  	} else {
  2121  		isMin = bx.Preds[0].i == 0
  2122  	}
  2123  	if c.Args[0] == x && c.Args[1] == y {
  2124  		// ok
  2125  	} else if c.Args[0] == y && c.Args[1] == x {
  2126  		// Comparison is reversed from how the values are listed in the Phi.
  2127  		isMin = !isMin
  2128  	} else {
  2129  		// Not comparing x and y.
  2130  		return
  2131  	}
  2132  	var dom domain
  2133  	switch c.Op {
  2134  	case OpLess64, OpLess32, OpLess16, OpLess8, OpLeq64, OpLeq32, OpLeq16, OpLeq8:
  2135  		dom = signed
  2136  	case OpLess64U, OpLess32U, OpLess16U, OpLess8U, OpLeq64U, OpLeq32U, OpLeq16U, OpLeq8U:
  2137  		dom = unsigned
  2138  	default:
  2139  		return
  2140  	}
  2141  	var rel relation
  2142  	if isMin {
  2143  		rel = lt | eq
  2144  	} else {
  2145  		rel = gt | eq
  2146  	}
  2147  	ft.update(b, v, x, dom, rel)
  2148  	ft.update(b, v, y, dom, rel)
  2149  }
  2150  
  2151  var ctzNonZeroOp = map[Op]Op{OpCtz8: OpCtz8NonZero, OpCtz16: OpCtz16NonZero, OpCtz32: OpCtz32NonZero, OpCtz64: OpCtz64NonZero}
  2152  var mostNegativeDividend = map[Op]int64{
  2153  	OpDiv16: -1 << 15,
  2154  	OpMod16: -1 << 15,
  2155  	OpDiv32: -1 << 31,
  2156  	OpMod32: -1 << 31,
  2157  	OpDiv64: -1 << 63,
  2158  	OpMod64: -1 << 63}
  2159  
  2160  // simplifyBlock simplifies some constant values in b and evaluates
  2161  // branches to non-uniquely dominated successors of b.
  2162  func simplifyBlock(sdom SparseTree, ft *factsTable, b *Block) {
  2163  	for _, v := range b.Values {
  2164  		switch v.Op {
  2165  		case OpSlicemask:
  2166  			// Replace OpSlicemask operations in b with constants where possible.
  2167  			x, delta := isConstDelta(v.Args[0])
  2168  			if x == nil {
  2169  				break
  2170  			}
  2171  			// slicemask(x + y)
  2172  			// if x is larger than -y (y is negative), then slicemask is -1.
  2173  			lim := ft.limits[x.ID]
  2174  			if lim.umin > uint64(-delta) {
  2175  				if v.Args[0].Op == OpAdd64 {
  2176  					v.reset(OpConst64)
  2177  				} else {
  2178  					v.reset(OpConst32)
  2179  				}
  2180  				if b.Func.pass.debug > 0 {
  2181  					b.Func.Warnl(v.Pos, "Proved slicemask not needed")
  2182  				}
  2183  				v.AuxInt = -1
  2184  			}
  2185  		case OpCtz8, OpCtz16, OpCtz32, OpCtz64:
  2186  			// On some architectures, notably amd64, we can generate much better
  2187  			// code for CtzNN if we know that the argument is non-zero.
  2188  			// Capture that information here for use in arch-specific optimizations.
  2189  			x := v.Args[0]
  2190  			lim := ft.limits[x.ID]
  2191  			if lim.umin > 0 || lim.min > 0 || lim.max < 0 {
  2192  				if b.Func.pass.debug > 0 {
  2193  					b.Func.Warnl(v.Pos, "Proved %v non-zero", v.Op)
  2194  				}
  2195  				v.Op = ctzNonZeroOp[v.Op]
  2196  			}
  2197  		case OpRsh8x8, OpRsh8x16, OpRsh8x32, OpRsh8x64,
  2198  			OpRsh16x8, OpRsh16x16, OpRsh16x32, OpRsh16x64,
  2199  			OpRsh32x8, OpRsh32x16, OpRsh32x32, OpRsh32x64,
  2200  			OpRsh64x8, OpRsh64x16, OpRsh64x32, OpRsh64x64:
  2201  			// Check whether, for a >> b, we know that a is non-negative
  2202  			// and b is all of a's bits except the MSB. If so, a is shifted to zero.
  2203  			bits := 8 * v.Args[0].Type.Size()
  2204  			if v.Args[1].isGenericIntConst() && v.Args[1].AuxInt >= bits-1 && ft.isNonNegative(v.Args[0]) {
  2205  				if b.Func.pass.debug > 0 {
  2206  					b.Func.Warnl(v.Pos, "Proved %v shifts to zero", v.Op)
  2207  				}
  2208  				switch bits {
  2209  				case 64:
  2210  					v.reset(OpConst64)
  2211  				case 32:
  2212  					v.reset(OpConst32)
  2213  				case 16:
  2214  					v.reset(OpConst16)
  2215  				case 8:
  2216  					v.reset(OpConst8)
  2217  				default:
  2218  					panic("unexpected integer size")
  2219  				}
  2220  				v.AuxInt = 0
  2221  				break // Be sure not to fallthrough - this is no longer OpRsh.
  2222  			}
  2223  			// If the Rsh hasn't been replaced with 0, still check if it is bounded.
  2224  			fallthrough
  2225  		case OpLsh8x8, OpLsh8x16, OpLsh8x32, OpLsh8x64,
  2226  			OpLsh16x8, OpLsh16x16, OpLsh16x32, OpLsh16x64,
  2227  			OpLsh32x8, OpLsh32x16, OpLsh32x32, OpLsh32x64,
  2228  			OpLsh64x8, OpLsh64x16, OpLsh64x32, OpLsh64x64,
  2229  			OpRsh8Ux8, OpRsh8Ux16, OpRsh8Ux32, OpRsh8Ux64,
  2230  			OpRsh16Ux8, OpRsh16Ux16, OpRsh16Ux32, OpRsh16Ux64,
  2231  			OpRsh32Ux8, OpRsh32Ux16, OpRsh32Ux32, OpRsh32Ux64,
  2232  			OpRsh64Ux8, OpRsh64Ux16, OpRsh64Ux32, OpRsh64Ux64:
  2233  			// Check whether, for a << b, we know that b
  2234  			// is strictly less than the number of bits in a.
  2235  			by := v.Args[1]
  2236  			lim := ft.limits[by.ID]
  2237  			bits := 8 * v.Args[0].Type.Size()
  2238  			if lim.umax < uint64(bits) || (lim.max < bits && ft.isNonNegative(by)) {
  2239  				v.AuxInt = 1 // see shiftIsBounded
  2240  				if b.Func.pass.debug > 0 && !by.isGenericIntConst() {
  2241  					b.Func.Warnl(v.Pos, "Proved %v bounded", v.Op)
  2242  				}
  2243  			}
  2244  		case OpDiv16, OpDiv32, OpDiv64, OpMod16, OpMod32, OpMod64:
  2245  			// On amd64 and 386 fix-up code can be avoided if we know
  2246  			//  the divisor is not -1 or the dividend > MinIntNN.
  2247  			// Don't modify AuxInt on other architectures,
  2248  			// as that can interfere with CSE.
  2249  			// TODO: add other architectures?
  2250  			if b.Func.Config.arch != "386" && b.Func.Config.arch != "amd64" {
  2251  				break
  2252  			}
  2253  			divr := v.Args[1]
  2254  			divrLim := ft.limits[divr.ID]
  2255  			divd := v.Args[0]
  2256  			divdLim := ft.limits[divd.ID]
  2257  			if divrLim.max < -1 || divrLim.min > -1 || divdLim.min > mostNegativeDividend[v.Op] {
  2258  				// See DivisionNeedsFixUp in rewrite.go.
  2259  				// v.AuxInt = 1 means we have proved both that the divisor is not -1
  2260  				// and that the dividend is not the most negative integer,
  2261  				// so we do not need to add fix-up code.
  2262  				v.AuxInt = 1
  2263  				if b.Func.pass.debug > 0 {
  2264  					b.Func.Warnl(v.Pos, "Proved %v does not need fix-up", v.Op)
  2265  				}
  2266  			}
  2267  		}
  2268  		// Fold provable constant results.
  2269  		// Helps in cases where we reuse a value after branching on its equality.
  2270  		for i, arg := range v.Args {
  2271  			lim := ft.limits[arg.ID]
  2272  			var constValue int64
  2273  			switch {
  2274  			case lim.min == lim.max:
  2275  				constValue = lim.min
  2276  			case lim.umin == lim.umax:
  2277  				constValue = int64(lim.umin)
  2278  			default:
  2279  				continue
  2280  			}
  2281  			switch arg.Op {
  2282  			case OpConst64, OpConst32, OpConst16, OpConst8, OpConstBool, OpConstNil:
  2283  				continue
  2284  			}
  2285  			typ := arg.Type
  2286  			f := b.Func
  2287  			var c *Value
  2288  			switch {
  2289  			case typ.IsBoolean():
  2290  				c = f.ConstBool(typ, constValue != 0)
  2291  			case typ.IsInteger() && typ.Size() == 1:
  2292  				c = f.ConstInt8(typ, int8(constValue))
  2293  			case typ.IsInteger() && typ.Size() == 2:
  2294  				c = f.ConstInt16(typ, int16(constValue))
  2295  			case typ.IsInteger() && typ.Size() == 4:
  2296  				c = f.ConstInt32(typ, int32(constValue))
  2297  			case typ.IsInteger() && typ.Size() == 8:
  2298  				c = f.ConstInt64(typ, constValue)
  2299  			case typ.IsPtrShaped():
  2300  				if constValue == 0 {
  2301  					c = f.ConstNil(typ)
  2302  				} else {
  2303  					// Not sure how this might happen, but if it
  2304  					// does, just skip it.
  2305  					continue
  2306  				}
  2307  			default:
  2308  				// Not sure how this might happen, but if it
  2309  				// does, just skip it.
  2310  				continue
  2311  			}
  2312  			v.SetArg(i, c)
  2313  			ft.initLimitForNewValue(c)
  2314  			if b.Func.pass.debug > 1 {
  2315  				b.Func.Warnl(v.Pos, "Proved %v's arg %d (%v) is constant %d", v, i, arg, constValue)
  2316  			}
  2317  		}
  2318  	}
  2319  
  2320  	if b.Kind != BlockIf {
  2321  		return
  2322  	}
  2323  
  2324  	// Consider outgoing edges from this block.
  2325  	parent := b
  2326  	for i, branch := range [...]branch{positive, negative} {
  2327  		child := parent.Succs[i].b
  2328  		if getBranch(sdom, parent, child) != unknown {
  2329  			// For edges to uniquely dominated blocks, we
  2330  			// already did this when we visited the child.
  2331  			continue
  2332  		}
  2333  		// For edges to other blocks, this can trim a branch
  2334  		// even if we couldn't get rid of the child itself.
  2335  		ft.checkpoint()
  2336  		addBranchRestrictions(ft, parent, branch)
  2337  		unsat := ft.unsat
  2338  		ft.restore()
  2339  		if unsat {
  2340  			// This branch is impossible, so remove it
  2341  			// from the block.
  2342  			removeBranch(parent, branch)
  2343  			// No point in considering the other branch.
  2344  			// (It *is* possible for both to be
  2345  			// unsatisfiable since the fact table is
  2346  			// incomplete. We could turn this into a
  2347  			// BlockExit, but it doesn't seem worth it.)
  2348  			break
  2349  		}
  2350  	}
  2351  }
  2352  
  2353  func removeBranch(b *Block, branch branch) {
  2354  	c := b.Controls[0]
  2355  	if b.Func.pass.debug > 0 {
  2356  		verb := "Proved"
  2357  		if branch == positive {
  2358  			verb = "Disproved"
  2359  		}
  2360  		if b.Func.pass.debug > 1 {
  2361  			b.Func.Warnl(b.Pos, "%s %s (%s)", verb, c.Op, c)
  2362  		} else {
  2363  			b.Func.Warnl(b.Pos, "%s %s", verb, c.Op)
  2364  		}
  2365  	}
  2366  	if c != nil && c.Pos.IsStmt() == src.PosIsStmt && c.Pos.SameFileAndLine(b.Pos) {
  2367  		// attempt to preserve statement marker.
  2368  		b.Pos = b.Pos.WithIsStmt()
  2369  	}
  2370  	if branch == positive || branch == negative {
  2371  		b.Kind = BlockFirst
  2372  		b.ResetControls()
  2373  		if branch == positive {
  2374  			b.swapSuccessors()
  2375  		}
  2376  	} else {
  2377  		// TODO: figure out how to remove an entry from a jump table
  2378  	}
  2379  }
  2380  
  2381  // isConstDelta returns non-nil if v is equivalent to w+delta (signed).
  2382  func isConstDelta(v *Value) (w *Value, delta int64) {
  2383  	cop := OpConst64
  2384  	switch v.Op {
  2385  	case OpAdd32, OpSub32:
  2386  		cop = OpConst32
  2387  	case OpAdd16, OpSub16:
  2388  		cop = OpConst16
  2389  	case OpAdd8, OpSub8:
  2390  		cop = OpConst8
  2391  	}
  2392  	switch v.Op {
  2393  	case OpAdd64, OpAdd32, OpAdd16, OpAdd8:
  2394  		if v.Args[0].Op == cop {
  2395  			return v.Args[1], v.Args[0].AuxInt
  2396  		}
  2397  		if v.Args[1].Op == cop {
  2398  			return v.Args[0], v.Args[1].AuxInt
  2399  		}
  2400  	case OpSub64, OpSub32, OpSub16, OpSub8:
  2401  		if v.Args[1].Op == cop {
  2402  			aux := v.Args[1].AuxInt
  2403  			if aux != -aux { // Overflow; too bad
  2404  				return v.Args[0], -aux
  2405  			}
  2406  		}
  2407  	}
  2408  	return nil, 0
  2409  }
  2410  
  2411  // isCleanExt reports whether v is the result of a value-preserving
  2412  // sign or zero extension.
  2413  func isCleanExt(v *Value) bool {
  2414  	switch v.Op {
  2415  	case OpSignExt8to16, OpSignExt8to32, OpSignExt8to64,
  2416  		OpSignExt16to32, OpSignExt16to64, OpSignExt32to64:
  2417  		// signed -> signed is the only value-preserving sign extension
  2418  		return v.Args[0].Type.IsSigned() && v.Type.IsSigned()
  2419  
  2420  	case OpZeroExt8to16, OpZeroExt8to32, OpZeroExt8to64,
  2421  		OpZeroExt16to32, OpZeroExt16to64, OpZeroExt32to64:
  2422  		// unsigned -> signed/unsigned are value-preserving zero extensions
  2423  		return !v.Args[0].Type.IsSigned()
  2424  	}
  2425  	return false
  2426  }
  2427  

View as plain text