flow

package
v1.5.9 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Feb 14, 2026 License: MIT Imports: 17 Imported by: 0

Documentation

Overview

Package flow provides control flow type propagation and flow-sensitive analysis.

Flow analysis computes the types of variables at each program point by propagating type information through the control flow graph. Unlike simple declared types, flow types account for assignments, conditionals, and narrowing constraints.

Usage

Build an Inputs struct from the CFG, declared types, and extracted constraints, then call Solve to compute the flow solution: 

inputs := &flow.Inputs{
	Graph:         cfg,
	DeclaredTypes: declaredTypes,
	Assignments:   assignments,
	EdgeConditions: edgeConditions,
	TypeKeys:      typeKeys,
	Decomposer:    decomposer,
}
solution := flow.Solve(inputs, resolver)

Query the solution for types at specific program points: 

t := solution.TypeAt(point, path)           // Base type lookup
narrowed := solution.NarrowedTypeAt(point, path)  // Type with narrowing applied
cond := solution.ConditionAt(point)         // Active constraints

Core Concepts

Inputs: All data needed by the flow solver, including CFG, declared types, assignments, conditions, and constraint metadata. Inputs are AST-free and deterministic for caching and incremental analysis.

Solution: The result of flow analysis, mapping versioned path keys to their narrowed types. Query methods apply point conditions to refine types further.

TypeState: Tracks whether a type at a program point is resolved, pending, or conflicted. Used for fixed-point iteration during solving.

SymbolTypes: Maps each CFG point to its per-symbol types, representing the complete type state at that point in the program.

Special Assignments

The solver handles several special assignment patterns:

  • IteratorSource: Derives iterator variable types from the iterated container
  • ContainerElementSource: Derives types from container methods (channel:receive())
  • MapElementSource: Derives types from dynamic map index reads (t[k])
  • SiblingAssignment: Correlates multi-return values (result, err patterns)

Widening

When recursive dependencies prevent convergence, symbols are widened to Unknown. WideningEvent records these cases for diagnostic reporting.

Subpackages

The flow package has several subpackages:

  • domain: Abstract domain interfaces for constraint solving
  • join: Type joining operations for phi node merging
  • numeric: Numeric range and interval tracking
  • pathkey: Canonical path key resolution for SSA versions
  • propagate: Condition propagation through the CFG

Integration

The flow package is used by the type checker to get refined types at each program point. The solver is invoked after CFG construction and constraint extraction, producing SymbolTypes consumed by narrowing and error reporting.

inference.go implements function effect inference from flow analysis results.

Function effects describe how a function's return value relates to its parameters. For predicate functions (returning boolean), effects capture when parameters are narrowed based on the return value (OnTrue/OnFalse). For assert-style functions, effects capture constraints that hold after the function returns (OnReturn).

Effects enable interprocedural narrowing: calling a predicate function in a conditional allows the checker to narrow argument types in the appropriate branch.

transfer.go implements the transfer functions for the flow analysis worklist algorithm.

Transfer functions define how types change at each CFG point. This file handles:

  • Phi node processing: Joining types from multiple incoming branches
  • Assignment processing: Computing types for assignment targets
  • Iterator derivation: Computing loop variable types from iterator sources
  • Widening: Expanding types for table mutations and dynamic indexing

The functions return changed keys to drive worklist propagation.

type_facts.go provides phase-safe type access for the type checker.

During type checking, it's critical to distinguish between declared types (from annotations) and refined types (from flow analysis). Mixing these can cause "early synthesis poisoning" where prematurely narrowed types influence later analysis incorrectly.

The TypeFacts interface provides clean separation:

  • DeclaredAt: Only annotation-based types
  • RefinedAt: Only flow-narrowed types
  • EffectiveTypeAt: Best available type for practical use

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func InferFunctionEffect 

func InferFunctionEffect(
	solution *Solution,
	g *cfg.CFG,
	params []ParamInfo,
	returnType typ.Type,
) *constraint.FunctionEffect

InferFunctionEffect computes a FunctionEffect from solved flow analysis.

This is the post-flow variant that uses the complete flow solution to determine which constraints hold at each return point. It examines return points to compute:

  • OnTrue: Constraints that hold when returning true (boolean predicates)
  • OnFalse: Constraints that hold when returning false (boolean predicates)
  • OnReturn: Constraints that hold on normal return (assert-style functions)
  • Terminates: Whether the function never returns normally

For boolean-returning functions, OnTrue/OnFalse are populated based on return statement analysis. Return statements with literal true/false are classified via ReturnKinds. Return statements with predicate expressions use ReturnConstraints.

For non-boolean functions, OnReturn is populated from path conditions at return points.

All constraints are converted to use placeholders ($0, $1, ...) for parameters, enabling the effect to be instantiated with actual arguments at call sites.

Example: For function `function is_string(x) return type(x) == "string" end`:

  • OnTrue: HasType($0, string)
  • OnFalse: NotHasType($0, string)

func InferFunctionEffectFromInputs 

func InferFunctionEffectFromInputs(
	inputs *Inputs,
	g *cfg.CFG,
	params []ParamInfo,
	returnType typ.Type,
) *constraint.FunctionEffect

InferFunctionEffectFromInputs computes a FunctionEffect without running full flow analysis.

