Skip to content

Commit 50d0d6f

Browse files
ankushdesaiclaude
andcommitted
Phase 3: pass-level tolerance classification in Analyzer.cs
Stacks on Phase 2 (#965). Closes the multi-error type-checker initiative by adding per-item try/catch isolation to the analyzer's gathering passes and a HasErrors gate before the analysis passes that assume a clean AST. ## What changed ### `TolerantStep` helper New private helper in `Analyzer.cs`: private static void TolerantStep(ITranslationErrorHandler handler, Action body) { try { body(); } catch (TranslationException e) when (handler.Diagnostics.ContinueOnError) { handler.Diagnostics.Report(e); } } In strict mode (ContinueOnError == false) the `when` filter is false so the exception propagates exactly as before — bit-for-bit preservation of today's throw-on-first-error semantics. In collecting mode the catch captures the TranslationException into the collector and the loop continues with the next item. Only TranslationException is caught; NREs and other runtime exceptions still propagate so genuine bugs surface loudly. ### Tolerant gathering passes (2a, 2b, 3, 3b, 7) Each iteration wrapped in `TolerantStep`: - **2a MachineChecker.Validate** — per-machine. One bad machine no longer aborts MachineChecker for siblings. - **3 FunctionBody + Validator** — per-function. One bad function (TypeResolver throw on a bad var decl, missing-paths-return, etc.) no longer aborts pass 3 for the rest of the program. - **3b Invariants / Axioms / AssumeOnStarts / Pures / Foreign** — per-item across all five subgroups. One bad invariant no longer blocks axiom checking. - **2b ValidateNoStaticHandlers** — per-machine. - **7 InferMachineCreates** — per-machine. Already gated by HasErrors in practice, but the wrapper is cheap insurance. ### Gathering→analysis boundary New HasErrors gate placed after pass 2b (the last gathering pass) and before pass 4 (ApplyPropagations): if (handler.Diagnostics.HasErrors) return globalScope; If any gathering pass collected an error, the analysis passes (4-7) and the module-system passes (8-10) are skipped. The duplicate gate before pass 8 (added in Phase 2 robustness) is kept as defense-in-depth — once Phase 4+ converts pass-5 capability checks to Report, that second gate will earn its keep. ## Why this matters Without Phase 3, a single machine with a bad start state aborts MachineChecker mid-pass, so a sibling machine's MoreThanOneParameterForHandlers error never gets reported. A single function with a malformed var decl aborts pass 3, so none of the OTHER functions' bodies get type-checked at all. Combined with Phase 2's expression-level recovery, Phase 3 means a user with N independent errors (in any combination of expressions, statements, machines, or functions) sees ALL of them in one compile. ## Tests ### New: `MultiMachineErrors.p` + pinned counts Three machines, each with one independent error (bool->int, missing declaration, int+string binop). Pinned in MultiErrorAcceptanceTest: strict=1, collecting=3. Validates that one machine's error doesn't clobber its siblings' diagnostics in collecting mode. ### Existing: All Phase 2 acceptance tests unchanged MultipleErrors (1/4), NestedExprErrors (1/2), ForeachBodyErrors (1/2), SpecReceiveBodyError (1/3). Same counts as Phase 2 — Phase 3 doesn't change behavior within a single machine. ### Existing: Phase1DormancyTest baseline The "collecting >= strict count" invariant on every Correct/StaticError test still holds. Phase 3 only *adds* errors (when multi-machine / multi-function scenarios exist); it never removes. ## Phase 4 (deferred, NOT in this PR) Convert pass 5 (capability checks) and pass 6 (ControlFlowChecker) throw sites to Report so capability and control-flow violations also accumulate across machines instead of aborting on first. The current HasErrors gate already prevents these passes from running on a broken AST, so they remain RequiresClean for now. Estimated: ~1 day if warranted by user feedback. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent bd1cafe commit 50d0d6f

3 files changed

Lines changed: 161 additions & 46 deletions

File tree

Src/PCompiler/CompilerCore/TypeChecker/Analyzer.cs

Lines changed: 112 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -18,88 +18,126 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config,
1818

1919
// Step 1: Build the global scope of declarations
2020
var globalScope = BuildGlobalScope(config, programUnits);
21-
22-
// Step 2a: Validate machine specifications
21+
22+
// Phase 3 — Tolerant passes (gathering phase). Each iteration is
23+
// wrapped in TolerantStep so a TranslationException on one item
24+
// (machine, function, invariant, ...) reports and continues to the
25+
// next instead of clobbering siblings. In strict mode the catch's
26+
// `when (ContinueOnError)` filter is false, so the original
27+
// throw-and-abort semantics are bit-for-bit preserved.
28+
29+
// Step 2a: Validate machine specifications — per-machine isolation.
2330
foreach (var machine in globalScope.Machines)
2431
{
25-
26-
MachineChecker.Validate(handler, machine, config, globalScope);
32+
TolerantStep(handler,
33+
() => MachineChecker.Validate(handler, machine, config, globalScope));
2734
}
2835

29-
// Step 3: Fill function bodies
36+
// Step 3: Fill function bodies — per-function isolation.
3037
var allFunctions = globalScope.GetAllMethods().ToList();
3138
foreach (var machineFunction in allFunctions)
3239
{
33-
FunctionBodyVisitor.PopulateMethod(config, machineFunction);
34-
FunctionValidator.CheckAllPathsReturn(handler, machineFunction);
40+
TolerantStep(handler, () =>
41+
{
42+
FunctionBodyVisitor.PopulateMethod(config, machineFunction);
43+
FunctionValidator.CheckAllPathsReturn(handler, machineFunction);
44+
});
3545
}
3646

37-
// Step 3b: for PVerifier, fill in body of Invariants, Axioms, Init conditions and Pure functions and functions with pre/post conditions
47+
// Step 3b: for PVerifier, fill in body of Invariants, Axioms, Init
48+
// conditions and Pure functions and functions with pre/post
49+
// conditions — per-item isolation across all five subgroups.
3850
foreach (var inv in globalScope.Invariants)
3951
{
40-
var ctx = (PParser.InvariantDeclContext)inv.SourceLocation;
41-
var temporaryFunction = new Function(inv.Name, inv.SourceLocation)
52+
TolerantStep(handler, () =>
4253
{
43-
Scope = globalScope
44-
};
45-
inv.Body = PopulateExpr(temporaryFunction, ctx.body, PrimitiveType.Bool, handler);
54+
var ctx = (PParser.InvariantDeclContext)inv.SourceLocation;
55+
var temporaryFunction = new Function(inv.Name, inv.SourceLocation)
56+
{
57+
Scope = globalScope
58+
};
59+
inv.Body = PopulateExpr(temporaryFunction, ctx.body, PrimitiveType.Bool, handler);
60+
});
4661
}
4762

