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

Strata/Languages/Python/PythonToLaurel.lean

@@ -1101,6 +1101,38 @@ def freeVar (name: String) := mkStmtExprMd (.Identifier name)
 def maybeExceptVar := freeVar "maybe_except"
 def nullcall_var := freeVar "nullcall_ret"
 
+-- Invariant: if `callExpr` is not `.Call`, returns `[]`.
+-- Otherwise the returned block always havocs `maybe_except`;
+-- additionally havocs callee (if non-composite instance call)
+-- and `$heap` (if any argument — or the implicit receiver — is composite).
+private def mkHavocStmtsForUnmodeledCall (ctx : TranslationContext)
+    (callExpr : Python.expr SourceRange)
+    (md : Imperative.MetaData Core.Expression) : List StmtExprMd :=
+  if let .Call _ funccall args kwords := callExpr then
+    let holeExceptHavoc := [mkStmtExprMdWithLoc (StmtExpr.Assign [maybeExceptVar] (mkStmtExprMd (.Hole false none))) md]
+    let (calleeHavoc, calleeIsComposite) :=
+      if let (.Attribute _ callee _ _) := funccall then
+        let (base, _) := getListAttributes callee
+        if let .Name _ n _ := base then
+          match ctx.variableTypes.find? (λ v => Prod.fst v == n.val) with
+          | some (varName, ty) =>
+            if isCompositeType ctx ty then ([], true)
+            else
+              ([mkStmtExprMdWithLoc (StmtExpr.Assign [freeVar varName] (mkStmtExprMd (.Hole false none))) md], false)
+          | _ => ([], false)
+        else ([], false)
+      else ([], false)
+    let inputExprs:= args.val.toList ++ kwords.val.toList.map (λ kw => match kw with
+            | keyword.mk_keyword _ _ expr => expr)
+    let involveHeap := calleeIsComposite || (inputExprs.any fun inputExpr =>
+        match inferExprType ctx inputExpr with
+        | .ok ty => isCompositeType ctx ty
+        | _ => false)
+    let heapHavoc := if !involveHeap then [] else
+        [mkStmtExprMdWithLoc (StmtExpr.Assign [freeVar "$heap"] (mkStmtExprMd (.Hole false none))) md]
+    [mkStmtExprMd $ .Block (holeExceptHavoc ++ calleeHavoc ++ heapHavoc) none]
+  else []
+
 partial def translateAssign  (ctx : TranslationContext)
                              (lhs: Python.expr SourceRange)
                              (annotation: Option (Python.expr SourceRange) )
@@ -1135,15 +1167,12 @@ partial def translateAssign  (ctx : TranslationContext)
   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 []
+    let havocStmts := mkHavocStmtsForUnmodeledCall ctx rhs md
     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 +1184,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
@@ -1488,10 +1517,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang
 
     -- 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 []
+    let havocStmts := mkHavocStmtsForUnmodeledCall ctx value md
+
     match expr.val with
     | .StaticCall fnname _ =>
         match ctx.functionSignatures.find? (λ funsig => funsig.name == fnname) with
@@ -1505,7 +1532,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,13 @@
+test_havoc_callee_after_hole_call.py(7, 0): ✅ pass - assert_assert(115)_calls_Any_to_bool_0
+test_havoc_callee_after_hole_call.py(7, 0): ❓ unknown - expected unknown because xs should be havocked
+test_havoc_callee_after_hole_call.py(12, 0): ✅ pass - assert_assert(230)_calls_Any_to_bool_0
+test_havoc_callee_after_hole_call.py(12, 0): ❓ unknown - expected unknown because xs should be havocked
+test_havoc_callee_after_hole_call.py(17, 0): ✅ pass - assert_assert(363)_calls_Any_to_bool_0
+test_havoc_callee_after_hole_call.py(17, 0): ❓ unknown - expected unknown because xs should be havocked
+test_havoc_callee_after_hole_call.py(21, 0): ✅ pass - assert_assert(486)_calls_Any_to_bool_0
+test_havoc_callee_after_hole_call.py(21, 0): ✅ pass - expected pass nothing should be havocked
+test_havoc_callee_after_hole_call.py(23, 0): ✅ pass - callElimAssert_requires_5
+test_havoc_callee_after_hole_call.py(26, 0): ✅ pass - assert_assert(612)_calls_Any_to_bool_0
+test_havoc_callee_after_hole_call.py(26, 0): ❓ unknown - expected unknown because heap should be havocked
+DETAIL: 7 passed, 0 failed, 4 inconclusive
+RESULT: Inconclusive

StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py

@@ -0,0 +1,26 @@
+class MyClass:
+    def __init__(self, n: int):
+        self.val : int = n
+
+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" 
+
+
+xs = [1,2]
+xs.some_unmodeled_call_3.some_unmodeled_call_4()
+assert xs == [1, 2], "expected unknown because xs should be havocked" 
+
+xs = [1,2]
+some_function().some_unmodeled_call_5()
+assert xs == [1, 2], "expected pass nothing should be havocked" 
+
+a : MyClass = MyClass(2)
+a.val = 1
+some_unmodeled_call_6(a)
+assert a.val == 1, "expected unknown because heap should be havocked"