This is the pre-flow variant that uses only the extracted return constraints without propagating conditions through the CFG. It produces conservative effects based on:

  • ReturnConstraints: Direct constraint extraction from return expressions
  • CFG structure: Detecting terminating functions (no return/exit nodes)

The pre-flow variant is faster but less precise than post-flow inference because it cannot account for path conditions from prior conditionals. It's suitable for bootstrapping effect extraction before the full type checking pass.

Example: For function `function assert_string(x) assert(type(x) == "string") end`:

  • OnReturn: HasType($0, string) (from assert expression)
  • Terminates: false (has implicit return via exit)

func WidenArrayElementType 

func WidenArrayElementType(arrayType typ.Type, elementType typ.Type, joinFn func(a, b typ.Type) typ.Type) typ.Type

WidenArrayElementType widens an array type by joining a new element type.

This function handles the common pattern of widening arrays as elements are added. The join function controls how types are combined:

  • For union: joinFn = join.Two (creates union types)
  • For intersection: joinFn = narrow.Intersect (narrows types)

Type handling:

  • Array: Joins element type with new type
  • Empty record: Converts to array with new element type
  • Union: Widens first array member found
  • nil/placeholder: Creates new array with element type
  • Other types: Returns unchanged (not an array)

Returns the widened type.

func WidenMapValueArray added in v1.5.6 

func WidenMapValueArray(mapType typ.Type, keyType, elementType typ.Type) typ.Type

WidenMapValueArray widens a map's value type by adding an element to its array component.

This handles the pattern: suites[name] = suites[name] or {}; table.insert(suites[name], test) where suites is {[string]: Test[]} and we need to widen the array element type.

Type handling:

  • Map: Widens key type and array element of value type
  • Empty record: Converts to map with array value
  • Union: Widens first map member found
  • Placeholder types: Creates new map with array value
  • Other types: Returns unchanged

Returns the widened type.

Types

type ConstKind 

type ConstKind uint8

ConstKind classifies the type of a constant value tracked for type narrowing. Constants are tracked to enable literal-based narrowing (e.g., x == "foo"). 

const (
	ConstUnknown ConstKind = iota // 0 = zero value = unknown
	ConstString
	ConstInt
	ConstFloat
	ConstBool
	ConstNil
)

type ConstValue 

type ConstValue struct {
	Kind  ConstKind
	Str   string
	Int   int64
	Float float64
	Bool  bool
}

ConstValue represents a constant value (string, int, float, bool, or nil).

func (*ConstValue) ToLiteralType 

func (c *ConstValue) ToLiteralType() typ.Type

ToLiteralType converts a ConstValue to its corresponding literal type.

type ContainerElementSource 

type ContainerElementSource struct {
	ContainerPath constraint.Path // Path to the container (e.g., channel variable)
	ReturnIndex   int             // Which return value (0-based)
}

ContainerElementSource tracks that an assignment's type should be derived from a container's element type at solve time. Used for methods like channel:receive() where the return type depends on the widened container type.

type ContainerMutatorAssignment 

type ContainerMutatorAssignment struct {
	Point     cfg.Point
	Target    constraint.Path // Container path (symbol-only, e.g., channel variable)
	ValuePath constraint.Path // Path to value expression for flow-resolved type lookup
	ValueType typ.Type        // Fallback type if ValuePath doesn't resolve
}

ContainerMutatorAssignment describes container mutations (channel.send, etc.) that widen element types. Uses the ContainerElementUnion effect pattern from specs.

type DeclaredTypes 

type DeclaredTypes = map[cfg.SymbolID]typ.Type

DeclaredTypes maps SymbolID to its declared type.

This type alias documents that the map should contain only annotation-derived types, not types synthesized from expression analysis. This distinction is enforced by the code that populates the map, not by the type system.

type EdgeCondition 

type EdgeCondition struct {
	From      cfg.Point
	To        cfg.Point
	Condition constraint.Condition
}

EdgeCondition ties a DNF condition to a control-flow edge.

type EdgeNumericConstraint 

type EdgeNumericConstraint struct {
	From        cfg.Point
	To          cfg.Point
	Constraints []constraint.NumericConstraint
}

EdgeNumericConstraint ties numeric constraints to a control-flow edge.

type GuardedTypeCorrelation added in v1.5.8 

type GuardedTypeCorrelation struct {
	GuardIndex    int
	TargetIndex   int
	GuardOnTruthy bool
	TargetType    typ.Type
}

GuardedTypeCorrelation describes branch-sensitive sibling narrowing: when guard return at GuardIndex is truthy/falsy (per GuardOnTruthy), target return at TargetIndex narrows to TargetType.

type IndexerAssignment 

type IndexerAssignment struct {
	Point     cfg.Point
	Root      string               // Variable name (for display)
	Symbol    cfg.SymbolID         // Unique symbol ID for the root variable
	Segments  []constraint.Segment // Field/index segments for nested tables
	KeyVar    string               // Variable name if key is an identifier
	KeySymbol cfg.SymbolID         // Symbol ID for the key variable (for SSA-aware lookup)
	KeyType   typ.Type             // Optional explicit key type (overrides KeySymbol lookup)
	ValuePath constraint.Path      // Path to value expression for flow-resolved type lookup
	ValType   typ.Type             // Fallback type when ValuePath is unavailable
}

