Lesson 3.7 — Error recovery and error messages in LR parsers

Techniques: yacc's error token recovery (Johnson 1975, as in Bison); Burke–Fisher repair (1987, as in ML-Yacc); hand-written error messages per state with Menhir's .messages files and Pottier's reachability analysis (2016) · Pebble implements: nothing (its recovery is recursive-descent panic mode, Lesson 2.7); the oracle implements all three (lr.yacc_recover_parse, lr.burke_fisher_repair, lr.error_sites_lower_bound) · Lab: stretch goal in the SPEC · Prerequisites: Lessons 3.1–3.3; panic mode and repair in Lesson 2.7 · Time: 3 hours

An LR parser detects an error at the first token that cannot continue a valid prefix (Corollary 3.2.16): the best possible position. What it does next is the problem of this lesson. It can resynchronize using error productions the grammar author placed (yacc), repair the input by the smallest edit near the error (Burke–Fisher), or — since a message is what the programmer reads — attach a hand-written explanation to every state in which an error can happen, a list that a generator can compute and keep complete (Menhir).

1. Problem and motivation

Input: an LR table and an input with syntax errors. Output: every error reported once, with a useful message, and parsing continued far enough to find the next independent error (or a best-effort tree for an IDE).

yacc's error token recovery

Johnson's yacc [Joh75] added a reserved terminal error to the grammar. On an error the parser pops states until one can shift error, shifts it, and then discards input until a token is acceptable; the author decides where recovery is possible (stmt: error ';'). Three tokens must be shifted before another error is reported, to avoid cascades. Bison keeps the design unchanged [BISON-Manual]; PostgreSQL, Ruby's former parse.y, and countless DSLs use it.

Burke–Fisher repair

Burke and Fisher [BF87] made LR parsers correct the input: keep the last \(k\) tokens unreduced ("deferred"), and on an error try every single-token insertion, deletion and substitution at each of those positions, re-parse, and choose the repair that lets the parser go furthest. Messages become "inserting )" or "deleting +". ML-Yacc (SML/NJ) implements it with a lookahead window of 15 tokens by default in its examples (the parse (15, …) call in the box).

Menhir .messages and reachability

The best messages are written by people, per parser state: in state I4 of an expression parser, "an operator or a closing parenthesis was expected". Jeffery's merr [Jef03] associated messages with states found by example inputs. Pottier [Pot16] made it systematic: menhir --list-errors computes, for every state and token where an error can actually occur, a shortest input that reaches it; --compile-errors turns the .messages file into a lookup function; and --compare-errors checks the file stays complete when the grammar changes. CompCert's verified C parser [JPL12] ships its messages this way (cparser/handcrafted.messages) [COMPCERT-msgs].

2. Definitions and algorithms

Definition 3.7.1 (Error configuration)

The driver (Algorithm 3.1.18) is in an error configuration \((q, t)\) when the top state is \(q\), the lookahead is \(t\), and ACTION\([q, t]\) is empty (or an error entry from %nonassoc). An error configuration is reachable if some input drives the parser into it. With default reductions (Bison, Menhir), a state whose only action is a reduction never detects errors itself.

Definition 3.7.2 (Error productions and recovery state)

An error production has the reserved terminal error on its right side. The parser has a recovery status \(e \in \{0, 1, 2, 3\}\): after recovering, \(e = 3\); each shift of a real token decrements it; an error is reported only when \(e = 0\).

Definition 3.7.3 (Simple repairs; Burke–Fisher choice)

A simple repair at position \(i\) is the insertion of a terminal before \(t_i\), the deletion of \(t_i\), or its substitution by another terminal. Given the first error position \(e\) and a window \(k\), a repair at \(i \in [e - k, e]\) is acceptable if the parser, run on the repaired input, accepts or consumes at least \(c\) tokens beyond the repair (the check distance). The Burke–Fisher choice is an acceptable repair that gets furthest; the course's oracle breaks ties by the position closest to the error, then deletion before insertion before substitution, then terminal order.

Definition 3.7.4 (Error sites and the reachability problem [Pot16])

An error site is a pair \((q, z)\) with ACTION\([q, z]\) empty. The reachability problem asks, for each error site, for a shortest input \(w\) such that the parser, after reading \(w\) and before reading \(z\), is in state \(q\) with lookahead \(z\) — or a proof that none exists.

