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  	"math/bits"
    11  
    12  	"cmd/compile/internal/ssa/ssaop"
    13  )
    14  
    15  // FitsInBitsU reports whether x fits in b bits (unsigned).
    16  func FitsInBitsU(x uint64, b uint) bool {
    17  	return x>>b == 0
    18  }
    19  
    20  // InitLimit sets initial constant limit for v.  This limit is based
    21  // only on the operation itself, not any of its input arguments. This
    22  // method is only used in two places, once when the prove pass startup
    23  // and the other when a new ssa value is created, both for init. (unlike
    24  // flowLimit, below, which computes additional constraints based on
    25  // ranges of opcode arguments).
    26  func InitLimit(v *Value) Limit {
    27  	if v.Type.IsBoolean() {
    28  		switch v.Op {
    29  		case ssaop.OpConstBool:
    30  			b := v.AuxInt
    31  			return Limit{Min: b, Max: b, Umin: uint64(b), Umax: uint64(b)}
    32  		default:
    33  			return Limit{Min: 0, Max: 1, Umin: 0, Umax: 1}
    34  		}
    35  	}
    36  	if v.Type.IsPtrShaped() { // These are the types that EqPtr/NeqPtr operate on, except uintptr.
    37  		switch v.Op {
    38  		case ssaop.OpConstNil:
    39  			return Limit{Min: 0, Max: 0, Umin: 0, Umax: 0}
    40  		case ssaop.OpAddr, ssaop.OpLocalAddr: // TODO: others?
    41  			l := NoLimit()
    42  			l.Umin = 1
    43  			return l
    44  		default:
    45  			return NoLimit()
    46  		}
    47  	}
    48  	if !v.Type.IsInteger() {
    49  		return NoLimit()
    50  	}
    51  
    52  	// Default limits based on type.
    53  	lim := NoLimitForBitsize(uint(v.Type.Size()) * 8)
    54  
    55  	// Tighter limits on some opcodes.
    56  	switch v.Op {
    57  	// constants
    58  	case ssaop.OpConst64:
    59  		lim = Limit{Min: v.AuxInt, Max: v.AuxInt, Umin: uint64(v.AuxInt), Umax: uint64(v.AuxInt)}
    60  	case ssaop.OpConst32:
    61  		lim = Limit{Min: v.AuxInt, Max: v.AuxInt, Umin: uint64(uint32(v.AuxInt)), Umax: uint64(uint32(v.AuxInt))}
    62  	case ssaop.OpConst16:
    63  		lim = Limit{Min: v.AuxInt, Max: v.AuxInt, Umin: uint64(uint16(v.AuxInt)), Umax: uint64(uint16(v.AuxInt))}
    64  	case ssaop.OpConst8:
    65  		lim = Limit{Min: v.AuxInt, Max: v.AuxInt, Umin: uint64(uint8(v.AuxInt)), Umax: uint64(uint8(v.AuxInt))}
    66  
    67  	// extensions
    68  	case ssaop.OpZeroExt8to64, ssaop.OpZeroExt8to32, ssaop.OpZeroExt8to16:
    69  		lim = lim.SignedMinMax(0, 1<<8-1)
    70  		lim = lim.UnsignedMax(1<<8 - 1)
    71  	case ssaop.OpZeroExt16to64, ssaop.OpZeroExt16to32:
    72  		lim = lim.SignedMinMax(0, 1<<16-1)
    73  		lim = lim.UnsignedMax(1<<16 - 1)
    74  	case ssaop.OpZeroExt32to64:
    75  		lim = lim.SignedMinMax(0, 1<<32-1)
    76  		lim = lim.UnsignedMax(1<<32 - 1)
    77  	case ssaop.OpSignExt8to64, ssaop.OpSignExt8to32, ssaop.OpSignExt8to16:
    78  		lim = lim.SignedMinMax(math.MinInt8, math.MaxInt8)
    79  	case ssaop.OpSignExt16to64, ssaop.OpSignExt16to32:
    80  		lim = lim.SignedMinMax(math.MinInt16, math.MaxInt16)
    81  	case ssaop.OpSignExt32to64:
    82  		lim = lim.SignedMinMax(math.MinInt32, math.MaxInt32)
    83  
    84  	// math/bits intrinsics
    85  	case ssaop.OpCtz64, ssaop.OpBitLen64, ssaop.OpPopCount64,
    86  		ssaop.OpCtz32, ssaop.OpBitLen32, ssaop.OpPopCount32,
    87  		ssaop.OpCtz16, ssaop.OpBitLen16, ssaop.OpPopCount16,
    88  		ssaop.OpCtz8, ssaop.OpBitLen8, ssaop.OpPopCount8:
    89  		lim = lim.UnsignedMax(uint64(v.Args[0].Type.Size() * 8))
    90  
    91  	// bool to uint8 conversion
    92  	case ssaop.OpCvtBoolToUint8:
    93  		lim = lim.UnsignedMax(1)
    94  
    95  	// length operations
    96  	case ssaop.OpSliceLen, ssaop.OpSliceCap:
    97  		f := v.Block.Func
    98  		elemSize := uint64(v.Args[0].Type.Elem().Size())
    99  		if elemSize > 0 {
   100  			heapSize := uint64(1)<<(uint64(f.Config.PtrSize)*8) - 1
   101  			maximumElementsFittingInHeap := heapSize / elemSize
   102  			lim = lim.UnsignedMax(maximumElementsFittingInHeap)
   103  		}
   104  		fallthrough
   105  	case ssaop.OpStringLen:
   106  		lim = lim.signedMin(0)
   107  	}
   108  
   109  	// signed <-> unsigned propagation
   110  	if lim.Min >= 0 {
   111  		lim = lim.UnsignedMinMax(uint64(lim.Min), uint64(lim.Max))
   112  	}
   113  	if FitsInBitsU(lim.Umax, uint(8*v.Type.Size()-1)) {
   114  		lim = lim.SignedMinMax(int64(lim.Umin), int64(lim.Umax))
   115  	}
   116  
   117  	return lim
   118  }
   119  
   120  // a Limit records known upper and lower bounds for a value.
   121  //
   122  // If we have min>max or umin>umax, then this Limit is
   123  // called "unsatisfiable". When we encounter such a Limit, we
   124  // know that any code for which that Limit applies is unreachable.
   125  // We don't particularly care how unsatisfiable limits propagate,
   126  // including becoming satisfiable, because any optimization
   127  // decisions based on those limits only apply to unreachable code.
   128  type Limit struct {
   129  	Min, Max   int64  // min <= value <= max, signed
   130  	Umin, Umax uint64 // umin <= value <= umax, unsigned
   131  	// For booleans, we use 0==false, 1==true for both ranges
   132  	// For pointers, we use 0,0,0,0 for nil and minInt64,maxInt64,1,maxUint64 for nonnil
   133  }
   134  
   135  func NoLimit() Limit {
   136  	return NoLimitForBitsize(64)
   137  }
   138  
   139  // If x and y can add without overflow or underflow
   140  // (using b bits), SafeAdd returns x+y, true.
   141  // Otherwise, returns 0, false.
   142  func SafeAdd(x, y int64, b uint) (int64, bool) {
   143  	s := x + y
   144  	if x >= 0 && y >= 0 && s < 0 {
   145  		return 0, false // 64-bit overflow
   146  	}
   147  	if x < 0 && y < 0 && s >= 0 {
   148  		return 0, false // 64-bit underflow
   149  	}
   150  	if !fitsInBits(s, b) {
   151  		return 0, false
   152  	}
   153  	return s, true
   154  }
   155  
   156  // same as safeAdd but for subtraction.
   157  func SafeSub(x, y int64, b uint) (int64, bool) {
   158  	if y == math.MinInt64 {
   159  		if x == math.MaxInt64 {
   160  			return 0, false // 64-bit overflow
   161  		}
   162  		x++
   163  		y++
   164  	}
   165  	return SafeAdd(x, -y, b)
   166  }
   167  
   168  // same as safeAddU but for subtraction.
   169  func SafeSubU(x, y uint64, b uint) (uint64, bool) {
   170  	if x < y {
   171  		return 0, false // 64-bit underflow
   172  	}
   173  	s := x - y
   174  	if !FitsInBitsU(s, b) {
   175  		return 0, false
   176  	}
   177  	return s, true
   178  }
   179  
   180  func ConvertIntWithBitsize[Target uint64 | int64, Source uint64 | int64](x Source, bitsize uint) Target {
   181  	if Target(0)-1 < 0 {
   182  		// Signed target: sign-extend the low bitsize bits.
   183  		switch bitsize {
   184  		case 64:
   185  			return Target(int64(x))
   186  		case 32:
   187  			return Target(int32(x))
   188  		case 16:
   189  			return Target(int16(x))
   190  		case 8:
   191  			return Target(int8(x))
   192  		}
   193  	} else {
   194  		// Unsigned target: zero-extend the low bitsize bits.
   195  		switch bitsize {
   196  		case 64:
   197  			return Target(uint64(x))
   198  		case 32:
   199  			return Target(uint32(x))
   200  		case 16:
   201  			return Target(uint16(x))
   202  		case 8:
   203  			return Target(uint8(x))
   204  		}
   205  	}
   206  	panic("unreachable")
   207  }
   208  
   209  // fitsInBits reports whether x fits in b bits (signed).
   210  func fitsInBits(x int64, b uint) bool {
   211  	if b == 64 {
   212  		return true
   213  	}
   214  	m := int64(-1) << (b - 1)
   215  	M := -m - 1
   216  	return x >= m && x <= M
   217  }
   218  
   219  func NoLimitForBitsize(bitsize uint) Limit {
   220  	return Limit{Min: -(1 << (bitsize - 1)), Max: 1<<(bitsize-1) - 1, Umin: 0, Umax: 1<<bitsize - 1}
   221  }
   222  
   223  // same as safeAdd for unsigned arithmetic.
   224  func safeAddU(x, y uint64, b uint) (uint64, bool) {
   225  	s := x + y
   226  	if s < x || s < y {
   227  		return 0, false // 64-bit overflow
   228  	}
   229  	if !FitsInBitsU(s, b) {
   230  		return 0, false
   231  	}
   232  	return s, true
   233  }
   234  
   235  func (l Limit) String() string {
   236  	return fmt.Sprintf("sm,SM=%d,%d um,UM=%d,%d", l.Min, l.Max, l.Umin, l.Umax)
   237  }
   238  
   239  func (l Limit) Intersect(l2 Limit) Limit {
   240  	l.Min = max(l.Min, l2.Min)
   241  	l.Umin = max(l.Umin, l2.Umin)
   242  	l.Max = min(l.Max, l2.Max)
   243  	l.Umax = min(l.Umax, l2.Umax)
   244  	return l
   245  }
   246  
   247  func (l Limit) signedMin(m int64) Limit {
   248  	l.Min = max(l.Min, m)
   249  	return l
   250  }
   251  
   252  func (l Limit) SignedMinMax(minimum, maximum int64) Limit {
   253  	l.Min = max(l.Min, minimum)
   254  	l.Max = min(l.Max, maximum)
   255  	return l
   256  }
   257  
   258  func (l Limit) UnsignedMin(m uint64) Limit {
   259  	l.Umin = max(l.Umin, m)
   260  	return l
   261  }
   262  
   263  func (l Limit) UnsignedMax(m uint64) Limit {
   264  	l.Umax = min(l.Umax, m)
   265  	return l
   266  }
   267  
   268  func (l Limit) UnsignedMinMax(minimum, maximum uint64) Limit {
   269  	l.Umin = max(l.Umin, minimum)
   270  	l.Umax = min(l.Umax, maximum)
   271  	return l
   272  }
   273  
   274  func (l Limit) nonzero() bool {
   275  	return l.Min > 0 || l.Umin > 0 || l.Max < 0
   276  }
   277  
   278  func (l Limit) MaybeZero() bool {
   279  	return !l.nonzero()
   280  }
   281  
   282  func (l Limit) Nonnegative() bool {
   283  	return l.Min >= 0
   284  }
   285  
   286  func (l Limit) Unsat() bool {
   287  	return l.Min > l.Max || l.Umin > l.Umax
   288  }
   289  
   290  // UnsignedFixedLeadingBits extracts the all the most significant fixed bits from the limit.
   291  // fixed and count are an other way to represent a limit, you can convert them to a limit as follows:
   292  //
   293  //	umin = fixed
   294  //	umax = fixed | (1<<(64-count) - 1)
   295  //
   296  // In order to be useful for bitmanip analysis fixed and count are a coarser tool than a limit:
   297  // 1. the varying section (umax-umin) is always one less than a power of two
   298  // 2. that section is naturally aligned inside the 64-bit space
   299  func (l Limit) UnsignedFixedLeadingBits() (fixed uint64, count uint) {
   300  	varying := uint(bits.Len64(l.Umin ^ l.Umax))
   301  	count = uint(bits.LeadingZeros64(l.Umin ^ l.Umax))
   302  	fixed = l.Umin &^ (1<<varying - 1)
   303  	return
   304  }
   305  
   306  // Add returns the limit obtained by adding a value with limit l
   307  // to a value with limit l2. The result must fit in b bits.
   308  func (l Limit) Add(l2 Limit, b uint) Limit {
   309  	var isLConst, isL2Const bool
   310  	var lConst, l2Const uint64
   311  	if l.Min == l.Max {
   312  		isLConst = true
   313  		lConst = ConvertIntWithBitsize[uint64](l.Min, b)
   314  	} else if l.Umin == l.Umax {
   315  		isLConst = true
   316  		lConst = l.Umin
   317  	}
   318  	if l2.Min == l2.Max {
   319  		isL2Const = true
   320  		l2Const = ConvertIntWithBitsize[uint64](l2.Min, b)
   321  	} else if l2.Umin == l2.Umax {
   322  		isL2Const = true
   323  		l2Const = l2.Umin
   324  	}
   325  	if isLConst && isL2Const {
   326  		r := lConst + l2Const
   327  		r &= (uint64(1) << b) - 1
   328  		int64r := ConvertIntWithBitsize[int64](r, b)
   329  		return Limit{Min: int64r, Max: int64r, Umin: r, Umax: r}
   330  	}
   331  
   332  	r := NoLimit()
   333  	min, minOk := SafeAdd(l.Min, l2.Min, b)
   334  	max, maxOk := SafeAdd(l.Max, l2.Max, b)
   335  	if minOk && maxOk {
   336  		r.Min = min
   337  		r.Max = max
   338  	}
   339  	umin, uminOk := safeAddU(l.Umin, l2.Umin, b)
   340  	umax, umaxOk := safeAddU(l.Umax, l2.Umax, b)
   341  	if uminOk && umaxOk {
   342  		r.Umin = umin
   343  		r.Umax = umax
   344  	}
   345  	return r
   346  }
   347  
   348  // same as add but for subtraction.
   349  func (l Limit) Sub(l2 Limit, b uint) Limit {
   350  	r := NoLimit()
   351  	min, minOk := SafeSub(l.Min, l2.Max, b)
   352  	max, maxOk := SafeSub(l.Max, l2.Min, b)
   353  	if minOk && maxOk {
   354  		r.Min = min
   355  		r.Max = max
   356  	}
   357  	umin, uminOk := SafeSubU(l.Umin, l2.Umax, b)
   358  	umax, umaxOk := SafeSubU(l.Umax, l2.Umin, b)
   359  	if uminOk && umaxOk {
   360  		r.Umin = umin
   361  		r.Umax = umax
   362  	}
   363  	return r
   364  }
   365  
   366  // same as add but for multiplication.
   367  func (l Limit) Mul(l2 Limit, b uint) Limit {
   368  	r := NoLimit()
   369  	umaxhi, umaxlo := bits.Mul64(l.Umax, l2.Umax)
   370  	if umaxhi == 0 && FitsInBitsU(umaxlo, b) {
   371  		r.Umax = umaxlo
   372  		r.Umin = l.Umin * l2.Umin
   373  		// Note: if the code containing this multiply is
   374  		// unreachable, then we may have umin>umax, and this
   375  		// multiply may overflow.  But that's ok for
   376  		// unreachable code. If this code is reachable, we
   377  		// know umin<=umax, so this multiply will not overflow
   378  		// because the max multiply didn't.
   379  	}
   380  	// Signed is harder, so don't bother. The only useful
   381  	// case is when we know both multiplicands are nonnegative,
   382  	// but that case is handled above because we would have then
   383  	// previously propagated signed info to the unsigned domain,
   384  	// and will propagate it back after the multiply.
   385  	return r
   386  }
   387  
   388  // Similar to add, but compute 1 << l if it fits without overflow in b bits.
   389  func (l Limit) Exp2(b uint) Limit {
   390  	r := NoLimit()
   391  	if l.Umax < uint64(b) {
   392  		r.Umin = 1 << l.Umin
   393  		r.Umax = 1 << l.Umax
   394  		// Same as above in mul, signed<->unsigned propagation
   395  		// will handle the signed case for us.
   396  	}
   397  	return r
   398  }
   399  
   400  // Similar to add, but computes the complement of the limit for bitsize b.
   401  func (l Limit) Com(b uint) Limit {
   402  	switch b {
   403  	case 64:
   404  		return Limit{
   405  			Min:  ^l.Max,
   406  			Max:  ^l.Min,
   407  			Umin: ^l.Umax,
   408  			Umax: ^l.Umin,
   409  		}
   410  	case 32:
   411  		return Limit{
   412  			Min:  int64(^int32(l.Max)),
   413  			Max:  int64(^int32(l.Min)),
   414  			Umin: uint64(^uint32(l.Umax)),
   415  			Umax: uint64(^uint32(l.Umin)),
   416  		}
   417  	case 16:
   418  		return Limit{
   419  			Min:  int64(^int16(l.Max)),
   420  			Max:  int64(^int16(l.Min)),
   421  			Umin: uint64(^uint16(l.Umax)),
   422  			Umax: uint64(^uint16(l.Umin)),
   423  		}
   424  	case 8:
   425  		return Limit{
   426  			Min:  int64(^int8(l.Max)),
   427  			Max:  int64(^int8(l.Min)),
   428  			Umin: uint64(^uint8(l.Umax)),
   429  			Umax: uint64(^uint8(l.Umin)),
   430  		}
   431  	default:
   432  		panic("unreachable")
   433  	}
   434  }
   435  
   436  // Similar to add, but computes the negation of the limit for bitsize b.
   437  func (l Limit) Neg(b uint) Limit {
   438  	return l.Com(b).Add(Limit{Min: 1, Max: 1, Umin: 1, Umax: 1}, b)
   439  }
   440  
   441  // Similar to add, but computes the TrailingZeros of the limit for bitsize b.
   442  func (l Limit) Ctz(b uint) Limit {
   443  	fixed, fixedCount := l.UnsignedFixedLeadingBits()
   444  	if fixedCount == 64 {
   445  		constResult := min(uint(bits.TrailingZeros64(fixed)), b)
   446  		return Limit{Min: int64(constResult), Max: int64(constResult), Umin: uint64(constResult), Umax: uint64(constResult)}
   447  	}
   448  
   449  	varying := 64 - fixedCount
   450  	if l.Umin&((1<<varying)-1) != 0 {
   451  		// there will always be at least one non-zero bit in the varying part
   452  		varying--
   453  		return NoLimit().UnsignedMax(uint64(varying))
   454  	}
   455  	return NoLimit().UnsignedMax(uint64(min(uint(bits.TrailingZeros64(fixed)), b)))
   456  }
   457  
   458  // Similar to add, but computes the Len of the limit for bitsize b.
   459  func (l Limit) Bitlen(b uint) Limit {
   460  	return NoLimit().UnsignedMinMax(
   461  		uint64(bits.Len64(l.Umin)),
   462  		uint64(bits.Len64(l.Umax)),
   463  	)
   464  }
   465  
   466  // Similar to add, but computes the PopCount of the limit for bitsize b.
   467  func (l Limit) Popcount(b uint) Limit {
   468  	fixed, fixedCount := l.UnsignedFixedLeadingBits()
   469  	varying := 64 - fixedCount
   470  	fixedContribution := uint64(bits.OnesCount64(fixed))
   471  
   472  	min := fixedContribution
   473  	max := fixedContribution + uint64(varying)
   474  
   475  	varyingMask := uint64(1)<<varying - 1
   476  
   477  	if varyingPartOfUmax := l.Umax & varyingMask; uint(bits.OnesCount64(varyingPartOfUmax)) != varying {
   478  		// there is at least one zero bit in the varying part
   479  		max--
   480  	}
   481  	if varyingPartOfUmin := l.Umin & varyingMask; varyingPartOfUmin != 0 {
   482  		// there is at least one non-zero bit in the varying part
   483  		min++
   484  	}
   485  
   486  	return NoLimit().UnsignedMinMax(min, max)
   487  }
   488  
   489  func (l Limit) ConstValue() (_ int64, ok bool) {
   490  	switch {
   491  	case l.Min == l.Max:
   492  		return l.Min, true
   493  	case l.Umin == l.Umax:
   494  		return int64(l.Umin), true
   495  	default:
   496  		return 0, false
   497  	}
   498  }
   499
View as plain text