IndexerAssignment describes an assignment via dynamic index: t[k] = v where k is non-const. Used to widen empty tables to maps. KeyVar stores the variable name if key is an identifier; KeyType is resolved during flow solving when we have flow-narrowed types.

type Inputs 

type Inputs struct {
	// Graph provides CFG, SSA versioning, and symbol scope information.
	Graph cfg.VersionedGraph

	// Decomposer extracts element/key/value types from composite types.
	Decomposer TypeDecomposer

	// DeclaredTypes maps SymbolID to declared type.
	// All per-variable type data is keyed by SymbolID for proper scope handling.
	DeclaredTypes map[cfg.SymbolID]typ.Type

	// AnnotatedVars tracks variables with explicit type annotations.
	AnnotatedVars map[cfg.SymbolID]bool

	Assignments    []UnifiedAssignment
	ConstValues    map[cfg.SymbolID]map[cfg.Point]*ConstValue
	EdgeConditions []EdgeCondition

	// EdgeNumericConstraints stores numeric constraints from comparison operators.
	// These are fed to theory solvers to detect contradictions.
	EdgeNumericConstraints []EdgeNumericConstraint

	// Type key resolution for HasType constraints.
	TypeKeys map[uint64]typ.Type

	// ReturnKinds classifies return points (true/false/unknown).
	// Populated by checker which has AST access.
	ReturnKinds map[cfg.Point]ReturnKind

	// ReturnConstraints stores constraints extracted from return expressions.
	// For predicate functions, the return expression encodes the constraint.
	// Example: "return type(x) == string" gives OnTrue: HasType{x, string}
	ReturnConstraints map[cfg.Point]ReturnExprConstraints

	// PredicateLinks tracks variables assigned from predicate calls.
	// Key is "varname@defpoint", value contains constraints to apply when var is truthy/falsy.
	// Example: local _, err = Point:is(data) -> err nil implies HasType{data, Point}
	PredicateLinks map[string]PredicateLink

	// SiblingAssignments tracks variables assigned from the same multi-return call.
	// Key is "varname@defpoint", maps to the sibling group.
	// Used for error return pattern where checking err narrows result.
	SiblingAssignments map[SiblingKey]*SiblingAssignment

	// IndexerAssignments tracks dynamic index assignments: t[k] = v with non-const k.
	// Used to widen {} to {[K]: V} based on key/value types.
	IndexerAssignments []IndexerAssignment

	// TableMutatorAssignments tracks table.insert-like mutations that widen
	// array element types (including map values that are arrays).
	TableMutatorAssignments []TableMutatorAssignment

	// ContainerMutatorAssignments tracks container mutations (e.g., channel.send)
	// that widen element types via ContainerElementUnion effects.
	ContainerMutatorAssignments []ContainerMutatorAssignment

	// DeadPoints marks CFG points that are unreachable.
	// Used when a terminating function (one that never returns) is called.
	DeadPoints map[cfg.Point]bool

	// ModuleAliases maps symbol IDs to module paths from require() assignments.
	// Example: local http = require("http_client") -> sym(http) -> "http_client"
	ModuleAliases map[cfg.SymbolID]string

	// FunctionAliases maps local symbols to their source function symbols.
	// For patterns like `local f = B`, maps sym(f) -> sym(B).
	// Used for effect propagation through aliases.
	FunctionAliases map[cfg.SymbolID]cfg.SymbolID

	// SiblingTypes provides captured variable types from parent scope.
	// Explicit overlay, never merged into DeclaredTypes.
	SiblingTypes map[cfg.SymbolID]typ.Type

	// LiteralTypes provides function literal types synthesized in the literal phase.
	// Explicit overlay, never merged into DeclaredTypes.
	LiteralTypes map[cfg.SymbolID]typ.Type

	// WideningEvents records symbols that were widened to Unknown during preflow inference.
	// Used for diagnostics to report precision loss.
	WideningEvents []WideningEvent

	// KeysProvenance tracks variables that contain keys of another table.
	// Key: symbol of variable holding keys (e.g., suite_names)
	// Value: symbol of table the keys came from (e.g., suites)
	// Used to emit KeyOf constraints when iterating over such variables.
	KeysProvenance map[cfg.SymbolID]cfg.SymbolID
}

Inputs bundles all data needed by the flow solver for type propagation. Inputs are AST-free and deterministic, enabling serialization, caching, and reproducible analysis across sessions.

func (*Inputs) Normalize 

func (in *Inputs) Normalize()

Normalize enforces deterministic ordering for slice-based inputs.

This does not change semantics; it only stabilizes iteration order for reproducible analysis and diagnostics.

type IteratorKind 

type IteratorKind int

IteratorKind describes the type of iteration for iterator variable derivation. 

const (
	IterateIndexed IteratorKind = iota // ipairs-style: (integer, element)
	IterateKeyed                       // pairs-style: (key, value)
)

type IteratorSource 

type IteratorSource struct {
	Path     constraint.Path // Path to iterator source (e.g., array being iterated)
	Kind     IteratorKind    // Type of iteration
	VarIndex int             // 0=key/index, 1=value
}

IteratorSource stores info for deriving iterator variable types from flow solution.

type MapElementSource 

type MapElementSource struct {
	MapPath   constraint.Path // Path to the map/table being indexed
	KeySymbol cfg.SymbolID    // Symbol for key variable (SSA lookup)
	KeyVar    string          // Key variable name (display)
}