yacc's error token recovery

Algorithm 3.7.5 (yacc/Bison error recovery)

• Input: a table for a grammar with error productions; the input.
• Output: a parse with every error reported at most once per recovery, or abort.
• Precondition: error is an ordinary terminal of the table (it has shifts); no default reductions in the course's version.
• Postcondition: terminates (Theorem 3.7.8); reports the first error exactly where the plain driver would.
• Invariant: the stack is a viable prefix over \(N \cup T \cup \{\mathtt{error}\}\).

Oracle: lr.yacc_recover_parse (Bison's yyerrlab/yyerrlab1 without default reductions).

on an error in configuration (q, t):
    if e = 0: report "syntax error at t"
    elif e = 3:
        if t = $: abort
        discard t (advance the input)
    # yyerrlab1
    e ← 3
    while ACTION[top, error] has no shift:
        if the stack has one state: abort
        pop one state
    shift error
    continue parsing (a shift of a real token decrements e)

Burke–Fisher repair

Algorithm 3.7.6 (Burke–Fisher simple repair, oracle version)

• Input: a conflict-free table, the input, window \(k\), check distance \(c\).
• Output: the error position \(e\) and the chosen repair, or none.
• Precondition: the plain driver finds an error at \(e\).
• Postcondition: Definition 3.7.3's choice.
• Invariant: candidates are tried at positions \(e - k .. e\); the best key seen so far is kept.

Oracle: lr.burke_fisher_repair (re-parses from the start for clarity; Burke and Fisher re-parse only the deferred window, because the parser kept the state from \(k\) tokens back).

function BurkeFisher(table, w, k, c):
    e ← error position of LRParse(w)
    best ← none
    for i in e − k .. e:
        for each edit in {delete t_i} ∪ {insert a before t_i} ∪ {replace t_i by a}:
            w' ← apply edit;  reached ← how far LRParse(w') gets, in original positions
            if accepted or reached − i ≥ c:
                key ← (−reached, e − i, kind rank, terminal order)
                if key < key(best): best ← edit
    return (e, best)

Menhir .messages and reachability

Algorithm 3.7.7 (Candidate error sentences: the lower bound Pottier refines)

• Input: the table and automaton.
• Output: for each error site \((q, z)\), a candidate input and whether it really reaches \((q, z)\).
• Precondition: every nonterminal is productive.
• Postcondition: candidates are shortest in the automaton's graph (nonterminal edges weighted by their shortest yield); a candidate that fails to reach the site is either the wrong witness or the site is unreachable — deciding which is what Pottier's algorithm does exactly.
• Invariant: Dijkstra's: popped states have final distances.

Oracle: lr.error_sites_lower_bound.

function CandidateSites(A, ACTION):
    y[A] ← a shortest terminal string of A, for every nonterminal (fixed point)
    dist, path ← Dijkstra over A from q0, edge X costs |y[X]| (1 for a terminal)
    for each state q, each z with ACTION[q, z] = ∅:
        w ← path[q] with each nonterminal X replaced by y[X]
        reaches ← (LRParse(w z) stops with error in state q before z)
        report (q, z, w, reaches)

Pottier's algorithm [Pot16] searches instead over facts \((s, w, z)\) — "from state \(s\), input \(w\) leads to state \(s'\) with lookahead \(z\) possible" — built by a Dijkstra-like saturation in which a nonterminal edge \(s \xrightarrow{A} s'\) can be taken with lookahead \(z\) only if the reductions that build \(A\) are enabled on \(z\). Its output is exactly the set of reachable sites, each with a shortest sentence.

3. Worked example

yacc's error token recovery on an example

