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

View as plain text