Definite Assignment as a Flow-Sensitive Dataflow Problem

Name resolution answers which variable an identifier denotes. It does not answer whether that variable holds a value at that point in the program. In languages where reading an uninitialized local is an error rather than a defined-but-arbitrary read, the compiler must prove a property of the control-flow graph rather than of the syntax tree, and that proof is a forward dataflow analysis over the set of variables assigned so far.

Why scope is the wrong question

Lexical scope is a static containment relation: a variable declared in a block is visible throughout that block. Visibility says nothing about execution. A variable declared without an initializer and assigned only inside one branch of an if is visible at the merge point and may hold nothing.

int x;
if (cond) { x = 1; }
use(x);          // legal in C: x is indeterminate if cond was false

C permits this and leaves the value indeterminate, which is why reading it is undefined behaviour. Java and C# reject it, and the rejection is a compile-time guarantee: the language specification requires the compiler to prove that every read of a local variable occurs on a path where the variable was assigned. The guarantee is worth the analysis because it makes the value of a local total — there is no such thing as an indeterminate local — which in turn lets the verifier and the JIT treat locals uniformly.

The property is not a property of a variable in isolation, and it is not compositional in the syntax tree, which is also why it cannot be folded into the scope walk described in Resolving Identifier Uses Against a Stack of Lexical Scopes. A statement’s effect depends on what is true before it, and a construct with multiple successors requires the analysis to combine states from each incoming edge. That is the definition of a dataflow problem.

The lattice and the direction

The natural formulation uses a forward analysis over the control-flow graph. The state at a program point is the set of variables that are definitely assigned on every path from the function entry to that point. The meet operation at a join is set intersection: a variable is definitely assigned after a branch only if it is definitely assigned on both arms.

The domain is the powerset of local variables, ordered by reverse inclusion: a larger set carries more information, so the top element is the set of all variables and the bottom is the empty set. Intersection is the meet under that order, which makes this a “must” analysis computing a property that holds on every path. Every node except the entry starts at the top element and the sets shrink as the analysis discovers assignments that may not have happened; the entry starts at whatever holds before the first statement, which is the parameters plus any variables the language treats as initialized. The dual question, “may be assigned on some path”, is ordered by inclusion, uses union as its join, and starts at the bottom; it is the property a warning about a possibly-uninitialized read would need.

Iteration proceeds by worklist. Each node has an in-set and an out-set; a node’s in-set is the intersection of its predecessors’ out-sets, and its out-set is the in-set plus whatever the node assigns. When an out-set changes, its successors are re-added to the worklist. The analysis terminates because the lattice is finite and the transfer functions are monotone: a smaller in-set can only produce a smaller out-set, so each node’s value changes at most as many times as there are variables.

The cost is bounded by the number of edges times the height of the lattice times the cost of the transfer function. In the acyclic part of the graph each node’s in-set is final the first time it is processed with all its predecessors settled, so the number of passes is driven by the nesting of loops rather than by the number of statements. A loop causes the only interesting iteration: the back edge carries the state from the loop body’s end to its head, and the head’s in-set shrinks as the analysis discovers that the body’s assignments may not have executed.

Transfer functions and the constructs that need care

A plain assignment adds its target to the set. A compound assignment such as x += 1 reads x before writing it, so it requires x to be already assigned and then adds it — a detail that a checker treating += as a write alone gets wrong.

Variable declarations are where the languages diverge. Java’s rule for a local declaration with an initializer is that the variable is definitely assigned after the declaration; a declaration without an initializer assigns nothing. C# is the same for locals. Go avoids the problem differently: every variable of a concrete type is initialized to its type’s zero value at the point of declaration, whether or not the declaration writes one, so a local is never indeterminate and the property holds without analysis. A variable declared with an untyped nil and given no type has no zero value to hold, which is why var x = nil is rejected at compile time rather than deferred to a definite-assignment check.

The constructs that require structural rules rather than plain dataflow are the ones with special semantics in the specification:

• && and || short-circuit, so the right operand is analyzed under the state after the left operand is known true (for &&) or false (for ||). A variable assigned in the right operand of && is not definitely assigned after the whole expression.
• The conditional operator analyzes each arm under the same incoming state and intersects the results.
• switch on a value analyzes each case under the state at the switch, plus whatever the preceding cases established for fall-through; a case reached only through fall-through inherits the preceding case’s out-state, and a case that cannot be reached contributes nothing to the intersection. Languages without fall-through analyze each case independently.
• try/catch/finally requires care: a catch block is reachable from any point in the try block where an exception could be thrown, and the variables that are definitely assigned at such a point must be assigned on every path to it. The finally block runs on both normal and exceptional exit, so its incoming state is the intersection of the two.
• Loops require the head’s in-set to include the state before the loop, and the analysis iterates until the back edge stops removing variables.