MapElementSource tracks that an assignment's type should be derived from a map/table's value type at solve time. Used for dynamic index reads like t[k] where k is a non-const variable and the path cannot be statically built.

type ParamInfo 

type ParamInfo struct {
	Name   string
	Symbol cfg.SymbolID
	Type   typ.Type
}

ParamInfo describes a function parameter for effect inference.

Both Name and Symbol are needed: Name for user-facing constraint paths, Symbol for SSA-based path resolution. Type is included for completeness but not currently used during inference. 

type PredicateLink struct {
	OnTruthy constraint.Condition
	OnFalsy  constraint.Condition
}

PredicateLink stores predicate constraints for a variable assigned from a predicate call. Example: local ok = Point:is(data) -> OnTruthy contains HasType{data, Point}

type ProductDomain 

type ProductDomain struct {
	Type    *domain.TypeDomain
	Numeric *numeric.Domain
	Shape   *domain.ShapeDomain
	EGraph  *theory.EGraph
	// contains filtered or unexported fields
}

ProductDomain combines Type, Numeric, and Shape domains into a single abstract domain for constraint solving in flow-sensitive type analysis.

ProductDomain is the central abstraction for narrowing types based on control flow constraints. It orchestrates three specialized subdomains, each handling different aspects of constraint narrowing:

  • Type domain: Handles HasType, NotHasType, Truthy, and Falsy constraints. Narrows union types by adding or removing type alternatives. For example, a Truthy constraint on `string|nil` narrows to `string`.

  • Numeric domain: Tracks numeric range constraints (Lt, Le, Gt, Ge) and modular arithmetic (ModEq). Maintains interval bounds for number values. For example, `x >= 0` establishes a lower bound of 0 for x.

  • Shape domain: Handles structural constraints on tables including field presence/absence, index constraints, and record shape narrowing. Uses the wrapped Solver for complex shape reasoning.

The E-graph component tracks path equality constraints (EqPath) and propagates narrowings across equivalence classes using congruence closure. When two paths are proven equal via `x == y`, type narrowings learned about one automatically apply to both. This is essential for code patterns like: 

if a == b and type(a) == "string" then
    -- both a and b are narrowed to string
end

ProductDomain routes constraint atoms to the appropriate subdomain via domain.ClassifyAtom, applies conjunctions by collecting atoms and leftovers, and handles disjunctions by cloning the domain state, speculatively applying each disjunct, and joining the results.

The domain satisfies the abstract domain interface with Clone, Join, and IsUnsat operations, enabling the flow analysis to track type information along different control flow paths and merge it at join points.

func NewProductDomain 

func NewProductDomain(env constraint.Env) *ProductDomain

NewProductDomain creates a new ProductDomain initialized with the given environment.

The environment provides type resolution functions needed by the subdomains:

  • env.PathTypeAt: Returns the base type at a given path key. Used to look up original types before narrowing is applied.

  • env.ResolvePath: Converts a constraint.Path to its canonical PathKey. Used for consistent key resolution across all operations.

  • env.ResolveType: Resolves type keys (like "string", "number") to actual types.

All three subdomains (Type, Numeric, Shape) share the same environment, ensuring consistent type resolution. The E-graph is initialized empty and will be populated when EqPath constraints are applied.

Example usage: 

env := constraint.Env{
    PathTypeAt: func(key constraint.PathKey) typ.Type { return types[key] },
    ResolvePath: resolver.KeyAt,
}
domain := NewProductDomain(env)
domain.ApplyCondition(condition) // Apply narrowing constraints
narrowedType := domain.TypeAt(key) // Get narrowed type

func (*ProductDomain) ApplyAtom 

func (d *ProductDomain) ApplyAtom(atom constraint.Atom) bool

ApplyAtom applies a constraint atom to the appropriate subdomain(s).

Atoms are the primitive building blocks of constraints. Each atom type is routed to the appropriate subdomain based on domain.ClassifyAtom:

  • AtomClassType: Routed to Type domain. Includes HasType, NotHasType, Truthy, and Falsy atoms that narrow union types.

  • AtomClassNumeric: Routed to Numeric domain. Includes Lt, Le, Gt, Ge, and ModEq atoms that establish numeric bounds.

  • AtomClassBoth: Applied to both Type and Numeric domains. Used for atoms that have implications in both domains (e.g., equality with a constant).

  • AtomClassNone: No-op, returns true. Used for atoms that don't affect type narrowing.

Returns false if the atom makes the domain unsatisfiable (proves a contradiction). For example, applying HasType("string") to a path known to be `number` returns false since a value cannot be both string and number.

For AtomClassBoth atoms, both domains must accept the atom; if either returns false, the overall result is false.

func (*ProductDomain) ApplyCondition 

func (d *ProductDomain) ApplyCondition(cond constraint.Condition) bool

ApplyCondition applies a DNF (Disjunctive Normal Form) condition.

A DNF condition is an OR of ANDs: (A1 AND A2) OR (B1 AND B2 AND B3) OR ... Each disjunct is a conjunction of primitive constraints.

The algorithm handles conditions based on their structure:

  • False condition (empty disjuncts): Returns false immediately. No possible narrowing can make a false condition true.

  • True condition (single empty disjunct): Returns true. No constraints to apply.

  • Single disjunct: Applies as a conjunction directly to the current domain. No cloning or joining needed.

  • Multiple disjuncts: Uses speculative evaluation with join: 1. For each disjunct, clone the current domain state 2. Apply the conjunction to the clone 3. If satisfiable, accumulate into the result via Join 4. If all disjuncts are unsatisfiable, return false

