prove.go

Documentation: cmd/compile/internal/ssa

     1  // Copyright 2016 The Go Authors. All rights reserved.
     2  // Use of this source code is governed by a BSD-style
     3  // license that can be found in the LICENSE file.
     4  
     5  package ssa
     6  
     7  import (
     8  	"fmt"
     9  	"math"
    10  )
    11  
    12  type branch int
    13  
    14  const (
    15  	unknown branch = iota
    16  	positive
    17  	negative
    18  )
    19  
    20  // relation represents the set of possible relations between
    21  // pairs of variables (v, w). Without a priori knowledge the
    22  // mask is lt | eq | gt meaning v can be less than, equal to or
    23  // greater than w. When the execution path branches on the condition
    24  // `v op w` the set of relations is updated to exclude any
    25  // relation not possible due to `v op w` being true (or false).
    26  //
    27  // E.g.
    28  //
    29  // r := relation(...)
    30  //
    31  // if v < w {
    32  //   newR := r & lt
    33  // }
    34  // if v >= w {
    35  //   newR := r & (eq|gt)
    36  // }
    37  // if v != w {
    38  //   newR := r & (lt|gt)
    39  // }
    40  type relation uint
    41  
    42  const (
    43  	lt relation = 1 << iota
    44  	eq
    45  	gt
    46  )
    47  
    48  var relationStrings = [...]string{
    49  	0: "none", lt: "<", eq: "==", lt | eq: "<=",
    50  	gt: ">", gt | lt: "!=", gt | eq: ">=", gt | eq | lt: "any",
    51  }
    52  
    53  func (r relation) String() string {
    54  	if r < relation(len(relationStrings)) {
    55  		return relationStrings[r]
    56  	}
    57  	return fmt.Sprintf("relation(%d)", uint(r))
    58  }
    59  
    60  // domain represents the domain of a variable pair in which a set
    61  // of relations is known. For example, relations learned for unsigned
    62  // pairs cannot be transferred to signed pairs because the same bit
    63  // representation can mean something else.
    64  type domain uint
    65  
    66  const (
    67  	signed domain = 1 << iota
    68  	unsigned
    69  	pointer
    70  	boolean
    71  )
    72  
    73  var domainStrings = [...]string{
    74  	"signed", "unsigned", "pointer", "boolean",
    75  }
    76  
    77  func (d domain) String() string {
    78  	s := ""
    79  	for i, ds := range domainStrings {
    80  		if d&(1<<uint(i)) != 0 {
    81  			if len(s) != 0 {
    82  				s += "|"
    83  			}
    84  			s += ds
    85  			d &^= 1 << uint(i)
    86  		}
    87  	}
    88  	if d != 0 {
    89  		if len(s) != 0 {
    90  			s += "|"
    91  		}
    92  		s += fmt.Sprintf("0x%x", uint(d))
    93  	}
    94  	return s
    95  }
    96  
    97  type pair struct {
    98  	v, w *Value // a pair of values, ordered by ID.
    99  	// v can be nil, to mean the zero value.
   100  	// for booleans the zero value (v == nil) is false.
   101  	d domain
   102  }
   103  
   104  // fact is a pair plus a relation for that pair.
   105  type fact struct {
   106  	p pair
   107  	r relation
   108  }
   109  
   110  // a limit records known upper and lower bounds for a value.
   111  type limit struct {
   112  	min, max   int64  // min <= value <= max, signed
   113  	umin, umax uint64 // umin <= value <= umax, unsigned
   114  }
   115  
   116  func (l limit) String() string {
   117  	return fmt.Sprintf("sm,SM,um,UM=%d,%d,%d,%d", l.min, l.max, l.umin, l.umax)
   118  }
   119  
   120  func (l limit) intersect(l2 limit) limit {
   121  	if l.min < l2.min {
   122  		l.min = l2.min
   123  	}
   124  	if l.umin < l2.umin {
   125  		l.umin = l2.umin
   126  	}
   127  	if l.max > l2.max {
   128  		l.max = l2.max
   129  	}
   130  	if l.umax > l2.umax {
   131  		l.umax = l2.umax
   132  	}
   133  	return l
   134  }
   135  
   136  var noLimit = limit{math.MinInt64, math.MaxInt64, 0, math.MaxUint64}
   137  
   138  // a limitFact is a limit known for a particular value.
   139  type limitFact struct {
   140  	vid   ID
   141  	limit limit
   142  }
   143  
   144  // factsTable keeps track of relations between pairs of values.
   145  //
   146  // The fact table logic is sound, but incomplete. Outside of a few
   147  // special cases, it performs no deduction or arithmetic. While there
   148  // are known decision procedures for this, the ad hoc approach taken
   149  // by the facts table is effective for real code while remaining very
   150  // efficient.
   151  type factsTable struct {
   152  	// unsat is true if facts contains a contradiction.
   153  	//
   154  	// Note that the factsTable logic is incomplete, so if unsat
   155  	// is false, the assertions in factsTable could be satisfiable
   156  	// *or* unsatisfiable.
   157  	unsat      bool // true if facts contains a contradiction
   158  	unsatDepth int  // number of unsat checkpoints
   159  
   160  	facts map[pair]relation // current known set of relation
   161  	stack []fact            // previous sets of relations
   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  	order [2]*poset
   167  
   168  	// known lower and upper bounds on individual values.
   169  	limits     map[ID]limit
   170  	limitStack []limitFact // previous entries
   171  
   172  	// For each slice s, a map from s to a len(s)/cap(s) value (if any)
   173  	// TODO: check if there are cases that matter where we have
   174  	// more than one len(s) for a slice. We could keep a list if necessary.
   175  	lens map[ID]*Value
   176  	caps map[ID]*Value
   177  }
   178  
   179  // checkpointFact is an invalid value used for checkpointing
   180  // and restoring factsTable.
   181  var checkpointFact = fact{}
   182  var checkpointBound = limitFact{}
   183  
   184  func newFactsTable(f *Func) *factsTable {
   185  	ft := &factsTable{}
   186  	ft.order[0] = f.newPoset() // signed
   187  	ft.order[1] = f.newPoset() // unsigned
   188  	ft.order[0].SetUnsigned(false)
   189  	ft.order[1].SetUnsigned(true)
   190  	ft.facts = make(map[pair]relation)
   191  	ft.stack = make([]fact, 4)
   192  	ft.limits = make(map[ID]limit)
   193  	ft.limitStack = make([]limitFact, 4)
   194  	return ft
   195  }
   196  
   197  // update updates the set of relations between v and w in domain d
   198  // restricting it to r.
   199  func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {
   200  	if parent.Func.pass.debug > 2 {
   201  		parent.Func.Warnl(parent.Pos, "parent=%s, update %s %s %s", parent, v, w, r)
   202  	}
   203  	// No need to do anything else if we already found unsat.
   204  	if ft.unsat {
   205  		return
   206  	}
   207  
   208  	// Self-fact. It's wasteful to register it into the facts
   209  	// table, so just note whether it's satisfiable
   210  	if v == w {
   211  		if r&eq == 0 {
   212  			ft.unsat = true
   213  		}
   214  		return
   215  	}
   216  
   217  	if d == signed || d == unsigned {
   218  		var ok bool
   219  		idx := 0
   220  		if d == unsigned {
   221  			idx = 1
   222  		}
   223  		switch r {
   224  		case lt:
   225  			ok = ft.order[idx].SetOrder(v, w)
   226  		case gt:
   227  			ok = ft.order[idx].SetOrder(w, v)
   228  		case lt | eq:
   229  			ok = ft.order[idx].SetOrderOrEqual(v, w)
   230  		case gt | eq:
   231  			ok = ft.order[idx].SetOrderOrEqual(w, v)
   232  		case eq:
   233  			ok = ft.order[idx].SetEqual(v, w)
   234  		case lt | gt:
   235  			ok = ft.order[idx].SetNonEqual(v, w)
   236  		default:
   237  			panic("unknown relation")
   238  		}
   239  		if !ok {
   240  			if parent.Func.pass.debug > 2 {
   241  				parent.Func.Warnl(parent.Pos, "unsat %s %s %s", v, w, r)
   242  			}
   243  			ft.unsat = true
   244  			return
   245  		}
   246  	} else {
   247  		if lessByID(w, v) {
   248  			v, w = w, v
   249  			r = reverseBits[r]
   250  		}
   251  
   252  		p := pair{v, w, d}
   253  		oldR, ok := ft.facts[p]
   254  		if !ok {
   255  			if v == w {
   256  				oldR = eq
   257  			} else {
   258  				oldR = lt | eq | gt
   259  			}
   260  		}
   261  		// No changes compared to information already in facts table.
   262  		if oldR == r {
   263  			return
   264  		}
   265  		ft.stack = append(ft.stack, fact{p, oldR})
   266  		ft.facts[p] = oldR & r
   267  		// If this relation is not satisfiable, mark it and exit right away
   268  		if oldR&r == 0 {
   269  			if parent.Func.pass.debug > 2 {
   270  				parent.Func.Warnl(parent.Pos, "unsat %s %s %s", v, w, r)
   271  			}
   272  			ft.unsat = true
   273  			return
   274  		}
   275  	}
   276  
   277  	// Extract bounds when comparing against constants
   278  	if v.isGenericIntConst() {
   279  		v, w = w, v
   280  		r = reverseBits[r]
   281  	}
   282  	if v != nil && w.isGenericIntConst() {
   283  		// Note: all the +1/-1 below could overflow/underflow. Either will
   284  		// still generate correct results, it will just lead to imprecision.
   285  		// In fact if there is overflow/underflow, the corresponding
   286  		// code is unreachable because the known range is outside the range
   287  		// of the value's type.
   288  		old, ok := ft.limits[v.ID]
   289  		if !ok {
   290  			old = noLimit
   291  			if v.isGenericIntConst() {
   292  				switch d {
   293  				case signed:
   294  					old.min, old.max = v.AuxInt, v.AuxInt
   295  					if v.AuxInt >= 0 {
   296  						old.umin, old.umax = uint64(v.AuxInt), uint64(v.AuxInt)
   297  					}
   298  				case unsigned:
   299  					old.umin = v.AuxUnsigned()
   300  					old.umax = old.umin
   301  					if int64(old.umin) >= 0 {
   302  						old.min, old.max = int64(old.umin), int64(old.umin)
   303  					}
   304  				}
   305  			}
   306  		}
   307  		lim := noLimit
   308  		switch d {
   309  		case signed:
   310  			c := w.AuxInt
   311  			switch r {
   312  			case lt:
   313  				lim.max = c - 1
   314  			case lt | eq:
   315  				lim.max = c
   316  			case gt | eq:
   317  				lim.min = c
   318  			case gt:
   319  				lim.min = c + 1
   320  			case lt | gt:
   321  				lim = old
   322  				if c == lim.min {
   323  					lim.min++
   324  				}
   325  				if c == lim.max {
   326  					lim.max--
   327  				}
   328  			case eq:
   329  				lim.min = c
   330  				lim.max = c
   331  			}
   332  			if lim.min >= 0 {
   333  				// int(x) >= 0 && int(x) >= N  ⇒  uint(x) >= N
   334  				lim.umin = uint64(lim.min)
   335  			}
   336  			if lim.max != noLimit.max && old.min >= 0 && lim.max >= 0 {
   337  				// 0 <= int(x) <= N  ⇒  0 <= uint(x) <= N
   338  				// This is for a max update, so the lower bound
   339  				// comes from what we already know (old).
   340  				lim.umax = uint64(lim.max)
   341  			}
   342  		case unsigned:
   343  			uc := w.AuxUnsigned()
   344  			switch r {
   345  			case lt:
   346  				lim.umax = uc - 1
   347  			case lt | eq:
   348  				lim.umax = uc
   349  			case gt | eq:
   350  				lim.umin = uc
   351  			case gt:
   352  				lim.umin = uc + 1
   353  			case lt | gt:
   354  				lim = old
   355  				if uc == lim.umin {
   356  					lim.umin++
   357  				}
   358  				if uc == lim.umax {
   359  					lim.umax--
   360  				}
   361  			case eq:
   362  				lim.umin = uc
   363  				lim.umax = uc
   364  			}
   365  			// We could use the contrapositives of the
   366  			// signed implications to derive signed facts,
   367  			// but it turns out not to matter.
   368  		}
   369  		ft.limitStack = append(ft.limitStack, limitFact{v.ID, old})
   370  		lim = old.intersect(lim)
   371  		ft.limits[v.ID] = lim
   372  		if v.Block.Func.pass.debug > 2 {
   373  			v.Block.Func.Warnl(parent.Pos, "parent=%s, new limits %s %s %s %s", parent, v, w, r, lim.String())
   374  		}
   375  		if lim.min > lim.max || lim.umin > lim.umax {
   376  			ft.unsat = true
   377  			return
   378  		}
   379  	}
   380  
   381  	// Derived facts below here are only about numbers.
   382  	if d != signed && d != unsigned {
   383  		return
   384  	}
   385  
   386  	// Additional facts we know given the relationship between len and cap.
   387  	//
   388  	// TODO: Since prove now derives transitive relations, it
   389  	// should be sufficient to learn that len(w) <= cap(w) at the
   390  	// beginning of prove where we look for all len/cap ops.
   391  	if v.Op == OpSliceLen && r&lt == 0 && ft.caps[v.Args[0].ID] != nil {
   392  		// len(s) > w implies cap(s) > w
   393  		// len(s) >= w implies cap(s) >= w
   394  		// len(s) == w implies cap(s) >= w
   395  		ft.update(parent, ft.caps[v.Args[0].ID], w, d, r|gt)
   396  	}
   397  	if w.Op == OpSliceLen && r&gt == 0 && ft.caps[w.Args[0].ID] != nil {
   398  		// same, length on the RHS.
   399  		ft.update(parent, v, ft.caps[w.Args[0].ID], d, r|lt)
   400  	}
   401  	if v.Op == OpSliceCap && r&gt == 0 && ft.lens[v.Args[0].ID] != nil {
   402  		// cap(s) < w implies len(s) < w
   403  		// cap(s) <= w implies len(s) <= w
   404  		// cap(s) == w implies len(s) <= w
   405  		ft.update(parent, ft.lens[v.Args[0].ID], w, d, r|lt)
   406  	}
   407  	if w.Op == OpSliceCap && r&lt == 0 && ft.lens[w.Args[0].ID] != nil {
   408  		// same, capacity on the RHS.
   409  		ft.update(parent, v, ft.lens[w.Args[0].ID], d, r|gt)
   410  	}
   411  
   412  	// Process fence-post implications.
   413  	//
   414  	// First, make the condition > or >=.
   415  	if r == lt || r == lt|eq {
   416  		v, w = w, v
   417  		r = reverseBits[r]
   418  	}
   419  	switch r {
   420  	case gt:
   421  		if x, delta := isConstDelta(v); x != nil && delta == 1 {
   422  			// x+1 > w  ⇒  x >= w
   423  			//
   424  			// This is useful for eliminating the
   425  			// growslice branch of append.
   426  			ft.update(parent, x, w, d, gt|eq)
   427  		} else if x, delta := isConstDelta(w); x != nil && delta == -1 {
   428  			// v > x-1  ⇒  v >= x
   429  			ft.update(parent, v, x, d, gt|eq)
   430  		}
   431  	case gt | eq:
   432  		if x, delta := isConstDelta(v); x != nil && delta == -1 {
   433  			// x-1 >= w && x > min  ⇒  x > w
   434  			//
   435  			// Useful for i > 0; s[i-1].
   436  			lim, ok := ft.limits[x.ID]
   437  			if ok && ((d == signed && lim.min > opMin[v.Op]) || (d == unsigned && lim.umin > 0)) {
   438  				ft.update(parent, x, w, d, gt)
   439  			}
   440  		} else if x, delta := isConstDelta(w); x != nil && delta == 1 {
   441  			// v >= x+1 && x < max  ⇒  v > x
   442  			lim, ok := ft.limits[x.ID]
   443  			if ok && ((d == signed && lim.max < opMax[w.Op]) || (d == unsigned && lim.umax < opUMax[w.Op])) {
   444  				ft.update(parent, v, x, d, gt)
   445  			}
   446  		}
   447  	}
   448  
   449  	// Process: x+delta > w (with delta constant)
   450  	// Only signed domain for now (useful for accesses to slices in loops).
   451  	if r == gt || r == gt|eq {
   452  		if x, delta := isConstDelta(v); x != nil && d == signed {
   453  			if parent.Func.pass.debug > 1 {
   454  				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)
   455  			}
   456  			if !w.isGenericIntConst() {
   457  				// If we know that x+delta > w but w is not constant, we can derive:
   458  				//    if delta < 0 and x > MinInt - delta, then x > w (because x+delta cannot underflow)
   459  				// This is useful for loops with bounds "len(slice)-K" (delta = -K)
   460  				if l, has := ft.limits[x.ID]; has && delta < 0 {
   461  					if (x.Type.Size() == 8 && l.min >= math.MinInt64-delta) ||
   462  						(x.Type.Size() == 4 && l.min >= math.MinInt32-delta) {
   463  						ft.update(parent, x, w, signed, r)
   464  					}
   465  				}
   466  			} else {
   467  				// With w,delta constants, we want to derive: x+delta > w  ⇒  x > w-delta
   468  				//
   469  				// We compute (using integers of the correct size):
   470  				//    min = w - delta
   471  				//    max = MaxInt - delta
   472  				//
   473  				// And we prove that:
   474  				//    if min<max: min < x AND x <= max
   475  				//    if min>max: min < x OR  x <= max
   476  				//
   477  				// This is always correct, even in case of overflow.
   478  				//
   479  				// If the initial fact is x+delta >= w instead, the derived conditions are:
   480  				//    if min<max: min <= x AND x <= max
   481  				//    if min>max: min <= x OR  x <= max
   482  				//
   483  				// Notice the conditions for max are still <=, as they handle overflows.
   484  				var min, max int64
   485  				var vmin, vmax *Value
   486  				switch x.Type.Size() {
   487  				case 8:
   488  					min = w.AuxInt - delta
   489  					max = int64(^uint64(0)>>1) - delta
   490  
   491  					vmin = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, min)
   492  					vmax = parent.NewValue0I(parent.Pos, OpConst64, parent.Func.Config.Types.Int64, max)
   493  
   494  				case 4:
   495  					min = int64(int32(w.AuxInt) - int32(delta))
   496  					max = int64(int32(^uint32(0)>>1) - int32(delta))
   497  
   498  					vmin = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, min)
   499  					vmax = parent.NewValue0I(parent.Pos, OpConst32, parent.Func.Config.Types.Int32, max)
   500  
   501  				default:
   502  					panic("unimplemented")
   503  				}
   504  
   505  				if min < max {
   506  					// Record that x > min and max >= x
   507  					ft.update(parent, x, vmin, d, r)
   508  					ft.update(parent, vmax, x, d, r|eq)
   509  				} else {
   510  					// We know that either x>min OR x<=max. factsTable cannot record OR conditions,
   511  					// so let's see if we can already prove that one of them is false, in which case
   512  					// the other must be true
   513  					if l, has := ft.limits[x.ID]; has {
   514  						if l.max <= min {
   515  							if r&eq == 0 || l.max < min {
   516  								// x>min (x>=min) is impossible, so it must be x<=max
   517  								ft.update(parent, vmax, x, d, r|eq)
   518  							}
   519  						} else if l.min > max {
   520  							// x<=max is impossible, so it must be x>min
   521  							ft.update(parent, x, vmin, d, r)
   522  						}
   523  					}
   524  				}
   525  			}
   526  		}
   527  	}
   528  
   529  }
   530  
   531  var opMin = map[Op]int64{
   532  	OpAdd64: math.MinInt64, OpSub64: math.MinInt64,
   533  	OpAdd32: math.MinInt32, OpSub32: math.MinInt32,
   534  }
   535  
   536  var opMax = map[Op]int64{
   537  	OpAdd64: math.MaxInt64, OpSub64: math.MaxInt64,
   538  	OpAdd32: math.MaxInt32, OpSub32: math.MaxInt32,
   539  }
   540  
   541  var opUMax = map[Op]uint64{
   542  	OpAdd64: math.MaxUint64, OpSub64: math.MaxUint64,
   543  	OpAdd32: math.MaxUint32, OpSub32: math.MaxUint32,
   544  }
   545  
   546  // isNonNegative reports whether v is known to be non-negative.
   547  func (ft *factsTable) isNonNegative(v *Value) bool {
   548  	if isNonNegative(v) {
   549  		return true
   550  	}
   551  
   552  	// Check if the recorded limits can prove that the value is positive
   553  	if l, has := ft.limits[v.ID]; has && (l.min >= 0 || l.umax <= math.MaxInt64) {
   554  		return true
   555  	}
   556  
   557  	// Check if v = x+delta, and we can use x's limits to prove that it's positive
   558  	if x, delta := isConstDelta(v); x != nil {
   559  		if l, has := ft.limits[x.ID]; has {
   560  			if delta > 0 && l.min >= -delta && l.max <= math.MaxInt64-delta {
   561  				return true
   562  			}
   563  			if delta < 0 && l.min >= -delta {
   564  				return true
   565  			}
   566  		}
   567  	}
   568  
   569  	return false
   570  }
   571  
   572  // checkpoint saves the current state of known relations.
   573  // Called when descending on a branch.
   574  func (ft *factsTable) checkpoint() {
   575  	if ft.unsat {
   576  		ft.unsatDepth++
   577  	}
   578  	ft.stack = append(ft.stack, checkpointFact)
   579  	ft.limitStack = append(ft.limitStack, checkpointBound)
   580  	ft.order[0].Checkpoint()
   581  	ft.order[1].Checkpoint()
   582  }
   583  
   584  // restore restores known relation to the state just
   585  // before the previous checkpoint.
   586  // Called when backing up on a branch.
   587  func (ft *factsTable) restore() {
   588  	if ft.unsatDepth > 0 {
   589  		ft.unsatDepth--
   590  	} else {
   591  		ft.unsat = false
   592  	}
   593  	for {
   594  		old := ft.stack[len(ft.stack)-1]
   595  		ft.stack = ft.stack[:len(ft.stack)-1]
   596  		if old == checkpointFact {
   597  			break
   598  		}
   599  		if old.r == lt|eq|gt {
   600  			delete(ft.facts, old.p)
   601  		} else {
   602  			ft.facts[old.p] = old.r
   603  		}
   604  	}
   605  	for {
   606  		old := ft.limitStack[len(ft.limitStack)-1]
   607  		ft.limitStack = ft.limitStack[:len(ft.limitStack)-1]
   608  		if old.vid == 0 { // checkpointBound
   609  			break
   610  		}
   611  		if old.limit == noLimit {
   612  			delete(ft.limits, old.vid)
   613  		} else {
   614  			ft.limits[old.vid] = old.limit
   615  		}
   616  	}
   617  	ft.order[0].Undo()
   618  	ft.order[1].Undo()
   619  }
   620  
   621  func lessByID(v, w *Value) bool {
   622  	if v == nil && w == nil {
   623  		// Should not happen, but just in case.
   624  		return false
   625  	}
   626  	if v == nil {
   627  		return true
   628  	}
   629  	return w != nil && v.ID < w.ID
   630  }
   631  
   632  var (
   633  	reverseBits = [...]relation{0, 4, 2, 6, 1, 5, 3, 7}
   634  
   635  	// maps what we learn when the positive branch is taken.
   636  	// For example:
   637  	//      OpLess8:   {signed, lt},
   638  	//	v1 = (OpLess8 v2 v3).
   639  	// If v1 branch is taken then we learn that the rangeMask
   640  	// can be at most lt.
   641  	domainRelationTable = map[Op]struct {
   642  		d domain
   643  		r relation
   644  	}{
   645  		OpEq8:   {signed | unsigned, eq},
   646  		OpEq16:  {signed | unsigned, eq},
   647  		OpEq32:  {signed | unsigned, eq},
   648  		OpEq64:  {signed | unsigned, eq},
   649  		OpEqPtr: {pointer, eq},
   650  
   651  		OpNeq8:   {signed | unsigned, lt | gt},
   652  		OpNeq16:  {signed | unsigned, lt | gt},
   653  		OpNeq32:  {signed | unsigned, lt | gt},
   654  		OpNeq64:  {signed | unsigned, lt | gt},
   655  		OpNeqPtr: {pointer, lt | gt},
   656  
   657  		OpLess8:   {signed, lt},
   658  		OpLess8U:  {unsigned, lt},
   659  		OpLess16:  {signed, lt},
   660  		OpLess16U: {unsigned, lt},
   661  		OpLess32:  {signed, lt},
   662  		OpLess32U: {unsigned, lt},
   663  		OpLess64:  {signed, lt},
   664  		OpLess64U: {unsigned, lt},
   665  
   666  		OpLeq8:   {signed, lt | eq},
   667  		OpLeq8U:  {unsigned, lt | eq},
   668  		OpLeq16:  {signed, lt | eq},
   669  		OpLeq16U: {unsigned, lt | eq},
   670  		OpLeq32:  {signed, lt | eq},
   671  		OpLeq32U: {unsigned, lt | eq},
   672  		OpLeq64:  {signed, lt | eq},
   673  		OpLeq64U: {unsigned, lt | eq},
   674  
   675  		OpGeq8:   {signed, eq | gt},
   676  		OpGeq8U:  {unsigned, eq | gt},
   677  		OpGeq16:  {signed, eq | gt},
   678  		OpGeq16U: {unsigned, eq | gt},
   679  		OpGeq32:  {signed, eq | gt},
   680  		OpGeq32U: {unsigned, eq | gt},
   681  		OpGeq64:  {signed, eq | gt},
   682  		OpGeq64U: {unsigned, eq | gt},
   683  
   684  		OpGreater8:   {signed, gt},
   685  		OpGreater8U:  {unsigned, gt},
   686  		OpGreater16:  {signed, gt},
   687  		OpGreater16U: {unsigned, gt},
   688  		OpGreater32:  {signed, gt},
   689  		OpGreater32U: {unsigned, gt},
   690  		OpGreater64:  {signed, gt},
   691  		OpGreater64U: {unsigned, gt},
   692  
   693  		// For these ops, the negative branch is different: we can only
   694  		// prove signed/GE (signed/GT) if we can prove that arg0 is non-negative.
   695  		// See the special case in addBranchRestrictions.
   696  		OpIsInBounds:      {signed | unsigned, lt},      // 0 <= arg0 < arg1
   697  		OpIsSliceInBounds: {signed | unsigned, lt | eq}, // 0 <= arg0 <= arg1
   698  	}
   699  )
   700  
   701  // prove removes redundant BlockIf branches that can be inferred
   702  // from previous dominating comparisons.
   703  //
   704  // By far, the most common redundant pair are generated by bounds checking.
   705  // For example for the code:
   706  //
   707  //    a[i] = 4
   708  //    foo(a[i])
   709  //
   710  // The compiler will generate the following code:
   711  //
   712  //    if i >= len(a) {
   713  //        panic("not in bounds")
   714  //    }
   715  //    a[i] = 4
   716  //    if i >= len(a) {
   717  //        panic("not in bounds")
   718  //    }
   719  //    foo(a[i])
   720  //
   721  // The second comparison i >= len(a) is clearly redundant because if the
   722  // else branch of the first comparison is executed, we already know that i < len(a).
   723  // The code for the second panic can be removed.
   724  //
   725  // prove works by finding contradictions and trimming branches whose
   726  // conditions are unsatisfiable given the branches leading up to them.
   727  // It tracks a "fact table" of branch conditions. For each branching
   728  // block, it asserts the branch conditions that uniquely dominate that
   729  // block, and then separately asserts the block's branch condition and
   730  // its negation. If either leads to a contradiction, it can trim that
   731  // successor.
   732  func prove(f *Func) {
   733  	ft := newFactsTable(f)
   734  	ft.checkpoint()
   735  
   736  	// Find length and capacity ops.
   737  	var zero *Value
   738  	for _, b := range f.Blocks {
   739  		for _, v := range b.Values {
   740  			// If we found a zero constant, save it (so we don't have
   741  			// to build one later).
   742  			if zero == nil && v.Op == OpConst64 && v.AuxInt == 0 {
   743  				zero = v
   744  			}
   745  			if v.Uses == 0 {
   746  				// We don't care about dead values.
   747  				// (There can be some that are CSEd but not removed yet.)
   748  				continue
   749  			}
   750  			switch v.Op {
   751  			case OpStringLen:
   752  				if zero == nil {
   753  					zero = b.NewValue0I(b.Pos, OpConst64, f.Config.Types.Int64, 0)
   754  				}
   755  				ft.update(b, v, zero, signed, gt|eq)
   756  			case OpSliceLen:
   757  				if ft.lens == nil {
   758  					ft.lens = map[ID]*Value{}
   759  				}
   760  				ft.lens[v.Args[0].ID] = v
   761  				if zero == nil {
   762  					zero = b.NewValue0I(b.Pos, OpConst64, f.Config.Types.Int64, 0)
   763  				}
   764  				ft.update(b, v, zero, signed, gt|eq)
   765  			case OpSliceCap:
   766  				if ft.caps == nil {
   767  					ft.caps = map[ID]*Value{}
   768  				}
   769  				ft.caps[v.Args[0].ID] = v
   770  				if zero == nil {
   771  					zero = b.NewValue0I(b.Pos, OpConst64, f.Config.Types.Int64, 0)
   772  				}
   773  				ft.update(b, v, zero, signed, gt|eq)
   774  			}
   775  		}
   776  	}
   777  
   778  	// Find induction variables. Currently, findIndVars
   779  	// is limited to one induction variable per block.
   780  	var indVars map[*Block]indVar
   781  	for _, v := range findIndVar(f) {
   782  		if indVars == nil {
   783  			indVars = make(map[*Block]indVar)
   784  		}
   785  		indVars[v.entry] = v
   786  	}
   787  
   788  	// current node state
   789  	type walkState int
   790  	const (
   791  		descend walkState = iota
   792  		simplify
   793  	)
   794  	// work maintains the DFS stack.
   795  	type bp struct {
   796  		block *Block    // current handled block
   797  		state walkState // what's to do
   798  	}
   799  	work := make([]bp, 0, 256)
   800  	work = append(work, bp{
   801  		block: f.Entry,
   802  		state: descend,
   803  	})
   804  
   805  	idom := f.Idom()
   806  	sdom := f.sdom()
   807  
   808  	// DFS on the dominator tree.
   809  	//
   810  	// For efficiency, we consider only the dominator tree rather
   811  	// than the entire flow graph. On the way down, we consider
   812  	// incoming branches and accumulate conditions that uniquely
   813  	// dominate the current block. If we discover a contradiction,
   814  	// we can eliminate the entire block and all of its children.
   815  	// On the way back up, we consider outgoing branches that
   816  	// haven't already been considered. This way we consider each
   817  	// branch condition only once.
   818  	for len(work) > 0 {
   819  		node := work[len(work)-1]
   820  		work = work[:len(work)-1]
   821  		parent := idom[node.block.ID]
   822  		branch := getBranch(sdom, parent, node.block)
   823  
   824  		switch node.state {
   825  		case descend:
   826  			ft.checkpoint()
   827  			if iv, ok := indVars[node.block]; ok {
   828  				addIndVarRestrictions(ft, parent, iv)
   829  			}
   830  
   831  			if branch != unknown {
   832  				addBranchRestrictions(ft, parent, branch)
   833  				if ft.unsat {
   834  					// node.block is unreachable.
   835  					// Remove it and don't visit
   836  					// its children.
   837  					removeBranch(parent, branch)
   838  					ft.restore()
   839  					break
   840  				}
   841  				// Otherwise, we can now commit to
   842  				// taking this branch. We'll restore
   843  				// ft when we unwind.
   844  			}
   845  
   846  			// Add inductive facts for phis in this block.
   847  			addLocalInductiveFacts(ft, node.block)
   848  
   849  			work = append(work, bp{
   850  				block: node.block,
   851  				state: simplify,
   852  			})
   853  			for s := sdom.Child(node.block); s != nil; s = sdom.Sibling(s) {
   854  				work = append(work, bp{
   855  					block: s,
   856  					state: descend,
   857  				})
   858  			}
   859  
   860  		case simplify:
   861  			simplifyBlock(sdom, ft, node.block)
   862  			ft.restore()
   863  		}
   864  	}
   865  
   866  	ft.restore()
   867  
   868  	// Return the posets to the free list
   869  	for _, po := range ft.order {
   870  		// Make sure it's empty as it should be. A non-empty poset
   871  		// might cause errors and miscompilations if reused.
   872  		if checkEnabled {
   873  			if err := po.CheckEmpty(); err != nil {
   874  				f.Fatalf("prove poset not empty after function %s: %v", f.Name, err)
   875  			}
   876  		}
   877  		f.retPoset(po)
   878  	}
   879  }
   880  
   881  // getBranch returns the range restrictions added by p
   882  // when reaching b. p is the immediate dominator of b.
   883  func getBranch(sdom SparseTree, p *Block, b *Block) branch {
   884  	if p == nil || p.Kind != BlockIf {
   885  		return unknown
   886  	}
   887  	// If p and p.Succs[0] are dominators it means that every path
   888  	// from entry to b passes through p and p.Succs[0]. We care that
   889  	// no path from entry to b passes through p.Succs[1]. If p.Succs[0]
   890  	// has one predecessor then (apart from the degenerate case),
   891  	// there is no path from entry that can reach b through p.Succs[1].
   892  	// TODO: how about p->yes->b->yes, i.e. a loop in yes.
   893  	if sdom.isAncestorEq(p.Succs[0].b, b) && len(p.Succs[0].b.Preds) == 1 {
   894  		return positive
   895  	}
   896  	if sdom.isAncestorEq(p.Succs[1].b, b) && len(p.Succs[1].b.Preds) == 1 {
   897  		return negative
   898  	}
   899  	return unknown
   900  }
   901  
   902  // addIndVarRestrictions updates the factsTables ft with the facts
   903  // learned from the induction variable indVar which drives the loop
   904  // starting in Block b.
   905  func addIndVarRestrictions(ft *factsTable, b *Block, iv indVar) {
   906  	d := signed
   907  	if isNonNegative(iv.min) && isNonNegative(iv.max) {
   908  		d |= unsigned
   909  	}
   910  
   911  	if iv.flags&indVarMinExc == 0 {
   912  		addRestrictions(b, ft, d, iv.min, iv.ind, lt|eq)
   913  	} else {
   914  		addRestrictions(b, ft, d, iv.min, iv.ind, lt)
   915  	}
   916  
   917  	if iv.flags&indVarMaxInc == 0 {
   918  		addRestrictions(b, ft, d, iv.ind, iv.max, lt)
   919  	} else {
   920  		addRestrictions(b, ft, d, iv.ind, iv.max, lt|eq)
   921  	}
   922  }
   923  
   924  // addBranchRestrictions updates the factsTables ft with the facts learned when
   925  // branching from Block b in direction br.
   926  func addBranchRestrictions(ft *factsTable, b *Block, br branch) {
   927  	c := b.Control
   928  	switch br {
   929  	case negative:
   930  		addRestrictions(b, ft, boolean, nil, c, eq)
   931  	case positive:
   932  		addRestrictions(b, ft, boolean, nil, c, lt|gt)
   933  	default:
   934  		panic("unknown branch")
   935  	}
   936  	if tr, has := domainRelationTable[b.Control.Op]; has {
   937  		// When we branched from parent we learned a new set of
   938  		// restrictions. Update the factsTable accordingly.
   939  		d := tr.d
   940  		if d == signed && ft.isNonNegative(c.Args[0]) && ft.isNonNegative(c.Args[1]) {
   941  			d |= unsigned
   942  		}
   943  		switch br {
   944  		case negative:
   945  			switch b.Control.Op { // Special cases
   946  			case OpIsInBounds, OpIsSliceInBounds:
   947  				// 0 <= a0 < a1 (or 0 <= a0 <= a1)
   948  				//
   949  				// On the positive branch, we learn a0 < a1,
   950  				// both signed and unsigned.
   951  				//
   952  				// On the negative branch, we learn (0 > a0 ||
   953  				// a0 >= a1). In the unsigned domain, this is
   954  				// simply a0 >= a1 (which is the reverse of the
   955  				// positive branch, so nothing surprising).
   956  				// But in the signed domain, we can't express the ||
   957  				// condition, so check if a0 is non-negative instead,
   958  				// to be able to learn something.
   959  				d = unsigned
   960  				if ft.isNonNegative(c.Args[0]) {
   961  					d |= signed
   962  				}
   963  			}
   964  			addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r^(lt|gt|eq))
   965  		case positive:
   966  			addRestrictions(b, ft, d, c.Args[0], c.Args[1], tr.r)
   967  		}
   968  	}
   969  }
   970  
   971  // addRestrictions updates restrictions from the immediate
   972  // dominating block (p) using r.
   973  func addRestrictions(parent *Block, ft *factsTable, t domain, v, w *Value, r relation) {
   974  	if t == 0 {
   975  		// Trivial case: nothing to do.
   976  		// Shoult not happen, but just in case.
   977  		return
   978  	}
   979  	for i := domain(1); i <= t; i <<= 1 {
   980  		if t&i == 0 {
   981  			continue
   982  		}
   983  		ft.update(parent, v, w, i, r)
   984  	}
   985  }
   986  
   987  // addLocalInductiveFacts adds inductive facts when visiting b, where
   988  // b is a join point in a loop. In contrast with findIndVar, this
   989  // depends on facts established for b, which is why it happens when
   990  // visiting b. addLocalInductiveFacts specifically targets the pattern
   991  // created by OFORUNTIL, which isn't detected by findIndVar.
   992  //
   993  // TODO: It would be nice to combine this with findIndVar.
   994  func addLocalInductiveFacts(ft *factsTable, b *Block) {
   995  	// This looks for a specific pattern of induction:
   996  	//
   997  	// 1. i1 = OpPhi(min, i2) in b
   998  	// 2. i2 = i1 + 1
   999  	// 3. i2 < max at exit from b.Preds[1]
  1000  	// 4. min < max
  1001  	//
  1002  	// If all of these conditions are true, then i1 < max and i1 >= min.
  1003  
  1004  	for _, i1 := range b.Values {
  1005  		if i1.Op != OpPhi {
  1006  			continue
  1007  		}
  1008  
  1009  		// Check for conditions 1 and 2. This is easy to do
  1010  		// and will throw out most phis.
  1011  		min, i2 := i1.Args[0], i1.Args[1]
  1012  		if i1q, delta := isConstDelta(i2); i1q != i1 || delta != 1 {
  1013  			continue
  1014  		}
  1015  
  1016  		// Try to prove condition 3. We can't just query the
  1017  		// fact table for this because we don't know what the
  1018  		// facts of b.Preds[1] are (in general, b.Preds[1] is
  1019  		// a loop-back edge, so we haven't even been there
  1020  		// yet). As a conservative approximation, we look for
  1021  		// this condition in the predecessor chain until we
  1022  		// hit a join point.
  1023  		uniquePred := func(b *Block) *Block {
  1024  			if len(b.Preds) == 1 {
  1025  				return b.Preds[0].b
  1026  			}
  1027  			return nil
  1028  		}
  1029  		pred, child := b.Preds[1].b, b
  1030  		for ; pred != nil; pred = uniquePred(pred) {
  1031  			if pred.Kind != BlockIf {
  1032  				continue
  1033  			}
  1034  
  1035  			br := unknown
  1036  			if pred.Succs[0].b == child {
  1037  				br = positive
  1038  			}
  1039  			if pred.Succs[1].b == child {
  1040  				if br != unknown {
  1041  					continue
  1042  				}
  1043  				br = negative
  1044  			}
  1045  
  1046  			tr, has := domainRelationTable[pred.Control.Op]
  1047  			if !has {
  1048  				continue
  1049  			}
  1050  			r := tr.r
  1051  			if br == negative {
  1052  				// Negative branch taken to reach b.
  1053  				// Complement the relations.
  1054  				r = (lt | eq | gt) ^ r
  1055  			}
  1056  
  1057  			// Check for i2 < max or max > i2.
  1058  			var max *Value
  1059  			if r == lt && pred.Control.Args[0] == i2 {
  1060  				max = pred.Control.Args[1]
  1061  			} else if r == gt && pred.Control.Args[1] == i2 {
  1062  				max = pred.Control.Args[0]
  1063  			} else {
  1064  				continue
  1065  			}
  1066  
  1067  			// Check condition 4 now that we have a
  1068  			// candidate max. For this we can query the
  1069  			// fact table. We "prove" min < max by showing
  1070  			// that min >= max is unsat. (This may simply
  1071  			// compare two constants; that's fine.)
  1072  			ft.checkpoint()
  1073  			ft.update(b, min, max, tr.d, gt|eq)
  1074  			proved := ft.unsat
  1075  			ft.restore()
  1076  
  1077  			if proved {
  1078  				// We know that min <= i1 < max.
  1079  				if b.Func.pass.debug > 0 {
  1080  					printIndVar(b, i1, min, max, 1, 0)
  1081  				}
  1082  				ft.update(b, min, i1, tr.d, lt|eq)
  1083  				ft.update(b, i1, max, tr.d, lt)
  1084  			}
  1085  		}
  1086  	}
  1087  }
  1088  
  1089  var ctzNonZeroOp = map[Op]Op{OpCtz8: OpCtz8NonZero, OpCtz16: OpCtz16NonZero, OpCtz32: OpCtz32NonZero, OpCtz64: OpCtz64NonZero}
  1090  var mostNegativeDividend = map[Op]int64{
  1091  	OpDiv16: -1 << 15,
  1092  	OpMod16: -1 << 15,
  1093  	OpDiv32: -1 << 31,
  1094  	OpMod32: -1 << 31,
  1095  	OpDiv64: -1 << 63,
  1096  	OpMod64: -1 << 63}
  1097  
  1098  // simplifyBlock simplifies some constant values in b and evaluates
  1099  // branches to non-uniquely dominated successors of b.
  1100  func simplifyBlock(sdom SparseTree, ft *factsTable, b *Block) {
  1101  	for _, v := range b.Values {
  1102  		switch v.Op {
  1103  		case OpSlicemask:
  1104  			// Replace OpSlicemask operations in b with constants where possible.
  1105  			x, delta := isConstDelta(v.Args[0])
  1106  			if x == nil {
  1107  				continue
  1108  			}
  1109  			// slicemask(x + y)
  1110  			// if x is larger than -y (y is negative), then slicemask is -1.
  1111  			lim, ok := ft.limits[x.ID]
  1112  			if !ok {
  1113  				continue
  1114  			}
  1115  			if lim.umin > uint64(-delta) {
  1116  				if v.Args[0].Op == OpAdd64 {
  1117  					v.reset(OpConst64)
  1118  				} else {
  1119  					v.reset(OpConst32)
  1120  				}
  1121  				if b.Func.pass.debug > 0 {
  1122  					b.Func.Warnl(v.Pos, "Proved slicemask not needed")
  1123  				}
  1124  				v.AuxInt = -1
  1125  			}
  1126  		case OpCtz8, OpCtz16, OpCtz32, OpCtz64:
  1127  			// On some architectures, notably amd64, we can generate much better
  1128  			// code for CtzNN if we know that the argument is non-zero.
  1129  			// Capture that information here for use in arch-specific optimizations.
  1130  			x := v.Args[0]
  1131  			lim, ok := ft.limits[x.ID]
  1132  			if !ok {
  1133  				continue
  1134  			}
  1135  			if lim.umin > 0 || lim.min > 0 || lim.max < 0 {
  1136  				if b.Func.pass.debug > 0 {
  1137  					b.Func.Warnl(v.Pos, "Proved %v non-zero", v.Op)
  1138  				}
  1139  				v.Op = ctzNonZeroOp[v.Op]
  1140  			}
  1141  
  1142  		case OpLsh8x8, OpLsh8x16, OpLsh8x32, OpLsh8x64,
  1143  			OpLsh16x8, OpLsh16x16, OpLsh16x32, OpLsh16x64,
  1144  			OpLsh32x8, OpLsh32x16, OpLsh32x32, OpLsh32x64,
  1145  			OpLsh64x8, OpLsh64x16, OpLsh64x32, OpLsh64x64,
  1146  			OpRsh8x8, OpRsh8x16, OpRsh8x32, OpRsh8x64,
  1147  			OpRsh16x8, OpRsh16x16, OpRsh16x32, OpRsh16x64,
  1148  			OpRsh32x8, OpRsh32x16, OpRsh32x32, OpRsh32x64,
  1149  			OpRsh64x8, OpRsh64x16, OpRsh64x32, OpRsh64x64,
  1150  			OpRsh8Ux8, OpRsh8Ux16, OpRsh8Ux32, OpRsh8Ux64,
  1151  			OpRsh16Ux8, OpRsh16Ux16, OpRsh16Ux32, OpRsh16Ux64,
  1152  			OpRsh32Ux8, OpRsh32Ux16, OpRsh32Ux32, OpRsh32Ux64,
  1153  			OpRsh64Ux8, OpRsh64Ux16, OpRsh64Ux32, OpRsh64Ux64:
  1154  			// Check whether, for a << b, we know that b
  1155  			// is strictly less than the number of bits in a.
  1156  			by := v.Args[1]
  1157  			lim, ok := ft.limits[by.ID]
  1158  			if !ok {
  1159  				continue
  1160  			}
  1161  			bits := 8 * v.Args[0].Type.Size()
  1162  			if lim.umax < uint64(bits) || (lim.max < bits && ft.isNonNegative(by)) {
  1163  				v.AuxInt = 1 // see shiftIsBounded
  1164  				if b.Func.pass.debug > 0 {
  1165  					b.Func.Warnl(v.Pos, "Proved %v bounded", v.Op)
  1166  				}
  1167  			}
  1168  		case OpDiv16, OpDiv32, OpDiv64, OpMod16, OpMod32, OpMod64:
  1169  			// On amd64 and 386 fix-up code can be avoided if we know
  1170  			//  the divisor is not -1 or the dividend > MinIntNN.
  1171  			divr := v.Args[1]
  1172  			divrLim, divrLimok := ft.limits[divr.ID]
  1173  			divd := v.Args[0]
  1174  			divdLim, divdLimok := ft.limits[divd.ID]
  1175  			if (divrLimok && (divrLim.max < -1 || divrLim.min > -1)) ||
  1176  				(divdLimok && divdLim.min > mostNegativeDividend[v.Op]) {
  1177  				v.AuxInt = 1 // see NeedsFixUp in genericOps - v.AuxInt = 0 means we have not proved
  1178  				// that the divisor is not -1 and the dividend is not the most negative,
  1179  				// so we need to add fix-up code.
  1180  				if b.Func.pass.debug > 0 {
  1181  					b.Func.Warnl(v.Pos, "Proved %v does not need fix-up", v.Op)
  1182  				}
  1183  			}
  1184  		}
  1185  	}
  1186  
  1187  	if b.Kind != BlockIf {
  1188  		return
  1189  	}
  1190  
  1191  	// Consider outgoing edges from this block.
  1192  	parent := b
  1193  	for i, branch := range [...]branch{positive, negative} {
  1194  		child := parent.Succs[i].b
  1195  		if getBranch(sdom, parent, child) != unknown {
  1196  			// For edges to uniquely dominated blocks, we
  1197  			// already did this when we visited the child.
  1198  			continue
  1199  		}
  1200  		// For edges to other blocks, this can trim a branch
  1201  		// even if we couldn't get rid of the child itself.
  1202  		ft.checkpoint()
  1203  		addBranchRestrictions(ft, parent, branch)
  1204  		unsat := ft.unsat
  1205  		ft.restore()
  1206  		if unsat {
  1207  			// This branch is impossible, so remove it
  1208  			// from the block.
  1209  			removeBranch(parent, branch)
  1210  			// No point in considering the other branch.
  1211  			// (It *is* possible for both to be
  1212  			// unsatisfiable since the fact table is
  1213  			// incomplete. We could turn this into a
  1214  			// BlockExit, but it doesn't seem worth it.)
  1215  			break
  1216  		}
  1217  	}
  1218  }
  1219  
  1220  func removeBranch(b *Block, branch branch) {
  1221  	if b.Func.pass.debug > 0 {
  1222  		verb := "Proved"
  1223  		if branch == positive {
  1224  			verb = "Disproved"
  1225  		}
  1226  		c := b.Control
  1227  		if b.Func.pass.debug > 1 {
  1228  			b.Func.Warnl(b.Pos, "%s %s (%s)", verb, c.Op, c)
  1229  		} else {
  1230  			b.Func.Warnl(b.Pos, "%s %s", verb, c.Op)
  1231  		}
  1232  	}
  1233  	b.Kind = BlockFirst
  1234  	b.SetControl(nil)
  1235  	if branch == positive {
  1236  		b.swapSuccessors()
  1237  	}
  1238  }
  1239  
  1240  // isNonNegative reports whether v is known to be greater or equal to zero.
  1241  func isNonNegative(v *Value) bool {
  1242  	switch v.Op {
  1243  	case OpConst64:
  1244  		return v.AuxInt >= 0
  1245  
  1246  	case OpConst32:
  1247  		return int32(v.AuxInt) >= 0
  1248  
  1249  	case OpStringLen, OpSliceLen, OpSliceCap,
  1250  		OpZeroExt8to64, OpZeroExt16to64, OpZeroExt32to64:
  1251  		return true
  1252  
  1253  	case OpRsh64Ux64:
  1254  		by := v.Args[1]
  1255  		return by.Op == OpConst64 && by.AuxInt > 0
  1256  
  1257  	case OpRsh64x64:
  1258  		return isNonNegative(v.Args[0])
  1259  	}
  1260  	return false
  1261  }
  1262  
  1263  // isConstDelta returns non-nil if v is equivalent to w+delta (signed).
  1264  func isConstDelta(v *Value) (w *Value, delta int64) {
  1265  	cop := OpConst64
  1266  	switch v.Op {
  1267  	case OpAdd32, OpSub32:
  1268  		cop = OpConst32
  1269  	}
  1270  	switch v.Op {
  1271  	case OpAdd64, OpAdd32:
  1272  		if v.Args[0].Op == cop {
  1273  			return v.Args[1], v.Args[0].AuxInt
  1274  		}
  1275  		if v.Args[1].Op == cop {
  1276  			return v.Args[0], v.Args[1].AuxInt
  1277  		}
  1278  	case OpSub64, OpSub32:
  1279  		if v.Args[1].Op == cop {
  1280  			aux := v.Args[1].AuxInt
  1281  			if aux != -aux { // Overflow; too bad
  1282  				return v.Args[0], -aux
  1283  			}
  1284  		}
  1285  	}
  1286  	return nil, 0
  1287  }
  1288
View as plain text