Eliminate redundant exception checks in try/except bodies (#1091)

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.

---------

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>

Author: 3 people

Strata/Languages/Python/PythonToLaurel.lean

@@ -1810,13 +1810,31 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
         handlerCtx := hCtx
         handlerStmts := handlerStmts ++ hStmts
 
-    -- Insert exception checks after each statement in try body
+    -- Insert exception checks only after statements that could modify
+    -- maybe_except (procedure calls that may throw). Consecutive checks
+    -- without intervening modifications are redundant and create unnecessary
+    -- ite branches in the verification conditions.
+    let targetIsMaybeExcept (target : AstNode Variable) : Bool :=
+      match target.val with | .Local n => n == "maybe_except" | _ => false
+    let rec modifiesMaybeExceptVal (e : StmtExpr) : Bool :=
+      match e with
+      | .Assign targets _ => targets.any targetIsMaybeExcept
+      | .Block stmts _ => stmts.any fun s => modifiesMaybeExceptVal s.val
+      | .IfThenElse _ t e => modifiesMaybeExceptVal t.val ||
+          (e.map (modifiesMaybeExceptVal ·.val)).getD false
+      | .While _ _ _ body => modifiesMaybeExceptVal body.val
+      | _ => false
+    let modifiesMaybeExcept (stmt : StmtExprMd) : Bool :=
+      modifiesMaybeExceptVal stmt.val
+    let isException := mkStmtExprMd (StmtExpr.StaticCall "isError"
+      [mkStmtExprMd (StmtExpr.Var (.Local "maybe_except"))])
+    let exitToHandler := mkStmtExprMd (StmtExpr.IfThenElse isException
+      (mkStmtExprMd (StmtExpr.Exit catchersLabel)) none)
     let bodyStmtsWithChecks := bodyStmts.flatMap fun stmt =>
-      let isException := mkStmtExprMd (StmtExpr.StaticCall "isError"
-        [mkStmtExprMd (StmtExpr.Var (.Local "maybe_except"))])
-      let exitToHandler := mkStmtExprMd (StmtExpr.IfThenElse isException
-        (mkStmtExprMd (StmtExpr.Exit catchersLabel)) none)
-      [stmt, exitToHandler]
+      if modifiesMaybeExcept stmt then
+        [stmt, exitToHandler]
+      else
+        [stmt]
 
     -- Normal completion: exit the try block, skipping handlers
     let exitTry := mkStmtExprMd (StmtExpr.Exit tryLabel)

StrataTest/Languages/Python/expected_laurel/test_missing_models.expected

@@ -1,13 +1,13 @@
-test_missing_models.py(12, 4): ❓ unknown (pass on 2 paths, unknown on 1 path) - (Origin_test_helper_procedure_Requires)req_name_is_foo
-test_missing_models.py(12, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
-test_missing_models.py(12, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
-test_missing_models.py(15, 4): ❓ unknown (pass on 2 paths, unknown on 1 path) - (Origin_test_helper_procedure_Requires)req_name_is_foo
-test_missing_models.py(15, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
-test_missing_models.py(15, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
 test_missing_models.py(8, 4): ❓ unknown - init_calls_Any_get_0
 test_missing_models.py(8, 4): ❓ unknown - init_calls_Any_get_1
 test_missing_models.py(9, 4): ❓ unknown - (Origin_test_helper_procedure_Requires)req_name_is_foo
 test_missing_models.py(9, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
 test_missing_models.py(9, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
-DETAIL: 6 passed, 0 failed, 5 inconclusive
+test_missing_models.py(12, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo
+test_missing_models.py(12, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
+test_missing_models.py(12, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
+test_missing_models.py(15, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo
+test_missing_models.py(15, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
+test_missing_models.py(15, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
+DETAIL: 8 passed, 0 failed, 3 inconclusive
 RESULT: Inconclusive

StrataTest/Languages/Python/expected_laurel/test_try_except_modeled.expected

@@ -0,0 +1,16 @@
+test_try_except_modeled.py(8, 4): ✅ pass - assert(337)
+test_try_except_modeled.py(10, 8): ✅ pass - set_result_calls_Any_get_0
+test_try_except_modeled.py(13, 4): ✅ pass - dict access should succeed
+test_try_except_modeled.py(6, 30): ✅ pass - (test_try_dict_access ensures) Return type constraint
+test_try_except_modeled.py(17, 4): ✅ pass - assert(541)
+test_try_except_modeled.py(18, 4): ✅ pass - assert(557)
+test_try_except_modeled.py(19, 4): ✅ pass - assert(572)
+test_try_except_modeled.py(21, 17): ✅ pass - Check PAdd exception
+test_try_except_modeled.py(24, 4): ✅ pass - addition should succeed
+test_try_except_modeled.py(16, 29): ✅ pass - (test_try_arithmetic ensures) Return type constraint
+test_try_except_modeled.py(32, 4): ✅ pass - assert(950)
+test_try_except_modeled.py(35, 12): ✅ pass - set_result_calls_Any_get_0
+test_try_except_modeled.py(38, 4): ✅ pass - nested dict access should succeed
+test_try_except_modeled.py(30, 37): ✅ pass - (test_try_nested_dict_access ensures) Return type constraint
+DETAIL: 14 passed, 0 failed, 0 inconclusive
+RESULT: Analysis success

StrataTest/Languages/Python/expected_laurel/test_try_except_nested.expected

@@ -0,0 +1,7 @@
+test_try_except_nested.py(5, 26): ✅ pass - (might_fail ensures) Return type constraint
+test_try_except_nested.py(9, 4): ✅ pass - assert(256)
+test_try_except_nested.py(12, 12): ✅ pass - (might_fail requires) Type constraint of x
+test_try_except_nested.py(15, 4): ❓ unknown - should succeed
+test_try_except_nested.py(8, 28): ✅ pass - (test_nested_except ensures) Return type constraint
+DETAIL: 4 passed, 0 failed, 1 inconclusive
+RESULT: Inconclusive

StrataTest/Languages/Python/tests/test_try_except_modeled.py

@@ -0,0 +1,43 @@
+# Test: modeled procedure calls in try body that set maybe_except.
+# Dict access (Any_get) and arithmetic (PAdd) are modeled operations
+# that can raise exceptions. The isError check must be inserted after
+# these calls so the except handler is entered on failure.
+
+def test_try_dict_access() -> bool:
+    d: dict = {"key": "value"}
+    result: str = ""
+    try:
+        result = d["key"]
+    except:
+        result = "error"
+    assert result == "value", "dict access should succeed"
+    return True
+
+def test_try_arithmetic() -> bool:
+    x: int = 10
+    y: int = 3
+    result: int = 0
+    try:
+        result = x + y
+    except:
+        result = -1
+    assert result == 13, "addition should succeed"
+    return True
+
+# Modeled call inside nested control flow in try body.
+# The isError check must still be inserted even though the
+# dict access is inside an if branch.
+def test_try_nested_dict_access() -> bool:
+    d: dict = {"key": "value"}
+    result: str = ""
+    try:
+        if True:
+            result = d["key"]
+    except:
+        result = "error"
+    assert result == "value", "nested dict access should succeed"
+    return True
+
+test_try_dict_access()
+test_try_arithmetic()
+test_try_nested_dict_access()

StrataTest/Languages/Python/tests/test_try_except_nested.py

@@ -0,0 +1,18 @@
+# Test: exception-raising call inside nested control flow in try body.
+# The except handler must still be entered when the call inside the if
+# branch raises an exception.
+
+def might_fail(x: int) -> int:
+    return x
+
+def test_nested_except() -> bool:
+    result: int = 0
+    try:
+        if True:
+            result = might_fail(42)
+    except:
+        result = -1
+    assert result == 42, "should succeed"
+    return True
+
+test_nested_except()