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

View as plain text