Fix Python->Laurel: Havoc callee or Heap after unmodeled InstanceCall

Strata/Languages/Python/PythonToLaurel.lean

@@ -1492,6 +1492,18 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
       if let .Call _ _ _ _ := value then
         [mkStmtExprMdWithLoc (StmtExpr.Assign [maybeExceptVar] (mkStmtExprMd (.Hole false none))) md]
       else []
+
+    let calleeHavoc :=
+      if let .Call _ (.Attribute _ callee _ _) _ _ := value then
+        let (base, _) := getListAttributes callee
+        if let .Name _ n _ := base then
+          if n.val ∈ ctx.variableTypes.unzip.fst then
+            [mkStmtExprMdWithLoc (StmtExpr.Assign [freeVar n.val] (mkStmtExprMd (.Hole false none))) md]
+          else
+            []
+        else []
+      else []
+
     match expr.val with
     | .StaticCall fnname _ =>
         match ctx.functionSignatures.find? (λ funsig => funsig.name == fnname) with
@@ -1505,7 +1517,7 @@ 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)
+    | .Hole => return (ctx, [expr] ++ holeExceptHavoc ++ calleeHavoc)
     | _ => return (ctx, exceptionCheck ++ [expr])
 
   | .Import _ _ | .ImportFrom _ _ _ _ |.Pass _ => return (ctx, [])

StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected

@@ -0,0 +1,4 @@
+test_havoc_callee_after_hole_call.py(3, 0): ✅ pass - assert_assert(38)_calls_Any_to_bool_0
+test_havoc_callee_after_hole_call.py(3, 0): ❓ unknown - expected unknown because xs should be havocked
+DETAIL: 1 passed, 0 failed, 1 inconclusive
+RESULT: Inconclusive

StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py

@@ -0,0 +1,3 @@
+xs = [1, 2]
+xs.some_unmodeled_call(3)
+assert xs == [1, 2], "expected unknown because xs should be havocked"