The Join operation computes the least upper bound (widening) of two domain states. For types, this means computing unions. For numeric ranges, this means taking the outer bounds. The result represents "values that could come from either branch."

This enables reasoning about conditionals like: 

if type(x) == "string" or type(x) == "number" then
    -- x is narrowed to string|number
end

The method mutates the receiver to match the accumulated result.

func (*ProductDomain) ApplyConjunction 

func (d *ProductDomain) ApplyConjunction(constraints []constraint.Constraint) bool

ApplyConjunction applies all constraints in a conjunction (AND of constraints).

This is the primary method for applying multiple constraints that must all hold simultaneously. The method performs several steps in order:

  1. Constraint conversion: Uses constraint.ToAtomsWithResolver to convert high-level constraints into atoms (primitive narrowings) and leftover constraints (complex shapes). The resolver ensures paths are converted to canonical keys.

  2. Congruence closure: Builds an E-graph from EqPath constraints. When `x == y` is asserted, the E-graph records that paths x and y are in the same equivalence class. Later narrowings to x will propagate to y.

  3. Atom application: Applies all atoms to their respective subdomains (Type and/or Numeric based on classification). Returns false immediately if any atom proves unsatisfiability.

  4. Type narrowing propagation: Propagates Type domain narrowings across equivalence classes via propagateTypeNarrowingsCC. If x and y are equivalent and x is narrowed to string, y is also narrowed to string.

  5. Leftover application: Applies leftover constraints to the Shape domain with access to Type domain narrowings for context.

  6. Shape narrowing propagation: Propagates Shape domain narrowings across equivalence classes via propagateShapeNarrowingsCC.

Returns false if any step proves the domain unsatisfiable.

func (*ProductDomain) ApplyLeftoverConstraint 

func (d *ProductDomain) ApplyLeftoverConstraint(c constraint.Constraint) bool

ApplyLeftoverConstraint applies a constraint that couldn't be converted to an atom.

Leftover constraints are those that cannot be represented as simple atoms. These include complex structural constraints like:

  • Field presence checks: HasField{Path, FieldName}
  • Index constraints: HasIndex{Path, IndexType}
  • Metatable constraints: HasMetatable{Path}
  • Record shape constraints that require structural reasoning

These constraints are routed to the Shape domain, which uses the wrapped Solver for more sophisticated shape analysis.

The method first resolves the target path to a canonical key using env.ResolvePath. If the constraint has no paths or the path cannot be resolved, the constraint is silently accepted (returns true) since we cannot reason about it without a target.

Returns false if the constraint proves the domain unsatisfiable.

func (*ProductDomain) Clone 

func (d *ProductDomain) Clone() domain.Domain

Clone creates a deep copy of the ProductDomain.

Clone is essential for speculative evaluation in ApplyCondition. When evaluating disjunctions (OR conditions), each branch is explored on a cloned domain to avoid polluting the original state with tentative narrowings.

The clone includes deep copies of:

  • Type domain: All narrowed type mappings
  • Numeric domain: All numeric bounds and constraints
  • Shape domain: All structural narrowings
  • E-graph: All path equivalences

The environment (env) is shared by reference since it contains only function pointers that don't change during analysis.

Clone operations are a significant cost in constraint solving. The ProductDomain minimizes this by only cloning the narrowed values maps, not the base types (which are immutable and shared).

Example: 

original := NewProductDomain(env)
original.ApplyAtom(hasTypeString)  // Narrows x to string

clone := original.Clone().(*ProductDomain)
clone.ApplyAtom(hasTypeNumber)  // Narrows x to number in clone only

original.TypeAt("x")  // Still string
clone.TypeAt("x")     // Now number

func (*ProductDomain) IsUnsat 

func (d *ProductDomain) IsUnsat() bool

IsUnsat returns true if the domain state represents a contradiction.

A domain is unsatisfiable when the applied constraints are mutually inconsistent. This can happen in several ways:

  • Type contradiction: HasType("string") followed by HasType("number") on the same path. No value can be both string and number.

  • Numeric contradiction: x > 10 followed by x < 5. No number satisfies both.

  • Shape contradiction: Record proven to lack a field that's required.

When any subdomain becomes unsatisfiable, the entire ProductDomain is considered unsatisfiable. This is used during ApplyCondition to detect dead branches and during ApplyConjunction to detect invalid constraints.

Returns true if Type, Numeric, OR Shape subdomain is unsatisfiable.

func (*ProductDomain) Join 

func (d *ProductDomain) Join(other domain.Domain) domain.Domain

Join computes the least upper bound of two ProductDomain states.

Join is used to merge type information at control flow join points, such as after if-else branches or at loop headers. The result represents values that could have come from either domain.

For each subdomain, Join computes a widening:

  • Type domain: Types are unioned. If d has x:string and o has x:number, the joined result has x:string|number.

  • Numeric domain: Bounds are widened. If d has x>5 and o has x>10, the joined result has x>5 (the weaker bound).

  • Shape domain: Structural constraints are intersected. Only fields proven in BOTH domains are preserved.

  • E-graph: Equivalences are intersected. Only path equalities that hold in BOTH domains are preserved. If d has a==b but o doesn't, the joined result does not have a==b.

