Improve exception logic for missing Python models (#714)

### Changes
- Improve handling of missing models by also assigning a hole to
`maybe_except`
- Improve Laurel's type inference for holes

### Testing
- Update expect file for `test_missing_models`

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: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
Co-authored-by: keyboardDrummer-bot <keyboarddrummer.bot@gmail.com>

Author: keyboardDrummer

Strata/Languages/Python/PythonRuntimeLaurelPart.lean

@@ -13,7 +13,7 @@ namespace Python
 
 /--
 Python prelude declarations expressed in Laurel grammar.
-Converted from PythonRuntimeCorePart.lean (Core dialect) to Laurel dialect.
+Converted from PythonLaurelCorePrelude.lean (Core dialect) to Laurel dialect.
 
 Core-specific constructs that Laurel does not support:
 - `inline` keyword: noted in comments

Strata/Languages/Python/PythonToLaurel.lean

@@ -1055,13 +1055,20 @@ partial def translateAssign  (ctx : TranslationContext)
       stmts := stmts ++ eltStmts
     return (curCtx, stmts)
   let rhs_trans ←  translateExpr ctx rhs
+  -- When an unmodeled call produces a Hole, also havoc maybe_except since
+  -- the call is a black box that could throw any exception.
+  let rhsIsCall := match rhs with | .Call _ _ _ _ => true | _ => false
   if let .Hole := rhs_trans.val then
   {
+    let exceptHavoc :=
+      if rhsIsCall then
+        [mkStmtExprMdWithLoc (StmtExpr.Assign [maybeExceptVar] (mkStmtExprMd (.Hole false none))) md]
+      else []
     match lhs with
     | .Name _ n _ =>
       if n.val ∈ ctx.variableTypes.unzip.1 then
         let targetExpr := mkStmtExprMd (StmtExpr.Identifier n.val)
-        return (ctx, [mkStmtExprMd (StmtExpr.Assign [targetExpr] rhs_trans)])
+        return (ctx, [mkStmtExprMd (StmtExpr.Assign [targetExpr] rhs_trans)] ++ exceptHavoc)
       else
         -- Use type annotation if it matches a known composite type
         let annType := annotation.map (fun a => pyExprToString a) |>.getD "Any"
@@ -1073,8 +1080,8 @@ partial def translateAssign  (ctx : TranslationContext)
           | _ => pure (AnyTy, "Any")
         let initStmt := mkStmtExprMd (StmtExpr.LocalVariable n.val varTy (mkStmtExprMd .Hole))
         let newctx := {ctx with variableTypes:=(n.val, trackType)::ctx.variableTypes}
-        return (newctx, [initStmt])
-    | _ => return (ctx, [mkStmtExprMd .Hole])
+        return (newctx, [initStmt] ++ exceptHavoc)
+    | _ => return (ctx, [mkStmtExprMd .Hole] ++ exceptHavoc)
   }
   let mut newctx := ctx
   match lhs with
@@ -1374,6 +1381,12 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     let expr := { expr with md := md }
     let exceptionCheck := getExceptionAssertions ctx expr
 
+    -- When a call has no model (translates to Hole), also havoc maybe_except
+    -- since an unmodeled call is a black box that could throw any exception.
+    let holeExceptHavoc :=
+      if let .Call _ _ _ _ := value then
+        [mkStmtExprMdWithLoc (StmtExpr.Assign [maybeExceptVar] (mkStmtExprMd (.Hole false none))) md]
+      else []
     match expr.val with
     | .StaticCall fnname _ =>
         match ctx.functionSignatures.find? (λ funsig => funsig.name == fnname) with
@@ -1385,6 +1398,9 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
             else
               return (ctx, exceptionCheck ++ [expr])
         | _ => return (ctx, exceptionCheck ++ [expr])
+    -- Unmodeled call: skip exception checks (no model to check against),
+    -- but havoc maybe_except since the call could throw.
+    | .Hole => return (ctx, [expr] ++ holeExceptHavoc)
     | _ => return (ctx, exceptionCheck ++ [expr])
 
   | .Import _ _ | .ImportFrom _ _ _ _ |.Pass _ => return (ctx, [])

StrataTest/Languages/Python/PreludeVerifyTest.lean

@@ -23,193 +23,16 @@ private def preludeProgram : Core.Program :=
   | some prog => prog
   | none => { decls := [] }
 
-private def verifyPrelude : IO Core.VCResults := do
+private def verifyPrelude : IO (Array DiagnosticModel) := do
   IO.FS.withTempDir fun tempDir => do
     let r ← EIO.toIO (IO.Error.userError ∘ toString)
       (Core.verify preludeProgram tempDir
         (options := .quiet)
         (moreFns := Strata.Python.ReFactory)
         (externalPhases := [Strata.frontEndPhase]))
-    return r
+    return r.flatMap (fun vcr => (toDiagnosticModel vcr []).toArray)
 
-/--
-info:
-Obligation: postcondition
-Property: assert
-Result: ✅ pass
-
-Obligation: List_take_body_calls_List_take_0
-Property: assert
-Result: ✅ pass
-
-Obligation: List_take_len_post_postcondition_calls_List_take_0
-Property: assert
-Result: ✅ pass
-
-Obligation: assume_postcondition_calls_List_take_0
-Property: assert
-Result: ✅ pass
-
-Obligation: postcondition
-Property: assert
-Result: ✅ pass
-
-Obligation: List_drop_body_calls_List_drop_0
-Property: assert
-Result: ✅ pass
-
-Obligation: List_drop_len_post_postcondition_calls_List_drop_0
-Property: assert
-Result: ✅ pass
-
-Obligation: assume_postcondition_calls_List_drop_0
-Property: assert
-Result: ✅ pass
-
-Obligation: postcondition
-Property: assert
-Result: ✅ pass
-
-Obligation: postcondition
-Property: assert
-Result: ✅ pass
-
-Obligation: List_get_non_neg_body_calls_List_get_0
-Property: assert
-Result: ✅ pass
-
-Obligation: List_get_body_calls_List_get_non_neg_0
-Property: assert
-Result: ✅ pass
-
-Obligation: List_get_body_calls_List_get_non_neg_1
-Property: assert
-Result: ✅ pass
-
-Obligation: List_slice_non_neg_body_calls_List_drop_0
-Property: assert
-Result: ✅ pass
-
-Obligation: List_slice_non_neg_body_calls_List_take_1
-Property: assert
-Result: ✅ pass
-
-Obligation: List_slice_body_calls_List_slice_non_neg_0
-Property: assert
-Result: ✅ pass
-
-Obligation: List_set_non_neg_body_calls_List_set_0
-Property: assert
-Result: ✅ pass
-
-Obligation: List_set_body_calls_List_set_non_neg_0
-Property: assert
-Result: ✅ pass
-
-Obligation: List_set_body_calls_List_set_non_neg_1
-Property: assert
-Result: ✅ pass
-
-Obligation: DictStrAny_get_body_calls_DictStrAny_get_0
-Property: assert
-Result: ✅ pass
-
-Obligation: DictStrAny_get_or_none_body_calls_DictStrAny_get_0
-Property: assert
-Result: ✅ pass
-
-Obligation: Any_get_body_calls_DictStrAny_get_0
-Property: assert
-Result: ✅ pass
-
-Obligation: Any_get_body_calls_List_get_1
-Property: assert
-Result: ✅ pass
-
-Obligation: Any_get!_body_calls_DictStrAny_get_0
-Property: assert
-Result: ✅ pass
-
-Obligation: Any_get!_body_calls_List_get_1
-Property: assert
-Result: ✅ pass
-
-Obligation: Any_set_body_calls_List_set_0
-Property: assert
-Result: ✅ pass
-
-Obligation: Any_set!_body_calls_List_set_0
-Property: assert
-Result: ✅ pass
-
-Obligation: PFloorDiv_body_calls_Int.SafeDiv_0
-Property: division by zero check
-Result: ✅ pass
-
-Obligation: PFloorDiv_body_calls_Int.SafeDiv_1
-Property: division by zero check
-Result: ✅ pass
-
-Obligation: PFloorDiv_body_calls_Int.SafeDiv_2
-Property: division by zero check
-Result: ✅ pass
-
-Obligation: PFloorDiv_body_calls_Int.SafeDiv_3
-Property: division by zero check
-Result: ✅ pass
-
-Obligation: PAnd_body_calls_Any_to_bool_0
-Property: assert
-Result: ✅ pass
-
-Obligation: POr_body_calls_Any_to_bool_0
-Property: assert
-Result: ✅ pass
-
-Obligation: PMod_body_calls_Int.SafeMod_0
-Property: division by zero check
-Result: ✅ pass
-
-Obligation: PMod_body_calls_Int.SafeMod_1
-Property: division by zero check
-Result: ✅ pass
-
-Obligation: PMod_body_calls_Int.SafeMod_2
-Property: division by zero check
-Result: ✅ pass
-
-Obligation: PMod_body_calls_Int.SafeMod_3
-Property: division by zero check
-Result: ✅ pass
-
-Obligation: postcondition
-Property: assert
-Result: ✅ pass
-
-Obligation: postcondition
-Property: assert
-Result: ✅ pass
-
-Obligation: postcondition
-Property: assert
-Result: ✅ pass
-
-Obligation: assert(43079)
-Property: assert
-Result: ✅ pass
-
-Obligation: assert(43146)
-Property: assert
-Result: ✅ pass
-
-Obligation: assert(43254)
-Property: assert
-Result: ✅ pass
-
-Obligation: postcondition
-Property: assert
-Result: ✅ pass
--/
+/-- info: #[] -/
 #guard_msgs in
 #eval verifyPrelude
 

StrataTest/Languages/Python/expected_laurel/test_missing_models.expected

@@ -1,7 +1,31 @@
+test_missing_models.py(12, 4): ❓ unknown - (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 - (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(12, 4): ❓ unknown - (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 - (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(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
 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: 2 passed, 0 failed, 3 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: 22 passed, 0 failed, 7 inconclusive
 RESULT: Inconclusive