sizefacts

Documentation

Overview

Package sizefacts provides the shared size-decrease primitives — constant resolution, canonical size variables, and provable lower-bound/upper-extent reasoning over SSA values — used by both tripcount and recurrence.

Index

• func ConstIntV(v ssa.Value) (int64, bool)
• func IsInteger(t types.Type) bool
• func IsPositiveStep(phi *ssa.Phi, e ssa.Value) bool
• func SizeVar(v ssa.Value) bound.Var
• func ZeroLen(v ssa.Value) bool
• type Facts
  • func (f *Facts) ArgSize(v ssa.Value) (bound.Var, bool)
  • func (f *Facts) LowerBoundConst(v ssa.Value, depth int) (int64, bool)
  • func (f *Facts) UpperExtent(v ssa.Value, depth int) (bound.Var, bool)

Functions

func ConstIntV

func ConstIntV(v ssa.Value) (int64, bool)

ConstIntV returns the exact int64 value of a constant.

func IsInteger

func IsInteger(t types.Type) bool

IsInteger reports whether t's underlying type is an integer basic type.

func IsPositiveStep

func IsPositiveStep(phi *ssa.Phi, e ssa.Value) bool

IsPositiveStep reports whether e is phi + c for a constant c > 0.

func SizeVar

func SizeVar(v ssa.Value) bound.Var

SizeVar maps a loop-bound value to a canonical size variable, or "".

func ZeroLen

func ZeroLen(v ssa.Value) bool

ZeroLen reports whether len(v) is provably ZERO — the gate for the append copy idiom, exported for the recurrence classifier's unwrap (which needs len(append(dst, x...)) == len(x) exactly, an equality only a zero-length dst provides). A nil slice constant and make([]T, 0, …) qualify; everything else is not proven and therefore does not.

Types

type Facts

type Facts struct {
	Stab *fieldpath.Stability
}

Facts answers the two extent questions the evolution rules share. It holds no cross-loop state; a fresh instance is built per Of call.

func (*Facts) ArgSize

func (f *Facts) ArgSize(v ssa.Value) (bound.Var, bool)

ArgSize resolves the canonical size of an argument value: collections and strings by length, integers by magnitude. The result is an UPPER bound on the size at every evaluation — the sound direction for cost and heap bounds, where over-approximation degrades Within to Unknown and never fabricates a tighter-than-true bound.

func (*Facts) LowerBoundConst

func (f *Facts) LowerBoundConst(v ssa.Value, depth int) (int64, bool)

LowerBoundConst returns a provable constant lower bound on v's value at every evaluation. ANY constant suffices: asymptotically a constant offset vanishes (the engine already accepts `for i := -5; i < n`).

The strict path runs FIRST and is the only source of exact values; the geometric rules' floor checks depend on that ordering (a fabricated 0 makes `i *= 2` look like a fixed point). The fallback proves only >= 0.

func (*Facts) UpperExtent

func (f *Facts) UpperExtent(v ssa.Value, depth int) (bound.Var, bool)

UpperExtent resolves v to a size variable dominating max(v, 0) at every in-loop evaluation (trip counts are non-negative, so dominating the non-negative part suffices; this is what keeps e/c sound when e can be negative). Rules may only WEAKEN extents — never construct growing ones.