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

Strata/Languages/Python/PythonToLaurel.lean

@@ -1139,11 +1139,22 @@ partial def translateAssign  (ctx : TranslationContext)
       if rhsIsCall then
         [mkStmtExprMdWithLoc (StmtExpr.Assign [maybeExceptVar] (mkStmtExprMd (.Hole false none))) md]
       else []
+    let calleeHavoc :=
+      if let .Call _ (.Attribute _ callee _ _) _ _ := rhs 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 []
+    let havocStmts := [mkStmtExprMd $ .Block (exceptHavoc ++ calleeHavoc) none]
     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)] ++ exceptHavoc, true)
+        return (ctx, [mkStmtExprMd (StmtExpr.Assign [targetExpr] rhs_trans)] ++ havocStmts, true)
       else
         -- Use type annotation if it matches a known composite type
         let annType := annotation.map (fun a => pyExprToString a) |>.getD "Any"
@@ -1155,8 +1166,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] ++ exceptHavoc, true)
-    | _ => return (ctx, [mkStmtExprMd .Hole] ++ exceptHavoc, false)
+        return (newctx, [initStmt] ++ havocStmts, true)
+    | _ => return (ctx, [mkStmtExprMd .Hole] ++ havocStmts, false)
   }
   let mut newctx := ctx
   match lhs with
@@ -1492,6 +1503,20 @@ 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 []
+
+    let havocStmts := [mkStmtExprMd $ .Block (holeExceptHavoc ++ calleeHavoc) none]
+
     match expr.val with
     | .StaticCall fnname _ =>
         match ctx.functionSignatures.find? (λ funsig => funsig.name == fnname) with
@@ -1505,7 +1530,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] ++ havocStmts)
     | _ => 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(3, 0): ✅ pass - assert_assert(40)_calls_Any_to_bool_0
+test_havoc_callee_after_hole_call.py(3, 0): ❓ unknown - expected unknown because xs should be havocked
+test_havoc_callee_after_hole_call.py(8, 0): ✅ pass - assert_assert(155)_calls_Any_to_bool_0
+test_havoc_callee_after_hole_call.py(8, 0): ❓ unknown - expected unknown because xs should be havocked
+DETAIL: 2 passed, 0 failed, 2 inconclusive
+RESULT: Inconclusive

StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py

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