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

type branch

const unknown

const positive

const negative

const jumpTable0

func (b branch) String() string {}

type relation

const lt

const eq

const gt

var relationStrings

func (r relation) String() string {}

type domain

const signed

const unsigned

const pointer

const boolean

var domainStrings

func (d domain) String() string {}

type limit

func (l limit) String() string {}

func (l limit) intersect(l2 limit) limit {}

func (l limit) signedMin(m int64) limit {}

func (l limit) signedMax(m int64) limit {}

func (l limit) signedMinMax(min, max int64) limit {}

func (l limit) unsignedMin(m uint64) limit {}

func (l limit) unsignedMax(m uint64) limit {}

func (l limit) unsignedMinMax(min, max uint64) limit {}

func (l limit) nonzero() bool {}

func (l limit) nonnegative() bool {}

func (l limit) unsat() bool {}

// If x and y can add without overflow or underflow
// (using b bits), safeAdd returns x+y, true.
// Otherwise, returns 0, false.
func safeAdd(x, y int64, b uint) (int64, bool) {}

// same as safeAdd for unsigned arithmetic.
func safeAddU(x, y uint64, b uint) (uint64, bool) {}

// same as safeAdd but for subtraction.
func safeSub(x, y int64, b uint) (int64, bool) {}

// same as safeAddU but for subtraction.
func safeSubU(x, y uint64, b uint) (uint64, bool) {}

// fitsInBits reports whether x fits in b bits (signed).
func fitsInBits(x int64, b uint) bool {}

// fitsInBitsU reports whether x fits in b bits (unsigned).
func fitsInBitsU(x uint64, b uint) bool {}

// add returns the limit obtained by adding a value with limit l
// to a value with limit l2. The result must fit in b bits.
func (l limit) add(l2 limit, b uint) limit {}

// same as add but for subtraction.
func (l limit) sub(l2 limit, b uint) limit {}

// same as add but for multiplication.
func (l limit) mul(l2 limit, b uint) limit {}

// Similar to add, but compute 1 << l if it fits without overflow in b bits.
func (l limit) exp2(b uint) limit {}

// Similar to add, but computes the complement of the limit for bitsize b.
func (l limit) com(b uint) limit {}

var noLimit

type limitFact

type ordering

type factsTable

var checkpointBound

func newFactsTable(f *Func) *factsTable {}

// signedMin records the fact that we know v is at least
// min in the signed domain.
func (ft *factsTable) signedMin(v *Value, min int64) bool {}

// signedMax records the fact that we know v is at most
// max in the signed domain.
func (ft *factsTable) signedMax(v *Value, max int64) bool {}

func (ft *factsTable) signedMinMax(v *Value, min, max int64) bool {}

// setNonNegative records the fact that v is known to be non-negative.
func (ft *factsTable) setNonNegative(v *Value) bool {}

// unsignedMin records the fact that we know v is at least
// min in the unsigned domain.
func (ft *factsTable) unsignedMin(v *Value, min uint64) bool {}

// unsignedMax records the fact that we know v is at most
// max in the unsigned domain.
func (ft *factsTable) unsignedMax(v *Value, max uint64) bool {}

func (ft *factsTable) unsignedMinMax(v *Value, min, max uint64) bool {}

func (ft *factsTable) booleanFalse(v *Value) bool {}

func (ft *factsTable) booleanTrue(v *Value) bool {}

func (ft *factsTable) pointerNil(v *Value) bool {}

func (ft *factsTable) pointerNonNil(v *Value) bool {}

// newLimit adds new limiting information for v.
// Returns true if the new limit added any new information.
func (ft *factsTable) newLimit(v *Value, newLim limit) bool {}

func (ft *factsTable) addOrdering(v, w *Value, d domain, r relation) {}

// update updates the set of relations between v and w in domain d
// restricting it to r.
func (ft *factsTable) update(parent *Block, v, w *Value, d domain, r relation) {}

