propagate

Documentation

Overview

Package propagate computes type constraints at CFG points via forward propagation.

Given edge conditions (constraints on control flow edges from conditionals), propagation computes the combined condition at each program point by merging conditions from all incoming paths. The result enables flow-sensitive type narrowing: at each point, the condition describes what type facts must hold.

The algorithm uses a worklist with RPO ordering for efficient convergence. Conditions are represented in DNF (disjunctive normal form) and combined using logical AND (through edges) and OR (at join points).

Index

• func FilterConditionSymbols(cond constraint.Condition, syms []cfg.SymbolID) constraint.Condition
• func KillRedefinedConditions(cond constraint.Condition, p cfg.Point, assignments []Assignment) constraint.Condition
• func PathAffectedByAssignment(cpath constraint.Path, assignSym cfg.SymbolID, assignSegs []constraint.Segment) bool
• type Assignment
• type EdgeConditions
• type EdgeKey
• type Graph
• type Inputs
• type Result
  • func Propagate(inputs *Inputs) *Result

Functions

func FilterConditionSymbols

func FilterConditionSymbols(cond constraint.Condition, syms []cfg.SymbolID) constraint.Condition

FilterConditionSymbols removes constraints that reference specified symbols.

This is used to filter out loop-variant constraints when reinforcing loop preheader conditions. If a variable is modified in the loop body, constraints about its preheader value are invalid on backedges.

For example, given loop "for i = 1, 10 do ... end", constraints on i from the preheader (i == 1) don't hold after the first iteration.

If any disjunct becomes empty after filtering, returns True (the constraint had no non-loop-variant component and should not restrict narrowing).

func KillRedefinedConditions

func KillRedefinedConditions(cond constraint.Condition, p cfg.Point, assignments []Assignment) constraint.Condition

KillRedefinedConditions removes constraints for paths assigned at a point.

When a variable is reassigned, constraints about its previous value become invalid. This function filters out such "killed" constraints to maintain soundness. Without killing, propagation would incorrectly conclude that preassignment constraints still hold.

Example: Given "if type(x) == 'string' then x = 5 end", after the assignment, the constraint HasType(x, string) must be killed because x is now a number.

The function checks each constraint path against each assignment at point p. If any constraint path is affected by an assignment, that constraint is removed.

func PathAffectedByAssignment

func PathAffectedByAssignment(cpath constraint.Path, assignSym cfg.SymbolID, assignSegs []constraint.Segment) bool

PathAffectedByAssignment checks if a constraint path is invalidated by an assignment.

A path is affected if:

1. The constraint path's symbol matches the assignment symbol
2. The assignment's segments are a prefix of (or equal to) the constraint's segments

Examples:

• Assigning to x affects x, x.foo, x.foo.bar (all have x's value)
• Assigning to x.foo affects x.foo, x.foo.bar (but not x or x.baz)
• Assigning to x.foo[0] affects x.foo[0], x.foo[0].bar (but not x.foo)

This captures that assigning to a path invalidates both the path itself and any nested paths that depend on the assigned value.

Types

type Assignment

type Assignment struct {
	// Point is the CFG point where the assignment occurs.
	Point cfg.Point
	// TargetSym is the symbol being assigned (provides unique identity).
	TargetSym cfg.SymbolID
	// TargetSegs specifies field path for nested assignments (x.foo.bar = ...).
	// Empty for simple variable assignments.
	TargetSegs []constraint.Segment
}

Assignment describes a variable assignment at a CFG point.

Used for constraint killing: when a variable is reassigned, constraints on that variable's previous value become invalid and must be removed from the propagated condition.

For example, after "x = 5", a prior constraint "type(x) == string" no longer applies because x now has a different value.

type EdgeConditions

type EdgeConditions map[EdgeKey]constraint.Condition

EdgeConditions maps CFG edges to their guard conditions.

An edge condition describes what must be true when control flows along that edge. For example, an if-then edge has a Truthy condition for the test expression, while the else edge has a Falsy condition.

type EdgeKey

type EdgeKey struct {
	From cfg.Point
	To   cfg.Point
}

EdgeKey identifies a CFG edge by its source and target points.

A CFG edge represents control flow from one program point to another. Edges have conditions when they come from conditional branches (if, while, etc.).

type Graph

type Graph interface {
	// Entry returns the entry point of the CFG (function start).
	Entry() cfg.Point
	// RPO returns CFG points in reverse postorder (optimal iteration order).
	RPO() []cfg.Point
	// Node returns the CFG node at point p, or nil if none.
	Node(p cfg.Point) *cfg.Node
	// Predecessors returns all CFG points that have edges to p.
	Predecessors(p cfg.Point) []cfg.Point
	// Successors returns all CFG points that p has edges to.
	Successors(p cfg.Point) []cfg.Point
}

Graph provides CFG traversal operations for propagation.

This interface abstracts the control flow graph, allowing propagation to work with any graph implementation that provides the required operations. Typically, this is a *cfg.CFG or cfg.VersionedGraph.

type Inputs

type Inputs struct {
	// Graph provides CFG traversal.
	Graph Graph
	// EdgeConditions maps edges to their guard conditions.
	EdgeConditions EdgeConditions
	// DeadPoints marks CFG points that are unreachable (e.g., after error()).
	// Propagation treats these as having False condition.
	DeadPoints map[cfg.Point]bool
	// Assignments lists all variable assignments for constraint killing.
	Assignments []Assignment
}

Inputs provides all data needed for constraint propagation.

The propagation algorithm uses these inputs to compute which conditions hold at each CFG point, accounting for edge conditions, dead code, and constraint killing from assignments.

type Result

type Result struct {
	// PointConditions maps CFG points to the conditions that hold there.
	// A point's condition is the OR of (predecessor condition AND edge condition)
	// for all incoming edges.
	PointConditions map[cfg.Point]constraint.Condition
}

Result holds the computed conditions at each CFG point.

After propagation, PointConditions maps each reachable CFG point to the disjunction of all path conditions that reach that point. Unreachable points have False conditions or are absent from the map.

func Propagate

func Propagate(inputs *Inputs) *Result

Propagate computes type constraints at each CFG point via forward dataflow.

This is the main entry point for constraint propagation. The algorithm:

1. Initialize entry point with True condition
2. Process points in worklist order (initially RPO for efficiency)
3. For each point, compute new condition from predecessors
4. If condition changed, add successors to worklist
5. Repeat until no changes (fixed point)

Condition computation at each point:

• For each predecessor with non-False condition:
• Combine predecessor condition with edge condition (AND)
• Apply loop preheader reinforcement for loop headers
• Kill constraints for reassigned variables
• Merge all incoming conditions (OR)

The result maps each point to its computed condition. Points unreachable from entry have False conditions (or are absent).