Python -> Laurel translation: unmodeled method calls to havoc non-receiver arguments too (strata-org#1019)

*Description of changes:*

Havocs locals passed as arguments to unmodeled calls. The call is a
black box that could have side effects on its arguments, and
(non-composite) locals are not reachable via heap havoc + havoc'ing
receiver.

Adds a test case (xs2.unknown_method_that_may_modify_arguments(ys)) to
test_havoc_callee_after_hole_call exercising the new behavior.

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: thanhnguyen-aws <ntson@amazon.com>
Co-authored-by: keyboardDrummer-bot <keyboardDrummer-bot@users.noreply.github.com>
Co-authored-by: Juneyoung Lee <136006969+aqjune-aws@users.noreply.github.com>
Co-authored-by: Joe Hendrix <joehx@amazon.com>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: keyboardDrummer-bot <keyboarddrummer.bot@gmail.com>
Co-authored-by: olivier-aws <obouisso@amazon.com>
Co-authored-by: Robin Salkeld <salkeldr@amazon.com>

Author: 8 people

Strata/Languages/Laurel/LaurelToCoreTranslator.lean

@@ -430,6 +430,9 @@ def translateStmt (stmt : StmtExprMd)
           | .InstanceCall .. =>
               -- Instance method call: havoc the target variable
               return [Core.Statement.havoc ident md]
+          | .Hole _ _ =>
+              -- Hole RHS: havoc the target (unmodeled call side-effect).
+              return [Core.Statement.havoc ident md]
           | _ =>
               let coreExpr ← translateExpr value
               return [Core.Statement.set ident coreExpr md]
@@ -504,6 +507,10 @@ def translateStmt (stmt : StmtExprMd)
       return [Imperative.Stmt.loop (.det condExpr) decreasingExprCore invExprs bodyStmts md]
   | .Exit target =>
       return [Imperative.Stmt.exit (some target) md]
+  | .Hole _ _ =>
+      -- Hole in statement position: treat as havoc (no-op).
+      -- This can occur when an unmodeled call's Block is flattened.
+      return []
   | _ =>
       -- Expression in statement position: preserve as an unused variable init
       exprAsUnusedInit stmt md

Strata/Languages/Python/PythonToLaurel.lean

@@ -1156,7 +1156,35 @@ partial def translateCall (ctx : TranslationContext)
           | .Attribute range _ attr _ => (attr.val, range)
           | _ => (funcName, .none)
         throwUserError range s!"Unknown method '{methodName}'"
-    return mkStmtExprMd .Hole
+    -- 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.
+    let receiverHavoc := match f with
+      | .Attribute _ (.Name _ receiverName _) _ _ =>
+        if receiverName.val ∈ ctx.variableTypes.unzip.1 then
+          [mkStmtExprMd (StmtExpr.Assign
+            [mkStmtExprMd (StmtExpr.Identifier receiverName.val)]
+            (mkStmtExprMd .Hole))]
+        else []
+      | _ => []
+    let argHavoc := args.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
+            [mkStmtExprMd (StmtExpr.Assign
+              [mkStmtExprMd (StmtExpr.Identifier varName)]
+              (mkStmtExprMd (.Hole false none)))]
+          else []
+        | _ => []
+      else []
+    let havocStmts := receiverHavoc ++ argHavoc
+    if havocStmts.isEmpty then
+      return mkStmtExprMd .Hole
+    else
+      return mkStmtExprMd (.Block (havocStmts ++ [mkStmtExprMd .Hole]) none)
   -- Step 3: translate the resolved call
   let methodName := match f with
     | .Attribute _ _ attr _ => attr.val
@@ -1737,7 +1765,9 @@ 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.
+    -- Unmodeled call: havoc is now handled in translateCall via Block.
     | .Hole => return (ctx, [expr] ++ holeExceptHavoc)
+    | .Block _ _ => return (ctx, [expr] ++ holeExceptHavoc)
     | _ => return (ctx, exceptionCheck ++ [expr])
 
   | .Import _ _ | .ImportFrom _ _ _ _ |.Pass _ => return (ctx, [])
@@ -1838,8 +1868,20 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
   -- and Any_iter_index is only called inside the loop body where that condition is satisfied,
   -- so it is sound to not put it inside AnyMaybeExceptionList
   | .For _ target iter body _orelse _ => do
-    -- The iterator expression (we abstract it away)
-    let iterExpr ← translateExpr ctx iter
+    -- The iterator expression (we abstract it away).
+    -- When the expression contains side-effect statements (e.g. a block with
+    -- receiver havoc from an unmodeled method call), bind it to a temporary
+    -- variable so the side effects execute once and the clean variable
+    -- reference can be used in PIn / Any_len / the while condition.
+    -- This mirrors Python semantics where the iterator is evaluated once.
+    let iterRaw ← translateExpr ctx iter
+    let (iterPreamble, iterExpr) := match iterRaw.val with
+      | .Block (_ :: _ :: _) _ =>
+        let varName := s!"$for_iter_{iter.toAst.ann.start.byteIdx}"
+        let varDecl := mkStmtExprMd (StmtExpr.LocalVariable varName AnyTy (some iterRaw))
+        let varRef  := mkStmtExprMd (StmtExpr.Identifier varName)
+        ([varDecl], varRef)
+      | _ => ([], iterRaw)
     if let .Call _ (.Name _ {val:= "range",..} _) _ _  := iter then
       if let .StaticCall "range" _ := iterExpr.val then
         pure ()
@@ -1897,7 +1939,7 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
     let loopStmt := mkStmtExprMdWithLoc (StmtExpr.While counterLtLen [] none innerBlock) md
     let loopBlock := mkStmtExprMdWithLoc (StmtExpr.Block [loopStmt] (some breakLabel)) md
     let (preamble, _) := getExceptionCheckPreamble ctx iterExpr s!"$for_iter_{iter.toAst.ann.start.byteIdx}"
-    return (finalCtx, preamble ++ [counterDecl] ++ [loopBlock])
+    return (finalCtx, iterPreamble ++ preamble ++ [counterDecl] ++ [loopBlock])
 
   | .Break _ =>
     match ctx.loopBreakLabel with

StrataTest/Languages/Python/expected_interpret/test_havoc_callee_after_hole_call.expected

@@ -0,0 +1 @@
+\[ERROR\] procedure '__main__': expected 1 arguments, got 0

StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected

@@ -0,0 +1,10 @@
+test_havoc_callee_after_hole_call.py(8, 0): ❓ unknown - expected unknown because xs should be havocked
+test_havoc_callee_after_hole_call.py(12, 0): ❓ unknown - expected unknown because xs should be havocked
+test_havoc_callee_after_hole_call.py(16, 0): ✔️ always true if reached - chained call: receiver not havocked (chained attribute is not a Name)
+test_havoc_callee_after_hole_call.py(20, 0): ✔️ always true if reached - unrelated variable: nothing should be havocked
+test_havoc_callee_after_hole_call.py(25, 0): ✔️ always true if reached - composite arg: heap not havocked (out of scope)
+test_havoc_callee_after_hole_call.py(30, 0): ❓ unknown - expected unknown because argument locals should be havocked
+test_havoc_callee_after_hole_call.py(36, 0): ❓ unknown - assume_assume(1193)_calls_PIn_0
+test_havoc_callee_after_hole_call.py(37, 4): ✔️ always true if reached - for-loop over unmodeled iterator should not crash
+DETAIL: 4 passed, 0 failed, 4 inconclusive
+RESULT: Inconclusive

StrataTest/Languages/Python/expected_laurel/test_missing_models.expected

@@ -1,7 +1,7 @@
-test_missing_models.py(12, 4): ❓ unknown (pass on 2 paths, unknown on 2 paths) - (Origin_test_helper_procedure_Requires)req_name_is_foo
+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 2 paths) - (Origin_test_helper_procedure_Requires)req_name_is_foo
+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

StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py

@@ -0,0 +1,37 @@
+# strata-args: --check-mode bugFinding --check-level full
+class MyClass:
+    def __init__(self, n: int):
+        self.val : int = n
+
+xs: list[int] = [1, 2]
+xs.some_unmodeled_call_1(3)
+assert xs == [1, 2], "expected unknown because xs should be havocked"
+
+xs = [1,2]
+ys: list[int] = xs.some_unmodeled_call_2()
+assert xs == [1, 2], "expected unknown because xs should be havocked"
+
+xs = [1,2]
+xs.some_unmodeled_call_3.some_unmodeled_call_4()
+assert xs == [1, 2], "chained call: receiver not havocked (chained attribute is not a Name)"
+
+xs = [1,2]
+some_function().some_unmodeled_call_5()
+assert xs == [1, 2], "unrelated variable: nothing should be havocked"
+
+a : MyClass = MyClass(2)
+a.val = 1
+some_unmodeled_call_6(a)
+assert a.val == 1, "composite arg: heap not havocked (out of scope)"
+
+xs2: list[int] = [1, 2]
+ys2: list[int] = []
+xs2.unknown_method_that_may_modify_arguments(ys2)
+assert ys2 == [], "expected unknown because argument locals should be havocked"
+
+# Regression: unmodeled method call as for-loop iterator.
+# The receiver havoc must be lifted out of the iterator expression so
+# the block does not end up in expression position inside the assume.
+response: dict = {"messages": []}
+for msg in response.unmodeled_iter_method():
+    assert True, "for-loop over unmodeled iterator should not crash"