The special case of final and effectively final

Java’s rules attach a second property to the same analysis. A local declared final must be assigned exactly once, and a variable that is never reassigned after initialization is “effectively final” and may be captured by a lambda or an inner class.

Checking assignment count is not the same as checking definite assignment. Counting requires a second component in the lattice state: for each variable, whether it is unassigned, assigned once, or assigned more than once. The join for that component is not intersection but a conservative combination that marks a conflict whenever two incoming paths both assign. A variable assigned only inside a loop body illustrates why the plain set is not enough. After the loop it is not definitely assigned at all, because the body may never execute, yet a final declaration of it is still illegal, because a path that iterates twice writes it twice. So the exactly-once property is a per-path property, not a join over paths, and no lattice of assigned-sets can express it. Java states the rule as a set of structural constraints over statements — a variable is “definitely unassigned” before its declaration and “definitely assigned” after a write — and derives both properties from the same walk, which is why the specification reads as grammar rules rather than as a lattice.

Capturing adds another dimension: a variable captured by an inner lambda must be definitely assigned before the lambda is created, not merely before the lambda’s body runs. That is because the capture copies the value at creation time. A checker that analyzes the lambda body under the state at the lambda’s textual position, rather than under the state at the enclosing point where the lambda expression is evaluated, accepts programs that read a variable assigned later.

A worklist implementation

The core of the analysis is short. The interesting parts are the graph construction and the per-node transfer, both of which are language-specific.

def definite_assignment(cfg, entry, assigned_at_entry):
    IN, OUT = {}, {}
    work = [entry]
    while work:
        node = work.pop()
        preds = cfg.preds(node)
        if node is entry:
            in_set = frozenset(assigned_at_entry)
        elif not preds:
            in_set = frozenset(cfg.variables())   # unreachable: no information lost
        else:
            if any(p not in OUT for p in preds):
                work.append(node)                 # predecessor not settled yet
                continue
            in_set = frozenset.intersection(*(OUT[p] for p in preds))
        out_set = transfer(node, in_set)
        if IN.get(node) != in_set or OUT.get(node) != out_set:
            IN[node], OUT[node] = in_set, out_set
            work.extend(cfg.succs(node))
    return IN, OUT

The worklist starts at the entry node with the set that holds on function entry, which is the parameters together with whatever the language treats as initialized. A node with no predecessors that is not the entry is unreachable, and there the analysis keeps the maximum rather than the minimum: it starts from the universal set, so that no definite-assignment error is reported for code that is never executed. A join is evaluated only when every predecessor’s out-set has been computed, which the loop enforces by re-queueing a node whose predecessors are still unsettled; the comparison against the previously stored sets, not a visited flag, is what drives re-visits.

transfer must be monotone with respect to the information order: whenever s1 contains everything s2 does, transfer(n, s1) contains everything transfer(n, s2) does. Every rule above satisfies this, which is what makes the fixpoint exist and the iteration terminate. A transfer function that removes a variable from the set when the variable’s scope ends breaks that property, because a smaller incoming set no longer maps to a smaller outgoing set, and the analysis can then revisit the same node indefinitely. The fix is to model scoping by tracking which variables are in scope at each node and intersecting the definite set with that, not by deleting during transfer.

Diagnostic quality and the interaction with resolution

The analysis produces the set at each node; the error is raised at a read whose variable is not in the set. Two refinements make the diagnostic useful.

The first is path-sensitivity in the message. “Variable x might not have been initialized” is the correct phrasing for a merge point, and it should name the branch that skipped the assignment when the analysis can reconstruct one. Reconstructing the path requires either a backward search over the graph or the analysis to retain, per variable, a witness predecessor. Retaining a single witness per variable per node costs one pointer and turns a vague message into a specific one.

The second is interaction with error recovery. A read of an unassigned variable should not poison the variable’s type, only flag the use, because the type is still known. But a variable whose declaration failed to resolve has no type, and the analysis should treat it as assigned to avoid a cascade — the same principle as binding failed names to a synthetic error binding, described in Error Types and Recovery in a Type Checker.

Finally, the analysis needs the control-flow graph, which means it cannot run during the syntax-directed walk that resolves names. It runs after resolution and after the graph is built, which places it after the checker’s main pass in a compiler that builds a graph per function, or as a second pass over the tree in a compiler that does not. The cost of not having a graph is a recursive formulation with the same lattice but a hand-written merge at each construct, which is more code and more places to get the intersection wrong. The graph-based formulation is worth building the graph for, and the same graph is reused by every other flow-sensitive check.