diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 1dea923141..d427d2301b 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -1109,38 +1109,6 @@ 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) ) @@ -1175,12 +1143,15 @@ partial def translateAssign (ctx : TranslationContext) let rhsIsCall := match rhs with | .Call _ _ _ _ => true | _ => false if let .Hole := rhs_trans.val then { - let havocStmts := mkHavocStmtsForUnmodeledCall ctx rhs md + let exceptHavoc := + if rhsIsCall then + [mkStmtExprMdWithLoc (StmtExpr.Assign [maybeExceptVar] (mkStmtExprMd (.Hole false none))) md] + else [] 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)] ++ havocStmts, true) + return (ctx, [mkStmtExprMd (StmtExpr.Assign [targetExpr] rhs_trans)] ++ exceptHavoc, true) else -- Use type annotation if it matches a known composite type let annType := annotation.map (fun a => pyExprToString a) |>.getD "Any" @@ -1192,8 +1163,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] ++ havocStmts, true) - | _ => return (ctx, [mkStmtExprMd .Hole] ++ havocStmts, false) + return (newctx, [initStmt] ++ exceptHavoc, true) + | _ => return (ctx, [mkStmtExprMd .Hole] ++ exceptHavoc, false) } let mut newctx := ctx match lhs with @@ -1528,8 +1499,10 @@ 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 havocStmts := mkHavocStmtsForUnmodeledCall ctx value md - + let holeExceptHavoc := + if let .Call _ _ _ _ := value then + [mkStmtExprMdWithLoc (StmtExpr.Assign [maybeExceptVar] (mkStmtExprMd (.Hole false none))) md] + else [] match expr.val with | .StaticCall fnname _ => match ctx.functionSignatures.find? (λ funsig => funsig.name == fnname) with @@ -1543,7 +1516,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] ++ havocStmts) + | .Hole => return (ctx, [expr] ++ holeExceptHavoc) | _ => 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 deleted file mode 100644 index cb803da6ac..0000000000 --- a/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected +++ /dev/null @@ -1,8 +0,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): ❓ unknown - expected unknown because xs should be havocked -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 - 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): ❓ unknown - expected unknown because heap should be havocked -DETAIL: 2 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 deleted file mode 100644 index 0dd809c501..0000000000 --- a/StrataTest/Languages/Python/tests/test_havoc_callee_after_hole_call.py +++ /dev/null @@ -1,26 +0,0 @@ -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"