tests/ch03/Inputs/error-stmts.grammar: \((1)\ S \to S\,L\), \((2)\ S \to L\), \((3)\ L \to x\ ;\), \((4)\ L \to \mathtt{error}\ ;\). LALR table (I2 = after error, I3 = \(S' \to S \bullet\) with \(S \to S \bullet L\)):

state	;	error	x	$	S	L
0		s2	s1		3	4
1	s5
2	s6
3		s2	s1	acc		7
4		r2	r2	r2
5		r3	r3	r3
6		r4	r4	r4
7		r1	r1	r1

Input x ; x x x ; x ; (the second statement has two extra x); oracle trace, one row per move:

step	stack	input	action	\(e\)
1	0	x ; x x x ; x ; $	shift 1	0
2	0 x 1	; x x x ; x ; $	shift 5	0
3	0 x 1 ; 5	x x x ; x ; $	reduce (3) L → x ;	0
4	0 L 4	x x x ; x ; $	reduce (2) S → L	0
5	0 S 3	x x x ; x ; $	shift 1	0
6	0 S 3 x 1	x x ; x ; $	error: report "syntax error at token 3 (x)"	0
7	0 S 3 x 1	x x ; x ; $	pop state 1 (I1 cannot shift error)	3
8	0 S 3	x x ; x ; $	shift error, go to 2	3
9	0 S 3 error 2	x x ; x ; $	error, \(e = 3\): discard x	3
10	0 S 3 error 2	x ; x ; $	pop state 2	3
11	0 S 3	x ; x ; $	shift error, go to 2	3
12	0 S 3 error 2	x ; x ; $	discard x	3
13	0 S 3 error 2	; x ; $	pop state 2	3
14	0 S 3	; x ; $	shift error, go to 2	3
15	0 S 3 error 2	; x ; $	shift 6	2
16	0 S 3 error 2 ; 6	x ; $	reduce (4) L → error ;	2
17	0 S 3 L 7	x ; $	reduce (1) S → S L	2
18	0 S 3	x ; $	shift 1	1
19	0 S 3 x 1	; $	shift 5	0
20	0 S 3 x 1 ; 5	$	reduce (3) L → x ;	0
21	0 S 3 L 7	$	reduce (1) S → S L	0
22	0 S 3	$	accept (with 1 error)	0

One message, tokens 3 and 4 discarded, parsing resumes at the third statement — the Bison run in §7 performs the same pops, shifts and discards.

Burke–Fisher repair on an example

Expression grammar tests/ch03/Inputs/expr.grammar, input ( id + id id ): the LALR parser stops at token 4 (the second id) with expected \(\{), *, +, \$\}\). Candidates with window \(k = 2\), check \(c = 3\) (oracle):

position	edit	repaired input	parser reaches	acceptable
2	delete +	( id id id )	error at 2	no
3	delete id	( id + id )	accepts	yes, best so far at 3
4	delete id	( id + id )	accepts	yes, closer to the error: chosen
4	insert +	( id + id + id )	accepts	yes, but insertion ranks after deletion
4	insert *	( id + id * id )	accepts	yes, same
4	replace id by )	( id + id ) )	error at 5	no