4863
foreach (var axiom in globalScope.Axioms)
4964
{
50-
var ctx = (PParser.AxiomDeclContext) axiom.SourceLocation;
51-
var temporaryFunction = new Function(axiom.Name, axiom.SourceLocation)
65+
TolerantStep(handler, () =>
5266
{
53-
Scope = globalScope
54-
};
55-
axiom.Body = PopulateExpr(temporaryFunction, ctx.body, PrimitiveType.Bool, handler);
67+
var ctx = (PParser.AxiomDeclContext)axiom.SourceLocation;
68+
var temporaryFunction = new Function(axiom.Name, axiom.SourceLocation)
69+
{
70+
Scope = globalScope
71+
};
72+
axiom.Body = PopulateExpr(temporaryFunction, ctx.body, PrimitiveType.Bool, handler);
73+
});
5674
}
5775

5876
foreach (var initCond in globalScope.AssumeOnStarts)
5977
{
60-
var ctx = (PParser.AssumeOnStartDeclContext)initCond.SourceLocation;
61-
var temporaryFunction = new Function(initCond.Name, initCond.SourceLocation)
78+
TolerantStep(handler, () =>
6279
{
63-
Scope = globalScope
64-
};
65-
initCond.Body = PopulateExpr(temporaryFunction, ctx.body, PrimitiveType.Bool, handler);
80+
var ctx = (PParser.AssumeOnStartDeclContext)initCond.SourceLocation;
81+
var temporaryFunction = new Function(initCond.Name, initCond.SourceLocation)
82+
{
83+
Scope = globalScope
84+
};
85+
initCond.Body = PopulateExpr(temporaryFunction, ctx.body, PrimitiveType.Bool, handler);
86+
});
6687
}
6788

