diff --git a/Strata/Languages/Python/PySpecPipeline.lean b/Strata/Languages/Python/PySpecPipeline.lean index d1fbadf17..055fd4d42 100644 --- a/Strata/Languages/Python/PySpecPipeline.lean +++ b/Strata/Languages/Python/PySpecPipeline.lean @@ -309,11 +309,16 @@ public def pyAnalyzeLaurel let preludeInfo := buildPreludeInfo result let metadataPath := sourcePath.getD pythonIonPath - let (laurelProgram, _ctx) ← + let (laurelProgram, ctx) ← match Python.pythonToLaurel' preludeInfo pyModule none metadataPath result.overloads with | .error (.userPythonError range msg) => throw (.userCode range msg) | .error e => throw (.internal s!"Python to Laurel translation failed: {e}") - | .ok result => pure result + | .ok r => pure r + + if !ctx.abstractedStatements.isEmpty then + let _ ← IO.eprintln s!"{ctx.abstractedStatements.length} abstracted construct(s) (not fully translated):" |>.toBaseIO + for (loc, kind) in ctx.abstractedStatements do + let _ ← IO.eprintln s!" {loc}: {kind}" |>.toBaseIO return combinePySpecLaurel preludeInfo result.laurelProgram laurelProgram diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean index bd8bba409..193707948 100644 --- a/Strata/Languages/Python/PythonToLaurel.lean +++ b/Strata/Languages/Python/PythonToLaurel.lean @@ -95,6 +95,8 @@ structure TranslationContext where currentClassName : Option String := none loopBreakLabel : Option String := none loopContinueLabel : Option String := none + /-- Abstracted statements recorded for warning emission -/ + abstractedStatements : List (SourceRange × String) := [] deriving Inhabited /-! ## Error Handling -/ @@ -121,6 +123,21 @@ def TranslationError.toString : TranslationError → String instance : ToString TranslationError where toString := TranslationError.toString +/-- Warnings about abstracted constructs (location × description) -/ +abbrev TranslationWarnings := List (SourceRange × String) + +/-- Monad for expression translation: can throw errors and accumulate warnings -/ +abbrev ExprM := StateT TranslationWarnings (Except TranslationError) + +/-- Record an abstraction warning -/ +def ExprM.warn (loc : SourceRange) (kind : String) : ExprM Unit := + modify ([(loc, kind)] ++ ·) + +/-- Run an ExprM computation, returning result and accumulated warnings -/ +def ExprM.run' (m : ExprM α) : Except TranslationError (α × TranslationWarnings) := do + let (result, warnings) ← StateT.run m [] + return (result, warnings.reverse) + /-- Throw a user code error indicating a detected bug in the Python source. -/ def throwUserError [MonadExceptOf TranslationError m] (range : SourceRange := .none) (msg : String) : m α := throw (.userPythonError range msg) @@ -156,6 +173,12 @@ def mkStmtExprMd (expr : StmtExpr) : StmtExprMd := def mkStmtExprMdWithLoc (expr : StmtExpr) (md : Imperative.MetaData Core.Expression) : StmtExprMd := { val := expr, md := md } +/-- Generate statements that havoc all in-scope variables (assign Hole to each) -/ +def havocAllVars (ctx : TranslationContext) : List StmtExprMd := + ctx.variableTypes.map fun (name, _) => + let target := mkStmtExprMd (.Identifier name) + mkStmtExprMd (.Assign [target] (mkStmtExprMd .Hole)) + /-- Extract string representation from Python expression (for type annotations) -/ partial def pyExprToString (e : Python.expr SourceRange) : String := match e with @@ -343,23 +366,23 @@ def ListAny_mk (es: List StmtExprMd) : StmtExprMd := match es with mutual partial def translateList (ctx : TranslationContext) (elmts: List (Python.expr SourceRange)) - : Except TranslationError StmtExprMd := do + : ExprM StmtExprMd := do let trans_elmts ← elmts.mapM (translateExpr ctx) return mkStmtExprMd (.StaticCall "from_ListAny" [ListAny_mk trans_elmts]) partial def translateDictStrAny (ctx : TranslationContext) (keys: List (Python.opt_expr SourceRange)) (values: List (Python.expr SourceRange)) - : Except TranslationError StmtExprMd := do + : ExprM StmtExprMd := do if keys.length != values.length then throw (.internalError s!"Invalid Dict: number of keys not match number of values" ) let kv := keys.zip values let val_trans ← kv.unzip.snd.mapM (translateExpr ctx) - let keys ← keys.mapM pyOptExprToString + let keys ← (keys.mapM pyOptExprToString : Except _ _) return mkStmtExprMd (.StaticCall "from_Dict" [DictStrAny_mk (keys.zip val_trans)]) /-- Translate Python expression to Laurel StmtExpr -/ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRange) - : Except TranslationError StmtExprMd := do + : ExprM StmtExprMd := do match e with -- Integer literals | .Constant _ (.ConPos _ n) _ => return intToAny n.val @@ -397,17 +420,19 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang let rightExpr ← translateExpr ctx right let preludeOpnames ← match op with -- Arithmetic - | .Add _ => .ok "PAdd" - | .Sub _ => .ok "PSub" - | .Mult _ => .ok "PMul" + | .Add _ => pure "PAdd" + | .Sub _ => pure "PSub" + | .Mult _ => pure "PMul" | .Div _ => return mkStmtExprMd .Hole -- Floating-point are not supported yet - | .FloorDiv _ => .ok "PFloorDiv" -- Python // maps to Laurel Div - | .Mod _ => .ok "PMod" + | .FloorDiv _ => pure "PFloorDiv" -- Python // maps to Laurel Div + | .Mod _ => pure "PMod" | .BitAnd _ => return mkStmtExprMd .Hole --TODO: Adding BitVector subtype in Any type, then the related operations | .BitOr _ => return mkStmtExprMd .Hole | .BitXor _ => return mkStmtExprMd .Hole - -- Unsupported for now - | _ => throw (.unsupportedConstruct s!"Binary operator not yet supported: {repr op}" (toString (repr e))) + -- Unsupported for now — abstract as Hole (uninterpreted value) + | _ => + ExprM.warn left.toAst.ann s!"BinOp({repr op})" + return mkStmtExprMd .Hole return mkStmtExprMd (StmtExpr.StaticCall preludeOpnames [leftExpr, rightExpr]) -- Comparison operations @@ -419,14 +444,14 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang let leftExpr ← translateExpr ctx left let rightExpr ← translateExpr ctx comparators.val[0]! let preludeOpnames ← match ops.val[0]! with - | .Eq _ => .ok "PEq" - | .NotEq _ => .ok "PNEq" - | .Lt _ => .ok "PLt" - | .LtE _ => .ok "PLe" - | .Gt _ => .ok "PGt" - | .GtE _ => .ok "PGe" - | .In _ => .ok "PIn" - | .NotIn _ => .ok "PNotIn" + | .Eq _ => pure "PEq" + | .NotEq _ => pure "PNEq" + | .Lt _ => pure "PLt" + | .LtE _ => pure "PLe" + | .Gt _ => pure "PGt" + | .GtE _ => pure "PGe" + | .In _ => pure "PIn" + | .NotIn _ => pure "PNotIn" | _ => throw (.unsupportedConstruct s!"Comparison operator not yet supported: {repr ops.val[0]!}" (toString (repr e))) return mkStmtExprMd (StmtExpr.StaticCall preludeOpnames [leftExpr, rightExpr]) @@ -435,8 +460,8 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang if values.val.size < 2 then throw (.internalError "BoolOp must have at least 2 operands") let preludeOpnames ← match op with - | .And _ => .ok "PAnd" - | .Or _ => .ok "POr" + | .And _ => pure "PAnd" + | .Or _ => pure "POr" -- Translate all operands let mut exprs : List StmtExprMd := [] for val in values.val do @@ -452,8 +477,8 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang | .UnaryOp _ op operand => do let operandExpr ← translateExpr ctx operand let preludeOpnames ← match op with - | .Not _ => .ok "PNot" - | .USub _ => .ok "PNeg" + | .Not _ => pure "PNot" + | .USub _ => pure "PNeg" | _ => throw (.unsupportedConstruct s!"Unary operator not yet supported: {repr op}" (toString (repr e))) return mkStmtExprMd (StmtExpr.StaticCall preludeOpnames [operandExpr]) @@ -536,7 +561,10 @@ partial def translateExpr (ctx : TranslationContext) (e : Python.expr SourceRang -- Generator expression: (x for x in items) | .GeneratorExp .. => return mkStmtExprMd .Hole - | _ => throw (.unsupportedConstruct "Expression type not yet supported" (toString (repr e))) + -- Unsupported expression — abstract as Hole (uninterpreted value) + | _ => + ExprM.warn e.toAst.ann s!"expr({(toString (repr e)).take 40})" + return mkStmtExprMd .Hole partial def getListAttributes (expr: Python.expr SourceRange): (Python.expr SourceRange) × List String := @@ -635,7 +663,7 @@ partial def refineFunctionCallExpr (ctx : TranslationContext) (func: Python.expr --Kwargs can be a single Dict variable: func_call (**var) or a normal Kwargs (key1 = val1, key2 =val2 ...) partial def translateDictKWords (ctx : TranslationContext) (kw : Python.keyword SourceRange) - : Except TranslationError (String × StmtExprMd) := do + : ExprM (String × StmtExprMd) := do match kw with | .mk_keyword _ name expr => let expr ← translateExpr ctx expr @@ -660,16 +688,15 @@ partial def isVarKwargs (kwords : List (Python.keyword SourceRange)) : Bool := | some _ => false | none => true -partial def translateVarKwargs (ctx : TranslationContext) (kwords : List (Python.keyword SourceRange)) : Except TranslationError StmtExprMd := do +partial def translateVarKwargs (ctx : TranslationContext) (kwords : List (Python.keyword SourceRange)) : ExprM StmtExprMd := do match kwords[0]! with | .mk_keyword _ name expr => match name.val with | some _ => throw (.internalError s!"Keyword arg should be a Dict") | none => - let expr ← translateExpr ctx expr - return expr + translateExpr ctx expr -partial def translateKwargs (ctx : TranslationContext) (kwords : List (Python.keyword SourceRange)): Except TranslationError StmtExprMd := do +partial def translateKwargs (ctx : TranslationContext) (kwords : List (Python.keyword SourceRange)): ExprM StmtExprMd := do if isVarKwargs kwords then translateVarKwargs ctx kwords else @@ -727,7 +754,7 @@ partial def translateCall (ctx : TranslationContext) (f : Python.expr SourceRange) (args : List (Python.expr SourceRange)) (kwords : List (Python.keyword SourceRange)) - : Except TranslationError StmtExprMd := do + : ExprM StmtExprMd := do -- Step 1: factory dispatch (e.g., boto3.client('iam')) if let some className ← resolveDispatch ctx f args.toArray then return mkStmtExprMd (.New className) @@ -773,6 +800,17 @@ partial def translateCall (ctx : TranslationContext) end +/-- Run translateExpr, discarding warnings -/ +def translateExprVal (ctx : TranslationContext) (e : Python.expr SourceRange) + : Except TranslationError StmtExprMd := do + let (result, _) ← (translateExpr ctx e).run' + return result + +/-- Run translateExpr, returning both result and warnings -/ +def translateExprW (ctx : TranslationContext) (e : Python.expr SourceRange) + : Except TranslationError (StmtExprMd × TranslationWarnings) := + (translateExpr ctx e).run' + /-! ## Statement Translation Translate Python statements to Laurel StmtExpr nodes. @@ -794,7 +832,8 @@ partial def translateAssign (ctx : TranslationContext) (rhs: Python.expr SourceRange) (md: Imperative.MetaData Core.Expression) : Except TranslationError (TranslationContext × List StmtExprMd) := do - let rhs_trans ← translateExpr ctx rhs + let (rhs_trans, rhsW) ← translateExprW ctx rhs + let ctx := { ctx with abstractedStatements := ctx.abstractedStatements ++ rhsW } if let .Hole := rhs_trans.val then { match lhs with @@ -861,8 +900,9 @@ partial def translateAssign (ctx : TranslationContext) | .Subscript _ _ _ _ => match getSubscriptList lhs with | target :: slices => - let target ← translateExpr ctx target - let slices ← slices.mapM (translateExpr ctx) + let (target, tW) ← translateExprW ctx target + let ctx := { ctx with abstractedStatements := ctx.abstractedStatements ++ tW } + let slices ← slices.mapM (fun e => do let (r, w) ← translateExprW ctx e; pure r) let anySetsExpr := mkStmtExprMd (StmtExpr.StaticCall "Any_sets" [target, ListAny_mk slices, rhs_trans]) let assignStmts := [mkStmtExprMd (StmtExpr.Assign [target] anySetsExpr)] return (ctx,assignStmts) @@ -878,7 +918,8 @@ partial def translateAssign (ctx : TranslationContext) let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [fieldAccess] rhs_trans) md return (ctx, [assignStmt]) else - let targetExpr ← translateExpr ctx lhs -- This will handle self.field via translateExpr + let (targetExpr, tW) ← translateExprW ctx lhs + let ctx := { ctx with abstractedStatements := ctx.abstractedStatements ++ tW } let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] rhs_trans) md return (ctx, [assignStmt]) | _ => throw (.unsupportedConstruct "Assignment targets not yet supported" (toString (repr lhs))) @@ -912,8 +953,22 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang -- If statement | .If _ test body orelse => do - let condExpr ← translateExpr ctx test - let (bodyCtx, bodyStmts) ← translateStmtList ctx body.val.toList + let (condExpr, exprW) ← translateExprW ctx test + let ctx := { ctx with abstractedStatements := ctx.abstractedStatements ++ exprW } + -- Check if condition contains a Hole - if so, hoist to variable to avoid free variable errors + let (condStmts, finalCondExpr, condCtx) := + match condExpr.val with + | .Hole => + -- Hoist Hole to fresh variable + let freshVar := s!"cond_{test.toAst.ann.start.byteIdx}" + let varType := mkHighTypeMd .TBool -- Conditions are bools + let varDecl := mkStmtExprMd (StmtExpr.LocalVariable freshVar varType (some condExpr)) + let varRef := mkStmtExprMd (StmtExpr.Identifier freshVar) + ([varDecl], varRef, { ctx with variableTypes := ctx.variableTypes ++ [(freshVar, "Bool")] }) + | _ => ([], condExpr, ctx) + + -- Translate body (list of statements) + let (bodyCtx, bodyStmts) ← translateStmtList condCtx body.val.toList let bodyBlock := mkStmtExprMd (StmtExpr.Block bodyStmts none) -- Translate else branch if present let elseBlock ← if orelse.val.isEmpty then @@ -928,7 +983,18 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang -- While loop | .While _ test body _orelse => do -- Note: Python while-else not supported yet - let condExpr ← translateExpr ctx test + let (condExpr, exprW) ← translateExprW ctx test + let ctx := { ctx with abstractedStatements := ctx.abstractedStatements ++ exprW } + -- Check if condition contains a Hole - if so, hoist to variable + let (condStmts, finalCondExpr, condCtx) := + match condExpr.val with + | .Hole => + let freshVar := s!"while_cond_{test.toAst.ann.start.byteIdx}" + let varType := mkHighTypeMd .TBool + let varDecl := mkStmtExprMd (StmtExpr.LocalVariable freshVar varType (some condExpr)) + let varRef := mkStmtExprMd (StmtExpr.Identifier freshVar) + ([varDecl], varRef, { ctx with variableTypes := ctx.variableTypes ++ [(freshVar, "bool")] }) + | _ => ([], condExpr, ctx) let breakLabel := s!"loop_break_{test.toAst.ann.start.byteIdx}" let continueLabel := s!"loop_continue_{test.toAst.ann.start.byteIdx}" let loopCtx := { ctx with loopBreakLabel := some breakLabel, loopContinueLabel := some continueLabel } @@ -942,7 +1008,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang | .Return _ value => do let stmts ← match value.val with | some expr => do - let e ← translateExpr ctx expr + let (e, exprW) ← translateExprW ctx expr + let ctx := { ctx with abstractedStatements := ctx.abstractedStatements ++ exprW } let assign := mkStmtExprMd (StmtExpr.Assign [mkStmtExprMd (StmtExpr.Identifier "LaurelResult")] e) .ok [assign, mkStmtExprMd (StmtExpr.Exit "$body")] | none => .ok [mkStmtExprMd (StmtExpr.Exit "$body")] @@ -950,16 +1017,30 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang -- Assert statement | .Assert _ test _msg => do - let condExpr ← translateExpr ctx test - let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert (Any_to_bool condExpr)) md - return (ctx, [assertStmt]) + let (condExpr, exprW) ← translateExprW ctx test + let ctx := { ctx with abstractedStatements := ctx.abstractedStatements ++ exprW } + -- Check if condition contains a Hole - if so, hoist to variable + let (condStmts, finalCondExpr, condCtx) := + match condExpr.val with + | .Hole => + let freshVar := s!"assert_cond_{test.toAst.ann.start.byteIdx}" + let varType := mkHighTypeMd .TBool + let varDecl := mkStmtExprMd (StmtExpr.LocalVariable freshVar varType (some condExpr)) + let varRef := mkStmtExprMd (StmtExpr.Identifier freshVar) + ([varDecl], varRef, { ctx with variableTypes := ctx.variableTypes ++ [(freshVar, "bool")] }) + | _ => ([], condExpr, ctx) + let assertStmt := mkStmtExprMdWithLoc (StmtExpr.Assert (Any_to_bool finalCondExpr)) md + let result := if condStmts.isEmpty then assertStmt + else mkStmtExprMdWithLoc (StmtExpr.Block (condStmts ++ [assertStmt]) none) md + return (condCtx, [result]) --Ignore comments in source code | .Expr _ (.Constant _ (.ConString _ _) _) => return (ctx, []) -- Expression statement (e.g., function call) | .Expr _ value => do - let expr ← translateExpr ctx value + let (expr, exprW) ← translateExprW ctx value + let ctx := { ctx with abstractedStatements := ctx.abstractedStatements ++ exprW } let expr := { expr with md := md } match expr.val with @@ -1059,7 +1140,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang match item with | .mk_withitem _ ctxExpr optVars => let mgrName := s!"with_mgr_{ctxExpr.toAst.ann.start.byteIdx}" - let mgrExpr ← translateExpr currentCtx ctxExpr + let (mgrExpr, exprW) ← translateExprW currentCtx ctxExpr + currentCtx := { currentCtx with abstractedStatements := currentCtx.abstractedStatements ++ exprW } let mgrTy ← inferExprType currentCtx ctxExpr let mgrLauTy ← translateType currentCtx mgrTy let mgrDecl := mkStmtExprMd (StmtExpr.LocalVariable mgrName mgrLauTy (some mgrExpr)) @@ -1094,7 +1176,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang | _ => throw (.unsupportedConstruct "Only simple variable in for target supported" (toString (repr s))) -- The iterator expression (we abstract it away) - let _iterExpr ← translateExpr ctx iter + let (_iterExpr, exprW) ← translateExprW ctx iter + let ctx := { ctx with abstractedStatements := ctx.abstractedStatements ++ exprW } -- Create context with target variable and loop labels let breakLabel := s!"for_break_{iter.toAst.ann.start.byteIdx}" @@ -1120,8 +1203,8 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang -- Augmented assignment: x += expr → x = x op expr | .AugAssign _ target op value => do - let targetExpr ← translateExpr ctx target - let valueExpr ← translateExpr ctx value + let targetExpr ← translateExprVal ctx target + let valueExpr ← translateExprVal ctx value let rhs := match op with | .Add _ => mkStmtExprMd (StmtExpr.StaticCall "PAdd" [targetExpr, valueExpr]) | .Sub _ => mkStmtExprMd (StmtExpr.StaticCall "PSub" [targetExpr, valueExpr]) @@ -1132,7 +1215,23 @@ partial def translateStmt (ctx : TranslationContext) (s : Python.stmt SourceRang let assignStmt := mkStmtExprMdWithLoc (StmtExpr.Assign [targetExpr] rhs) md return (ctx, [assignStmt]) - | _ => throw (.unsupportedConstruct "Statement type not yet supported" (toString (repr s))) + -- Unsupported statement — record the abstraction, havoc all in-scope + -- variables (sound: the statement could modify anything), and emit + -- `assert *` so the verifier flags the location. + | _ => + let stmtName := match s with + | .Global _ _ => "Global" + | .Nonlocal _ _ => "Nonlocal" + | .Import _ _ => "Import" + | .ImportFrom _ _ _ _ => "ImportFrom" + | .Delete _ _ => "Delete" + | .With _ _ _ _ => "With" + | _ => "unknown" + let newCtx := { ctx with + abstractedStatements := ctx.abstractedStatements ++ [(s.toAst.ann, stmtName)] } + let assertStar := mkStmtExprMdWithLoc (StmtExpr.Assert (mkStmtExprMd .Hole)) md + let block := mkStmtExprMdWithLoc (StmtExpr.Block (havocAllVars ctx ++ [assertStar]) none) md + return (newCtx, [block]) partial def translateStmtList (ctx : TranslationContext) (stmts : List (Python.stmt SourceRange)) : Except TranslationError (TranslationContext × List StmtExprMd) := do @@ -1656,7 +1755,7 @@ def pythonToLaurel' (info : PreludeInfo) otherStmts := otherStmts ++ [stmt] ctx := {ctx with variableTypes:= [("nullcall_ret", PyLauType.Any)]} - let (_, bodyStmts) ← translateStmtList ctx otherStmts + let (finalCtx, bodyStmts) ← translateStmtList ctx otherStmts let bodyStmts := prependExceptHandlingHelper bodyStmts let bodyStmts := mkStmtExprMd (.LocalVariable "__name__" AnyTy (some <| strToAny "__main__")) :: bodyStmts let bodyStmts := (mkStmtExprMd (.LocalVariable "nullcall_ret" AnyTy (some AnyNone))) :: bodyStmts