From 64868102202604df70ddc43a93893405466b1fdb Mon Sep 17 00:00:00 2001 From: Jules Date: Thu, 21 May 2026 14:13:16 -0700 Subject: [PATCH] pyspec: add --reject-approximations CLI flag Adds a strict mode for the Python frontend: every site that would silently approximate an unsupported construct as a havoc'd Hole or silently drop it instead raises a hard unsupportedConstruct error. Default-off for back-compat; the --reject-approximations flag on pyAnalyzeLaurel turns it on. Useful when running a verification you intend to trust: if the run succeeds with the flag on, no Hole was emitted along the way and no statement was silently dropped, so the obligation set is faithful to the source. --- Strata/Languages/Python/PySpecPipeline.lean | 4 +- Strata/Languages/Python/PythonToLaurel.lean | 112 ++++++++++++++---- StrataMain.lean | 7 +- .../Python/RejectApproximationsTest.lean | 48 ++++++++ 4 files changed, 148 insertions(+), 23 deletions(-) create mode 100644 StrataTest/Languages/Python/RejectApproximationsTest.lean diff --git a/Strata/Languages/Python/PySpecPipeline.lean b/Strata/Languages/Python/PySpecPipeline.lean index 21129ebe39..0310febdde 100644 --- a/Strata/Languages/Python/PySpecPipeline.lean +++ b/Strata/Languages/Python/PySpecPipeline.lean @@ -429,6 +429,7 @@ public def pythonAndSpecToLaurel (profile : Bool := false) (quiet : Bool := false) (warningSummaryFile : Option String := none) + (rejectApproximations : Bool := false) : EIO PipelineError Laurel.Program := do let stmts ← profileStep profile "Read Python Ion" do match ← Python.readPythonStrata pythonIonPath |>.toBaseIO with @@ -470,7 +471,8 @@ public def pythonAndSpecToLaurel let metadataPath := sourcePath.getD pythonIonPath let (laurelProgram, _ctx) ← profileStep profile "Translate Python to Laurel" do - match Python.pythonToLaurel preludeInfo stmts metadataPath result.overloads with + match Python.pythonToLaurel preludeInfo stmts metadataPath result.overloads + (rejectApproximations := rejectApproximations) with | .error (.userPythonError range msg) => throw (.userCode range msg) | .error (.unsupportedConstruct msg ast) => throw (.knownLimitation s!"Unsupported construct: {msg}\nAST: {ast}") diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index 0310fb473f..d9a09f0452 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -129,6 +129,11 @@ structure TranslationContext where classesInHierarchy : Std.HashSet String := {} loopBreakLabel : Option String := none loopContinueLabel : Option String := none + /-- When `true`, every site that would silently emit a `Hole` for a + Python construct outside the precise sound subset raises a hard + `unsupportedConstruct` error instead. Default is `false` for + back-compat; the `--reject-approximations` CLI flag turns it on. -/ + rejectApproximations : Bool := false deriving Inhabited /-! ## Error Handling -/ @@ -207,6 +212,32 @@ def stmtExprToVar (e : StmtExprMd) : Except TranslationError VariableMd := /-- A wildcard modifies list, meaning the procedure may modify anything. -/ def wildcardModifies : List StmtExprMd := [mkStmtExprMd .All] +/-- Emit a `Hole` (the lax behavior) or raise `unsupportedConstruct` + under `--reject-approximations`. Used at every site that would + otherwise approximate an unsupported Python construct as a havoc'd + Hole. The `construct` argument names the surface form (e.g., + `"BinOp Div"`) for the error message. -/ +def rejectableHole (rejectApproximations : Bool) (construct astRepr : String) + : Except TranslationError StmtExprMd := + if rejectApproximations then + throw (.unsupportedConstruct + s!"[approximation] {construct} is approximated as Hole; not in the sound subset" + astRepr) + else + pure (mkStmtExprMd .Hole) + +/-- Same as `rejectableHole` but for sites that silently drop a Python + statement (e.g., `raise`, `try…else`, `for…else`) under lax mode. + The error message names the dropped construct. -/ +def rejectableDrop (rejectApproximations : Bool) (construct astRepr : String) + : Except TranslationError Unit := + if rejectApproximations then + throw (.unsupportedConstruct + s!"[approximation] {construct} is silently dropped today; not in the sound subset" + astRepr) + else + pure () + /-- Create a StmtExprMd with source location metadata. -/ def mkStmtExprMdWithLoc (expr : StmtExpr) (source : Option FileRange) : StmtExprMd := { val := expr, source := source } @@ -577,21 +608,25 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang -- Bytes literal | .Constant _ (.ConBytes _ _) _ => - return mkStmtExprMd .Hole + rejectableHole ctx.rejectApproximations + "bytes literal" (toString (repr e)) -- Float literal | .Constant _ (.ConFloat _ f) _ => match parseFloatString f.val with | some d => return floatToAny d - | none => return mkStmtExprMd .Hole + | none => rejectableHole ctx.rejectApproximations + "unparseable float literal" (toString (repr e)) -- Complex literal | .Constant _ (.ConComplex _ _ _) _ => - return mkStmtExprMd .Hole + rejectableHole ctx.rejectApproximations + "complex literal" (toString (repr e)) -- Ellipsis literal | .Constant _ (.ConEllipsis _) _ => - return mkStmtExprMd .Hole + rejectableHole ctx.rejectApproximations + "ellipsis (...) as expression" (toString (repr e)) -- Variable references | .Name _ name _ => @@ -606,15 +641,19 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang | .Add _ => .ok "PAdd" | .Sub _ => .ok "PSub" | .Mult _ => .ok "PMul" - | .Div _ => return mkStmtExprMd .Hole -- Floating-point are not supported yet + | .Div _ => return ← rejectableHole ctx.rejectApproximations + "BinOp Div (true division)" (toString (repr e)) | .FloorDiv _ => .ok "PFloorDiv" -- Python // maps to Laurel Div | .Mod _ => .ok "PMod" | .Pow _ => .ok "PPow" | .LShift _ => .ok "PLShift" | .RShift _ => .ok "PRShift" - | .BitAnd _ => return mkStmtExprMd .Hole --TODO: Adding BitVector subtype in Any type, then the related operations - | .BitOr _ => return mkStmtExprMd .Hole - | .BitXor _ => return mkStmtExprMd .Hole + | .BitAnd _ => return ← rejectableHole ctx.rejectApproximations + "BinOp BitAnd" (toString (repr e)) + | .BitOr _ => return ← rejectableHole ctx.rejectApproximations + "BinOp BitOr" (toString (repr e)) + | .BitXor _ => return ← rejectableHole ctx.rejectApproximations + "BinOp BitXor" (toString (repr e)) -- Unsupported for now | _ => throw (.unsupportedConstruct s!"Binary operator not yet supported: {repr op}" (toString (repr e))) return mkStmtExprMdWithLoc (StmtExpr.StaticCall preludeOpnames [leftExpr, rightExpr]) md @@ -769,8 +808,12 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang return mkStmtExprMd (.StaticCall "from_str" [concat]) -- Interpolation / TemplateStr (Python 3.14+ t-strings) - not yet supported - | .Interpolation .. => return mkStmtExprMd .Hole - | .TemplateStr .. => return mkStmtExprMd .Hole + | .Interpolation .. => + rejectableHole ctx.rejectApproximations + "string interpolation (t-string)" (toString (repr e)) + | .TemplateStr .. => + rejectableHole ctx.rejectApproximations + "template string (t-string)" (toString (repr e)) | .IfExp _ cond thenb elseb => let condExpr ← translateExpr ctx cond @@ -846,7 +889,8 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang else if isPackage ctx obj then -- FIXME: Module attribute (e.g., sys.argv): modules are not modeled as -- Laurel values, so return Hole like we do for unmodeled package calls. - return mkStmtExprMd .Hole + rejectableHole ctx.rejectApproximations + "module attribute access" (toString (repr e)) else -- Regular object.field access let objExpr ← translateExpr ctx obj @@ -872,24 +916,34 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang -- Set literal: {1, 2, 3} -- Abstract: return havoc'd set (sound abstraction) - | .Set .. => return mkStmtExprMd .Hole + | .Set .. => + rejectableHole ctx.rejectApproximations + "Set literal" (toString (repr e)) -- Tuple literal: (1, 2) | .Tuple _ elems _ => translateList ctx elems.val.toList -- List comprehension: [x for x in items] -- Abstract: return havoc'd list (sound abstraction) - | .ListComp .. => return mkStmtExprMd .Hole + | .ListComp .. => + rejectableHole ctx.rejectApproximations + "list comprehension" (toString (repr e)) -- Set comprehension: {x for x in items} -- Abstract: return havoc'd set (sound abstraction) - | .SetComp .. => return mkStmtExprMd .Hole + | .SetComp .. => + rejectableHole ctx.rejectApproximations + "set comprehension" (toString (repr e)) -- Dict comprehension: {k: v for k, v in items} - | .DictComp .. => return mkStmtExprMd .Hole + | .DictComp .. => + rejectableHole ctx.rejectApproximations + "dict comprehension" (toString (repr e)) -- Generator expression: (x for x in items) - | .GeneratorExp .. => return mkStmtExprMd .Hole + | .GeneratorExp .. => + rejectableHole ctx.rejectApproximations + "generator expression" (toString (repr e)) | _ => throw (.unsupportedConstruct "Expression type not yet supported" (toString (repr e))) @@ -1703,8 +1757,11 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang return (bodyCtx, preamble ++ [ifStmt]) -- While loop - | .While _ test body _orelse => do + | .While _ test body orelse => do -- Note: Python while-else not supported yet + if !orelse.val.isEmpty then + rejectableDrop ctx.rejectApproximations + "while…else clause" (toString (repr s)) let condExpr ← translateExpr ctx test let breakLabel := s!"loop_break_{test.toAst.ann.start.byteIdx}" let continueLabel := s!"loop_continue_{test.toAst.ann.start.byteIdx}" @@ -1795,7 +1852,13 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang | .Import _ _ | .ImportFrom _ _ _ _ |.Pass _ => return (ctx, []) -- Try/except - wrap body with exception checks and handlers - | .Try _ body handlers _ _ => do + | .Try _ body handlers orelse finalbody => do + if !orelse.val.isEmpty then + rejectableDrop ctx.rejectApproximations + "try…else clause" (toString (repr s)) + if !finalbody.val.isEmpty then + rejectableDrop ctx.rejectApproximations + "try…finally clause" (toString (repr s)) let tryLabel := s!"try_end_{s.toAst.ann.start.byteIdx}" let catchersLabel := s!"exception_handlers_{s.toAst.ann.start.byteIdx}" let (bodyCtx, bodyStmts) ← translateStmtList ctx body.val.toList @@ -1854,7 +1917,9 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang -- FIXME: Placeholder — `raise` is dropped so the Hole type inferrer doesn't -- produce Unknown types. Must be replaced to correctly model exceptions later. - | .Raise _ _ _ => return (ctx, []) + | .Raise _ _ _ => do + rejectableDrop ctx.rejectApproximations "raise" (toString (repr s)) + return (ctx, []) -- With statement: with EXPR as VAR: BODY -- Desugars to: mgr = EXPR; VAR = mgr.__enter__(); BODY; mgr.__exit__() @@ -1907,7 +1972,10 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang -- Note that Any_iter_index(iter, index) should not return an exception when 0 <= index < Any_len(iter) -- and Any_iter_index is only called inside the loop body where that condition is satisfied, -- so it is sound to not put it inside AnyMaybeExceptionList - | .For _ target iter body _orelse _ => do + | .For _ target iter body orelse _ => do + if !orelse.val.isEmpty then + rejectableDrop ctx.rejectApproximations + "for…else clause" (toString (repr s)) -- The iterator expression (we abstract it away). -- When the expression contains side-effect statements (e.g. a block with -- receiver havoc from an unmodeled method call), bind it to a temporary @@ -2714,6 +2782,7 @@ def pythonToLaurel (info : PreludeInfo) (body : Array (stmt SourceRange)) (filePath : String := "") (overloadTable : OverloadTable := {}) + (rejectApproximations : Bool := false) : Except TranslationError (Laurel.Program × TranslationContext) := do -- Collect user function names (top-level and class methods) let userFunctions := body.toList.flatMap fun stmt => @@ -2822,7 +2891,8 @@ def pythonToLaurel (info : PreludeInfo) compositeTypeReverse := compositeTypeReverse, exhaustiveClasses := exhaustiveClasses, classesInHierarchy := classesInHierarchy, - filePath := filePath + filePath := filePath, + rejectApproximations := rejectApproximations } -- Separate functions from other statements diff --git a/StrataMain.lean b/StrataMain.lean index 1e6700ff54..78e51ae3a9 100644 --- a/StrataMain.lean +++ b/StrataMain.lean @@ -587,6 +587,9 @@ def pyAnalyzeLaurelCommand : Command where takesArg := .arg "file" }, { name := "skip-verification", help := "Run Python-to-Laurel and Laurel-to-Core translation only (skip SMT verification).", + takesArg := .none }, + { name := "reject-approximations", + help := "Reject every Python construct currently approximated as a havoc'd Hole or silently dropped. First error stops translation. Off by default.", takesArg := .none }] help := "Verify a Python Ion program via the Laurel pipeline. Translates Python to Laurel to Core, then runs SMT verification." callback := fun v pflags => do @@ -612,11 +615,13 @@ def pyAnalyzeLaurelCommand : Command where | some (pyPath, srcText) => some (pyPath, .ofString srcText) | none => none let warningSummaryFile := pflags.getString "warning-summary" + let rejectApproximations := pflags.getBool "reject-approximations" let combinedLaurel ← match ← Strata.pythonAndSpecToLaurel filePath dispatchModules pyspecModules sourcePath (specDir := specDir) (profile := profile) (quiet := quiet) - (warningSummaryFile := warningSummaryFile) |>.toBaseIO with + (warningSummaryFile := warningSummaryFile) + (rejectApproximations := rejectApproximations) |>.toBaseIO with | .ok r => pure r | .error (.userCode range msg) => let location := if range.isNone then "" else diff --git a/StrataTest/Languages/Python/RejectApproximationsTest.lean b/StrataTest/Languages/Python/RejectApproximationsTest.lean new file mode 100644 index 0000000000..ca5a17b101 --- /dev/null +++ b/StrataTest/Languages/Python/RejectApproximationsTest.lean @@ -0,0 +1,48 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Python.PythonToLaurel + +/-! # `--reject-approximations` flag tests + +Unit tests for the `rejectableHole` / `rejectableDrop` helpers: with +the flag off, they emit a `Hole` / no-op (lax behavior); with the flag +on, they raise `unsupportedConstruct` with an `[approximation]` tag. +-/ + +namespace Strata.Python.RejectApproximationsTest + +open Strata.Python (rejectableHole rejectableDrop) +open Strata.Python.TranslationError + +-- rejectableHole false -> emits a Hole (lax behavior preserved) +#guard + match rejectableHole false "BinOp Div" "" with + | .ok ⟨.Hole, _⟩ => true + | _ => false + +-- rejectableHole true -> raises unsupportedConstruct with [approximation] tag +#guard + match rejectableHole true "BinOp Div" "" with + | .error (.unsupportedConstruct msg _) => + msg.startsWith "[approximation]" && (msg.splitOn "BinOp Div").length > 1 + | _ => false + +-- rejectableDrop false -> no-op +#guard + match rejectableDrop false "raise" "" with + | .ok () => true + | _ => false + +-- rejectableDrop true -> raises with "silently dropped" wording +#guard + match rejectableDrop true "raise" "" with + | .error (.unsupportedConstruct msg _) => + msg.startsWith "[approximation]" + && (msg.splitOn "silently dropped").length > 1 + | _ => false + +end Strata.Python.RejectApproximationsTest