6889
foreach (var pure in globalScope.Pures)
6990
{
70-
var temporaryFunction = new Function(pure.Name, pure.SourceLocation)
91+
TolerantStep(handler, () =>
7192
{
72-
Scope = pure.Scope
73-
};
74-
var context = (PParser.PureDeclContext) pure.SourceLocation;
75-
if (context.body is not null)
76-
{
77-
pure.Body = PopulateExpr(temporaryFunction, context.body, pure.Signature.ReturnType, handler);
78-
}
93+
var temporaryFunction = new Function(pure.Name, pure.SourceLocation)
94+
{
95+
Scope = pure.Scope
96+
};
97+
var context = (PParser.PureDeclContext)pure.SourceLocation;
98+
if (context.body is not null)
99+
{
100+
pure.Body = PopulateExpr(temporaryFunction, context.body, pure.Signature.ReturnType, handler);
101+
}
102+
});
79103
}
80104

81105
foreach (var func in allFunctions.Where(func => func.Role.HasFlag(FunctionRole.Foreign)))
82106
{
83-
// populate pre/post conditions
84-
var ctx = (PParser.ForeignFunDeclContext)func.SourceLocation;
85-
foreach (var req in ctx._requires)
86-
{
87-
var preExpr = PopulateExpr(func, req, PrimitiveType.Bool, handler);
88-
func.AddRequire(preExpr);
89-
}
90-
foreach (var post in ctx._ensures)
107+
TolerantStep(handler, () =>
91108
{
92-
var postExpr = PopulateExpr(func, post, PrimitiveType.Bool, handler);
93-
func.AddEnsure(postExpr);
94-
}
109+
// populate pre/post conditions
110+
var ctx = (PParser.ForeignFunDeclContext)func.SourceLocation;
111+
foreach (var req in ctx._requires)
112+
{
113+
var preExpr = PopulateExpr(func, req, PrimitiveType.Bool, handler);
114+
func.AddRequire(preExpr);
115+
}
116+
foreach (var post in ctx._ensures)
117+
{
118+
var postExpr = PopulateExpr(func, post, PrimitiveType.Bool, handler);
119+
func.AddEnsure(postExpr);
120+
}
121+
});
95122
}
96123

97-
// Step 2b: Validate no static handlers
124+
// Step 2b: Validate no static handlers — per-machine isolation.
98125
foreach (var machine in globalScope.Machines)
99126
{
100-
MachineChecker.ValidateNoStaticHandlers(handler, machine);
127+
TolerantStep(handler,
128+
() => MachineChecker.ValidateNoStaticHandlers(handler, machine));
101129
}
102130

