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

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

View as plain text