Lesson 5.7 — Control-flow-sensitive checks: reachability, missing returns, loop context and definite assignment¶
Techniques: structural reachability ("can complete normally") for missing returns and unreachable code, and loop-context checks for
break/continue(Java JLS §14.22; C#; rustc; pebble-spec §12.3–12.4), and definite assignment as a forward "must" dataflow problem on the AST — Java's JLS chapter 16 rules with "assigned when true/false", C#'s definite assignment, Swift's definite initialization (DI) on SIL, Rust's initialization checks in the MIR borrow checker (pebble-spec §12.2; a preview of Ch 14) · Pebble implements: all of them incheckFlow(exercises E5–E6);break/continuetargets inresolveNames(E3); drilldefinite-assignment· Prerequisites: Lessons 5.1–5.3; lattices and fixed points are defined here and generalized in Ch 14 · Time: 4 hours
Some errors are not about what a name means but about when it can be used: a function that can fall off its end without returning a value; a statement after return that can never run; a break with no loop around it; a variable read before anything was assigned to it. The first three are decided by the program's structure alone. The last needs a dataflow analysis: a variable is safe to read only if an assignment happened on every path that reaches the read. This lesson treats all four as the course's first flow analyses, proves the definite-assignment analysis sound, and shows how Java, C#, Swift and Rust state the same rules with different precision.
1. Problem and motivation¶
The problem. Given a resolved function body (every break/continue knows its loop, every name its declaration), report: (1) if the function has a result type and the end of its body is reachable (E0305); (2) statements that directly follow a jump (W0314); (3) break/continue outside a loop (E0304, found by resolveNames); (4) reads of scalar vars declared without an initializer that are not definitely assigned (E0306). The checks must be decidable, fast, predictable for programmers — two compilers must agree — and sound: an accepted program never reads an unassigned variable and never falls off the end of a value-returning function.
Reachability, missing returns and loop context¶
Exact reachability is undecidable (it would decide halting), so languages define a conservative, syntax-directed approximation. Java's rules [JLS21-14, §14.22] say which statements "can complete normally": a return cannot; a block cannot if any of its statements cannot; while (true) without a break cannot, because its condition is a constant expression. Java makes a statement that is not reachable by these rules an error; C#, Rust and Pebble make it a warning. Pebble's rules (pebble-spec §12.3) are simpler than Java's: loops are always assumed to complete, even while true, so a programmer writes an explicit return after an infinite loop. Loop-context checks are the easiest of all: a break outside a loop is found by name resolution's loop stack (Lesson 5.6's annotation BreakStmt::getTarget).
Definite assignment¶
C lets you read an uninitialized local and calls it undefined behavior; compilers warn heuristically (§7). Java made reading a local before assignment a compile-time error with precise rules — definite assignment, chapter 16 of the JLS [JLS21-16] — so that every compiler rejects exactly the same programs; C# adopted the same idea [CSHARP-DA]. Swift's definite initialization checks locals, let constants and the fields of self in initializers on SIL [SWIFT-DI]; Rust's borrow checker checks initialization (and moves) on MIR with a maybe-uninitialized dataflow analysis (error E0381). All of them are instances of one textbook problem — a forward, "must" (all paths) dataflow analysis over a lattice of variable sets [ALSU07, §9.2; EaC3, Ch. 9] — which Chapter 14 generalizes. Pebble's version (pebble-spec §12.2) tracks scalar vars without initializer; aggregates are zero-initialized and exempt.
2. Definitions and algorithms¶
Reachability, missing returns and loop context¶
Definition 5.7.1 (Can complete normally, Pebble's rules)
The predicate \(\mathrm{cc}(s)\) ("\(s\) can complete normally") is defined by structural recursion: \(\mathrm{cc}(\texttt{return}) = \mathrm{cc}(\texttt{break}) = \mathrm{cc}(\texttt{continue}) = \mathsf{false}\); \(\mathrm{cc}(\{ s_1 \cdots s_n \}) = \bigwedge_i \mathrm{cc}(s_i)\) (\(\mathsf{true}\) for an empty block); \(\mathrm{cc}(\texttt{if } c\ B) = \mathsf{true}\); \(\mathrm{cc}(\texttt{if } c\ B_1 \texttt{ else } B_2) = \mathrm{cc}(B_1) \lor \mathrm{cc}(B_2)\); \(\mathrm{cc}(\texttt{while} \cdots) = \mathrm{cc}(\texttt{for} \cdots) = \mathsf{true}\); every other statement can complete normally. A function with a result type is missing a return if \(\mathrm{cc}(\mathit{body})\). A statement is directly unreachable if it follows a return, break or continue in the same block.
Algorithm 5.7.2 (Structural flow checks)
- Input: a resolved function body; whether the function has a result type.
- Output: E0305 at the function name if a return is missing; W0314 at the first directly unreachable statement of each block.
- Precondition: name resolution succeeded (
break/continueoutside loops were already reported, E0304). - Postcondition: the diagnostics of pebble-spec §12.3–12.4.
- Invariant:
CanCompletereturns \(\mathrm{cc}(s)\) of Definition 5.7.1.
function CheckFunction(F):
if F has a result type and CanComplete(F.body): report E0305 at F's name
WarnUnreachable(F.body)
function CanComplete(s):
case s of
return, break, continue: return false
block B: return all(CanComplete(t) for t in B)
if c then B1 else B2: return CanComplete(B1) or CanComplete(B2)
if c then B1: return true
otherwise: return true # while and for included
function WarnUnreachable(s):
if s is a block with statements t1 … tn:
for i in 2..n:
if t(i−1) is return, break or continue: report W0314 at t(i); stop the loop
for each ti: WarnUnreachable(ti)
else: WarnUnreachable on every block nested directly in s
Definite assignment¶
Definition 5.7.3 (The definite-assignment lattice and transfer functions)
Let \(V\) be the tracked variables of a function. The state at a program point is either a set \(S \subseteq V\) (the variables definitely assigned there) or \(\mathsf{U}\) ("unreachable"). The order is \(S \sqsubseteq S' \iff S \subseteq S'\) and \(x \sqsubseteq \mathsf{U}\) for all \(x\); the meet is \(S \sqcap S' = S \cap S'\) with \(\mathsf{U}\) as identity (\(\mathsf{U} \sqcap x = x\)). This is a lattice of height \(\lvert V \rvert + 1\) with top \(\mathsf{U}\) and bottom \(\emptyset\). The transfer function \(f_s\) of a simple statement maps \(\mathsf{U}\) to \(\mathsf{U}\) and a set \(S\) to: \(S \cup \{x\}\) for x = e;; \(S \setminus \{x\}\) for the declaration var x: T; of a tracked \(x\); \(S\) for any other simple statement; and \(\mathsf{U}\) after return, break and continue (whose incoming state is sent to the function exit or the loop). A read of tracked \(x\) at a point with state \(S\) is legal iff \(S = \mathsf{U}\) or \(x \in S\).
Definition 5.7.4 (Meet over all paths)
Consider the control-flow graph of the body (Ch 8): conditions are not interpreted, so both branches of every if, and zero or more iterations of every loop, are possible. For a program point \(p\), \(\mathrm{MOP}(p) = \mathop{\Large\sqcap}_{\pi} f_{\pi}(\emptyset)\) over all paths \(\pi\) from the entry to \(p\), where \(f_\pi\) composes the transfer functions along \(\pi\) (\(\mathsf{U}\) if no path exists). Variable \(x\) is definitely assigned at \(p\) iff \(\mathrm{MOP}(p) = \mathsf{U}\) or \(x \in \mathrm{MOP}(p)\): every path from the entry to \(p\) assigns \(x\) after its last declaration.
Algorithm 5.7.5 (Definite assignment by structural dataflow on the AST)
- Input: a resolved function body; the tracked variables \(V\) (scalar
vars without initializer). - Output: the set of illegal reads; pebblec reports the first one of each variable (E0306).
- Precondition: every
break/continuetargets an enclosing loop; expressions do not assign (true in Pebble). - Postcondition: a read is reported iff it is illegal under \(\mathrm{MOP}\) (Theorem 5.7.8).
- Invariant:
Exec(s, S)returns the state after \(s\) completes normally, and adds to the innermost loop'sbreaks/continuesthe states at its jumps; each loop head's state only decreases across iterations.
function Exec(s, S):
case s of
block t1 … tn: for each ti: S ← Exec(ti, S); return S
var x: T (tracked): return S = U ? U : S − {x}
x = e (x tracked): CheckReads(e, S); return S = U ? U : S ∪ {x}
if c then B1 else B2: CheckReads(c, S); return Exec(B1, S) ⊓ Exec(B2, S) # no else: B2 = {}
while c { B }: return Loop(c, B, S)
for i in a..b { B }: CheckReads(a, S); CheckReads(b, S); return Loop(none, B, S)
break: loops.top.breaks ← loops.top.breaks ⊓ S; return U
continue: loops.top.continues ← loops.top.continues ⊓ S; return U
return e: CheckReads(e, S); return U
other statement: CheckReads(every expression of s, S); return S
function Loop(c, B, In):
head ← In
repeat
CheckReads(c, head)
push {breaks: U, continues: U} on loops
out ← Exec(B, head); ex ← pop loops
next ← In ⊓ out ⊓ ex.continues # the loop head's incoming edges
stable ← (next = head); head ← next
until stable
return head ⊓ ex.breaks # exit: condition false, or a break
function CheckReads(e, S): # `&x`, `&mut x`, `x += e` all read x
for each read of a tracked x in e:
if S ≠ U and x ∉ S: record (x, position) as illegal
3. Worked example¶
Reachability, missing returns and loop context¶
The functions of tests/ch05/Inputs/err-flow.pbl and the reference tool's verdicts:
| function body | \(\mathrm{cc}\) computation | verdict |
|---|---|---|
noret: { if n > 0 { return 1; } } |
if without else → true; block → true |
E0305 at noret |
looped: { while true { return 1; } } |
while → true (loops always complete) |
E0305 at looped |
pick: { if c { return 1; } else { return 2; } } |
then false, else false → false | no error |
dead: { var u: int; return 1; print(u); } |
return false → block false |
no E0305; W0314 at print(u) |
deadloop: while … { break; print(n); }, for … { continue; let a = 1; let b = 2; } |
W0314 at print(n) and at let a (once per block) |
ch05-resolve tests/ch05/Inputs/err-flow.pbl prints 1:4: error[E0305], 5:4: error[E0305], and 31:5, 37:9, 41:9: warning[W0314] — exactly these.
Definite assignment¶
The running program (every read numbered; k is an unknown condition):
fn f(k: bool) -> int {
var a: int;
var b: int;
b = 1;
while k {
if k { a = 1; continue; }
print(a); // r1
a = 2;
}
print(b); // r2
return a; // r3
}
Algorithm 5.7.5 (the trace format of the drill; states in braces, U = unreachable):
| step | statement | IN | OUT |
|---|---|---|---|
| 1 | b = 1 |
{} | {b} |
| 2 | while k: iteration 1, head |
{b} | {b} |
| 3 | if k (then) |
{b} | {b} |
| 4 | a = 1 |
{b} | {a, b} |
| 5 | continue (continues ← {a, b}) |
{a, b} | U |
| 6 | end if: meet(then = U, skip = {b}) |
{b} | {b} |
| 7 | print(a) r1 ✗ |
{b} | {b} |
| 8 | a = 2 |
{b} | {a, b} |
| 9 | head check: next = In ⊓ out ⊓ continues = {b} ⊓ {a, b} ⊓ {a, b} = {b} = head: stable; exit = head ⊓ breaks = {b} ⊓ U | {b} | {b} |
| 10 | print(b) r2 |
{b} | {b} |
| 11 | return a r3 ✗ |
{b} | U |
Illegal reads: r1 and r3. pebblec reports one E0306, at r1 (7:15, with a note at the declaration of a): after the first report the variable is poisoned (pebble-spec §12.2, Lesson 5.8).
The same problem on the CFG, round-robin in reverse postorder (the Ch 14 view; OUT initialized to ⊤ = U, which is what "start the head at In" encodes):
flowchart TD
B0(["B0: var a, b; b = 1"]) --> B1{"B1: while k"}
B1 -->|true| B2{"B2: if k"}
B2 -->|true| B3["B3: a = 1; continue"]
B3 --> B1
B2 -->|false| B4["B4: print(a) r1; a = 2"]
B4 --> B1
B1 -->|false| B5["B5: print(b) r2; return a r3"]| block | init OUT | pass 1 IN | pass 1 OUT | pass 2 IN | pass 2 OUT |
|---|---|---|---|---|---|
| B0 | U | {} | {b} | {} | {b} |
| B1 | U | {b} ⊓ U ⊓ U = {b} | {b} | {b} ⊓ {a,b} ⊓ {a,b} = {b} | {b} |
| B2 | U | {b} | {b} | {b} | {b} |
| B3 | U | {b} | {a, b} | {b} | {a, b} |
| B4 | U | {b} | {a, b} | {b} | {a, b} |
| B5 | U | {b} | U (return) | {b} | U |
- Pass 1: B1's back-edge predecessors B3 and B4 still hold U, the identity of ⊓, so IN[B1] is OUT[B0] alone — the same "head starts at In" as Algorithm 5.7.5.
- Pass 2: nothing changes; the fixed point is reached. r1 reads
awith IN[B4] = {b}: illegal; r3 readsawith IN[B5] = {b}: illegal; r2 is legal.
Try it
./course drill definite-assignment --seed 519 --difficulty hard --solution traces a generated program with nested loops and break; --difficulty easy drills if/else joins only.
4. Invariants and correctness¶
Reachability, missing returns and loop context¶
Theorem 5.7.6 (Structural reachability is conservative)
For every statement \(s\): if some execution of \(s\) (from some state, for some values of the conditions) completes normally, then \(\mathrm{cc}(s) = \mathsf{true}\). Consequently, if E0305 is not reported, no execution falls off the end of the function.
Proof
By structural induction on \(s\). Jumps: no execution of return, break or continue completes normally, and \(\mathrm{cc}\) is false — consistent (the claim is an implication). Block: an execution that completes normally executes every statement and each completes normally, so by the induction hypothesis \(\mathrm{cc}\) holds for each, and their conjunction is true. If with else: a normally completing execution runs one branch to normal completion, so that branch's \(\mathrm{cc}\) is true, hence the disjunction. If without else, loops, simple statements: \(\mathrm{cc}\) is true unconditionally. Consequence: falling off the end of the body is the body completing normally; if E0305 was not reported then \(\mathrm{cc}(\mathit{body})\) is false, so no execution does. The converse fails on purpose: while true { return 1; } never completes, but \(\mathrm{cc}\) says it may, and Pebble demands an explicit return (Java decides the constant condition and accepts it).
Definite assignment¶
Lemma 5.7.7 (Transfer functions are monotone and distributive)
Every transfer function of Definition 5.7.3 is monotone (\(x \sqsubseteq y \Rightarrow f(x) \sqsubseteq f(y)\)) and distributive (\(f(x \sqcap y) = f(x) \sqcap f(y)\)).
Proof
Each \(f\) is \(\mathsf{U} \mapsto \mathsf{U}\) and, on sets, \(S \mapsto (S \setminus \mathrm{kill}) \cup \mathrm{gen}\) (assignment: \(\mathrm{gen} = \{x\}\); declaration: \(\mathrm{kill} = \{x\}\)), or the constant \(\mathsf{U}\) (jumps). Distributivity: for sets, \(((S \cap S') \setminus K) \cup G = ((S \setminus K) \cup G) \cap ((S' \setminus K) \cup G)\) by the distributive laws of \(\cup\) and \(\cap\); if one argument is \(\mathsf{U}\), say \(x = \mathsf{U}\), then \(f(\mathsf{U} \sqcap y) = f(y) = \mathsf{U} \sqcap f(y) = f(\mathsf{U}) \sqcap f(y)\); the constant function \(\mathsf{U}\) is trivially distributive. Monotonicity follows from distributivity: \(x \sqsubseteq y\) means \(x = x \sqcap y\), so \(f(x) = f(x) \sqcap f(y) \sqsubseteq f(y)\).
Theorem 5.7.8 (Algorithm 5.7.5 terminates and computes the meet over all paths)
Algorithm 5.7.5 terminates, and the state it computes at every read equals \(\mathrm{MOP}\) of Definition 5.7.4. Hence it reports a read iff some path from the entry reaches the read without assigning the variable after its declaration.
Proof
Termination: each Loop iteration computes \(\mathit{next} = \mathit{In} \sqcap \dots \sqsubseteq \mathit{In}\), and by monotonicity (Lemma 5.7.7) of the composed body function, the sequence of head states is descending: \(\mathit{head}_1 = \mathit{In} \sqsupseteq \mathit{head}_2 \sqsupseteq \cdots\) (induction: if \(\mathit{head}_{j+1} \sqsubseteq \mathit{head}_j\) then \(\mathit{out}_{j+1} \sqsubseteq \mathit{out}_j\), so \(\mathit{head}_{j+2} \sqsubseteq \mathit{head}_{j+1}\)). A strictly descending chain in a lattice of height \(\lvert V \rvert + 1\) has at most \(\lvert V \rvert + 1\) steps, and nested loops terminate by induction on nesting.
Fixed point: when Loop stops, \(\mathit{head} = \mathit{In} \sqcap F(\mathit{head})\) where \(F\) collects the states at the end of the body and at the continues. It is the greatest solution below \(\mathit{In}\): any solution \(h\) satisfies \(h \sqsubseteq \mathit{In} = \mathit{head}_1\), and if \(h \sqsubseteq \mathit{head}_j\) then \(h = \mathit{In} \sqcap F(h) \sqsubseteq \mathit{In} \sqcap F(\mathit{head}_j) = \mathit{head}_{j+1}\). The states computed by Exec are therefore the maximal fixed point (MFP) of the dataflow equations of the CFG (the structural recursion is the CFG's equations solved block by block, loops innermost first).
MFP = MOP: for a monotone framework, \(\mathrm{MFP} \sqsubseteq \mathrm{MOP}\); for a distributive one they are equal (Kam and Ullman [KU77]; Ch 14 proves it). Lemma 5.7.7 gives distributivity, so the computed states are exactly \(\mathrm{MOP}\). The final statement is Definition 5.7.4 unfolded: \(x \notin \mathrm{MOP}(p)\) with \(\mathrm{MOP}(p) \ne \mathsf{U}\) iff some path to \(p\) ends with \(x\) not assigned since its last declaration.
Corollary 5.7.9 (Soundness: accepted programs never read an unassigned variable)
If Algorithm 5.7.5 reports no illegal read, then in every execution every read of a tracked variable happens after an assignment to it (since its most recent declaration).
Proof
An execution follows a path of the CFG in which each if takes one branch and each loop runs some number of times — one of the paths of Definition 5.7.4 (conditions are uninterpreted, so every executed path is a path of the CFG). If a read of \(x\) at \(p\) happened with \(x\) unassigned, that path would witness \(x \notin f_\pi(\emptyset)\), hence \(x \notin \mathrm{MOP}(p)\) and \(\mathrm{MOP}(p) \ne \mathsf{U}\) (the path exists), and by Theorem 5.7.8 the read would have been reported.
Lemma 5.7.10 (In Pebble, every loop stabilizes after one iteration)
In Algorithm 5.7.5, \(\mathit{head}_2 = \mathit{head}_1\) for every loop, so the repeat runs exactly twice (one pass and one confirming comparison).
Proof
Let \(\mathit{In} \ne \mathsf{U}\) (otherwise everything is \(\mathsf{U}\)). For a variable declared outside the loop, no statement of the body kills it (the only kill is its own declaration, which is outside), so along every path through the body the set can only grow: \(x \in \mathit{In}\) implies \(x \in \mathit{out}\) and \(x\) in every continue state (or those are \(\mathsf{U}\)). For a variable declared inside the body, \(x \notin \mathit{In}\): before the loop runs, its declaration has not been executed on any path, and the function starts from \(\emptyset\). So \(\mathit{In} \sqcap \mathit{out} \sqcap \mathit{continues}\) agrees with \(\mathit{In}\) on every variable, i.e. \(\mathit{head}_2 = \mathit{In} = \mathit{head}_1\). (In Java, while (true) and blank final fields break this lemma, and so do analyses whose transfer functions kill variables declared outside the loop — Chapter 14's liveness, for example.)
5. Complexity¶
Variables: \(n\) statements and expressions of the function; \(\lvert V \rvert\) tracked variables; \(w\) the machine word size; \(\ell\) the maximum loop nesting depth.
| Technique | Time | Space | Pathological input |
|---|---|---|---|
| Structural reachability (Alg. 5.7.2) | \(\Theta(n)\) (one recursion per statement, plus one scan per block) | \(O(\text{nesting depth})\) | none |
| Loop-context check | \(\Theta(n)\) inside name resolution (a loop stack) | \(O(\ell)\) | none |
| Definite assignment, Alg. 5.7.5 with bit vectors | as written, \(O(2^{\ell}\, n \lceil \lvert V \rvert / w \rceil)\) (each loop body twice per enclosing iteration); with loops memoized by entry state, \(O(n \lceil \lvert V \rvert / w \rceil)\) in Pebble | \(O(\lvert V \rvert / w)\) words per live state, plus one memo entry per loop | \(\ell\) nested loops without the memo: the work doubles per level |
| Definite assignment on a CFG (worklist, Ch 14) | \(O(e \cdot h \cdot \lceil \lvert V \rvert / w \rceil)\) with \(h = \lvert V \rvert + 1\); in RPO, \(d(G) + 2\) passes | \(O(\text{blocks} \cdot \lvert V \rvert / w)\) | none beyond the bound |
Justification. A bit-vector meet or transfer costs one pass over \(\lceil \lvert V \rvert / w \rceil\) words. In Algorithm 5.7.5 each loop's body is executed once per repeat iteration, i.e. twice (Lemma 5.7.10), and an inner loop is re-executed inside each outer iteration, which gives the \(2^{\ell}\) factor. The reference checkFlow avoids it by memoizing each loop by its entry state: a loop entered again with a state it has already been analyzed from (typically during the confirming iteration of an enclosing loop) returns its recorded exit state, and its illegal reads were already recorded. By Lemma 5.7.10 every loop is entered with at most one distinct state per enclosing analysis, so each body is evaluated at most twice in total: \(O(n \lceil \lvert V \rvert / w \rceil)\) for the whole function. The test E6_DeeplyNestedLoopsStayFast (40 nested loops, \(2^{40}\) evaluations without the memo) enforces it. A CFG-based worklist solver has no such factor: every block is visited \(O(h)\) times [KU77; Ch 14], and on reducible CFGs in reverse postorder \(d(G) + 2\) passes suffice (\(d\) = loop connectedness).
6. Variants and refinements¶
Reachability, missing returns and loop context¶
- Constant conditions (Java, C#):
while (true)withoutbreakcannot complete normally,if (false)is deliberately not treated as unreachable (to allow conditional compilation) [JLS21-14, §14.22]. - Never-returning calls (
noreturnin C,-> !in Rust,Neverin Swift): a call to such a function cannot complete normally, which removes spurious "missing return" diagnostics afterpanic!orabort(). - Labeled
break/continue(Java, Rust, Swift): the target is found by label instead of the innermost loop; the loop stack becomes a map from labels to loops.
Definite assignment¶
- Assigned when true / when false (JLS §16.1): because Java expressions can assign (
(x = f()) != 0 && …), the analysis tracks two states per boolean expression, so thatif (a && (x = 1) > 0) use(x);is legal. Pebble's expressions never assign, so one state suffices. - Definitely unassigned (JLS §16, for blank
finalvariables): the dual "may" analysis that checks afinalis assigned at most once; Swift's DI checks the same forlet. - Field-sensitive initialization (Swift DI for
selfin initializers; Rust for struct fields and moves): the tracked "variables" are fields and element paths, and moves (Rust) un-assign a place; Rust'sMaybeUninitializedPlacesis the may-dual of this lesson's must-analysis, run on MIR. - Warnings instead of errors (Clang
-Wsometimes-uninitialized, GCC-Wmaybe-uninitialized): C does not forbid the read, so compilers warn, Clang from a CFG-based analysis at-O0, GCC from the optimized SSA form (so its warnings depend on the optimization level, §7).
7. In real compilers¶
Reachability, missing returns and loop context¶
javac: Flow.AliveAnalyzer implements JLS §14.22 and reports "missing return statement" and "unreachable statement" (src/jdk.compiler/share/classes/com/sun/tools/javac/comp/Flow.java, jdk-21+35 [JAVAC-Flow]). Clang: CheckFallThroughForBody in clang/lib/Sema/AnalysisBasedWarnings.cpp [CLANG-ABW] (-Wreturn-type, from the CFG). rustc: unreachable code is a lint computed during type checking; break outside a loop is E0268 (compiler/rustc_hir_typeck/src/errors.rs [RUSTC-TypeckErrors]).
Missing returns and unreachable code in javac 21 and rustc 1.94
Reproduce (javac 21.0.10, rustc 1.94.1):
mkdir -p j2 && cat > j2/Flow.java <<'EOF'
class Flow {
static int sign(int n) {
int s;
if (n < 0) s = -1; else if (n > 0) s = 1;
return s; // not definitely assigned when n == 0
}
static int loop(boolean c) {
int x;
while (true) { if (c) { x = 1; break; } }
return x; // OK: while (true) exits only through break
}
static int noReturn(int n) {
if (n > 0) return 1;
} // missing return
static void dead() {
return;
System.out.println("never"); // unreachable statement is an error in Java
}
static final int k; // a blank final must be definitely assigned once
static { k = 1; }
}
EOF
javac -d j2 j2/Flow.java
mkdir -p rs2 && cat > rs2/flow.rs <<'EOF'
fn sign(n: i32) -> i32 {
let s: i32;
if n < 0 { s = -1; } else if n > 0 { s = 1; }
s
}
fn dead() -> i32 {
return 1;
println!("never");
}
fn main() {
break;
println!("{} {}", sign(1), dead());
}
EOF
rustc --edition 2021 rs2/flow.rs -o rs2/flow
Output (complete; javac, then rustc):
j2/Flow.java:14: error: missing return statement
} // missing return
^
j2/Flow.java:17: error: unreachable statement
System.out.println("never"); // unreachable statement is an error in Java
^
j2/Flow.java:5: error: variable s might not have been initialized
return s; // not definitely assigned when n == 0
^
3 errors
warning: unreachable statement
--> rs2/flow.rs:8:5
|
7 | return 1;
| -------- any code following this expression is unreachable
8 | println!("never");
| ^^^^^^^^^^^^^^^^^ unreachable statement
|
= note: `#[warn(unreachable_code)]` (part of `#[warn(unused)]`) on by default
= note: this warning originates in the macro `println` (in Nightly builds, run with -Z macro-backtrace for more info)
error[E0268]: `break` outside of a loop or labeled block
--> rs2/flow.rs:11:5
|
11 | break;
| ^^^^^ cannot `break` outside of a loop or labeled block
error[E0381]: used binding `s` is possibly-uninitialized
--> rs2/flow.rs:4:5
|
2 | let s: i32;
| - binding declared here but left uninitialized
3 | if n < 0 { s = -1; } else if n > 0 { s = 1; }
| ----- - an `else` arm might be missing here, initializing `s`
| |
| if this `if` condition is `false`, `s` is not initialized
4 | s
| ^ `s` used here but it is possibly-uninitialized
error: aborting due to 2 previous errors; 1 warning emitted
Some errors have detailed explanations: E0268, E0381.
For more information about an error, try `rustc --explain E0268`.
What to notice: javac's noReturn is Pebble's noret (E0305), and its unreachable statement is an error where Rust (and Pebble, W0314) only warn. javac accepts loop: Java decides the constant while (true), so return x is reached only through the break, where x is assigned — under Pebble's rules (loops may exit at the condition) the same program would get E0306. rustc finds break outside a loop (E0268) during resolution/type checking, like Pebble's resolveNames (E0304).
Definite assignment¶
javac: Flow.AssignAnalyzer tracks inits and uninits bit sets, with separate "when true/when false" sets for conditions (Flow.java, jdk-21+35 [JAVAC-Flow]). Roslyn: DefiniteAssignmentPass (src/Compilers/CSharp/Portable/FlowAnalysis/DefiniteAssignment.cs, Visual-Studio-2022-Version-17.8 [ROSLYN-DA]). Swift: lib/SILOptimizer/Mandatory/DefiniteInitialization.cpp checks locals, lets and self's stored properties on SIL (swift-6.1-RELEASE [SWIFT-DIsrc]; not runnable here). rustc: E0381 comes from the MIR borrow checker's maybe-uninitialized analysis (report_use_of_moved_or_uninitialized in compiler/rustc_borrowck/src/diagnostics/conflict_errors.rs, rustc 1.94.1 [RUSTC-Borrowck]); the E0381 output is in the box above. Clang: runUninitializedVariablesAnalysis (clang/lib/Analysis/UninitializedValues.cpp [CLANG-Uninit]); GCC: warn_uninitialized_vars on SSA (gcc/tree-ssa-uninit.cc, gcc-15 [GCC-Uninit]).
Uninitialized reads in C: Clang 23 at -O0, GCC 14 only after optimization
Reproduce (clang 23.1.2, gcc 14.2.0):
cat > flow.c <<'EOF'
int sign(int n) {
int s;
if (n < 0) s = -1; else if (n > 0) s = 1;
return s;
}
int noret(int n) {
if (n > 0) return 1;
}
EOF
clang-23 -fsyntax-only -Wall flow.c
gcc-14 -fsyntax-only -Wall flow.c
gcc-14 -c -Wall -O2 flow.c -o /dev/null
Output (complete; Clang, then GCC with -fsyntax-only (nothing), then GCC with -O2):
flow.c:3:31: warning: variable 's' is used uninitialized whenever 'if' condition is false [-Wsometimes-uninitialized]
3 | if (n < 0) s = -1; else if (n > 0) s = 1;
| ^~~~~
flow.c:4:10: note: uninitialized use occurs here
4 | return s;
| ^
flow.c:3:27: note: remove the 'if' if its condition is always true
3 | if (n < 0) s = -1; else if (n > 0) s = 1;
| ^~~~~~~~~~
flow.c:2:8: note: initialize the variable 's' to silence this warning
2 | int s;
| ^
| = 0
flow.c:8:1: warning: non-void function does not return a value in all control paths [-Wreturn-type]
8 | }
| ^
2 warnings generated.
flow.c: In function 'noret':
flow.c:8:1: warning: control reaches end of non-void function [-Wreturn-type]
8 | }
| ^
flow.c: In function 'sign':
flow.c:4:10: warning: 's' may be used uninitialized [-Wmaybe-uninitialized]
4 | return s;
| ^
flow.c:2:7: note: 's' was declared here
2 | int s;
| ^
What to notice: the same two checks as Pebble's E0306 and E0305, as warnings (C allows the read). Clang runs a CFG dataflow analysis in the front end, so it warns even with -fsyntax-only and names the path ("whenever 'if' condition is false" — the path of Definition 5.7.4 that lacks the assignment). GCC's warnings come from the optimizer's SSA form: nothing with -fsyntax-only, and their exact set depends on the optimization level — the unpredictability that Java's and Pebble's specified rules avoid.
8. Comparison¶
| Technique | Power / precision | Speed (asymptotic · practical) | Output / error quality | Implementation effort | Typical use |
|---|---|---|---|---|---|
| Reachability, missing returns and loop context | Conservative (Theorem 5.7.6): never misses a fall-off; rejects some infinite loops without return (Pebble) or decides constant conditions (Java) |
\(\Theta(n)\), one structural pass | Precise locations; predictable because specified per construct | Lowest | Every statically checked language; E0304/E0305/W0314 in pebblec |
| Definite assignment (dataflow) | Exactly MOP for gen/kill rules (Theorem 5.7.8); sound (Corollary 5.7.9); conditions uninterpreted | \(O(n \lceil \lvert V \rvert / w \rceil)\) per pass, 2 passes per loop in Pebble (Lemma 5.7.10) | One error per variable at the first bad read, with a note at the declaration; Clang/rustc explain the missing branch | Low–medium (bit vectors, loop fixed points, jump states) | Java, C#, Swift DI, Rust (E0381), Pebble (E0306); C compilers as warnings |
Choose structural rules for reachability and returns: they are cheap, and programmers can predict them from the syntax. Decide constant conditions (Java) only if you are willing to specify exactly which expressions are constant. Choose a specified dataflow rule for definite assignment instead of optimizer-based warnings: the verdict must not depend on -O. Track "when true/false" states only if expressions can assign, and fields/moves only if the language has in-place initialization or moves (Swift, Rust).
9. Assessment¶
| Technique | Quiz ids | Drill | Flashcard tag | Exercises |
|---|---|---|---|---|
| Reachability, missing returns and loop context | cc-verdicts, java-while-true, find-clang-fallthrough |
— (the verdicts are one structural rule; definite-assignment covers unreachable states) |
reachability |
E3 (loop context), E5 |
| Definite assignment | da-errors, da-mop-mfp, da-lattice-height |
definite-assignment (all levels) |
definite-assignment |
E6 |
References¶
See the chapter references.