131+
// Phase 3 gathering→analysis boundary. Everything above is
132+
// "Tolerant" (per-item try/catch, errors collected); everything
133+
// below is "RequiresClean" — assumes a fully-typed AST. If any
134+
// gathering pass collected an error, skip the analysis passes
135+
// entirely. Compiler.cs's flush at the end of compilation will
136+
// surface what we have. The duplicate gate before pass 8 (further
137+
// below) remains as defense-in-depth for the case where a future
138+
// analysis pass converts its throws to Diagnostics.Report.
139+
if (handler.Diagnostics.HasErrors) return globalScope;
140+
103141
// Step 4: Propagate purity properties
104142
ApplyPropagations(allFunctions,
105143
CreatePropagation(fn => fn.CanRaiseEvent, (fn, value) => fn.CanRaiseEvent = value,
@@ -147,10 +185,13 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config,
147185
// Step 6: Check control flow well-formedness
148186
ControlFlowChecker.AnalyzeMethods(handler, allFunctions);
149187

150-
// Step 7: Infer the creates set for each machine.
188+
// Step 7: Infer the creates set for each machine — per-machine
189+
// isolation. Gated by the HasErrors check above so the partial-AST
190+
// risk is low, but per-machine try/catch is cheap insurance.
151191
foreach (var machine in globalScope.Machines)
152192
{
153-
InferMachineCreates.Populate(machine, handler);
193+
TolerantStep(handler,
194+
() => InferMachineCreates.Populate(machine, handler));
154195
}
155196

156197
// Phase 2 robustness gate: passes 8-10 ("RequiresClean" in the
@@ -193,6 +234,31 @@ public static Scope AnalyzeCompilationUnit(ICompilerConfiguration config,
193234
return globalScope;
194235
}
195236

237+
/// <summary>
238+
/// Run a single analysis step (per-machine, per-function, per-item)
239+
/// under cascade-suppression rules. In strict mode (default), any
240+
/// TranslationException propagates as before — the <c>when</c> filter
241+
/// is false so the catch doesn't fire. In collecting mode, the
242+
/// exception is captured into the diagnostic collector and the loop
243+
/// continues with the next item, so one bad machine / function /
244+
/// invariant doesn't suppress siblings' diagnostics.
245+
///
246+
/// Only TranslationException is caught: NREs and other unexpected
247+
/// runtime exceptions still propagate so they surface as bugs to fix
248+
/// rather than being silently swallowed.
249+
/// </summary>
250+
private static void TolerantStep(ITranslationErrorHandler handler, Action body)
251+
{
252+
try
253+
{
254+
body();
255+
}
256+
catch (TranslationException e) when (handler.Diagnostics.ContinueOnError)
257+
{
258+
handler.Diagnostics.Report(e);
259+
}
260+
}
261+
196262
private static IPExpr PopulateExpr(Function func, ParserRuleContext ctx, PLanguageType type, ITranslationErrorHandler handler)
197263
{
198264
var exprVisitor = new ExprVisitor(func, handler, isPVerifier: true);
Lines changed: 39 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
// Phase 3 acceptance test for per-machine error isolation.
2+
//
3+
// Three independent machines, each with one error. Validates that
4+
// Analyzer.cs's TolerantStep wrappers around pass 2a (MachineChecker) and
5+
// pass 3 (FunctionBodyVisitor) report errors from EACH machine without one
6+
// bad machine clobbering the diagnostics of its siblings.
7+
//
8+
// Errors (collecting mode):
9+
// 1. MachineA: `x = true` — bool assigned to int
10+
// 2. MachineB: `y = undeclaredVar` — missing declaration
11+
// 3. MachineC: `z = z + "str"` — int + string binop mismatch
12+
//
13+
// Strict mode aborts on the first error: count = 1.
14+
// Collecting mode reports all three: count = 3.
15+
16+
machine MachineA {
17+
var x: int;
18+
start state S {
19+
entry { x = true; }
20+
}
21+
}
22+
23+
machine MachineB {
24+
var y: int;
25+
start state S {
26+
entry { y = undeclaredVar; }
27+
}
28+
}
29+
30+
machine MachineC {
31+
var z: int;
32+
start state S {
33+
entry { z = z + "str"; }
34+
}
35+
}
36+
37+
machine Main {
38+
start state S { entry { } }
39+
}

Tst/UnitTests/TypeChecker/MultiErrorAcceptanceTest.cs

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,16 @@ private static IEnumerable<TestCaseData> PinnedCases()
6262
"but is PVerifier-only syntax — covered by a separate PVerifier test suite.")
6363
.SetName("ForeachBodyErrors (body visit)");
6464

65+
yield return new TestCaseData(
66+
"RegressionTests/Feature3Exprs/StaticError/MultiMachineErrors/MultiMachineErrors.p",
67+
1, 3,
68+
"Phase 3 per-machine isolation: 3 machines, one error each (bool->int, " +
69+
"missing decl, int+string). Validates that TolerantStep wrappers around " +
70+
"pass 2a / pass 3 in Analyzer.cs catch a TranslationException on one machine " +
71+
"and continue to siblings. A regression here (count back to 1) means " +
72+
"TolerantStep stopped re-Reporting or stopped iterating after a throw.")
73+
.SetName("MultiMachineErrors (Phase 3 isolation)");
74+
6575
yield return new TestCaseData(
6676
"RegressionTests/Feature3Exprs/StaticError/SpecReceiveBodyError/SpecReceiveBodyError.p",
6777
1, 3,

0 commit comments

Comments
 (0)