The E-graph join is conservative: we only keep equivalences where both domains agree on the same root. This prevents unsound conclusions when equality only holds on one branch.

Example: 

// Branch 1: x is string
d := NewProductDomain(env)
d.ApplyAtom(hasTypeString)

// Branch 2: x is number
o := NewProductDomain(env)
o.ApplyAtom(hasTypeNumber)

// After join: x is string|number
joined := d.Join(o).(*ProductDomain)

Join is commutative: d.Join(o) equals o.Join(d).

func (*ProductDomain) NarrowedChildPaths 

func (d *ProductDomain) NarrowedChildPaths(parentKey constraint.PathKey) map[constraint.PathKey]typ.Type

NarrowedChildPaths returns all narrowed paths that are children of the given parent key.

This method collects narrowings for all paths that extend the parent path, such as fields or indices. Given a parent key "t@1", it returns narrowings for paths like "t@1.foo", "t@1.bar", "t@1[0]", etc.

The method combines narrowings from both Type and Shape domains:

  • Type domain narrowings: Direct type constraints on child paths
  • Shape domain narrowings: Structural constraints that narrow field types

When both domains have narrowings for the same child path, their intersection is computed. This ensures the returned types reflect all known constraints.

The parentKey is matched as a prefix with a dot separator. For example:

  • Parent "sym1@1" matches children "sym1@1.foo", "sym1@1.bar"
  • Parent "sym1@1" does NOT match "sym1@10" (different version)
  • Parent "sym1@1" does NOT match "sym1@1foo" (no separator)

This is used during type synthesis to collect narrowings learned about table fields, which can then be merged back into the parent table type.

Example: 

// After narrowing t.x to string and t.y to number:
children := domain.NarrowedChildPaths("t@1")
// Returns: {"t@1.x": string, "t@1.y": number}

Returns an empty map if no child paths have narrowings.

func (*ProductDomain) TypeAt 

func (d *ProductDomain) TypeAt(key constraint.PathKey) typ.Type

TypeAt returns the narrowed type for a PathKey, combining all domain information.

This is the primary query method for retrieving type information after constraint application. It combines narrowings from multiple sources:

  1. Type domain narrowing: If the Type domain has a narrowed type for this key (from HasType, Truthy, etc. constraints), it takes precedence.

  2. Shape domain narrowing: If the Shape domain has a narrowed type (from structural constraints), it's considered.

  3. Combined narrowing: If both domains have narrowings, computes their intersection. A value must satisfy both type and shape constraints.

  4. Base type fallback: If no narrowings exist, falls back to env.PathTypeAt to retrieve the original declared or inferred type.

Returns nil if the path has no type information in any source.

Example usage: 

// After applying HasType(x, "string") constraint:
t := domain.TypeAt("x@1")  // Returns typ.String

// After applying field presence constraint:
t := domain.TypeAt("t@1")  // Returns record type with proven fields

The intersection semantics ensure soundness: if Type domain says "string" and Shape domain says "has field .len", the result is their intersection (which would be string, since strings have .len in Lua).

type ReturnCorrelation 

type ReturnCorrelation struct {
	ValueIndex int
	ErrorIndex int
}

ReturnCorrelation describes a correlated (value, error) pair in a multi-return. Derived from effect.ErrorReturn on the callee's spec.

type ReturnExprConstraints 

type ReturnExprConstraints struct {
	OnTrue  constraint.Condition
	OnFalse constraint.Condition
}

ReturnExprConstraints holds constraints extracted from a return expression.

type ReturnKind 

type ReturnKind uint8

ReturnKind classifies the constant value of a return statement for predicate analysis. Used to determine if a return is definitively true, false, or dynamic. 

const (
	ReturnUnknown ReturnKind = iota
	ReturnTrue               // return true
	ReturnFalse              // return false
)

type SiblingAssignment 

type SiblingAssignment struct {
	Symbols             []cfg.SymbolID           // Symbol IDs in order (primary identity)
	Names               []string                 // Variable names (for constraint path construction)
	Types               []typ.Type               // Declared types for each variable
	Correlations        []ReturnCorrelation      // Inverse correlations (ErrorReturn): value nil <-> error non-nil
	CoCorrelations      []ReturnCorrelation      // Same-direction correlations (CorrelatedReturn): all nil or all non-nil
	GuardedCorrelations []GuardedTypeCorrelation // Branch-sensitive type narrowing from guard/result relations
}

SiblingAssignment tracks variables assigned from the same multi-return call. Used for error return pattern: `local result, err = call()` where checking err narrows result.

type SiblingKey 

type SiblingKey struct {
	Symbol    cfg.SymbolID
	VersionID int
}

SiblingKey uniquely identifies a variable in a sibling assignment by SymbolID+SSA version.

type Solution 

type Solution struct {
	// contains filtered or unexported fields
}

Solution holds flow-narrowed types for all paths after solving.

Solution is the result of running flow analysis on a function's CFG. It maps versioned path keys to their narrowed types at each program point, taking into account control flow constraints, assignments, and phi merges.

The solver uses a worklist algorithm that propagates types through the CFG until reaching a fixed point. Edge conditions from conditionals narrow types along specific branches, while phi nodes merge types from different paths.

