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

View as plain text