var opMin

var opMax

var opUMax

// isNonNegative reports whether v is known to be non-negative.
func (ft *factsTable) isNonNegative(v *Value) bool {}

// checkpoint saves the current state of known relations.
// Called when descending on a branch.
func (ft *factsTable) checkpoint() {}

// restore restores known relation to the state just
// before the previous checkpoint.
// Called when backing up on a branch.
func (ft *factsTable) restore() {}

var reverseBits

var domainRelationTable

// cleanup returns the posets to the free list
func (ft *factsTable) cleanup(f *Func) {}

// prove removes redundant BlockIf branches that can be inferred
// from previous dominating comparisons.
//
// By far, the most common redundant pair are generated by bounds checking.
// For example for the code:
//
//	a[i] = 4
//	foo(a[i])
//
// The compiler will generate the following code:
//
//	if i >= len(a) {
//	    panic("not in bounds")
//	}
//	a[i] = 4
//	if i >= len(a) {
//	    panic("not in bounds")
//	}
//	foo(a[i])
//
// The second comparison i >= len(a) is clearly redundant because if the
// else branch of the first comparison is executed, we already know that i < len(a).
// The code for the second panic can be removed.
//
// prove works by finding contradictions and trimming branches whose
// conditions are unsatisfiable given the branches leading up to them.
// It tracks a "fact table" of branch conditions. For each branching
// block, it asserts the branch conditions that uniquely dominate that
// block, and then separately asserts the block's branch condition and
// its negation. If either leads to a contradiction, it can trim that
// successor.
func prove(f *Func) {}

// initLimit sets initial constant limit for v.  This limit is based
// only on the operation itself, not any of its input arguments. This
// method is only called once on prove pass startup (unlike
// flowLimit, below, which computes additional constraints based on
// ranges of opcode arguments).
func initLimit(v *Value) limit {}

// flowLimit updates the known limits of v in ft. Returns true if anything changed.
// flowLimit can use the ranges of input arguments.
//
// Note: this calculation only happens at the point the value is defined. We do not reevaluate
// it later. So for example:
//
//	v := x + y
//	if 0 <= x && x < 5 && 0 <= y && y < 5 { ... use v ... }
//
// we don't discover that the range of v is bounded in the conditioned
// block. We could recompute the range of v once we enter the block so
// we know that it is 0 <= v <= 8, but we don't have a mechanism to do
// that right now.
func (ft *factsTable) flowLimit(v *Value) bool {}

// getBranch returns the range restrictions added by p
// when reaching b. p is the immediate dominator of b.
func getBranch(sdom SparseTree, p *Block, b *Block) branch {}

// addIndVarRestrictions updates the factsTables ft with the facts
// learned from the induction variable indVar which drives the loop
// starting in Block b.
func addIndVarRestrictions(ft *factsTable, b *Block, iv indVar) {}

// addBranchRestrictions updates the factsTables ft with the facts learned when
// branching from Block b in direction br.
func addBranchRestrictions(ft *factsTable, b *Block, br branch) {}

// addRestrictions updates restrictions from the immediate
// dominating block (p) using r.
func addRestrictions(parent *Block, ft *factsTable, t domain, v, w *Value, r relation) {}

func addLocalFacts(ft *factsTable, b *Block) {}

func addLocalFactsPhi(ft *factsTable, v *Value) {}

var ctzNonZeroOp

var mostNegativeDividend

// simplifyBlock simplifies some constant values in b and evaluates
// branches to non-uniquely dominated successors of b.
func simplifyBlock(sdom SparseTree, ft *factsTable, b *Block) {}

func removeBranch(b *Block, branch branch) {}

// isConstDelta returns non-nil if v is equivalent to w+delta (signed).
func isConstDelta(v *Value) (w *Value, delta int64) {}

// isCleanExt reports whether v is the result of a value-preserving
// sign or zero extension.
func isCleanExt(v *Value) bool {}