From 43af1460673fc90d727d001b5a75b06ce2a302f8 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 20 Apr 2026 10:23:33 -0700 Subject: [PATCH 1/5] havoc callee for Hole call --- Strata/Languages/Python/PythonToLaurel.lean | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 7cb878359f..2c1ae4e6b7 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/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, []) From 4655c3c5237d1cfde6f4c5a9174f0ff927790da7 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 20 Apr 2026 11:14:58 -0700 Subject: [PATCH 2/5] add expected test --- .../test_havoc_callee_after_hole_call.expected | 4 ++++ .../Python/tests/test_havoc_callee_after_hole_call.py | 3 +++ 2 files changed, 7 insertions(+) create mode 100644 StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected create mode 100644 StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py diff --git a/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected b/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected new file mode 100644 index 0000000000..b2b0dc7117 --- /dev/null +++ b/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 diff --git a/StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py b/StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py new file mode 100644 index 0000000000..fc0dbd26da --- /dev/null +++ b/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" From c823f7265bd5a166e10c459f522c8484b32afc8e Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Mon, 20 Apr 2026 15:27:26 -0700 Subject: [PATCH 3/5] add havoc after assignment --- Strata/Languages/Python/PythonToLaurel.lean | 21 +++++++++++++++---- ...test_havoc_callee_after_hole_call.expected | 6 ++++-- .../test_havoc_callee_after_hole_call.py | 9 +++++++- 3 files changed, 29 insertions(+), 7 deletions(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 2c1ae4e6b7..8c3c2e3e3d 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/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 @@ -1504,6 +1515,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang else [] else [] + let havocStmts := [mkStmtExprMd $ .Block (holeExceptHavoc ++ calleeHavoc) none] + match expr.val with | .StaticCall fnname _ => match ctx.functionSignatures.find? (λ funsig => funsig.name == fnname) with @@ -1517,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 ++ calleeHavoc) + | .Hole => return (ctx, [expr] ++ havocStmts) | _ => return (ctx, exceptionCheck ++ [expr]) | .Import _ _ | .ImportFrom _ _ _ _ |.Pass _ => return (ctx, []) diff --git a/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected b/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected index b2b0dc7117..6932da81de 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected @@ -1,4 +1,6 @@ -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): ✅ 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 -DETAIL: 1 passed, 0 failed, 1 inconclusive +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 diff --git a/StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py b/StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py index fc0dbd26da..c873f1fd7a 100644 --- a/StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py +++ b/StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py @@ -1,3 +1,10 @@ xs = [1, 2] -xs.some_unmodeled_call(3) +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" + + From 2d011ce3a2b67aaa82823cfe7e83404811b1de20 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 21 Apr 2026 10:43:04 -0700 Subject: [PATCH 4/5] add heap havoc --- Strata/Languages/Python/PythonToLaurel.lean | 62 +++++++++---------- ...test_havoc_callee_after_hole_call.expected | 17 +++-- .../test_havoc_callee_after_hole_call.py | 16 +++++ 3 files changed, 58 insertions(+), 37 deletions(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 99881f456a..e7fb9f7f9c 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1101,6 +1101,34 @@ def freeVar (name: String) := mkStmtExprMd (.Identifier name) def maybeExceptVar := freeVar "maybe_except" def nullcall_var := freeVar "nullcall_ret" +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 := + if let (.Attribute _ callee _ _) := funccall then + let (base, _) := getListAttributes callee + if let .Name _ n _ := base then + match ctx.variableTypes.find? (fun (v, _) => v == n.val) with + | some (varName, ty) => + if isCompositeType ctx ty then [] + else + [mkStmtExprMdWithLoc (StmtExpr.Assign [freeVar varName] (mkStmtExprMd (.Hole false none))) md] + | _ => [] + else [] + else [] + let inputExprs:= args.val.toList ++ kwords.val.toList.map (λ kw => match kw with + | .mk_keyword _ _ expr => expr) + let involveHeap := 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,21 +1163,7 @@ 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 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] + let havocStmts := mkHavocStmtsForUnmodeledCall ctx rhs md match lhs with | .Name _ n _ => if n.val ∈ ctx.variableTypes.unzip.1 then @@ -1499,23 +1513,7 @@ 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 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] + let havocStmts := mkHavocStmtsForUnmodeledCall ctx value md match expr.val with | .StaticCall fnname _ => diff --git a/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected b/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected index 6932da81de..02f9ab0efb 100644 --- a/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected +++ b/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected @@ -1,6 +1,13 @@ -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 +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 diff --git a/StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py b/StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py index c873f1fd7a..0dd809c501 100644 --- a/StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py +++ b/StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py @@ -1,3 +1,7 @@ +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" @@ -8,3 +12,15 @@ 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" From 66c1750772613ca435a96596a00c757eb9238989 Mon Sep 17 00:00:00 2001 From: thanhnguyen-aws Date: Tue, 21 Apr 2026 14:10:18 -0700 Subject: [PATCH 5/5] havoc Heap when callee is composite + add comments --- Strata/Languages/Python/PythonToLaurel.lean | 24 ++++++++++++--------- 1 file changed, 14 insertions(+), 10 deletions(-) diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 6086bce649..d9401c7b06 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1101,29 +1101,33 @@ 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 := + let (calleeHavoc, calleeIsComposite) := if let (.Attribute _ callee _ _) := funccall then let (base, _) := getListAttributes callee if let .Name _ n _ := base then - match ctx.variableTypes.find? (fun (v, _) => v == n.val) with + match ctx.variableTypes.find? (λ v => Prod.fst v == n.val) with | some (varName, ty) => - if isCompositeType ctx ty then [] + if isCompositeType ctx ty then ([], true) else - [mkStmtExprMdWithLoc (StmtExpr.Assign [freeVar varName] (mkStmtExprMd (.Hole false none))) md] - | _ => [] - else [] - 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 - | .mk_keyword _ _ expr => expr) - let involveHeap := inputExprs.any fun inputExpr => + | keyword.mk_keyword _ _ expr => expr) + let involveHeap := calleeIsComposite || (inputExprs.any fun inputExpr => match inferExprType ctx inputExpr with | .ok ty => isCompositeType ctx ty - | _ => false + | _ => false) let heapHavoc := if !involveHeap then [] else [mkStmtExprMdWithLoc (StmtExpr.Assign [freeVar "$heap"] (mkStmtExprMd (.Hole false none))) md] [mkStmtExprMd $ .Block (holeExceptHavoc ++ calleeHavoc ++ heapHavoc) none]