func Solve 

func Solve(inputs *Inputs, resolver narrow.Resolver) *Solution

Solve computes flow analysis and returns the solution.

Solve is the main entry point for flow-sensitive type analysis. It takes the analysis inputs (CFG, declared types, assignments, constraints) and a type resolver, then computes narrowed types at each program point.

The algorithm:

  1. Builds edge conditions from input constraints
  2. Checks numeric constraints to mark unreachable edges
  3. Propagates conditions through the CFG to compute point conditions
  4. Runs worklist iteration to compute final narrowed types

func (*Solution) ArrayLenBoundAt 

func (s *Solution) ArrayLenBoundAt(p cfg.Point, varName string) (arrKey string, ok bool)

ArrayLenBoundAt returns the array key if the variable has an array length upper bound.

func (*Solution) ArrayLenBoundWithOffsetAt added in v1.5.8 

func (s *Solution) ArrayLenBoundWithOffsetAt(p cfg.Point, varName string) (arrKey string, offset int64, ok bool)

ArrayLenBoundWithOffsetAt returns the array key and offset for a symbolic length bound.

func (*Solution) BoundsAt 

func (s *Solution) BoundsAt(p cfg.Point, name string) (lower, upper int64, ok bool)

BoundsAt returns the integer bounds for a variable at a CFG point.

func (*Solution) ConditionAt 

func (s *Solution) ConditionAt(p cfg.Point) constraint.Condition

ConditionAt returns the full DNF condition at a CFG point.

func (*Solution) ConstValueAt 

func (s *Solution) ConstValueAt(p cfg.Point, name string) *ConstValue

ConstValueAt returns a constant value for a name at a CFG point.

func (*Solution) ConstValueAtSym 

func (s *Solution) ConstValueAtSym(p cfg.Point, sym cfg.SymbolID) *ConstValue

ConstValueAtSym returns a constant value for a SymbolID at a CFG point.

func (*Solution) DebugEdgeCondition 

func (s *Solution) DebugEdgeCondition(from, to cfg.Point) constraint.Condition

DebugEdgeCondition returns the condition stored for a specific edge.

func (*Solution) DebugEdgeValues 

func (s *Solution) DebugEdgeValues(from, to cfg.Point) map[string]typ.Type

DebugEdgeValues returns nil (edge values removed in single narrowing system consolidation).

func (*Solution) DebugIterations 

func (s *Solution) DebugIterations() int

DebugIterations returns worklist iterations used for convergence.

func (*Solution) DebugValueAt 

func (s *Solution) DebugValueAt(key string, p cfg.Point) typ.Type

DebugValueAt returns the raw value stored for a version key.

func (*Solution) DebugVersionValues 

func (s *Solution) DebugVersionValues() map[string]typ.Type

DebugVersionValues returns the version values for debugging.

func (*Solution) DebugVersionedKey 

func (s *Solution) DebugVersionedKey(root string, p cfg.Point) string

DebugVersionedKey returns the canonical key for root at point.

func (*Solution) DeclaredAt 

func (s *Solution) DeclaredAt(p cfg.Point, sym cfg.SymbolID) TypedValue

DeclaredAt returns the declared (annotated) type for a symbol. Lookup order: LiteralTypes > SiblingTypes (captured vars) > DeclaredTypes. Returns typ.Unknown if no declaration exists.

func (*Solution) EffectiveTypeAt 

func (s *Solution) EffectiveTypeAt(p cfg.Point, sym cfg.SymbolID) TypedValue

EffectiveTypeAt returns the best available type: refined if exists, else declared.

func (*Solution) ExcludesTypeAt 

func (s *Solution) ExcludesTypeAt(p cfg.Point, path constraint.Path, t typ.Type) bool

ExcludesTypeAt checks if a NotHasType constraint applies to the path at point p.

func (*Solution) HasKeyOf 

func (s *Solution) HasKeyOf(p cfg.Point, tablePath, keyPath constraint.Path) bool

HasKeyOf checks if a KeyOf constraint exists at point p for the given table and key paths.

func (*Solution) IsAnnotated 

func (s *Solution) IsAnnotated(sym cfg.SymbolID) bool

IsAnnotated returns true if the symbol has an explicit type annotation.

func (*Solution) IsEdgeUnreachable 

func (s *Solution) IsEdgeUnreachable(from, to cfg.Point) bool

IsEdgeUnreachable returns true if edge's numeric constraints are unsatisfiable.

func (*Solution) IsPointDead 

func (s *Solution) IsPointDead(p cfg.Point) bool

IsPointDead returns true if the given CFG point is unreachable due to divergence.

func (*Solution) NarrowedTypeAt 

func (s *Solution) NarrowedTypeAt(p cfg.Point, path constraint.Path) typ.Type

NarrowedTypeAt returns the type at point p for path, narrowed by the DNF condition. This is a pure query that composes: baseTypeAt + ConditionAt + applyCondition.

func (*Solution) RefinedAt 

func (s *Solution) RefinedAt(p cfg.Point, sym cfg.SymbolID) TypedValue

RefinedAt returns the flow-narrowed type for a symbol at a point. Returns TypedValue with nil Type if no refinement exists.

func (*Solution) TypeAt 

func (s *Solution) TypeAt(p cfg.Point, path constraint.Path) typ.Type

TypeAt returns the type for a path at a CFG point using canonical keys.

