Python -> Laurel translation: unmodeled method calls to havoc non-receiver arguments too

Strata/Languages/Python/PythonToLaurel.lean

@@ -1674,7 +1674,32 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
         | _ => 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)
+    -- Also havoc the receiver and Any-typed arguments since the unmodeled
+    -- call may mutate them and value-typed locals are not reachable via heap havoc.
+    -- Note: composite-typed arguments are NOT havoc'd here. If the unmodeled
+    -- call mutates a composite's fields, the heap should be havoc'd, but that
+    -- requires coordination with HeapParameterization and is out of scope.
+    | .Hole =>
+      let receiverHavoc := match value with
+        | .Call _ (.Attribute _ (.Name _ receiverName _) _ _) _ _ =>
+          if receiverName.val ∈ ctx.variableTypes.unzip.1 then
+            let target := mkStmtExprMd (StmtExpr.Identifier receiverName.val)
+            [mkStmtExprMdWithLoc (StmtExpr.Assign [target] (mkStmtExprMd .Hole)) md]
+          else []
+        | _ => []
+      let argHavoc := match value with
+        | .Call _ _ args _ =>
+          args.val.toList.flatMap fun arg =>
+            if let .Name _ n _ := arg then
+              match ctx.variableTypes.find? (λ v => Prod.fst v == n.val) with
+              | some (varName, ty) =>
+                if ty == PyLauType.Any then
+                  [mkStmtExprMdWithLoc (StmtExpr.Assign [freeVar varName] (mkStmtExprMd (.Hole false none))) md]
+                else []
+              | _ => []
+            else []
+        | _ => []
+      return (ctx, [expr] ++ receiverHavoc ++ argHavoc ++ holeExceptHavoc)
     | _ => return (ctx, exceptionCheck ++ [expr])
 
   | .Import _ _ | .ImportFrom _ _ _ _ |.Pass _ => return (ctx, [])

StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected

@@ -0,0 +1,6 @@
+test_havoc_callee_after_hole_call.py(9, 4): ❓ unknown - set_x_calls_Any_get_0
+test_havoc_callee_after_hole_call.py(9, 4): ❓ unknown - assert(176)
+test_havoc_callee_after_hole_call.py(14, 4): ❓ unknown - set_y_calls_Any_get_0
+test_havoc_callee_after_hole_call.py(14, 4): ❓ unknown - assert(270)
+DETAIL: 0 passed, 0 failed, 4 inconclusive
+RESULT: Inconclusive

StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py

@@ -0,0 +1,14 @@
+# strata-args: --check-mode bugFinding --check-level full
+class MyClass:
+    def __init__(self, n: int):
+        self.val : int = n
+
+xs: list[int] = []
+xs.append(1)
+if xs:
+    x: int = xs[0]
+
+ys: list[int] = []
+xs.unknown_method_that_may_modify_arguments(ys)
+if ys:
+    y: int = ys[0]