Eliminate redundant exception checks in try/except bodies#1091
Conversation
Only insert isError(maybe_except) checks after statements that actually modify maybe_except (procedure calls that may throw). Previously, every statement in a try body got an isError check, creating massive ite nesting in verification conditions. For a chosen benchmark this reduces 62 down to 8 isError checks (87% reduction). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
There was a problem hiding this comment.
Pull request overview
This PR optimizes Python try/except translation in PythonToLaurel by reducing redundant isError(maybe_except) checks, aiming to shrink verification-condition size while preserving exception-control-flow behavior.
Changes:
- Add a
modifiesMaybeExceptpredicate to decide when to insertisError(maybe_except)checks intrybodies. - Emit
exitToHandlerchecks only after statements deemed capable of updatingmaybe_except, instead of after every statement.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
- Make modifiesMaybeExcept recursive: descend into IfThenElse, While, and Block to detect maybe_except assignments in nested control flow. Previously only checked top-level and one level of Block. - Add test_try_except_nested.py: exception-raising call inside an if branch within a try body, exercising the nested detection path. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The recursive modifiesMaybeExcept correctly eliminates redundant exception checks at lines 12 and 15 (which were inside try/except bodies with nested control flow), reducing from 6 passed + 5 inconclusive to 2 passed + 3 inconclusive. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
The optimization idea is sound: skipping isError(maybe_except) checks after statements that provably don't modify maybe_except is a valid way to reduce ite nesting. The existing review comments about the shallow traversal in modifiesMaybeExcept (missing writes inside IfThenElse, While, nested try, With, etc.) are the main correctness concern and I won't repeat them.
One additional observation: the existing test suite has no try-body that contains a modeled procedure call (one that actually sets maybe_except). Every current try-body test uses only simple assignments or raise. This means the optimization's core behavior — inserting isError checks selectively after throwing calls — is exercised by zero tests, not just the nested-construct edge case.
Exercises the core optimization: isError checks are selectively inserted after modeled calls (Any_get for dict access, PAdd for arithmetic) that set maybe_except. Covers: - Dict access in try body (top-level) - Arithmetic in try body (top-level) - Dict access inside nested if in try body All 14 checks pass, confirming the optimization correctly inserts isError checks after modeled calls while skipping non-modifying statements. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
|
@keyboardDrummer-bot Please resolve git conflicts. |
The optimization only eliminates redundant isError checks in the try body. The procedure calls at lines 12 and 15 are in except handlers, so their verification results remain in the output.
Only insert isError(maybe_except) checks after statements that actually modify maybe_except (procedure calls that may throw). Previously, every statement in a try body got an isError check, creating massive ite nesting in verification conditions.
For a chosen benchmark this reduces 62 down to 8 isError checks (87% reduction).
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.