Exception Support Prototype#1435
Draft
kadirayk wants to merge 28 commits into
Draft
Conversation
Add the prelude composite `BaseException` (E1 exceptional-channel root) as a separate, gated prelude: it is prepended only when a program references it, so heap/SMT reasoning for non-exception programs is unaffected. Add a public `referencedNames` helper to drive the gating. Tests: ExceptionHierarchy (subtyping/is/fields), ExceptionPreludeGating (prelude injected iff referenced).
Introduce a value-carrying 'throw e' statement (E2): one StmtExpr.Throw node, 'throw' surface syntax, and resolution that types the operand at the E1 channel root BaseException (subtypes accepted). No dedicated rethrow form. Reaches resolution/type-check end-to-end. Core lowering is stubbed as NotYetImplemented: the documented Result<Val, Err> lowering (E7) needs generic datatypes Laurel does not have yet, and we deliberately do not monomorphize. Details: AST adds StmtExpr.Throw (+ constrName/constructorName) and moves shared baseExceptionTypeName to LaurelAST next to bodyLabel. Grammar adds 'op throw' plus concrete/abstract translators. Resolution adds Synth dispatch + Check.throw, which checks operand <: BaseException but skips the check once heapParameterization erases the operand to the heap Composite reference (avoids a spurious re-resolution failure). FilterPrelude.collectExprNames treats a throw as a reference to BaseException so the exception prelude is gated in and kept. Throw is threaded through the remaining exhaustive matches: MapStmtExpr (both traversals), LaurelTypes.computeExprType (TVoid), Resolution collectStmtExpr, InferHoleTypes, and the Core translator stubs. Tests: ThrowStatement.lean - ill-typed 'throw 5' reports a BaseException type error; well-typed 'throw e' resolves and reaches the NYI lowering.
Add a structured exception handler: a try body, an ordered list of predicate-based catch clauses (first-match-wins, E3), and an optional finally arm (E5). A catch binds the caught value at the channel root BaseException (E1) and may carry a 'when' guard (checked at bool); type dispatch is written 'catch e when e is T', multi-catch as 'catch e when e is A || e is B'. No new clause kinds beyond the guard. Reaches resolution/type-check end-to-end. Core lowering is stubbed as NotYetImplemented: like throw, it targets a generic Result<Val, Err> (E7), which needs generic datatypes Laurel does not have yet. Details: AST adds a CatchClause struct (binding, optional predicate, body) in the mutual block and StmtExpr.Try (body, catches, finally?), with CatchClause sizeOf lemmas for traversal termination. Grammar adds try/catch/when/finally surface syntax (CatchGuard, CatchClause, FinallyClause categories + tryCatch op) plus both tree translators. Resolution adds Check.tryCatch, which opens a per-clause scope, binds the catch variable at BaseException, checks guards at bool and bodies/finally in statement position; Try synthesizes TVoid; collectStmtExpr registers each binding and is now partial (it recurses through clause fields). Try is threaded through the exhaustive matches: MapStmtExpr (both traversals), LaurelTypes.computeExprType (TVoid), FilterPrelude (gates the exception prelude in), and the Core translator stubs. InferHoleTypes intentionally does not recurse into Try (left to the wildcard): adding the arm forced the mutual block onto well-founded recursion, so holes inside try/catch/finally are not inferred yet (documented in-place). Tests: TryCatch.lean - well-typed try/catch/finally and a boolean 'when' guard reach the NYI lowering; an int guard reports expected 'bool', got 'int'.
…t enforced Add the E4 exceptional contract: an optional single throws type and onThrow exceptional postconditions on a procedure. Laurel records and type-checks them; it performs no declare-or-catch enforcement (front-end policy) and does not yet lower them (E7), so a well-formed contract is ignored at translation and verifies cleanly. AST: OnThrowClause (binding + predicate) in the mutual block; Procedure gains throwsType (Option HighType := none) and onThrow (List OnThrowClause := []), defaults keeping all constructor sites compiling. Grammar: 'throws T' and 'onThrow (e) P' procedure clauses; the procedure/function ops grow from 8 to 10 args. Translators: parseProcedure (10-arg) parses both; procedureToOp prints them. Resolution: resolveExceptionalContract resolves the throws type and checks it is a subtype of BaseException, and resolves each onThrow clause in a fresh scope binding the value at BaseException with the predicate checked at bool; wired into resolveProcedure and resolveInstanceProcedure. mapProcedureM rewrites onThrow predicates; collectProcDeps records throws/onThrow names and forces BaseException into scope (gating). Semantics: multiple onThrow clauses conjoin (like ensures). A multi-type throw set is a single disjunctive clause 'onThrow (e) e is A || e is B'; per-type facts are guarded implications 'onThrow (e) e is T ==> P' (the guard scopes each claim so conjoined clauses don't contradict). Tests: ThrowsContract.lean (valid throws/onThrow verify clean; 'throws int' and a non-bool onThrow predicate rejected). ExceptionScenarios.lean (broad E1-E4 coverage: multiple/union/catch-all catches, try/finally, nested try, throw-subtype reaching the NYI lowering; multi-throws contract, per-type guarded-implication onThrow, deeper hierarchy verifying clean; two negatives). Predicates are kept free of binding field-dereference to avoid the known post-heapParameterization rough edge; a value-level per-type postcondition like 'onThrow (e) e is ParseError ==> (e as ParseError)#pos >= 0' is noted as future work pending that fix and E7 lowering.
heapParameterization skipped Try/Throw nodes in both the heap analysis (collectExpr) and the transform (heapTransformExpr). A procedure that calls a heap-using procedure inside a 'try' was therefore never classified as heap-using (the call wasn't counted as a callee), and even when classified, calls inside the 'try' body weren't given the $heap argument. The result was an internal strata-bug at re-resolution ("expected 'Heap', got 'int'") for otherwise ordinary try/catch code.
collectExpr/collectExprMd: recurse into Throw and Try (body, catch predicates/bodies, finally). Made partial, since the nested catch-clause list makes structural recursion impractical; consistent with other analysis traversals already marked partial (collectStmtExpr, collectExprNames). heapTransformExpr: recurse into Throw and Try the same way; add the CatchClause sizeOf lemmas to its decreasing_by (kept total).
Effect: programs that call heap-using procedures inside try/catch (or throw a freshly allocated exception) now parse, resolve, heap-parameterize, and re-resolve cleanly, reaching the expected not-yet-implemented lowering (E7) instead of crashing with an internal error.
Test: TryHeapCalls.lean - a minimal heap-allocating callee invoked inside a try, plus a realistic multi-catch with throwing heap-using callees.
Replace the throw/try NotYetImplemented stubs with real lowering to Core, building on the generic Result datatype. Exceptions now parse, resolve, heap-parameterize, lower, and verify end-to-end. Lowering (LaurelToCoreTranslator): - A procedure declaring `throws` returns a single `Result<Val, Composite>` output; its normal value output becomes an internal local, and inout outputs (notably `$heap`) are preserved. Err is always `Composite`, since after heap parameterization every exception is a heap reference, so the declared throws type is not needed at the Core boundary. - In-flight exception state is carried by synthesized `$thrown`/`$exc` locals; `throw v` sets them and exits to the nearest enclosing `try` label (or `$body` to escape), where the result is built as `Bad($exc)` / `Good(value)`. - `try/catch/finally` reuses Block/Exit: the body runs in a labeled block a throw exits to, followed by a first-match-wins chain of guarded handlers (`$thrown && predicate`, catch binding substituted with `$exc`); an unmatched exception stays in flight and propagates outward; `finally` runs on the fall-through edge. - A call to a throwing procedure binds its Result, then propagates `Bad` outward or unwraps `Good` into the target. - Add the Result datatype to the exception prelude (gated in with BaseException). Supporting changes: - translateStmt is now `partial`: recursion into the catch-clause list and optional finally makes a structural/well-founded termination proof impractical (consistent with existing partial AST-walking helpers). It is a translation function, not used in proofs. - translateType lowers an unresolved `BaseException` (the catch/onThrow binding's type, which has no AST node for heap parameterization to rewrite) to `Composite` instead of emitting a spurious strata-bug. A throw or thrower-call whose exception would escape a procedure that does not declare `throws` reports not-yet-implemented (E4 no-escape enforcement is deferred). Tests: ThrowStatement, TryCatch, ExceptionScenarios, and TryHeapCalls now verify real exception programs instead of stopping at the stubs.
Add a static "check, don't trust" escape analysis in resolution that enforces the two invariants the design assigns to Laurel: - No-escape: a procedure that declares no `throws` may not let any exception escape, whether thrown directly or propagated from a callee. - Upper-bound: a procedure declaring `throws T` may only let exceptions whose type is a subtype of T escape. Analysis (Resolution.lean): - exceptionEscapes over-approximates the exception types (with source locations) that can leave a statement uncaught: a `throw` contributes its operand type (only when it is a BaseException subtype, so an ill-typed throw is not double-reported), a call to a `throws T` procedure contributes T, and a `try` removes a body type only when some `catch` clause provably handles it (a catch-all, or an `x is T` guard / disjunction thereof with the type a subtype of T). Any other guard catches nothing, keeping the analysis sound. - checkProcedureThrows turns escaping types into no-escape or subtype upper-bound diagnostics per procedure. - Wired into resolve alongside the diamond-field check, gated on the initial resolution (existingModel = none), where throw operands still carry their declared types and `is`-guards are not yet lowered. Java-style declare-or-catch at call sites remains front-end policy and is not enforced here. Tests: - ThrowStatement: `throwsWithoutDeclaring` now fails at resolution with the no-escape error instead of the translation-time NYI stub. - ThrowsContract: header updated; add upper-bound violation, call-based no-escape, coarsened-throws-allowed, and caught-so-no-escape cases.
| each area serves the relevant `F<n>`. | ||
|
|
||
| It is anchored in a design baseline: a single optional `throws` type per procedure, a | ||
| separate `onThrow` exceptional postcondition, a value-carrying `throw`, and |
Contributor
There was a problem hiding this comment.
Do we not also need to specify when the throws occurs? We could have syntax like on <conditionForThrowing> throws <postconditionWhenThrowing>
Contributor
Author
There was a problem hiding this comment.
Right! I didn't think about this case, this is added now.
| throw, bounded by the channel root `BaseException`. Recorded as | ||
| exceptional-contract data; not enforced (declare-or-catch is front-end | ||
| policy) and not yet lowered (E7). -/ | ||
| throwsType : Option (AstNode HighType) := none |
Contributor
There was a problem hiding this comment.
Small design decision: whether to bind the exception variable here or in the onThrow clauses.
Binding it in the onThrow might be good since the variable is not available in the body, unlike the return variables.
Contributor
Author
There was a problem hiding this comment.
Exception variable binding is per clause, like onThrow(e) P, catch e when ..., when C throws (e) P, etc.
| - any program containing a `throw` (or naming this type) pulls the | ||
| exception prelude in (gating), since the channel root must be in scope | ||
| wherever the exceptional channel is used. -/ | ||
| def baseExceptionTypeName : String := "BaseException" |
Contributor
There was a problem hiding this comment.
Doesn't this mechanism imply that we can't throw arbitrary types? Is there a benefit to having that restriction?
Contributor
Author
There was a problem hiding this comment.
It is still possible to throw arbitrary types. Currently the idea is that we require exceptions to be rooted on BaseException, so that everything lowers to a single composite Errand we can reuse composite subtyping for catch/is dispatch. The frontends of languages that throw arbitrary values can box such values in a composite extending BaseExceotion, a demo of this is inThrowArbitraryValue.lean.
| -- Hole in statement position: treat as havoc (no-op). | ||
| -- This can occur when an unmodeled call's Block is flattened. | ||
| return [] | ||
| | .Throw value => |
Contributor
There was a problem hiding this comment.
If you extract the code in LaurelToCoreTranslator to a separate pass, and then add a test that shows the Laurel before and after that pass, then it'll be much easier to review the quality of the transformation.
Contributor
Author
There was a problem hiding this comment.
Done! EliminateExceptionPass.lean shows the before/after.
The no-escape error now names both remedies — catch the exception or declare a `throws` clause — matching Java's "must be caught or declared to be thrown". Updates the two annotations that pin the message.
Add TryCatchBehavior.lean asserting observable outcomes of the lowered control flow, not just that the constructs lower/verify: - a caught throw skips the rest of the body and resumes after the handler - finally runs on both the normal and caught-exception paths - predicate dispatch skips a non-matching clause and takes the matching one - first-match-wins when guards overlap (parent clause before child clause)
LiftImperativeExpressions.transformStmt skipped Try/Throw via its wildcard, so
assignments and imperative calls inside a try region — notably the heap
operations a lowered `new` expands to — were not lifted out of expression
position and hit a strata-bug ("destructive assignments ... should have been
lifted") at Core translation. Add Throw and Try arms that recurse into the
thrown operand, the try body, each handler body, and the finally arm. Catch
guards are left as-is (post-typeHierarchyTransform they are pure).
The transformExpr/transformStmt mutual block is now `partial`: recursion into
the catch-clause list and optional finally makes a structural/well-founded
termination proof impractical (same as translateStmt); they are transforms, not
used in proofs.
Add TryLifting.lean regression tests: `new` inside the try body, inside a catch
handler, and inside a finally body all lower and verify.
The E4 escape check previously ran inside the initial `resolve` and only scanned top-level `staticProcedures`, so instance-method bodies were never checked — a throwing method that did not declare `throws` slipped through. Move the check to a dedicated `ExceptionEscapeCheck` pipeline pass placed after `LiftInstanceProcedures` (methods are now lifted top-level procedures, so their bodies are scanned uniformly and a method calling another throwing method resolves the callee's `throws`) and before `HeapParameterization` (so `throw` operands and `throws` types still carry their real, un-erased types). A `comesBefore heapParameterizationPass` constraint makes the ordering a load-time-checked invariant rather than a silent assumption. Diagnostics render a lifted method name `Composite$method` with a dot (`Composite.method`); user procedure names cannot contain `$`, so top-level procedure names are unaffected. Add MethodExceptionEscape.lean: a throwing method without `throws` is rejected, a declaring method verifies, and method->method propagation is caught (the case that motivated running after lifting).
A throwing procedure's Core output is a single Result<Val, Composite>. Its
contract is now split by channel and verified (checked on exit, assumed at
call sites) instead of being dropped at translation:
- normal `ensures P` -> Result..isGood($result) ==> P[out := Result..value($result)]
- each `onThrow (e) Q` -> Result..isBad($result) ==> Q[e := Result..err($result)]
Changes:
- LaurelToCoreTranslator.lean: build Good/Bad-path postconditions;
translateChecks gains a `wrap` hook for the Good-path guard.
- Resolution.lean: collectProcedure registers onThrow bindings in the model,
fixing an "Unknown type" strata-bug when an onThrow predicate references
its binding.
- HeapParameterization.lean: onThrow predicates are heap-parameterized
(analyzeProc + heapTransformProcedure), so an onThrow consequent may
dereference a composite parameter (e.g. i >= a#length).
Tests (ThrowsPostconditions.lean): good-path ensures checked on exit and
assumed across a throwing call; onThrow checked against a thrown value
(positive + negative); and an array read whose onThrow dereferences a#length.
A `return` inside a `try` body previously jumped straight to `bodyLabel`,
skipping the enclosing `finally`. It now unwinds through each enclosing `try`
so their `finally` arms run:
- a synthesized `$returning` bool is set, and the `return` exits to the
nearest `try` label (landing ahead of the catch chain, which is guarded on
`$thrown` and so skipped), letting `finally` run;
- each `try`'s tail re-checks `$returning` and exits to the next enclosing
`try` label (or `bodyLabel`), so outer `finally` arms run too.
`$returning` is declared alongside `$thrown`/`$exc` whenever the exceptional
channel is used (every `try` sets that flag).
Still open: a `return` inside a `catch` handler (and explicit `exit`) is not yet
routed through the pending `finally`.
Tests (TryCatchBehavior.lean): earlyReturnRunsFinally,
returnSkipsCatchRunsFinally, nestedReturnRunsAllFinally.
…F18)
Lowers `try`/`catch`/`finally` with two nested blocks so `finally` runs on
every exit edge:
block $tryfin {
block $try { B } -- throw in B -> $try (enters catch chain)
<catch chain>
}
F
if $thrown then exit <enclosing throw target | $body>
if $returning then exit <enclosing finally target | $body>
- throw in the body targets $try (runs the catch chain);
- re-throw in a handler targets $tryfin (skips the chain, still runs F);
- return anywhere in the body or a handler sets $returning and targets $tryfin
(skips the chain, runs F);
- after F, the re-dispatch keeps a pending exception or return unwinding through
the enclosing try (so its finally runs too) or to $body.
This extends the earlier body-only fix to returns inside catch handlers, makes
re-throw run finally, and makes unhandled/re-thrown exceptions propagate (skip
subsequent statements) instead of falling through with $thrown set. The
tryLabelStack now carries per-try throw/finally targets (TryTarget).
Tests (TryCatchBehavior.lean): returnInCatchRunsFinally,
returnInCatchNestedFinally.
A throwing procedure lowers to a single Result<Val, Composite> output, so it can carry at most one value output on the Good path. Previously a `throws` procedure with two or more value outputs silently degraded its Result payload to a bool placeholder, which could misrepresent the result. translateProcedure now emits a clear not-yet-implemented diagnostic at the procedure name instead. Void throwers (no value output) and single-value-output throwers are unchanged. Test (ThrowsContract.lean): twoOut is rejected loudly.
A `catch`/`onThrow` predicate can now narrow the binding with a cast and read a
field of the thrown value, e.g.
`onThrow (e) e is IndexError ==> (e as IndexError)#badIndex >= alen`. Three fixes,
one per blocking layer:
- Resolution.targetTypeName: add an AsType case so `(e as T)#f` resolves `f`
on `T` (this affected any `(x as T)#f`, not just the exception binding).
- LaurelAST.isConsistent: treat the erased binding type `BaseException` as
consistent with the synthesized `Composite`, so a heap `readField` on the
binding type-checks after heap parameterization.
- HeapParameterization.dropCastAsserts: a cast `(e as T)` heap-lowers to
`Block [assert (e is T); e]`; strip that downcast assert from `onThrow`
predicates, since a contract cannot execute an `assert` and the clause guard
already conditions validity. Body statements (incl. `catch` handlers) keep
the assert, so a downcast there is still checked.
Tests: ThrowsPostconditions.lean (relational and concrete field reads in
`onThrow`) and TryCatchBehavior.lean (a `catch` handler checking a condition on
the caught exception's field).
… cast)
Add UncheckedExceptions.lean: four one-line Java methods whose implicit runtime
exception is desugared into an explicit guarded throw, with the triggering
condition captured as an onThrow contract ("if the procedure exits by throwing
X, then C held"):
- NullPointerException x.f (nullness via a boolean flag) + a negative
- IndexOutOfBoundsException a[i] (array as Map int int + alen)
- ArithmeticException a / b (guard also discharges the built-in div check)
- ClassCastException (Sub) x
Adds a procedure/function clause pairing a pre-state trigger with an exceptional postcondition: `when C throws (e) P` means "if C holds on entry, the procedure exits exceptionally and P holds of the thrown value e". It lowers to a Core postcondition `C ==> (Result..isBad($result) ∧ P[e := err])` — checked on exit and assumed at call sites, so a caller can prove a throw will happen (and what then holds). Complements the existing `onThrow (e) P` (`isBad ==> P`, a postcondition on every exceptional exit): the two are converse directions, mirroring JML's `signals` and `exceptional_behavior`. The exception variable is bound per-clause (not procedure-wide), consistent with `catch`/`onThrow`. Threaded through grammar (+ tree translators), AST (`OnThrowsClause`), resolution (+ collectProcedure, mapProcedureM), heap parameterization, and the translator. The `when` keyword mirrors the `catch e when ...` guard. Tests: OnThrows.lean (positive, negative, caller proves the throw from an opaque contract) and an added array behavior-case in UncheckedExceptions.lean.
… pass (E7) Move the exception->Result lowering (throw, try/catch/finally, throws/onThrow/when-throws) out of LaurelToCoreTranslator into a dedicated Laurel-to-Laurel pass so the transformation is reviewable as Laurel in / Laurel out. The translator is now exception-agnostic. Adds a before/after reviewability test that runs the pipeline on a progression of small programs (minimal throw through nested try/finally, each with its Java equivalent) and prints the procedures before and after the pass.
Following the StrataTest/Transform/PrecondElim convention: each case's input is an authored #strata program (the before), and the pass output is pinned with #guard_msgs (the after), so the effect of the pass is explicitly captured and a regression fails the test. The pass is run in isolation on the resolved surface program, keeping the snapshots free of heap-parameterization plumbing (the heap-interaction path is covered by the pipeline verifying tests). Covers onThrow, when-throws, call+catch, finally-on-return (F18), re-throw from catch, nested try/finally, and multi-clause catch.
When a procedure declares a valid `throws T` but states no explicit `onThrow`, resolution now synthesizes `onThrow (e) e is T`. Without this a bare `throws` is consumed only by the (early, static) ExceptionEscapeCheck and the declared exception type is dropped at lowering; the synthesized clause flows through heap parameterization and the type-hierarchy transform, and EliminateExceptions turns it into `Result..isBad($result) ==> Result..err($result) is T`, so the type survives into Core. Gated on the throws type being a well-formed BaseException subtype (so an invalid `throws int` does not cascade a spurious "cannot test unrelated type" diagnostic) and on there being no author-written onThrow. Idempotent under re-resolution. Updates the EliminateExceptionsPass golden and regenerates the lowering-examples doc.
…ng examples Case 4 (closeAndReturn) now maps the Java local to a distinct Laurel local and uses a value-carrying return, so the return value is snapshotted into the output at the return site (before finally) — matching Java's return semantics; both yield 0. The showcase's layer-3 view now runs EliminateValueInReturns before EliminateExceptions so value-returns are shown faithfully rather than dropped.
… (E3) A catch handler's binding was substituted with the shared $exc, so a throw or throwing-call inside the handler that is caught by a nested try/catch overwrote $exc; a later use of the outer handler's binding then read the inner exception. lowerTry now snapshots the caught value into a fresh per-handler local (only when the handler references its binding) and substitutes the binding with it. The dispatch guard still reads $exc (evaluated before any nested throw). Adds regression nestedCatchKeepsBinding and showcase case 8 (nestedCatch); updates the EliminateExceptions golden (case 5, whose handler re-throws its binding) and regenerates the lowering-examples doc.
Add `onThrow modifies …`, a modifies clause for the throwing path distinct from the normal-path `modifies`. It lowers to a frame axiom guarded by Result..isBad($result), built in EliminateExceptions (reusing the ModifiesClauses frame builder); the normal frame stays Good-path-guarded. Emitted only when declared, so existing programs are unaffected. Threads the clause through grammar/parse/print, AST, MapStmtExpr, resolution, and heap parameterization. Adds ExceptionalModifies.lean (positive + negative) and lowering-examples showcase case 9.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.