func (*Solution) UnreachableEdges 

func (s *Solution) UnreachableEdges() []cfg.Edge

UnreachableEdges returns all edges proven unreachable by constraint analysis.

An edge is unreachable when its guard condition is unsatisfiable given the types flowing into it. This enables dead code detection and exhaustiveness checking for control flow.

type SymbolTypes 

type SymbolTypes = map[cfg.Point]map[cfg.SymbolID]TypedValue

SymbolTypes is the per-point symbol type map.

type TableMutatorAssignment 

type TableMutatorAssignment struct {
	Point     cfg.Point
	Target    constraint.Path // Base table path (or base map path for indexed targets)
	KeyVar    string          // Variable name if key is an identifier
	KeySymbol cfg.SymbolID    // Symbol ID for the key variable (for SSA-aware lookup)
	KeyType   typ.Type        // Optional explicit key type (overrides KeySymbol lookup)
	ValuePath constraint.Path // Path to value expression for flow-resolved type lookup
	ValueType typ.Type        // Fallback type if ValuePath doesn't resolve
}

TableMutatorAssignment describes table.insert-like mutations that widen array element types. If KeySymbol/KeyType is set, the target is treated as a map index (e.g., suites[suite]) and the map value's array element type is widened.

type TypeDecomposer 

type TypeDecomposer interface {
	ElementType(t typ.Type) typ.Type
	KeyType(t typ.Type) typ.Type
	ValueType(t typ.Type) typ.Type
}

TypeDecomposer extracts element, key, and value types from composite types. Used by the flow solver for iterator and container element derivation without depending on query/core.

type TypeFacts 

type TypeFacts interface {
	// DeclaredAt returns the declared (annotated) type for a symbol at a point.
	// Returns typ.Unknown if no declaration exists.
	DeclaredAt(p cfg.Point, sym cfg.SymbolID) TypedValue

	// RefinedAt returns the flow-narrowed type for a symbol at a point.
	// Returns TypedValue with nil Type if no refinement exists.
	RefinedAt(p cfg.Point, sym cfg.SymbolID) TypedValue

	// EffectiveTypeAt returns the best available type: refined if exists, else declared, else unknown.
	EffectiveTypeAt(p cfg.Point, sym cfg.SymbolID) TypedValue

	// IsAnnotated returns true if the symbol has an explicit type annotation.
	IsAnnotated(sym cfg.SymbolID) bool
}

TypeFacts provides phase-safe type access by separating declared types from refined types.

The interface has three access methods with distinct semantics:

  • DeclaredAt: Returns type from annotations only (SiblingTypes > DeclaredTypes). Never includes types synthesized from RHS expressions.

  • RefinedAt: Returns type from flow analysis only. Returns nil Type if the symbol has no flow-narrowed type at this point.

  • EffectiveTypeAt: Returns refined type if available, else declared type. This is the practical "best known type" for error checking.

This separation prevents early synthesis poisoning where:

  1. A variable gets an imprecise type from RHS before narrowing
  2. That type influences constraint extraction
  3. Constraints based on the imprecise type cause false errors or missed errors

type TypeState 

type TypeState uint8

TypeState tracks the resolution progress of a type during fixed-point iteration. The solver uses this to detect convergence and handle cyclic dependencies. 

const (
	StateUnknown    TypeState = iota // Type not yet resolved
	StateResolved                    // Type fully resolved
	StatePending                     // Type resolution in progress
	StateConflicted                  // Conflicting type assignments
)

type TypedValue 

type TypedValue struct {
	Type  typ.Type
	State TypeState
}

TypedValue pairs a type with its resolution state.

type UnifiedAssignment 

type UnifiedAssignment struct {
	Point      cfg.Point
	TargetPath constraint.Path
	SourcePath constraint.Path
	Type       typ.Type
	IterSource *IteratorSource // For iterator vars, derives type from source at solve time

	// ContainerElementSource tracks assignments from container methods (e.g., channel:receive())
	// that return element types. At solve time, the type is derived from the container's
	// widened element type instead of using the statically extracted Type field.
	ContainerElementSource *ContainerElementSource

	// MapElementSource tracks assignments from dynamic map index reads (t[k]).
	// At solve time, the type is derived from the map's value type instead of
	// using the statically extracted Type field.
	MapElementSource *MapElementSource
}

UnifiedAssignment describes an assignment in the CFG with typed info.

type WideningEvent 

type WideningEvent struct {
	Symbol   cfg.SymbolID   // Widened symbol
	SCCIndex int            // Index of the non-converged SCC
	SCC      []cfg.SymbolID // All symbols in the SCC
}

WideningEvent records when preflow inference widens a symbol to Unknown.

Source Files

View all Source files

Directories

Path Synopsis
Package domain provides abstract domain interfaces for constraint solving.
 Package domain provides abstract domain interfaces for constraint solving.
Package join provides type joining operations for phi node merging.
 Package join provides type joining operations for phi node merging.
domain.go implements the numeric subdomain for the flow solver's ProductDomain.
 domain.go implements the numeric subdomain for the flow solver's ProductDomain.
key.go provides path key construction and manipulation utilities.
 key.go provides path key construction and manipulation utilities.
Package propagate computes type constraints at CFG points via forward propagation.
 Package propagate computes type constraints at CFG points via forward propagation.

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.