Result: "delete id at 4". For ( id + id id (no closing parenthesis) every deletion leaves an unclosed (; the best repair is "replace id by )" at 4, which accepts.

Menhir .messages and reachability on an example

The expression grammar \(E \to E + E \mid (\,E\,) \mid \mathit{id}\) with %left + has 8 LALR states and 21 empty ACTION cells. Algorithm 3.7.7 gives (oracle error_sites_lower_bound; ✓ = the candidate really stops in that state on that token):

state	items (kernel)	error tokens	candidate input	reaches?
0	\(E' \to \bullet E\)	) + $	ε	✓
1	\(E \to ( \bullet E )\)	) + $	(	✓
2	\(E \to \mathit{id} \bullet\)	( id	id	✓
3	\(E' \to E \bullet\), \(E \to E \bullet + E\)	)	id	✓
3	(same)	( id	id	✗ (the parser stops in state 2)
4	\(E \to ( E \bullet )\), \(E \to E \bullet + E\)	$	( id	✓
4	(same)	( id	( id	✗
5	\(E \to E + \bullet E\)	) + $	id +	✓
6	\(E \to ( E ) \bullet\)	( id	( id )	✓
7	\(E \to E + E \bullet\), \(E \to E \bullet + E\)	( id	id + id	✗

The ✗ sites are unreachable: states 3, 4 and 7 are entered only after reducing \(E\), which LALR does only on \(\{), +, \$\}\), so ( or id can never be the lookahead there. A message file written for them would be dead text; Pottier's algorithm omits them and proves the others reachable. With Menhir's default reductions, states 2, 6 and 7 never detect errors at all (their only action is a reduction), which is why menhir --list-errors reports just one sentence per remaining state (the box in §7 shows 5 sentences for this grammar with an explicit EOF).

Try it

python3 -c "import sys; sys.path.insert(0, 'tools'); from course.lib import lr, grammar; g = grammar.Grammar.parse(open('tests/ch03/Inputs/error-stmts.grammar').read()); t = lr.build_table(lr.augment(g), 'lalr'); tr = []; print(lr.yacc_recover_parse(t, 'x ; x x x ; x ;'.split(), tr)); [print(r) for r in tr]" reproduces the first trace; change the input and predict the discards first.

4. Invariants and correctness

yacc's error token recovery

Theorem 3.7.8 (yacc recovery terminates and never reports cascades within three tokens)

For any input, Algorithm 3.7.5 halts; between two reported errors at least three real tokens are shifted.

Proof

Define the measure \(\mu = (\text{remaining input length},\ \text{phase})\) ordered lexicographically, where the phase counts the moves since the last input consumption. Normal moves are those of the driver, whose reductions are bounded between two shifts (Proposition 3.1.20, on the grammar extended with error as a terminal). Consider an error. If \(e = 3\), a token is discarded (or the parse aborts at \(\$\)), so the remaining input shrinks. If \(e < 3\), the handler pops a finite number of states and shifts error; the next error before any real shift finds \(e = 3\) and discards. So between two consecutive discards or shifts of real tokens only finitely many moves happen, and each real token is consumed once: the parse halts. Errors are reported only when \(e = 0\); after a recovery \(e = 3\), and only shifts of real tokens decrease it, one per shift.

Proposition 3.7.9 (What recovery preserves)

(a) The first error is reported at the same token as without recovery (the correct-prefix position). (b) Every tree built after recovery is a tree of the grammar extended with error: the parse is correct for the repaired input in which the discarded tokens are replaced by error.

Proof

(a) Before the first error the recovering parser performs the plain driver's moves. (b) Every reduction is by a production of the extended grammar and every shift consumes the next symbol of the sequence obtained from the input by replacing each maximal discarded segment, together with the position where error was shifted, by the terminal error — so Theorem 3.1.13 applies to that sequence.

Burke–Fisher repair

Proposition 3.7.10 (The chosen repair is locally optimal)

Among single-token repairs within the window, Burke–Fisher's choice lets the parser advance furthest; if the input is at distance 1 from \(L(G)\) by a single edit within the window, some acceptable repair makes the repaired input a sentence.

Proof

The first claim is the definition of the choice (the key's first component). For the second, let the single edit at position \(i\) turn the input into a sentence. The plain parser on the original input detects the error at \(e \ge i\) at the earliest possible position (correct-prefix property), and at most at \(i\) plus the tokens before which the prefix stays viable; with the window chosen to cover \([e - k, e] \ni i\), that edit is among the candidates, it accepts, and accepting ranks above every non-accepting candidate. (If several accept, the tie-breaks pick one of them.) When \(i < e - k\) the edit is outside the window and the method can only find a worse repair: this is why Burke and Fisher defer \(k\) tokens.

Menhir .messages and reachability

Theorem 3.7.11 (Completeness and minimality of LRijkstra [Pot16])

Pottier's algorithm reports every reachable error site \((q, z)\), never an unreachable one, and each reported sentence is a shortest input reaching it.

Proof sketch (full proof: [Pot16, §3–5])

The facts \((s, w, s', z)\) ("from \(s\), reading \(w\) leads to \(s'\), and \(z\) can follow") are generated by rules mirroring the LR driver: a terminal edge extends \(w\) by one token; a nonterminal edge \(s \xrightarrow{A} s'\) can be used with lookahead \(z\) only if some production of \(A\) can be reduced when \(z\) follows, which is itself a fact about shorter inputs. Every run of the driver corresponds to a derivation of facts and vice versa (soundness and completeness), and a Dijkstra-style priority on \(\lvert w \rvert\) discovers facts in order of input length, so the first fact reaching an error site gives a shortest sentence. Algorithm 3.7.7 is the special case that ignores the lookahead side conditions; the ✗ rows of §3 are exactly the facts it wrongly assumes.

5. Complexity

Variables: \(n\) input length; \(\lvert Q \rvert\) states; \(d\) maximum stack depth popped during recovery; \(k\) repair window; \(c\) check distance; \(\lvert T \rvert\) terminals.

Technique	Time (worst)	Time (typical)	Space	Variables
yacc error recovery	\(O(n \cdot d)\) extra moves over the plain parse (each discard can pop \(d\) states)	negligible	none	as above
Burke–Fisher	per error \(O(k \cdot \lvert T \rvert)\) candidates, each re-parsing \(O(k + c)\) tokens from the deferred state	milliseconds	the \(k\) deferred tokens and states	as above
Candidate sites (Alg. 3.7.7)	\(O(\lvert Q \rvert \log \lvert Q \rvert + \lvert Q\rvert \cdot \lvert T \rvert \cdot L)\) with \(L\) the candidate length	instant	\(O(\lvert Q \rvert)\)	as above
LRijkstra	polynomial in \(\lvert Q \rvert\), \(\lvert T \rvert\) and the answer length [Pot16]	practical on CompCert's C grammar [Pot16]	facts table	as above

Pathological input for yacc recovery: a grammar whose only error production is at the top (S: error) makes every error discard the rest of the input — one message, nothing else checked. For Burke–Fisher, a missing token far before the detection point (an unclosed comment-like construct) lies outside any reasonable window, and the "repair" becomes a series of deletions.

6. Variants and refinements

yacc's error token recovery

• yyerrok and yyclearin [BISON-Manual]: an action can end recovery early or drop the lookahead — trade-off: faster resynchronization, risk of cascades.
• Menhir's --strategy [MENHIR-Manual] selects between a yacc-compatible (legacy) and a simplified treatment of the error token, and its incremental API lets the program inspect the state on an error instead — trade-off: the program, not the grammar, decides how to resume.

Burke–Fisher repair

• Secondary (scope) recovery [BF87]: when no simple repair works, insert closing tokens for open scopes (end, )) — trade-off: handles structural errors, more candidates.
• Minimum-cost global repair (Aho–Peterson 1972, Lesson 2.7) — trade-off: optimal but cubic; CPCT+ (Diekmann and Tratt 2020 [DT20]) — searches repair sequences with bounded time and reports all minimal-cost ones, used in the Rust grmtools LR library.

Menhir .messages and reachability

• merr (Jeffery 2003) [Jef03]: generate a message table from (bad input, message) examples — trade-off: easy to start, no completeness guarantee.
• --compare-errors / --merge-errors / --update-errors [MENHIR-Manual]: keep a message file complete and up to date as the grammar evolves — trade-off: needs discipline in the build.

7. In real compilers

yacc's error token recovery

• Bison (3.8.2) data/skeletons/yacc.c — labels yyerrlab (report and discard), yyerrorlab and yyerrlab1 (pop until a state shifts error, then shift it; yyerrstatus = 3) [BISON-src].
• PostgreSQL (REL_17_0) src/backend/parser/gram.y — SQL statements; errors abort the statement (%expect 0, no error productions in the statement list), recovery happens at the protocol level [PG-gram].

Bison's recovery on the example

Reproduce (bison 3.8.2, clang 23.1.2; any OS):

cat > stmts.y <<'EOF'
%{
#include <stdio.h>
int yylex(void);
void yyerror(const char *s) { fprintf(stderr, "%s\n", s); }
%}
%define parse.trace
%define parse.error verbose
%%
s: s l | l ;
l: 'x' ';'          { fprintf(stderr, "statement ok\n"); }
 | error ';'        { fprintf(stderr, "recovered at ';'\n"); yyerrok; }
 ;
%%
static const char *in;
int yylex(void) { return *in ? *in++ : 0; }
int main(int argc, char **argv) { in = argv[1]; yydebug = 1; return yyparse(); }
EOF
bison -o stmts.c stmts.y
clang-23 -w -o stmts stmts.c
./stmts 'x;xxx;x;' 2>&1 | grep -E '^(Error|Shifting|Next token|syntax|recovered|statement)'

Output (complete):

Next token is token 'x' ()
Shifting token 'x' ()
Next token is token ';' ()
Shifting token ';' ()
statement ok
Next token is token 'x' ()
Shifting token 'x' ()
Next token is token 'x' ()
syntax error, unexpected 'x', expecting ';'
Error: popping token 'x' ()
Shifting token error ()
Next token is token 'x' ()
Error: discarding token 'x' ()
Error: popping token error ()
Shifting token error ()
Next token is token 'x' ()
Error: discarding token 'x' ()
Error: popping token error ()
Shifting token error ()
Next token is token ';' ()
Shifting token ';' ()
recovered at ';'
Next token is token 'x' ()
Shifting token 'x' ()
Next token is token ';' ()
Shifting token ';' ()
statement ok
Shifting token "end of file" ()

What to notice: steps 6–15 of §3 exactly: one report, pop the x, shift error, then for each extra x "discarding" followed by popping and re-shifting error (Bison's yyerrlab1 loop), until ; can be shifted. yyerrok in the action resets the recovery status so the next statement is checked normally.

Burke–Fisher repair

• ML-Yacc (SML/NJ, tag v110.99.9) ml-yacc/lib/parser2.sml — its header: it implements "the partial, deferred method" of Burke and Fisher; it keeps a queue of recent tokens and tries insertions, deletions and substitutions, with the grammar's %change/%prefer/%subst declarations as preferred changes [MLYACC-parser].
• grmtools (Rust) — CPCT+ repairs in lrpar [DT20].

ML-Yacc repairs the input and keeps parsing

Reproduce (ml-yacc and sml from Ubuntu's ml-yacc and smlnj 110.79 packages; Linux):

cat > calc.grm <<'EOF'
%%
%name Calc
%term ID of unit | PLUS | TIMES | LPAREN | RPAREN | SEMI | EOF
%nonterm start | stmts | exp
%pos int
%eop EOF
%noshift EOF
%left PLUS
%left TIMES
%value ID (())
%%
start : stmts ()
stmts : exp SEMI stmts () | ()
exp : exp PLUS exp () | exp TIMES exp () | LPAREN exp RPAREN () | ID ()
EOF
cat > main.sml <<'EOF'
structure CalcLrVals = CalcLrValsFun(structure Token = LrParser.Token)
structure T = CalcLrVals.Tokens
structure CalcLex = struct
  structure UserDeclarations = struct
    type pos = int
    type svalue = T.svalue
    type ('a, 'b) token = ('a, 'b) T.token
  end
  val words = ref (String.tokens Char.isSpace (valOf (OS.Process.getEnv "INPUT")))
  val n = ref 0
  fun makeLexer (_ : int -> string) () =
    case !words of
        [] => T.EOF (!n, !n)
      | w :: rest =>
          let val i = !n before (n := !n + 1; words := rest)
          in case w of
                 "+" => T.PLUS (i, i) | "*" => T.TIMES (i, i) | "(" => T.LPAREN (i, i)
               | ")" => T.RPAREN (i, i) | ";" => T.SEMI (i, i) | _ => T.ID ((), i, i)
          end
end
structure CalcParser = Join(structure LrParser = LrParser
                            structure ParserData = CalcLrVals.ParserData
                            structure Lex = CalcLex)
val _ =
  let fun err (msg, p, _) = print ("token " ^ Int.toString p ^ ": " ^ msg ^ "\n")
  in CalcParser.parse (15, CalcParser.makeLexer (fn _ => ""), err, ()); print "parsed\n" end
  handle CalcParser.ParseError => print "ParseError\n"
EOF
printf 'Group is\n  $/basis.cm\n  $/ml-yacc-lib.cm\n  calc.grm.sig\n  calc.grm.sml\n  main.sml\n' > sources.cm
ml-yacc calc.grm
for input in 'id id ; id * id ;' 'id + ; id ;' 'id + ( id * id ; id ;' '( id + id ) ) ; id ;'; do
  echo "== $input"
  INPUT="$input" sml <<< 'CM.make "sources.cm";' 2>&1 | grep -E '^(token|parsed|ParseError)'
done

Output (complete):

== id id ; id * id ;
token 1: syntax error: inserting  PLUS
parsed
== id + ; id ;
token 1: syntax error: deleting  PLUS
parsed
== id + ( id * id ; id ;
token 4: syntax error: inserting  RPAREN
parsed
== ( id + id ) ) ; id ;
token 0: syntax error: inserting  LPAREN
parsed

What to notice: every input is repaired by one edit and parsed to the end. The last two show the deferred window: the error is detected at ; (token 6) and at the second ) (token 5), but the repair is placed earlier — ) inserted before * (token 4), ( inserted at token 0 — because ML-Yacc tries positions back in its queue and those repairs let the parser go furthest (Definition 3.7.3). The course oracle's tie-break prefers positions near the error, so it would choose differently among equally good repairs.

Menhir .messages and reachability

• Menhir (20231231) src/LRijkstra.ml and src/LRijkstraFast.ml — --list-errors; the header explains why shortest paths in the automaton are only a lower bound (the ✗ rows of §3) [MENHIR-src].
• CompCert cparser/handcrafted.messages — the hand-written messages of CompCert's Menhir-generated, formally validated C parser [COMPCERT-msgs].

menhir --list-errors: one reachable sentence per error state

Reproduce (menhir 20231231, Ubuntu 24.04 package menhir 20231231+ds-1; any OS):

cat > expr.mly <<'EOF'
%token ID PLUS LPAREN RPAREN EOF
%left PLUS
%start <unit> main
%type <unit> e
%%
main: e EOF {}
e: e PLUS e {} | LPAREN e RPAREN {} | ID {}
EOF
menhir --list-errors expr.mly | sed -n '/^main: LPAREN ID LPAREN/,/^<YOUR SYNTAX ERROR MESSAGE HERE>/p'
menhir --list-errors expr.mly | grep -c '^main:'

Output (complete):

main: LPAREN ID LPAREN
##
## Ends in an error in state: 3.
##
## e -> e . PLUS e [ RPAREN PLUS ]
## e -> LPAREN e . RPAREN [ RPAREN PLUS EOF ]
##
## The known suffix of the stack is as follows:
## LPAREN e
##

<YOUR SYNTAX ERROR MESSAGE HERE>
5

What to notice: the entry is our state I4 (\(E \to ( E \bullet )\), \(E \to E \bullet + E\)) reached by ( id and then the erroneous (: Menhir reaches it with LPAREN where our lower bound failed, because with its default reduction in the id state, the reduction \(E \to \mathit{id}\) happens before the lookahead is examined. You replace the placeholder with a message; --compile-errors turns the file into a function from state to message. Five states can detect an error, so five sentences [MENHIR-Manual, Pot16].

Find where LLVM does it. Open clang/lib/Parse/Parser.cpp (LLVM 23.1.2) and read Parser::SkipUntil [CLANG-Parser]. Clang's recursive-descent parser recovers by skipping tokens until one of a given set — which yacc concept (§2) plays the role of that set in an LR parser with error productions? (quiz clang-skipuntil)

8. Comparison

Technique	Power / precision	Speed (asymptotic · practical)	Output / error quality	Implementation effort	Typical use
yacc error token	Resynchronizes where the author put error productions	\(O(n \cdot d)\) extra · negligible	Generic "syntax error, unexpected X, expecting Y"; cascades limited by the 3-token rule	Low for the generator; the grammar author places error rules	Bison/yacc parsers, PostgreSQL-style DSLs
Burke–Fisher repair	Best single-token edit within a window	\(O(k \lvert T \rvert (k + c))\) per error · milliseconds	"inserting )" style messages; can guess wrong	Moderate: deferred window, candidate generation	ML-Yacc; CPCT+ (grmtools)
Menhir .messages + reachability	Complete list of reachable error states; hand-written messages	LRijkstra polynomial · seconds–minutes offline	The best messages, maintained per state	High for the tool (done once), moderate for the grammar author	Menhir (OCaml, CompCert, Coq)

Choose the error token when you need simple resynchronization at statement boundaries in a Bison grammar. Choose Burke–Fisher (or CPCT+) when you want automatic, local repairs and messages without per-grammar work. Choose .messages when error message quality matters (a compiler for people): the reachability analysis turns an open-ended task into a finite checklist.

9. Assessment

Technique	Quiz ids (solutions/quizzes/ch03.yaml)	Drill	Flashcard tag	Exercises
yacc error token	yacc-discards, clang-skipuntil	./course drill shift-reduce-trace --difficulty hard (inputs with an error; recovery itself is traced in §3 and by the oracle)	yacc-error	E5 stretch
Burke–Fisher	bf-repair, recovery-compare	none: repairs are searched, not computed by hand; §3's table is the pattern	burke-fisher	—
Menhir .messages	unreachable-error-site, recovery-compare	none: menhir --list-errors is the drill (box above)	messages	—

An error state is not the same as an error site

With default reductions, a state that only reduces never reports errors, and some empty cells can never be reached (§3's ✗ rows). Writing messages per cell wastes effort on impossible cases; writing them per reachable state, as Menhir does, covers every case exactly once.

References

See the chapter references.