diff --git a/Examples/CFGNondet.core.st b/Examples/CFGNondet.core.st new file mode 100644 index 0000000000..ab23e62eb8 --- /dev/null +++ b/Examples/CFGNondet.core.st @@ -0,0 +1,23 @@ +program Core; + +// Nondeterministic CFG: y is set to either 1 or 2. +procedure NondetChoice(out y : int) +spec { + ensures (y == 1 || y == 2); +} +cfg entry { + entry: { + goto left, right; + } + left: { + y := 1; + goto done; + } + right: { + y := 2; + goto done; + } + done: { + return; + } +}; diff --git a/Examples/CFGSimple.core.st b/Examples/CFGSimple.core.st new file mode 100644 index 0000000000..9e1af0ee9c --- /dev/null +++ b/Examples/CFGSimple.core.st @@ -0,0 +1,48 @@ +program Core; + +// A simple deterministic CFG: compute max of two integers. +procedure Max(x : int, y : int, out m : int) +spec { + ensures (m >= x); + ensures (m >= y); + ensures (m == x || m == y); +} +cfg entry { + entry: { + branch (x >= y) goto then_branch else else_branch; + } + then_branch: { + m := x; + goto done; + } + else_branch: { + m := y; + goto done; + } + done: { + return; + } +}; + +// A CFG with a simple loop: increment y until it reaches n. +procedure CountUp(n : int, out y : int) +spec { + requires (n >= 0); + ensures (y == n); +} +cfg entry { + entry: { + y := 0; + goto loop; + } + loop: { + branch (y < n) goto body else done; + } + body: { + y := y + 1; + goto loop; + } + done: { + return; + } +}; diff --git a/Strata/Backends/CBMC/CoreToCBMC.lean b/Strata/Backends/CBMC/CoreToCBMC.lean index 04617c385c..e8ceee5a9a 100644 --- a/Strata/Backends/CBMC/CoreToCBMC.lean +++ b/Strata/Backends/CBMC/CoreToCBMC.lean @@ -346,7 +346,8 @@ def createImplementationSymbolFromAST (func : Core.Procedure) : Except String CB -- For now, keep the hardcoded implementation but use function name from AST let loc : SourceLoc := { functionName := (func.header.name.toPretty), lineNum := "1" } - let stmtJsons ← (func.body.mapM (stmtToJson (I:=CoreLParams) · loc)) + let bodyStmts ← func.body.getStructured + let stmtJsons ← (bodyStmts.mapM (stmtToJson (I:=CoreLParams) · loc)) let implValue := Json.mkObj [ ("id", "code"), diff --git a/Strata/Backends/CBMC/GOTO.lean b/Strata/Backends/CBMC/GOTO.lean index 132440f8af..77eab4f29e 100644 --- a/Strata/Backends/CBMC/GOTO.lean +++ b/Strata/Backends/CBMC/GOTO.lean @@ -5,6 +5,7 @@ -/ module +import Strata.Backends.CBMC.GOTO.CoreCFGToGOTOPipeline import Strata.Backends.CBMC.GOTO.CoreToCProverGOTO import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline import Strata.Backends.CBMC.GOTO.DefaultSymbols diff --git a/Strata/Backends/CBMC/GOTO/CoreCFGToGOTOPipeline.lean b/Strata/Backends/CBMC/GOTO/CoreCFGToGOTOPipeline.lean new file mode 100644 index 0000000000..889210f62d --- /dev/null +++ b/Strata/Backends/CBMC/GOTO/CoreCFGToGOTOPipeline.lean @@ -0,0 +1,304 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +module + +public import Strata.Backends.CBMC.CollectSymbols +public import Strata.Backends.CBMC.GOTO.CoreToCProverGOTO +import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline +import Strata.Transform.StructuredToUnstructured + +/-! ## Core-to-GOTO translation via CFG + +Alternative pipeline that translates Core procedures to CProver GOTO by going +through the CFG representation: + +- **Structured body** → `stmtsToCFG` → `coreCFGToGotoTransform` +- **CFG body** → `coreCFGToGotoTransform` + +This coexists with the direct path in `CoreToGOTOPipeline.lean`. +-/ + +namespace Strata + +public section + +/-! ### Rename helpers for Core commands (CmdExt) -/ + +private def renameCoreCallArg + (rn : Std.HashMap String String) + : Core.CallArg Core.Expression → Core.CallArg Core.Expression + | .inArg e => .inArg (renameExpr rn e) + | .inoutArg id => .inoutArg (renameIdent rn id) + | .outArg id => .outArg (renameIdent rn id) + +private def renameCoreCommand + (rn : Std.HashMap String String) + : Core.Command → Core.Command + | .cmd c => .cmd (renameCmd rn c) + | .call procName callArgs md => + .call procName (callArgs.map (renameCoreCallArg rn)) md + +private partial def renameCoreStmt + (rn : Std.HashMap String String) + : Core.Statement → Core.Statement + | .cmd c => .cmd (renameCoreCommand rn c) + | .block l stmts md => + .block l (stmts.map (renameCoreStmt rn)) md + | .ite c t e md => + .ite (c.map (renameExpr rn)) (t.map (renameCoreStmt rn)) (e.map (renameCoreStmt rn)) md + | .loop g m i body md => + .loop (g.map (renameExpr rn)) (m.map (renameExpr rn)) + (i.map (fun (l, e) => (l, renameExpr rn e))) + (body.map (renameCoreStmt rn)) md + | .exit l md => .exit l md + | .funcDecl d md => .funcDecl d md + | .typeDecl tc md => .typeDecl tc md + +private def renameCoreDetCFG + (rn : Std.HashMap String String) + (cfg : Core.DetCFG) : Core.DetCFG := + { cfg with blocks := cfg.blocks.map fun (label, block) => + (label, { cmds := block.cmds.map (renameCoreCommand rn), + transfer := match block.transfer with + | .condGoto cond lt lf md => + .condGoto (renameExpr rn cond) lt lf md + | .finish md => .finish md }) } + +/-! ### Core-specific CFG-to-GOTO translation -/ + +/-- +Translate a Core `DetCFG` to CProver GOTO instructions. + +Like `detCFGToGotoTransform` but handles `Core.Command` (which includes +`CmdExt.call`). The CFG should already have identifiers renamed via +`renameCoreDetCFG`. +-/ +def coreCFGToGotoTransform + (_Env : Core.Expression.TyEnv) (functionName : String) + (cfg : Core.DetCFG) + (trans : Imperative.GotoTransform Core.Expression.TyEnv) + : Except Std.Format (Imperative.GotoTransform Core.Expression.TyEnv) := do + let toExpr := Lambda.LExpr.toGotoExprCtx + (TBase := ⟨Core.ExpressionMetadata, Unit⟩) [] + -- Verify entry block is first + match cfg.blocks with + | (firstLabel, _) :: _ => + if firstLabel != cfg.entry then + throw f!"[coreCFGToGotoTransform] Entry label '{cfg.entry}' does not match \ + first block label '{firstLabel}'." + | [] => pure () + let mut trans := trans + let mut pendingPatches : Array (Nat × String) := #[] + let mut labelMap : Std.HashMap String Nat := {} + let mut loopContracts : Std.HashMap String (Imperative.MetaData Core.Expression) := {} + for (label, block) in cfg.blocks do + labelMap := labelMap.insert label trans.nextLoc + let srcLoc : CProverGOTO.SourceLocation := + { CProverGOTO.SourceLocation.nil with function := functionName } + trans := Imperative.emitLabel label srcLoc trans + -- Translate each command + for cmd in block.cmds do + match cmd with + | .cmd c => + trans ← Imperative.Cmd.toGotoInstructions trans.T functionName c trans + | .call procName callArgs _md => + let lhs := Core.CallArg.getLhs callArgs + let args := Core.CallArg.getInputExprs callArgs + let argExprs ← args.mapM toExpr + let lhsExpr := match lhs with + | id :: _ => + let name := Core.CoreIdent.toPretty id + let ty := match trans.T.context.types.find? id with + | some lty => + match lty.toMonoTypeUnsafe.toGotoType with + | .ok gty => gty + | .error _ => + dbg_trace s!"warning: type conversion failed for {name}, defaulting to Integer" + .Integer + | none => + dbg_trace s!"warning: no type found for {name}, defaulting to Integer" + .Integer + CProverGOTO.Expr.symbol name ty + | [] => CProverGOTO.Expr.symbol "" .Empty + let calleeExpr := CProverGOTO.Expr.symbol procName + (CProverGOTO.Ty.mkCode (argExprs.map (·.type)) lhsExpr.type) + let callCode := CProverGOTO.Code.functionCall lhsExpr calleeExpr argExprs + let inst : CProverGOTO.Instruction := + { type := .FUNCTION_CALL, code := callCode, locationNum := trans.nextLoc } + trans := { trans with + instructions := trans.instructions.push inst + nextLoc := trans.nextLoc + 1 } + -- Translate the transfer command + match block.transfer with + | .condGoto cond lt lf md => + let transferSrcLoc := Imperative.metadataToSourceLoc md functionName trans.sourceText + let cond_expr ← toExpr cond + let hasLoopContract := md.any fun elem => + elem.fld == Imperative.MetaData.specLoopInvariant || + elem.fld == Imperative.MetaData.specDecreases + if hasLoopContract then + loopContracts := loopContracts.insert label md + let (trans', falseIdx) := + Imperative.emitCondGoto (CProverGOTO.Expr.not cond_expr) transferSrcLoc trans + trans := trans' + pendingPatches := pendingPatches.push (falseIdx, lf) + let (trans', trueIdx) := Imperative.emitUncondGoto transferSrcLoc trans + trans := trans' + pendingPatches := pendingPatches.push (trueIdx, lt) + | .finish _md => + pure () + -- Second pass: resolve labels and annotate backward-edge GOTOs with loop contracts + let mut resolvedPatches : List (Nat × Nat) := [] + for (idx, label) in pendingPatches do + match labelMap[label]? with + | some targetLoc => + resolvedPatches := (idx, targetLoc) :: resolvedPatches + if let some md := loopContracts[label]? then + let instLoc := trans.instructions[idx]!.locationNum + if targetLoc ≤ instLoc then + let mut guard := trans.instructions[idx]!.guard + for elem in md do + if elem.fld == Imperative.MetaData.specLoopInvariant then + if let .expr e := elem.value then + let gotoExpr ← toExpr e + guard := guard.setNamedField "#spec_loop_invariant" gotoExpr + if elem.fld == Imperative.MetaData.specDecreases then + if let .expr e := elem.value then + let gotoExpr ← toExpr e + guard := guard.setNamedField "#spec_decreases" gotoExpr + trans := { trans with + instructions := trans.instructions.set! idx + { trans.instructions[idx]! with guard := guard } } + | none => + throw f!"[coreCFGToGotoTransform] Unresolved label '{label}' referenced \ + by GOTO at instruction index {idx}." + return Imperative.patchGotoTargets trans resolvedPatches + +/-! ### Pipeline wrapper -/ + +/-- +Translate a Core procedure to CProver GOTO via the CFG representation. + +Mirrors `procedureToGotoCtx` but routes through `stmtsToCFG` + +`coreCFGToGotoTransform` instead of the direct Stmt-to-GOTO path. +-/ +def procedureToGotoCtxViaCFG + (Env : Core.Expression.TyEnv) (p : Core.Procedure) + (sourceText : Option String := none) + (axioms : List Core.Axiom := []) + (distincts : + List (Core.Expression.Ident × List Core.Expression.Expr) := []) + : Except Std.Format + (CoreToGOTO.CProverGOTO.Context × List Core.Function) := do + let pname := Core.CoreIdent.toPretty p.header.name + if !p.header.typeArgs.isEmpty then + .error f!"[procedureToGotoCtxViaCFG] Polymorphic procedures unsupported." + let ret_ty := CProverGOTO.Ty.Empty + let formals := p.header.inputs.keys.map Core.CoreIdent.toPretty + let formals_tys ← p.header.inputs.values.mapM Lambda.LMonoTy.toGotoType + let new_formals := formals.map (CProverGOTO.mkFormalSymbol pname ·) + let formals_tys : Map String CProverGOTO.Ty := formals.zip formals_tys + let outputs := p.header.outputs.keys.map Core.CoreIdent.toPretty + let new_outputs := outputs.map (CProverGOTO.mkLocalSymbol pname ·) + let locals_from_body := match p.body with + | .structured ss => (Imperative.Block.definedVars ss).map Core.CoreIdent.toPretty + | .cfg c => c.blocks.flatMap (fun (_, blk) => + blk.cmds.flatMap Core.Command.definedVars) + |>.map Core.CoreIdent.toPretty + let new_locals := locals_from_body.map (CProverGOTO.mkLocalSymbol pname ·) + let rn : Std.HashMap String String := + (formals.zip new_formals ++ outputs.zip new_outputs ++ locals_from_body.zip new_locals).foldl + (init := {}) fun m (k, v) => m.insert k v + -- Seed the type environment with renamed input and output parameter types + let inputEntries : Map Core.Expression.Ident Core.Expression.Ty := + (new_formals.zip p.header.inputs.values).map fun (n, ty) => + (((n : Core.CoreIdent)), .forAll [] ty) + let outputEntries : Map Core.Expression.Ident Core.Expression.Ty := + (new_outputs.zip p.header.outputs.values).map fun (n, ty) => + (((n : Core.CoreIdent)), .forAll [] ty) + let Env' : Core.Expression.TyEnv := + Lambda.TEnv.addInNewestContext (T := ⟨Core.ExpressionMetadata, Unit⟩) + Env (inputEntries ++ outputEntries) + -- Emit axioms as ASSUME instructions + let mut axiomInsts : Array CProverGOTO.Instruction := #[] + let mut axiomLoc : Nat := 0 + for ax in axioms do + let gotoExpr ← Lambda.LExpr.toGotoExprCtx + (TBase := ⟨Core.ExpressionMetadata, Unit⟩) [] ax.e + if gotoExpr.hasUnsupportedQuantifierTypes then continue + axiomInsts := axiomInsts.push + { type := .ASSUME, locationNum := axiomLoc, + guard := gotoExpr, + sourceLoc := { CProverGOTO.SourceLocation.nil with + function := pname, comment := s!"axiom {ax.name}" } } + axiomLoc := axiomLoc + 1 + -- Emit distinct declarations as pairwise != ASSUME instructions + for (dname, exprs) in distincts do + let gotoExprs ← exprs.mapM + (Lambda.LExpr.toGotoExprCtx (TBase := ⟨Core.ExpressionMetadata, Unit⟩) []) + for i in List.range gotoExprs.length do + for j in List.range gotoExprs.length do + if i < j then + let ei := gotoExprs[i]! + let ej := gotoExprs[j]! + let neqExpr : CProverGOTO.Expr := + { id := .binary .NotEqual, type := .Boolean, operands := [ei, ej] } + let srcLoc : CProverGOTO.SourceLocation := + { CProverGOTO.SourceLocation.nil with + function := pname + comment := s!"distinct {Core.CoreIdent.toPretty dname}" } + axiomInsts := axiomInsts.push + { type := .ASSUME, locationNum := axiomLoc, guard := neqExpr, sourceLoc := srcLoc } + axiomLoc := axiomLoc + 1 + -- Build the CFG (from structured body or use existing CFG) + let (cfg, liftedFuncs) ← match p.body with + | .structured ss => do + let (liftedFuncs, body) ← collectFuncDecls ss + let renamedBody := body.map (renameCoreStmt rn) + let cfg := Imperative.stmtsToCFG renamedBody + pure (cfg, liftedFuncs) + | .cfg c => do + let cfg := renameCoreDetCFG rn c + pure (cfg, []) + -- Translate CFG to GOTO + let ans ← coreCFGToGotoTransform Env' pname cfg + { instructions := axiomInsts, nextLoc := axiomLoc, T := Env', sourceText := sourceText } + let ending_insts : Array CProverGOTO.Instruction := + #[{ type := .END_FUNCTION, locationNum := ans.nextLoc + 1 }] + let pgm := { name := pname, + parameterIdentifiers := new_formals.toArray, + instructions := ans.instructions ++ ending_insts } + -- Translate procedure contracts + let mut contracts : List (String × Lean.Json) := [] + let preExprs := p.spec.preconditions.values.filter (fun c => c.attr == .Default) + |>.map (fun c => renameExpr rn c.expr) + let postExprs := p.spec.postconditions.values.filter (fun c => c.attr == .Default) + |>.map (fun c => renameExpr rn c.expr) + let toGotoExpr := Lambda.LExpr.toGotoExprCtx + (TBase := ⟨Core.ExpressionMetadata, Unit⟩) [] + if !preExprs.isEmpty then + let preGoto ← preExprs.mapM toGotoExpr + let preJson ← (preGoto.mapM CProverGOTO.exprToJson).mapError (fun e => f!"{e}") + contracts := contracts ++ [("#spec_requires", + Lean.Json.mkObj [("id", ""), ("sub", Lean.Json.arr preJson.toArray)])] + if !postExprs.isEmpty then + let postGoto ← postExprs.mapM toGotoExpr + let postJson ← (postGoto.mapM CProverGOTO.exprToJson).mapError (fun e => f!"{e}") + contracts := contracts ++ [("#spec_ensures", + Lean.Json.mkObj [("id", ""), ("sub", Lean.Json.arr postJson.toArray)])] + -- Build localTypes map for output parameters + let output_tys ← p.header.outputs.values.mapM Lambda.LMonoTy.toGotoType + let localTypes : Std.HashMap String CProverGOTO.Ty := + (outputs.zip output_tys).foldl (init := {}) fun m (k, v) => m.insert k v + let ctx : CoreToGOTO.CProverGOTO.Context := + { program := pgm, formals := formals_tys, ret := ret_ty, + locals := outputs ++ locals_from_body, contracts := contracts, + localTypes := localTypes } + return (ctx, liftedFuncs) + +end -- public section + +end Strata diff --git a/Strata/Backends/CBMC/GOTO/CoreToCProverGOTO.lean b/Strata/Backends/CBMC/GOTO/CoreToCProverGOTO.lean index a0ef4725c2..de2a53559a 100644 --- a/Strata/Backends/CBMC/GOTO/CoreToCProverGOTO.lean +++ b/Strata/Backends/CBMC/GOTO/CoreToCProverGOTO.lean @@ -201,7 +201,11 @@ def transformToGoto (cprog : Core.Program) : Except Format CProverGOTO.Context : if !p.header.typeArgs.isEmpty then throw f!"[transformToGoto] Translation for polymorphic Strata Core procedures is unimplemented." - let cmds ← p.body.mapM + -- TODO: This pass could be split into a two-stage transformation: + -- 1. structured → cfg (via StructuredToUnstructured) + -- 2. cfg → CProverGOTO (always operates on CFG, no pattern matching needed) + let bodyStmts ← p.body.getStructured.mapError fun s => f!"{s}" + let cmds ← bodyStmts.mapM (fun b => match b with | .cmd (.cmd c) => return c | _ => throw f!"[transformToGoto] We can process Strata Core commands only, not statements! \ @@ -218,7 +222,7 @@ def transformToGoto (cprog : Core.Program) : Except Format CProverGOTO.Context : let formals_renamed := formals.zip new_formals let formals_tys : Map String CProverGOTO.Ty := formals.zip formals_tys - let locals := (Imperative.Block.definedVars p.body).map Core.CoreIdent.toPretty + let locals := (Imperative.Block.definedVars bodyStmts).map Core.CoreIdent.toPretty let new_locals := locals.map (fun l => CProverGOTO.mkLocalSymbol pname l) let locals_renamed := locals.zip new_locals diff --git a/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean b/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean index 2cc5e57433..08cc27ec17 100644 --- a/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean +++ b/Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean @@ -40,12 +40,12 @@ namespace Strata public section -private def renameIdent (rn : Std.HashMap String String) (id : Core.CoreIdent) : Core.CoreIdent := +def renameIdent (rn : Std.HashMap String String) (id : Core.CoreIdent) : Core.CoreIdent := match rn[id.name]? with | some new => ⟨new, id.metadata⟩ | none => id -private partial def renameExpr +partial def renameExpr (rn : Std.HashMap String String) : Core.Expression.Expr → Core.Expression.Expr | .fvar m name ty => .fvar m (renameIdent rn name) ty @@ -56,7 +56,7 @@ private partial def renameExpr | .eq m e1 e2 => .eq m (renameExpr rn e1) (renameExpr rn e2) | e => e -private def renameCmd +def renameCmd (rn : Std.HashMap String String) : Imperative.Cmd Core.Expression → Imperative.Cmd Core.Expression | .init name ty e md => .init (renameIdent rn name) ty (e.map (renameExpr rn)) md @@ -102,7 +102,7 @@ private def hasCallStmt : List Core.Statement → Bool Collect all funcDecl statements from a procedure body (recursively) and return them as Core.Functions, stripping them from the body. -/ -private def collectFuncDecls : List Core.Statement → +def collectFuncDecls : List Core.Statement → Except Std.Format (List Core.Function × List Core.Statement) | [] => return ([], []) | .funcDecl decl _ :: rest => do @@ -259,7 +259,11 @@ def procedureToGotoCtx : Except Std.Format (CoreToGOTO.CProverGOTO.Context × List Core.Function) := do -- Lift local function declarations out of the body - let (liftedFuncs, body) ← collectFuncDecls p.body + -- TODO: This pass could be split into a two-stage transformation: + -- 1. structured → cfg (via StructuredToUnstructured) + -- 2. cfg → CProverGOTO (always operates on CFG, no pattern matching needed) + let bodyStmts ← p.body.getStructured.mapError fun s => f!"{s}" + let (liftedFuncs, body) ← collectFuncDecls bodyStmts let pname := Core.CoreIdent.toPretty p.header.name if !p.header.typeArgs.isEmpty then .error f!"[procedureToGotoCtx] Polymorphic procedures unsupported." diff --git a/Strata/DL/Imperative/BasicBlock.lean b/Strata/DL/Imperative/BasicBlock.lean index c956006655..416c587a64 100644 --- a/Strata/DL/Imperative/BasicBlock.lean +++ b/Strata/DL/Imperative/BasicBlock.lean @@ -40,8 +40,8 @@ inductive DetTransferCmd (Label : Type) (P : PureExpr) where model it instead using `condGoto`. By defining this function, we can easily create unconditional jumps, and future proof against the possibility of adding it as a constructor in the future. -/ -def DetTransferCmd.goto [HasBool P] (l : Label) : DetTransferCmd Label P := - condGoto HasBool.tt l l +def DetTransferCmd.goto [HasBool P] (l : Label) (md : MetaData P := .empty) : DetTransferCmd Label P := + condGoto HasBool.tt l l md /-- A `NondetTransfer` command terminates a non-deterministic basic block, indicating the list of possible blocks where execution could proceed next, if @@ -80,6 +80,26 @@ structure CFG (Label Block : Type) where -------- +/-- Strip metadata from a deterministic transfer command. -/ +def DetTransferCmd.stripMetaData : DetTransferCmd Label P → DetTransferCmd Label P + | .condGoto p lt lf _ => .condGoto p lt lf .empty + | .finish _ => .finish .empty + +/-- Strip metadata from a non-deterministic transfer command. -/ +def NondetTransferCmd.stripMetaData : NondetTransferCmd Label P → NondetTransferCmd Label P + | .goto ls _ => .goto ls .empty + +/-- Strip transfer metadata from a deterministic basic block. -/ +def DetBlock.stripMetaData (blk : DetBlock Label Cmd P) : DetBlock Label Cmd P := + { blk with transfer := blk.transfer.stripMetaData } + +/-- Strip transfer metadata from all blocks in a deterministic CFG. -/ +def CFG.stripDetMetaData (cfg : CFG Label (DetBlock Label Cmd P)) : + CFG Label (DetBlock Label Cmd P) := + { cfg with blocks := cfg.blocks.map fun (lbl, blk) => (lbl, blk.stripMetaData) } + +-------- + open Std (ToFormat Format format) def formatDetTransferCmd (P : PureExpr) (c : DetTransferCmd Label P) diff --git a/Strata/DL/Imperative/CFGSemantics.lean b/Strata/DL/Imperative/CFGSemantics.lean index f472e56d04..61bc0af1a3 100644 --- a/Strata/DL/Imperative/CFGSemantics.lean +++ b/Strata/DL/Imperative/CFGSemantics.lean @@ -23,18 +23,6 @@ This module defines small-step operational semantics for the Imperative dialect's control-flow graph representation. -/ -inductive EvalCmds - {CmdT : Type} - (P : PureExpr) - (EvalCmd : EvalCmdParam P CmdT) : - SemanticEval P → SemanticStore P → List CmdT → SemanticStore P → Bool → Prop where - | eval_cmds_none : - EvalCmds P EvalCmd δ σ [] σ false - | eval_cmds_some : - EvalCmd δ σ c σ' failed → - EvalCmds P EvalCmd δ σ' cs σ'' failed' → - EvalCmds P EvalCmd δ σ (c :: cs) σ'' (failed || failed') - /-- Configuration for small-step semantics, representing the current execution state. A configuration consists of a store and a failure indication flag paired @@ -49,11 +37,24 @@ inductive CFGConfig (l : Type) (P : PureExpr): Type where /-- A terminal configuration, indicating that execution has finished. -/ | terminal : SemanticStore P → Bool → CFGConfig l P -/-- Small-step operational semantics for deterministic basic blocks. Each case -first evaluates the commands in the block. A block ending in `.condGoto` results -in a configuration pointing to the true or false label, depending on the -evaluation of the condition. A block ending in `.finish` results in a terminal -configuration. -/ +/-- Monotonically update the `failure` flag in a `CFGConfig`. It will be set to +`true` if the provided Boolean is `true`. -/ +def updateFailure : CFGConfig l P → Bool → CFGConfig l P +| .cont t σ failed, failed' => .cont t σ (failed || failed') +| .terminal σ failed, failed' => .terminal σ (failed || failed') + +/-- Small-step operational semantics for deterministic basic blocks. Evaluates +commands sequentially, then transfers control based on the block's terminator. + +This is a single recursive inductive that combines command evaluation with +transfer semantics. The `cmd` constructor evaluates one command and recurses +on the remaining commands. The terminal constructors handle the transfer once +all commands are exhausted. + +Structuring it this way (rather than delegating to a separate `EvalCmds` +inductive) ensures that `EvalCmd` is referenced directly in a constructor, +which is required for Lean 4's kernel to accept this type as a nested +inductive in mutual blocks. -/ inductive EvalDetBlock {CmdT : Type} (P : PureExpr) @@ -62,31 +63,31 @@ inductive EvalDetBlock [HasNot P] : SemanticStore P → DetBlock l CmdT P → CFGConfig l P → Prop where - | step_goto_true : - EvalCmds P EvalCmd δ σ cs σ' failed → + | cmd : + EvalCmd δ σ c σ' failed → + EvalDetBlock P EvalCmd extendEval σ' ⟨cs, transfer⟩ config → + EvalDetBlock P EvalCmd extendEval + σ ⟨ c :: cs, transfer ⟩ (updateFailure config failed) + + | goto_true : δ σ c = .some HasBool.tt → WellFormedSemanticEvalBool δ → EvalDetBlock P EvalCmd extendEval - σ ⟨ cs, .condGoto c t e _ ⟩ (.cont t σ' failed) + σ ⟨ [], .condGoto c t e _ ⟩ (.cont t σ false) - | step_goto_false : - EvalCmds P EvalCmd δ σ cs σ' failed → + | goto_false : δ σ c = .some HasBool.ff → WellFormedSemanticEvalBool δ → EvalDetBlock P EvalCmd extendEval - σ ⟨ cs, .condGoto c t e _ ⟩ (.cont e σ' failed) + σ ⟨ [], .condGoto c t e _ ⟩ (.cont e σ false) - | step_terminal : - EvalCmds P EvalCmd δ σ cs σ' failed → + | terminal : EvalDetBlock P EvalCmd extendEval - σ ⟨ cs, .finish _ ⟩ (.terminal σ' failed) + σ ⟨ [], .finish _ ⟩ (.terminal σ false) /-- -Small-step operational semantics for non-deterministic basic blocks. Each case -first evaluates the commands in the block. A block ending in `.goto` with no -labels results in a terminal configuration. A block ending in `.goto` with a -non-empty list of labels results in a configuration pointing to a -non-deterministic choice of one of the labels. +Small-step operational semantics for non-deterministic basic blocks. Evaluates +commands sequentially, then transfers control nondeterministically. -/ inductive EvalNondetBlock {CmdT : Type} @@ -96,24 +97,20 @@ inductive EvalNondetBlock [HasNot P] : SemanticStore P → NondetBlock l CmdT P → CFGConfig l P → Prop where - | step_goto_none : - EvalCmds P EvalCmd δ σ cs σ' failed → + | cmd : + EvalCmd δ σ c σ' failed → + EvalNondetBlock P EvalCmd extendEval σ' ⟨cs, transfer⟩ config → EvalNondetBlock P EvalCmd extendEval - σ ⟨ cs, .goto [] _ ⟩ (.terminal σ' failed) + σ ⟨ c :: cs, transfer ⟩ (updateFailure config failed) - | step_goto_some : - EvalCmds P EvalCmd δ σ cs σ' failed → - lt ∈ ls → + | goto_none : EvalNondetBlock P EvalCmd extendEval - σ ⟨ cs, .goto ls _ ⟩ (.cont lt σ' failed) + σ ⟨ [], .goto [] _ ⟩ (.terminal σ false) -/-- -Monotonically update the `failure` flag in a `CFGConfig`. It will be set to -`true` if the provided Boolean is `true`. --/ -def updateFailure : CFGConfig l P → Bool → CFGConfig l P -| .cont t σ failed, failed' => .cont t σ (failed || failed') -| .terminal σ failed, failed' => .terminal σ (failed || failed') + | goto_some : + lt ∈ ls → + EvalNondetBlock P EvalCmd extendEval + σ ⟨ [], .goto ls _ ⟩ (.cont lt σ false) /-- Operational semantics to step between two configurations of a control-flow diff --git a/Strata/DL/Imperative/CFGToCProverGOTO.lean b/Strata/DL/Imperative/CFGToCProverGOTO.lean index 4faeb5f1db..8b3ad750bf 100644 --- a/Strata/DL/Imperative/CFGToCProverGOTO.lean +++ b/Strata/DL/Imperative/CFGToCProverGOTO.lean @@ -29,27 +29,9 @@ of any particular backend. ## Gaps relative to the direct `Stmt.toGotoInstructions` path -The following features are not yet supported via the CFG path, and would need -to be addressed before it can fully replace the direct path: - -- **Source locations on control flow**: `DetTransferCmd` already carries a - `MetaData` field, but `StructuredToUnstructured.stmtsToBlocks` currently - passes `MetaData.empty` when constructing transfer commands (the metadata - from `ite`/`loop`/`block`/`exit` statements is discarded as `_md`). - Once `stmtsToBlocks` propagates the metadata, this module will pick it up - automatically via `metadataToSourceLoc`. -- **Loop contracts**: The direct path emits `#spec_loop_invariant` and - `#spec_decreases` as named sub-expressions on the backward-edge GOTO - instruction (recognized by CBMC's DFCC). In the CFG, invariants are lowered - to plain `assert` commands and measures are discarded entirely. - To fix: `StructuredToUnstructured.stmtsToBlocks` (the `.loop` case) would - need to preserve invariants and measures in the `DetTransferCmd` (or in a - side channel), and this module would need to emit them as named - sub-expressions on the backward-edge GOTO, mirroring the logic in the - `.loop` case of `Stmt.toGotoInstructions` in `ToCProverGOTO.lean`. - **`Core.CmdExt.call`**: This translation handles `Imperative.Cmd` only. - Core procedure calls (`CmdExt.call`) would need a command translator - analogous to `coreStmtsToGoto` in `CoreToGOTOPipeline.lean`. + Core procedure calls (`CmdExt.call`) are handled by the Core-specific + wrapper `coreCFGToGotoTransform` in `CoreCFGToGOTOPipeline.lean`. -/ namespace Imperative @@ -92,49 +74,64 @@ def detCFGToGotoTransform {P} [G : ToGoto P] [BEq P.Ident] -- Pending GOTO patches: (instruction array index, target label) let mut pendingPatches : Array (Nat × String) := #[] let mut labelMap : Std.HashMap String Nat := {} + -- Loop contract metadata: maps loop entry labels to their contract metadata. + -- Used in the second pass to annotate backward-edge GOTOs. + let mut loopContracts : Std.HashMap String (MetaData P) := {} for (label, block) in cfg.blocks do -- Record this block's entry location labelMap := labelMap.insert label trans.nextLoc - -- Emit a LOCATION marker for the block - -- NOTE(source-locations): `DetTransferCmd` already carries a `MetaData` - -- field, but `StructuredToUnstructured.stmtsToBlocks` currently fills it - -- with `MetaData.empty`. Once `stmtsToBlocks` propagates the metadata - -- from `ite`/`loop`/`block`/`exit` statements, use `metadataToSourceLoc` - -- here (see `Stmt.toGotoInstructions` in ToCProverGOTO.lean for the - -- pattern). let srcLoc : SourceLocation := { SourceLocation.nil with function := functionName } trans := emitLabel label srcLoc trans -- Translate each command via the existing Cmd-to-GOTO mapping. - -- NOTE: This only handles `Imperative.Cmd`. To support `Core.CmdExt.call`, - -- either: - -- (a) generalize this function over the command type and accept a - -- command translator as a parameter, or - -- (b) create a Core-specific wrapper (like `coreStmtsToGoto` in - -- `CoreToGOTOPipeline.lean`) that pattern-matches on `CmdExt` and - -- emits `FUNCTION_CALL` instructions for `.call`, delegating `.cmd` - -- to `Cmd.toGotoInstructions`. for cmd in block.cmds do trans ← Cmd.toGotoInstructions trans.T functionName cmd trans -- Translate the transfer command match block.transfer with - | .condGoto cond lt lf _md => + | .condGoto cond lt lf md => + let transferSrcLoc := metadataToSourceLoc md functionName trans.sourceText let cond_expr ← G.toGotoExpr cond + -- Record loop contracts if present (invariants and/or decreases on this + -- transfer indicate a loop entry block). + let hasLoopContract := md.any fun elem => + elem.fld == MetaData.specLoopInvariant || elem.fld == MetaData.specDecreases + if hasLoopContract then + loopContracts := loopContracts.insert label md -- Emit: GOTO [!cond] lf - let (trans', falseIdx) := emitCondGoto (Expr.not cond_expr) srcLoc trans + let (trans', falseIdx) := emitCondGoto (Expr.not cond_expr) transferSrcLoc trans trans := trans' pendingPatches := pendingPatches.push (falseIdx, lf) -- Emit: GOTO lt (unconditional) - let (trans', trueIdx) := emitUncondGoto srcLoc trans + let (trans', trueIdx) := emitUncondGoto transferSrcLoc trans trans := trans' pendingPatches := pendingPatches.push (trueIdx, lt) | .finish _md => -- No instruction needed; the caller appends END_FUNCTION pure () - -- Second pass: resolve all pending labels, then patch in one call + -- Second pass: resolve all pending labels and annotate backward-edge GOTOs + -- with loop contracts when the target is a loop entry block. let mut resolvedPatches : List (Nat × Nat) := [] for (idx, label) in pendingPatches do match labelMap[label]? with - | some targetLoc => resolvedPatches := (idx, targetLoc) :: resolvedPatches + | some targetLoc => + resolvedPatches := (idx, targetLoc) :: resolvedPatches + -- If this GOTO targets a loop entry with contracts, annotate its guard. + if let some md := loopContracts[label]? then + let instLoc := trans.instructions[idx]!.locationNum + -- Only annotate backward edges (target location <= source location). + if targetLoc ≤ instLoc then + let mut guard := trans.instructions[idx]!.guard + for elem in md do + if elem.fld == MetaData.specLoopInvariant then + if let .expr e := elem.value then + let gotoExpr ← G.toGotoExpr e + guard := guard.setNamedField "#spec_loop_invariant" gotoExpr + if elem.fld == MetaData.specDecreases then + if let .expr e := elem.value then + let gotoExpr ← G.toGotoExpr e + guard := guard.setNamedField "#spec_decreases" gotoExpr + trans := { trans with + instructions := trans.instructions.set! idx + { trans.instructions[idx]! with guard := guard } } | none => throw f!"[detCFGToGotoTransform] Unresolved label '{label}' referenced \ by GOTO at instruction index {idx}." diff --git a/Strata/DL/Imperative/MetaData.lean b/Strata/DL/Imperative/MetaData.lean index f3d3a384d1..9630955c9c 100644 --- a/Strata/DL/Imperative/MetaData.lean +++ b/Strata/DL/Imperative/MetaData.lean @@ -328,6 +328,14 @@ def MetaData.getPropertyType {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Op | _ => none | none => none +/-- Metadata field for a loop invariant expression preserved during structured-to-CFG + lowering. Multiple entries may appear when a loop has multiple invariants. -/ +def MetaData.specLoopInvariant : MetaDataElem.Field P := .label "#spec_loop_invariant" + +/-- Metadata field for a loop decreases (measure) expression preserved during + structured-to-CFG lowering. -/ +def MetaData.specDecreases : MetaDataElem.Field P := .label "#spec_decreases" + /-- Metadata field for property summaries attached to assert/requires/ensures clauses. -/ def MetaData.propertySummary : MetaDataElem.Field P := .label "propertySummary" diff --git a/Strata/Languages/Boole/Verify.lean b/Strata/Languages/Boole/Verify.lean index 5c237ab6e5..7bc2e5f084 100644 --- a/Strata/Languages/Boole/Verify.lean +++ b/Strata/Languages/Boole/Verify.lean @@ -746,6 +746,7 @@ private def registerCommandSymbols (cmd : BooleDDM.Command SourceRange) : List B | .command_block _ _ => [] | .command_axiom _ _ _ => [] | .command_distinct _ _ _ => [] + | .command_cfg_procedure _ _ _ _ _ _ => [] /-- Build the symbol-class table used by `getFVarIsOp`. @@ -806,7 +807,7 @@ private def translateProcedureDecl return [.proc { header := { name := mkIdent n, typeArgs := tys, inputs := allInputs, outputs := allOutputs } spec := spec - body := body + body := .structured body } .empty] def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List Core.Decl) := do @@ -878,8 +879,10 @@ def toCoreDecls (cmd : BooleDDM.Command SourceRange) : TranslateM (List Core.Dec return [.proc { header := { name := mkIdent topLevelBlockProcedureName, typeArgs := [], inputs := [], outputs := [] } spec := { preconditions := [], postconditions := [] } - body := ← toCoreBlock b + body := .structured (← toCoreBlock b) } .empty] + | .command_cfg_procedure _ _ _ _ _ _ => + throwAt default "CFG procedures are not supported in Boole dialect" | .command_datatypes _ ⟨_, decls⟩ => return [.type (.data (← decls.toList.mapM toCoreDatatypeDecl)) .empty] diff --git a/Strata/Languages/C_Simp/Verify.lean b/Strata/Languages/C_Simp/Verify.lean index b04c557882..621769f17c 100644 --- a/Strata/Languages/C_Simp/Verify.lean +++ b/Strata/Languages/C_Simp/Verify.lean @@ -172,7 +172,7 @@ def loop_elimination_function(f : C_Simp.Function) : Core.Procedure := outputs := [("return", f.ret_ty)]}, spec := {preconditions := core_preconditions, postconditions := core_postconditions}, - body := f.body.map loop_elimination_statement} + body := .structured (f.body.map loop_elimination_statement)} def loop_elimination(program : C_Simp.Program) : Core.Program := diff --git a/Strata/Languages/Core/CallGraph.lean b/Strata/Languages/Core/CallGraph.lean index 0ddbc39c53..b4c3fc4794 100644 --- a/Strata/Languages/Core/CallGraph.lean +++ b/Strata/Languages/Core/CallGraph.lean @@ -228,12 +228,17 @@ def extractCallsFromFunction (func : Function) : List String := | some body => extractFunctionCallsFromExpr body | none => [] +/-- Extract procedure calls from a CmdExt -/ +def extractCallsFromCmdExt (cmd : Command) : List String := + match cmd with + | .call procName _ _ => [procName] + | .cmd _ => [] + mutual /-- Extract procedure calls from a single statement -/ def extractCallsFromStatement (stmt : Statement) : List String := match stmt with - | .cmd (.call procName _ _) => [procName] - | .cmd _ => [] + | .cmd c => extractCallsFromCmdExt c | .block _ body _ => extractCallsFromStatements body | .ite _ thenBody elseBody _ => extractCallsFromStatements thenBody ++ @@ -251,9 +256,16 @@ def extractCallsFromStatements (stmts : List Statement) : List String := extractCallsFromStatements rest end +/-- Extract procedure calls from a deterministic CFG -/ +def extractCallsFromDetCFG (cfg : DetCFG) : List String := + cfg.blocks.flatMap fun (_, blk) => + blk.cmds.flatMap extractCallsFromCmdExt + /-- Extract all procedure calls from a procedure's body -/ def extractCallsFromProcedure (proc : Procedure) : List String := - extractCallsFromStatements proc.body + match proc.body with + | .structured ss => extractCallsFromStatements ss + | .cfg c => extractCallsFromDetCFG c @[expose] abbrev ProcedureCG := CallGraph @[expose] abbrev FunctionCG := CallGraph diff --git a/Strata/Languages/Core/Core.lean b/Strata/Languages/Core/Core.lean index e600ad3601..d9582934e9 100644 --- a/Strata/Languages/Core/Core.lean +++ b/Strata/Languages/Core/Core.lean @@ -95,7 +95,12 @@ def buildEnv (options : VerifyOptions) (program : Program) for func in funcs do E ← E.addFactoryFunc func | .distinct _ es _ => E := { E with distinct := es :: E.distinct } | .proc proc _ => - for stmt in proc.body.flatMap collectFuncDecls do + let stmts := match proc.body with + | .structured ss => ss + -- CFG bodies cannot contain local function declarations; + -- funcDecl is a structured statement-level construct only. + | .cfg _ => [] + for stmt in stmts.flatMap collectFuncDecls do match E.exprEnv.addFactoryFunc stmt with | .ok σ' => E := { E with exprEnv := σ' } | .error _ => pure () @@ -174,7 +179,7 @@ def toCoreProofObligationProgram (options : VerifyOptions) (program : Program) | some name => [Decl.proc { header := { name := name, typeArgs := [], inputs := [], outputs := [] }, spec := { preconditions := [], postconditions := [] }, - body := body + body := .structured body } .empty] | none => [] diff --git a/Strata/Languages/Core/DDMTransform/FormatCore.lean b/Strata/Languages/Core/DDMTransform/FormatCore.lean index 0bc517fd8a..32e6975253 100644 --- a/Strata/Languages/Core/DDMTransform/FormatCore.lean +++ b/Strata/Languages/Core/DDMTransform/FormatCore.lean @@ -919,6 +919,49 @@ partial def invariantsToCST {M} [Inhabited M] let restCST ← invariantsToCST rest pure (.consInvariants default labelAnn exprCST restCST) +/-- Convert a `DetTransferCmd` to its CFG-specific CST `Transfer` node. -/ +partial def transferToCST {M} [Inhabited M] + (t : Imperative.DetTransferCmd String Expression) : ToCSTM M (CoreDDM.Transfer M) := do + match t with + | .condGoto cond lt lf _ => + if lt == lf then + pure (.transfer_goto default ⟨default, lt⟩) + else + match cond with + | .fvar _ id _ => + if id.name.startsWith "$__nondet_" then + pure (.transfer_nondet_goto default ⟨default, lt⟩ ⟨default, lf⟩) + else + let condCST ← lexprToExpr cond 0 + pure (.transfer_cond_goto default condCST ⟨default, lt⟩ ⟨default, lf⟩) + | _ => + let condCST ← lexprToExpr cond 0 + pure (.transfer_cond_goto default condCST ⟨default, lt⟩ ⟨default, lf⟩) + | .finish _ => pure (.transfer_return default) + +/-- Convert a single `DetBlock` to a CST `CFGBlock`. -/ +partial def detBlockToCST {M} [Inhabited M] + (label : String) (blk : Imperative.DetBlock String Core.Command Expression) + : ToCSTM M (CoreDDM.CFGBlock M) := do + modify ToCSTContext.pushScope + let cmdStmts ← blk.cmds.toArray.mapM (stmtToCST ∘ Imperative.Stmt.cmd) + let transfer ← transferToCST blk.transfer + modify ToCSTContext.popScope + pure (.cfg_block default ⟨default, label⟩ ⟨default, cmdStmts⟩ transfer) + +/-- Convert a `DetCFG` to a CST `CFGBody`. -/ +partial def detCFGToCST {M} [Inhabited M] (cfg : Core.DetCFG) + : ToCSTM M (CoreDDM.CFGBody M) := do + let cfgBlocks ← cfg.blocks.mapM fun (label, blk) => detBlockToCST label blk + let blocks := cfgBlocks.foldr (init := none) fun blk acc => + match acc with + | none => some (.cfg_blocks_one default blk) + | some rest => some (.cfg_blocks_cons default blk rest) + match blocks with + | some bs => pure (.cfg_body default ⟨default, cfg.entry⟩ bs) + | none => pure (.cfg_body default ⟨default, cfg.entry⟩ + (.cfg_blocks_one default (.cfg_block default ⟨default, cfg.entry⟩ ⟨default, #[]⟩ (.transfer_return default)))) + partial def measureToCST {M} [Inhabited M] (measure : Option (Lambda.LExpr CoreLParams.mono)) : ToCSTM M (Ann (Option (Measure M)) M) := do @@ -988,10 +1031,16 @@ def procToCST {M} [Inhabited M] (proc : Core.Procedure) : ToCSTM M (Command M) : ⟨default, none⟩ else ⟨default, some (Spec.spec_mk default specAnn)⟩ - let bodyCST ← blockToCST proc.body - let body : Ann (Option (CoreDDM.Block M)) M := ⟨default, some bodyCST⟩ + let cmd ← match proc.body with + | .structured ss => + let bodyCST ← blockToCST ss + let body : Ann (Option (CoreDDM.Block M)) M := ⟨default, some bodyCST⟩ + pure (.command_procedure default name typeArgs arguments spec body) + | .cfg c => + let cfgBody ← detCFGToCST c + pure (.command_cfg_procedure default name typeArgs arguments spec cfgBody) modify ToCSTContext.popScope - pure (.command_procedure default name typeArgs arguments spec body) + pure cmd -- Recreate enough of `GlobalContext` from `ToCSTContext` obtained from -- `programToCST`, purely for formatting. diff --git a/Strata/Languages/Core/DDMTransform/Grammar.lean b/Strata/Languages/Core/DDMTransform/Grammar.lean index 0375a10596..3680ec9524 100644 --- a/Strata/Languages/Core/DDMTransform/Grammar.lean +++ b/Strata/Languages/Core/DDMTransform/Grammar.lean @@ -25,7 +25,7 @@ namespace Strata -- Sequence operations and lambda/application syntax increase the grammar size enough -- to require higher recursion and heartbeat limits. -set_option maxRecDepth 10000 +set_option maxRecDepth 20000 set_option maxHeartbeats 400000 /- DDM support for parsing and pretty-printing Strata Core -/ @@ -465,6 +465,59 @@ op datatype_decl (name : Ident, op command_datatypes (datatypes : NewlineSepBy DatatypeDecl) : Command => datatypes ";\n"; +// ===================================================================== +// CFG (Unstructured Control Flow) Syntax +// ===================================================================== + +// Transfer commands: how a basic block ends +category Transfer; + +// Unconditional goto: exactly one target. +op transfer_goto (label : Ident) : Transfer => + "goto " label ";"; + +// Nondeterministic goto: exactly two targets chosen nondeterministically. +op transfer_nondet_goto (label1 : Ident, label2 : Ident) : Transfer => + "goto " label1 ", " label2 ";"; + +// Conditional goto (deterministic: condition selects between two targets) +// NOTE: We use "branch" instead of "if" to avoid ambiguity with the +// structured if-statement syntax. The DDM parser registers tokens globally, +// so "if (" in Transfer would conflict with "if (" in Statement. +op transfer_cond_goto (c : Expr, lt : Ident, lf : Ident) : Transfer => + "branch (" c ") goto " lt " else " lf ";"; + +// Return/finish (terminate execution) +op transfer_return : Transfer => + "return;"; + +// A single CFG basic block: label, commands, transfer +category CFGBlock; +@[scope(cmds)] +op cfg_block (label : Ident, cmds : Seq Statement, tr : Transfer) : CFGBlock => + label ":" " {\n" indent(2, cmds) " " tr "\n}"; + +// A list of CFG blocks +category CFGBlocks; +op cfg_blocks_one (b : CFGBlock) : CFGBlocks => b; +op cfg_blocks_cons (b : CFGBlock, rest : CFGBlocks) : CFGBlocks => + b "\n" rest; + +// CFG body: entry label + blocks +category CFGBody; +op cfg_body (entry : Ident, blocks : CFGBlocks) : CFGBody => + "cfg " entry " {\n" indent(2, blocks) "\n}"; + +// Procedure with CFG body +op command_cfg_procedure (name : Ident, + typeArgs : Option TypeArgs, + @[scope(typeArgs)] b : Bindings, + @[scope(b)] s : Option Spec, + @[scope(b)] body : CFGBody) : + Command => + @[prec(10)] "procedure " name typeArgs b "\n" + s body ";\n"; + #end --------------------------------------------------------------------- diff --git a/Strata/Languages/Core/DDMTransform/Translate.lean b/Strata/Languages/Core/DDMTransform/Translate.lean index 1fa2b4fe95..0a7cf0bd37 100644 --- a/Strata/Languages/Core/DDMTransform/Translate.lean +++ b/Strata/Languages/Core/DDMTransform/Translate.lean @@ -1671,7 +1671,7 @@ def translateProcedure (p : Program) (bindings : TransBindings) (op : Operation) outputs := ret }, spec := { preconditions := requires, postconditions := ensures }, - body := body + body := .structured body } md, origBindings) @@ -1690,13 +1690,131 @@ def translateBlockCommand (p : Program) (bindings : TransBindings) (op : Operati outputs := [] }, spec := { preconditions := [], postconditions := [] }, - body := body + body := .structured body } md, bindings) --------------------------------------------------------------------- +/-- Translate a transfer command from the CFG syntax -/ + +private instance : Inhabited TransBindings := ⟨{}⟩ +private instance : Inhabited (Imperative.DetTransferCmd String Core.Expression) := ⟨.finish⟩ +private instance : Inhabited (Imperative.BasicBlock (Imperative.DetTransferCmd String Core.Expression) Core.Command) := ⟨⟨[], .finish⟩⟩ +private instance : Inhabited (Imperative.CFG String (Imperative.DetBlock String Core.Command Core.Expression)) := ⟨⟨"", []⟩⟩ + +partial def translateTransfer (p : Program) (bindings : TransBindings) (arg : Arg) : + TransM (Imperative.DetTransferCmd String Core.Expression × TransBindings) := do + let .op op := arg + | TransM.error s!"translateTransfer expected op {repr arg}" + match op.name with + | q`Core.transfer_goto => + let label ← translateIdent String op.args[0]! + return (.condGoto (Lambda.LExpr.boolConst () Bool.true) label label, bindings) + | q`Core.transfer_nondet_goto => + let label1 ← translateIdent String op.args[0]! + let label2 ← translateIdent String op.args[1]! + -- Nondeterministic choice: introduce an unbound free variable as the branch + -- condition. The symbolic evaluator returns the fvar unchanged (via findD), + -- which is neither .true nor .false, causing evalCFGStep to fork into both + -- paths with complementary path conditions. The concrete interpreter (runCFG) + -- will error on this, which is expected — nondeterministic gotos are only + -- meaningful under symbolic execution. + let condName := s!"$__nondet_{bindings.gen.var_def}" + let bindings := incrNum .var_def bindings + return (.condGoto (Lambda.LExpr.fvar () ⟨condName, ()⟩ none) label1 label2, bindings) + | q`Core.transfer_cond_goto => + let cond ← translateExpr p bindings op.args[0]! + let lt ← translateIdent String op.args[1]! + let lf ← translateIdent String op.args[2]! + return (.condGoto cond lt lf, bindings) + | q`Core.transfer_return => + return (.finish, bindings) + | _ => TransM.error s!"translateTransfer: unknown transfer {repr op.name}" + +/-- Translate a single CFG block -/ +partial def translateCFGBlock (p : Program) (bindings : TransBindings) (arg : Arg) : + TransM (String × Imperative.BasicBlock (Imperative.DetTransferCmd String Core.Expression) Core.Command × TransBindings) := do + let .op op := arg + | TransM.error s!"translateCFGBlock expected op {repr arg}" + let label ← translateIdent String op.args[0]! + -- Translate commands - handle both Seq and empty cases + let stmts : Array Arg := match op.args[1]! with + | .seq _ _ arr => arr + | other => #[other] -- single statement or empty + let mut cmds : Array Core.Command := #[] + let mut bindings := bindings + for s in stmts do + -- Skip empty/null args + if let .op _ := s then + let (translated, bindings') ← translateStmt p bindings s + bindings := bindings' + for stmt in translated do + match stmt with + | .cmd c => cmds := cmds.push c + | _ => TransM.error s!"translateCFGBlock: only commands allowed in CFG blocks, got statement" + let (transfer, bindings') ← translateTransfer p bindings op.args[2]! + return (label, ⟨cmds.toList, transfer⟩, bindings') + +/-- Translate a list of CFG blocks -/ +partial def translateCFGBlocks (p : Program) (bindings : TransBindings) (arg : Arg) : + TransM (List (String × Imperative.BasicBlock (Imperative.DetTransferCmd String Core.Expression) Core.Command) × TransBindings) := do + let .op op := arg + | TransM.error s!"translateCFGBlocks expected op {repr arg}" + match op.name with + | q`Core.cfg_blocks_one => + let (label, blk, bindings) ← translateCFGBlock p bindings op.args[0]! + return ([(label, blk)], bindings) + | q`Core.cfg_blocks_cons => + let (label, blk, bindings) ← translateCFGBlock p bindings op.args[0]! + let (rest, bindings) ← translateCFGBlocks p bindings op.args[1]! + return ((label, blk) :: rest, bindings) + | _ => TransM.error s!"translateCFGBlocks: unknown {repr op.name}" + +/-- Translate a CFG body -/ +partial def translateCFGBody (p : Program) (bindings : TransBindings) (arg : Arg) : + TransM (Imperative.CFG String (Imperative.DetBlock String Core.Command Core.Expression) × TransBindings) := do + let .op op := arg + | TransM.error s!"translateCFGBody expected op {repr arg}" + let entry ← translateIdent String op.args[0]! + let (blocks, bindings) ← translateCFGBlocks p bindings op.args[1]! + return ({ entry := entry, blocks := blocks }, bindings) + +/-- Translate a procedure with CFG body -/ +def translateCFGProcedure (p : Program) (bindings : TransBindings) (op : Operation) : + TransM (Core.Decl × TransBindings) := do + let _ ← @checkOp (Core.Decl × TransBindings) op q`Core.command_cfg_procedure 5 + let pname ← translateIdent Core.CoreIdent op.args[0]! + let typeArgs ← translateTypeArgs op.args[1]! + let (sig, ret) ← translateBindingsPartitioned bindings op.args[2]! + let in_bindings := (sig.map (fun (v, ty) => (LExpr.fvar () v ty))).toArray + let out_bindings_only := (ret.filter (fun (v, _) => !sig.any (fun (iv, _) => iv == v))).map + (fun (v, ty) => (LExpr.fvar () v ty)) + let out_bindings := out_bindings_only.toArray + let origBindings := bindings + let bbindings := bindings.boundVars ++ in_bindings ++ out_bindings + let bindings := { bindings with boundVars := bbindings } + let .option _ speca := op.args[3]! + | TransM.error s!"translateCFGProcedure spec expected: {repr op.args[3]!}" + let (requires, ensures) ← + if speca.isSome then translateSpec p pname bindings speca.get! else pure ([], []) + let (cfg, bindings) ← translateCFGBody p bindings op.args[4]! + let origBindings := { origBindings with gen := bindings.gen } + let md ← getOpMetaData op + return (.proc { header := { name := pname, + typeArgs := typeArgs.toList, + inputs := sig, + outputs := ret }, + spec := { preconditions := requires, + postconditions := ensures }, + body := .cfg cfg + } + md, + origBindings) + +--------------------------------------------------------------------- + def translateConstant (bindings : TransBindings) (op : Operation) : TransM (Core.Decl × TransBindings) := do let _ ← @checkOp (Core.Decl × TransBindings) op q`Core.command_constdecl 3 @@ -2114,6 +2232,8 @@ partial def translateCoreDecls (p : Program) (bindings : TransBindings) : translateRecFuncBlock p bindings op | q`Core.command_block => translateBlockCommand p bindings op + | q`Core.command_cfg_procedure => + translateCFGProcedure p bindings op | _ => TransM.error s!"translateCoreDecls unimplemented for {repr op}" pure ([decl], bindings) let (decls, bindings) ← go (count + 1) max bindings ops diff --git a/Strata/Languages/Core/ObligationExtraction.lean b/Strata/Languages/Core/ObligationExtraction.lean index 34eb371291..3fcdfcf822 100644 --- a/Strata/Languages/Core/ObligationExtraction.lean +++ b/Strata/Languages/Core/ObligationExtraction.lean @@ -45,6 +45,25 @@ def isValidObligationInput : Statements → Bool | s :: rest => isValidObligationStatement s && isValidObligationInput rest end +/-- Extract proof obligations from a single command, accumulating path conditions. -/ +def extractFromCmd (pc : PathConditions Expression) (cmd : Command) + : PathConditions Expression × Array (ProofObligation Expression) := + match cmd with + | .cmd (.assert label e md) => + let propType := match md.getPropertyType with + | some s => if s == MetaData.divisionByZero then .divisionByZero + else if s == MetaData.arithmeticOverflow then .arithmeticOverflow + else .assert + | none => .assert + (pc, #[ProofObligation.mk label propType pc e md]) + | .cmd (.cover label e md) => + (pc, #[ProofObligation.mk label .cover pc e md]) + | .cmd (.assume label e _md) => + (pc.addInNewest [.assumption label e], #[]) + | .cmd (.init name ty e _md) => + (pc.addEntry (.varDecl name ty e), #[]) + | _ => (pc, #[]) + mutual /-- Core recursive worker for `extractFromStatements`. Walks the statement list, accumulating path conditions and collecting proof obligations. -/ @@ -54,28 +73,15 @@ def extractGo (pc : PathConditions Expression) : Statements → | [], acc => .ok acc | s :: rest, acc => match s with - | .cmd (.cmd (.assert label e md)) => - let propType := match md.getPropertyType with - | some s => if s == MetaData.divisionByZero then .divisionByZero - else if s == MetaData.arithmeticOverflow then .arithmeticOverflow - else .assert - | none => .assert - extractGo pc rest (acc.push (ProofObligation.mk label propType pc e md)) - - | .cmd (.cmd (.cover label e md)) => - extractGo pc rest (acc.push (ProofObligation.mk label .cover pc e md)) - - | .cmd (.cmd (.assume label e _md)) => - extractGo (pc.addInNewest [.assumption label e]) rest acc + | .cmd c => + let (newPc, newObs) := extractFromCmd pc c + extractGo newPc rest (acc ++ newObs) | .ite .nondet thenSs elseSs _md => do let thenObs ← extractFromStatements pc thenSs let elseObs ← extractFromStatements pc elseSs extractGo pc rest (acc ++ thenObs ++ elseObs) - | .cmd (.cmd (.init name ty e _md)) => - extractGo (pc.addEntry (.varDecl name ty e)) rest acc - | _other => .error s!"ObligationExtraction: unsupported statement" @@ -92,6 +98,21 @@ def extractFromStatements extractGo pathConditions ss #[] end +/-- Extract proof obligations from a deterministic CFG by walking all blocks. + Path conditions restart from the global `pc` for each block independently, so + obligations are over-approximated (no false negatives — every real bug is caught). + However, obligations in block B that depend on `assume` from block A will fail to + discharge, surfacing as false alarms (false positives) to the user. + TODO: dominator-based path-condition propagation to reduce false alarms. -/ +def extractFromDetCFG (pc : PathConditions Expression) (cfg : DetCFG) + : Except String (Array (ProofObligation Expression)) := + let obs := cfg.blocks.foldl (init := #[]) fun acc (_, blk) => + let (_, blockObs) := blk.cmds.foldl (init := (pc, #[])) fun (curPc, obs) cmd => + let (newPc, newObs) := extractFromCmd curPc cmd + (newPc, obs ++ newObs) + acc ++ blockObs + .ok obs + /-- Extract proof obligations from a program. Axioms become global assumptions that are prepended to the path conditions of every obligation. -/ def extractObligations (p : Program) : Except String (ProofObligations Expression) := do @@ -103,7 +124,9 @@ def extractObligations (p : Program) : Except String (ProofObligations Expressio .ok (axiomPc ++ [.assumption a.name a.e], allObs) | .proc proc _md => do let globalPc : PathConditions Expression := [axiomPc] - let obs ← extractFromStatements globalPc proc.body + let obs ← match proc.body with + | .structured ss => extractFromStatements globalPc ss + | .cfg c => extractFromDetCFG globalPc c .ok (axiomPc, allObs ++ obs) | _ => .ok (axiomPc, allObs) return allObs @@ -124,8 +147,6 @@ private theorem extractGo_ok (pc : PathConditions Expression) (ss : Statements) obtain ⟨hs, hrest⟩ := h unfold extractGo; split · exact extractGo_ok _ _ _ hrest - · exact extractGo_ok _ _ _ hrest - · exact extractGo_ok _ _ _ hrest · rename_i thenSs elseSs _ unfold isValidObligationStatement at hs simp [Bool.and_eq_true] at hs @@ -140,8 +161,8 @@ private theorem extractGo_ok (pc : PathConditions Expression) (ss : Statements) cases extractGo pc elseSs #[] with | error => intro _ h; simp [Except.isOk, Except.toBool] at h | ok v2 => intro _ _; simp; exact extractGo_ok _ _ _ hrest - · exact extractGo_ok _ _ _ hrest · unfold isValidObligationStatement at hs; simp at hs + split at hs <;> simp at * /-- If the input satisfies `isValidObligationInput`, then `extractFromStatements` never returns an error. -/ diff --git a/Strata/Languages/Core/Procedure.lean b/Strata/Languages/Core/Procedure.lean index 90b00cce92..7f8c7255a1 100644 --- a/Strata/Languages/Core/Procedure.lean +++ b/Strata/Languages/Core/Procedure.lean @@ -7,6 +7,7 @@ module public import Strata.DL.Imperative.HasVars +public import Strata.DL.Imperative.BasicBlock public import Strata.Languages.Core.Statement --------------------------------------------------------------------- @@ -278,21 +279,78 @@ def Procedure.Spec.updateCheckExprs | e :: erest, c :: crest => { c with expr := e } :: go erest crest +/-- A deterministic control-flow graph over Core commands and expressions. -/ +@[expose] abbrev DetCFG := Imperative.CFG String (Imperative.DetBlock String Command Expression) + +/-- The body of a Core procedure: either structured (a list of statements) or +unstructured (a control-flow graph of basic blocks). An empty structured body +(`structured []`) represents an abstract/bodyless procedure. -/ +inductive Procedure.Body where + /-- A structured body: a sequential list of statements. -/ + | structured : List Statement → Procedure.Body + /-- An unstructured body: a control-flow graph of deterministic basic blocks. + Labels are strings; each block contains Core commands and ends with a + deterministic transfer (conditional goto or finish). -/ + | cfg : DetCFG → Procedure.Body + deriving Inhabited + +/-- Extract the structured statements, or error if the body is a CFG. -/ +@[simp, expose] +def Procedure.Body.getStructured : Procedure.Body → Except String (List Statement) + | .structured ss => .ok ss + | .cfg _ => .error "expected structured body, got CFG" + +/-- Extract the CFG, or error if the body is structured. -/ +@[simp] +def Procedure.Body.getCfg : Procedure.Body → Except String DetCFG + | .cfg c => .ok c + | .structured _ => .error "expected CFG body, got structured" + +/-- Get variables referenced in the body. -/ +@[simp] +def Procedure.Body.getVars : Procedure.Body → List Expression.Ident + | .structured ss => ss.flatMap Imperative.HasVarsPure.getVars + | .cfg c => c.blocks.flatMap fun (_, blk) => + blk.cmds.flatMap Imperative.HasVarsPure.getVars + +/-- Is this body abstract (no implementation)? Only empty structured bodies + are abstract. CFG bodies always have an implementation. -/ +@[simp] +def Procedure.Body.isAbstract : Procedure.Body → Bool + | .structured ss => ss.isEmpty + | .cfg _ => false + +/-- Does this body have a structured implementation? -/ +@[simp] +def Procedure.Body.isStructured : Procedure.Body → Bool + | .structured _ => true + | .cfg _ => false + +/-- Does this body have a CFG implementation? -/ +@[simp] +def Procedure.Body.isCfg : Procedure.Body → Bool + | .structured _ => false + | .cfg _ => true + +def Procedure.Body.structuredLength : Procedure.Body → Nat + | .structured ss => ss.length + | .cfg _ => 0 + /-- A Strata Core procedure: the main verification unit. A procedure consists of a header (name, type parameters, input/output signatures), -a specification (contract), and an optional body (list of statements). If the body -is empty, the procedure is abstract and can only be reasoned about via its contract. -If the body is present, it is verified against the specification. +a specification (contract), and an optional body (list of statements or a CFG). +If the body is empty, the procedure is abstract and can only be reasoned about +via its contract. If the body is present, it is verified against the specification. -/ structure Procedure where /-- The procedure header: name, type parameters, and parameter signatures. -/ header : Procedure.Header /-- The procedure's contract: modifies clause, preconditions, and postconditions. -/ spec : Procedure.Spec - /-- The procedure body. Empty for abstract (bodyless) procedures. -/ - body : List Statement + /-- The procedure body. -/ + body : Procedure.Body := .structured [] deriving Inhabited --------------------------------------------------------------------- @@ -306,21 +364,56 @@ def Procedure.modifiedVars (p : Procedure) : List Expression.Ident := def Procedure.getVars (p : Procedure) : List Expression.Ident := (p.spec.postconditions.values.map Procedure.Check.expr).flatMap HasVarsPure.getVars ++ (p.spec.preconditions.values.map Procedure.Check.expr).flatMap HasVarsPure.getVars ++ - p.body.flatMap HasVarsPure.getVars |> List.filter (not $ Membership.mem p.header.inputs.keys ·) + p.body.getVars |> List.filter (not $ Membership.mem p.header.inputs.keys ·) instance : HasVarsPure Expression Procedure where getVars := Procedure.getVars +instance : HasVarsPure Expression Procedure.Body where + getVars := Procedure.Body.getVars + +instance : HasVarsImp Expression DetCFG where + definedVars cfg := cfg.blocks.flatMap fun (_, blk) => + blk.cmds.flatMap Command.definedVars + modifiedVars cfg := cfg.blocks.flatMap fun (_, blk) => + blk.cmds.flatMap Command.modifiedVars + +instance : HasVarsImp Expression Procedure.Body where + definedVars b := match b with + | .structured ss => HasVarsImp.definedVars ss + | .cfg cfgBody => HasVarsImp.definedVars cfgBody + modifiedVars b := match b with + | .structured ss => HasVarsImp.modifiedVars ss + | .cfg cfgBody => HasVarsImp.modifiedVars cfgBody + instance : HasVarsImp Expression Procedure where definedVars := Procedure.definedVars modifiedVars := Procedure.modifiedVars +def DetCFG.eraseTypes (cfg : DetCFG) : DetCFG := + { cfg with blocks := cfg.blocks.map fun (lbl, blk) => + (lbl, { blk with cmds := blk.cmds.map Command.eraseTypes, + transfer := match blk.transfer with + | .condGoto p lt lf md => .condGoto p.eraseTypes lt lf md + | .finish md => .finish md }) } + +-- Only transfer metadata is stripped because command metadata (on assert, +-- assume, init, set, cover) is not included in formatted output — formatCmd +-- discards it. Transfer metadata, however, appears in CFG formatting. +def DetCFG.stripMetaData (cfg : DetCFG) : DetCFG := + Imperative.CFG.stripDetMetaData cfg + def Procedure.eraseTypes (p : Procedure) : Procedure := - { p with body := Statements.eraseTypes p.body, spec := p.spec } + let body' := match p.body with + | .structured ss => .structured (Statements.eraseTypes ss) + | .cfg c => .cfg c.eraseTypes + { p with body := body', spec := p.spec } -/-- Remove all metadata from procedure. -/ def Procedure.stripMetaData (p : Procedure) : Procedure := - { p with body := Imperative.Block.stripMetaData p.body } + let body' := match p.body with + | .structured ss => .structured (Imperative.Block.stripMetaData ss) + | .cfg c => .cfg c.stripMetaData + { p with body := body' } /-- Transitive variable lookup for procedures. This is a version that looks into the body, diff --git a/Strata/Languages/Core/ProcedureEval.lean b/Strata/Languages/Core/ProcedureEval.lean index 9ea328f41b..d29a40a120 100644 --- a/Strata/Languages/Core/ProcedureEval.lean +++ b/Strata/Languages/Core/ProcedureEval.lean @@ -58,6 +58,93 @@ private def mergeResults (fallback : Env) (results : List Env) : Env := deferred := allDeferred, exprEnv := { E.exprEnv with config := { E.exprEnv.config with usedNames := mergedNames } } } +private def evalBlockCmds (E : Env) (old_var_subst : SubstMap) + (cmds : List Command) : Env := + cmds.foldl (fun env cmd => + if env.error.isSome then env + else (Statement.Command.eval env old_var_subst cmd).snd) E + +private def evalCFGStep (cfg : DetCFG) (old_var_subst : SubstMap) + (active : List (String × Env)) : + List (String × Env) × List Env × Statistics := + active.foldl (fun (newActive, finished, stats) (label, env) => + if env.error.isSome then + (newActive, env :: finished, stats) + else + match cfg.blocks.lookup label with + | none => + let env' := { env with error := some (.Misc + s!"evalCFG: block '{label}' not found in CFG") } + (newActive, env' :: finished, stats) + | some blk => + let env' := evalBlockCmds env old_var_subst blk.cmds + if env'.error.isSome then + (newActive, env' :: finished, stats) + else + let stats := stats.increment s!"{Evaluator.Stats.simulatedStmts}" + match blk.transfer with + | .finish _ => + (newActive, env' :: finished, stats) + | .condGoto cond lt lf _ => + let cond' := env'.exprEval cond + match cond' with + | .true _ => ((lt, env') :: newActive, finished, stats) + | .false _ => ((lf, env') :: newActive, finished, stats) + | _ => + let condErased := cond.eraseTypes + let label_t := toString (f!"") + let label_f := toString (f!"") + let env_t := { env' with pathConditions := + (env'.pathConditions.addInNewest + [.assumption label_t cond']) } + let env_f := { env' with pathConditions := + (env'.pathConditions.addInNewest + [.assumption label_f + (Lambda.LExpr.ite () cond' (LExpr.false ()) (LExpr.true ()))]) } + ((lt, env_t) :: (lf, env_f) :: newActive, finished, stats)) + ([], [], {}) + +private def evalCFGBlocks (cfg : DetCFG) (old_var_subst : SubstMap) + (fuel : Nat) (active : List (String × Env)) (finished : List Env) + (stats : Statistics) : List Env × Statistics := + match active with + | [] => (finished, stats) + | _ => + match fuel with + | 0 => + let errorEnvs := active.map fun (_, e) => + { e with error := some .OutOfFuel } + (errorEnvs ++ finished, + stats.increment s!"{Evaluator.Stats.simulatingStmtHitOutOfFuel}" active.length) + | fuel' + 1 => + let (newActive, newFinished, stepStats) := + evalCFGStep cfg old_var_subst active + evalCFGBlocks cfg old_var_subst fuel' newActive + (newFinished ++ finished) (stats.merge stepStats) + termination_by fuel + +private def evalCFGBody (E : Env) (old_var_subst : SubstMap) + (precond_assumes postcond_asserts : Statements) + (cfg : DetCFG) (fuel : Nat) : List Env × Statistics := + let (preEnvs, preStats) := Statement.eval E old_var_subst precond_assumes + let emptyAcc : List Env × Statistics := ([], {}) + let (cfgResultsRev, cfgStats) := + preEnvs.foldl (fun acc preEnv => + let (accEnvs, accStats) := acc + let (envs, stats) := + evalCFGBlocks cfg old_var_subst fuel [(cfg.entry, preEnv)] [] {} + (envs.reverse ++ accEnvs, accStats.merge stats)) emptyAcc + let cfgResults := cfgResultsRev.reverse + let (postResultsRev, postStats) := + cfgResults.foldl (fun acc cfgEnv => + let (accEnvs, accStats) := acc + if cfgEnv.error.isSome then + (cfgEnv :: accEnvs, accStats) + else + let (envs, stats) := Statement.eval cfgEnv old_var_subst postcond_asserts + (envs.reverse ++ accEnvs, accStats.merge stats)) emptyAcc + (postResultsRev.reverse, preStats.merge (cfgStats.merge postStats)) + /-- Evaluate a single procedure: generate fresh variables for parameters, execute the body, check postconditions, and collect proof obligations. @@ -113,8 +200,18 @@ def eval (E : Env) (p : Procedure) : Env × Statistics := /- the assumptions from preconditions are set to have empty metadata -/ (.assume label check.expr check.md)) p.spec.preconditions - let (ssEs, evalStats) := Statement.eval E old_g_subst (precond_assumes ++ p.body ++ postcond_asserts) - (mergeResults E (ssEs.map (fun sE => fixupError sE)), evalStats) + match p.body with + | .cfg cfgBody => + -- 100 iterations per block: enough to unroll moderate loops while keeping + -- symbolic execution bounded. Fuel is consumed per block visit, so a + -- single-block loop unrolls ~100 times and a 4-block diamond uses ~400. + let fuel := cfgBody.blocks.length * 100 + let (ssEs, evalStats) := + evalCFGBody E old_g_subst precond_assumes postcond_asserts cfgBody fuel + (mergeResults E (ssEs.map (fun sE => fixupError sE)), evalStats) + | .structured bodyStmts => + let (ssEs, evalStats) := Statement.eval E old_g_subst (precond_assumes ++ bodyStmts ++ postcond_asserts) + (mergeResults E (ssEs.map (fun sE => fixupError sE)), evalStats) --------------------------------------------------------------------- diff --git a/Strata/Languages/Core/ProcedureType.lean b/Strata/Languages/Core/ProcedureType.lean index 9b5b9bdbed..27c9a69f1e 100644 --- a/Strata/Languages/Core/ProcedureType.lean +++ b/Strata/Languages/Core/ProcedureType.lean @@ -16,7 +16,7 @@ public section namespace Core open Std (ToFormat Format format) -open Imperative (MetaData) +open Imperative (MetaData HasVarsImp) open Strata (DiagnosticModel FileRange) namespace Procedure @@ -30,10 +30,10 @@ private def checkNoDuplicates (proc : Procedure) (sourceLoc : FileRange) : private def checkModificationRights (proc : Procedure) (sourceLoc : FileRange) : Except DiagnosticModel Unit := do - let modifiedVars := (Imperative.Block.modifiedVars proc.body).eraseDups - let definedVars := (Imperative.Block.definedVars proc.body).eraseDups + let modifiedVars := (HasVarsImp.modifiedVars (P := Expression) proc.body).eraseDups + let definedVars := (HasVarsImp.definedVars (P := Expression) proc.body).eraseDups let allowedVars := proc.header.outputs.keys ++ definedVars - let disallowed := modifiedVars.filter (fun v => v ∉ allowedVars) + let disallowed := modifiedVars.filter (fun v => !allowedVars.contains v) if !disallowed.isEmpty then .error <| DiagnosticModel.withRange sourceLoc f!"[{proc.header.name}]: This procedure modifies variables it \ is not allowed to!\n\ @@ -50,6 +50,73 @@ private def setupInputEnv (C : Core.Expression.TyContext) (Env : Core.Expression let Env := Env.addInNewestContext inp_lty_sig return (inp_mty_sig, Env) +private def checkUniqueLabels (procName : CoreIdent) (cfg : DetCFG) (sourceLoc : FileRange) : + Except DiagnosticModel Unit := do + let labels := cfg.blocks.map (·.1) + if !labels.Nodup then + let dups := labels.filter (fun l => labels.countP (· == l) > 1) |>.eraseDups + .error <| DiagnosticModel.withRange sourceLoc + f!"[{procName}]: Duplicate block labels in CFG: {dups}" + +private def checkEntryExists (procName : CoreIdent) (cfg : DetCFG) (sourceLoc : FileRange) : + Except DiagnosticModel Unit := do + let labels := cfg.blocks.map (·.1) + if !labels.contains cfg.entry then + .error <| DiagnosticModel.withRange sourceLoc + f!"[{procName}]: Entry label \"{cfg.entry}\" not found in CFG blocks. \ + Available labels: {labels}" + +private def checkTargetLabels (procName : CoreIdent) (cfg : DetCFG) (sourceLoc : FileRange) : + Except DiagnosticModel Unit := do + let labels := cfg.blocks.map (·.1) + for (lbl, blk) in cfg.blocks do + match blk.transfer with + | .condGoto _ lt lf _ => + if !labels.contains lt then + .error <| DiagnosticModel.withRange sourceLoc + f!"[{procName}]: Block \"{lbl}\" branches to unknown label \"{lt}\". \ + Available labels: {labels}" + if !labels.contains lf then + .error <| DiagnosticModel.withRange sourceLoc + f!"[{procName}]: Block \"{lbl}\" branches to unknown label \"{lf}\". \ + Available labels: {labels}" + | .finish _ => pure () + +-- Type environment flows sequentially through all blocks in list order, +-- regardless of control-flow reachability. This is a sound over-approximation: +-- it may accept a program that uses an uninitialized variable at runtime (the +-- verifier will still catch the error), but it never misses a real type error. +-- Per-block scoping would require a dataflow fixpoint over the CFG. +open Lambda Lambda.LTy.Syntax in +private def typeCheckCFG (C : Core.Expression.TyContext) (Env : Core.Expression.TyEnv) + (P : Program) (proc : Procedure) (cfg : DetCFG) (sourceLoc : FileRange) : + Except DiagnosticModel (DetCFG × Core.Expression.TyEnv) := do + checkUniqueLabels proc.header.name cfg sourceLoc + checkEntryExists proc.header.name cfg sourceLoc + checkTargetLabels proc.header.name cfg sourceLoc + let mut currentEnv := Env + let mut annotatedBlocks : List (String × Imperative.DetBlock String Command Expression) := [] + for (lbl, blk) in cfg.blocks do + let mut cmds' := [] + for cmd in blk.cmds do + let (cmd', newEnv) ← Statement.typeCheckCmd C currentEnv P cmd + currentEnv := newEnv + cmds' := cmds' ++ [cmd'] + let transfer' ← match blk.transfer with + | .condGoto p lt lf md => + let (pa, newEnv) ← LExpr.resolve C currentEnv p + |>.mapError DiagnosticModel.fromFormat + currentEnv := newEnv + if pa.toLMonoTy != mty[bool] then + .error <| DiagnosticModel.withRange sourceLoc + f!"[{proc.header.name}]: Branch condition in block \"{lbl}\" \ + is not of type bool, got {pa.toLMonoTy}" + pure (Imperative.DetTransferCmd.condGoto pa.unresolved lt lf md) + | .finish md => pure (.finish md) + annotatedBlocks := annotatedBlocks ++ [(lbl, { cmds := cmds', transfer := transfer' })] + let annotatedCFG : DetCFG := { entry := cfg.entry, blocks := annotatedBlocks } + return (annotatedCFG, currentEnv) + -- Error message prefix for errors in processing procedure pre/post conditions. def conditionErrorMsgPrefix (procName : CoreIdent) (condName : CoreLabel) (md : MetaData Expression) : DiagnosticModel := @@ -111,7 +178,13 @@ def typeCheck (C : Core.Expression.TyContext) (Env : Core.Expression.TyEnv) (p : -- Type check body. -- Note that `Statement.typeCheck` already reports source locations in -- error messages. - let (annotated_body, finalEnv) ← Statement.typeCheck C envAfterPostconds p (.some proc) proc.body + let (annotated_body, annotated_cfg, finalEnv) ← match proc.body with + | .structured ss => + let (ss', env') ← Statement.typeCheck C envAfterPostconds p (.some proc) ss + pure (ss', none, env') + | .cfg cfgBody => + let (cfg', env') ← typeCheckCFG C envAfterPostconds p proc cfgBody fileRange + pure ([], some cfg', env') -- Remove formals and returns from the context -- they ought to be local to -- the procedure body. @@ -126,7 +199,10 @@ def typeCheck (C : Core.Expression.TyContext) (Env : Core.Expression.TyEnv) (p : outputs := out_mty_sig } let new_spec := { proc.spec with preconditions := finalPreconditions, postconditions := finalPostconditions } - let new_proc := { proc with header := new_hdr, spec := new_spec, body := annotated_body } + let new_body := match annotated_cfg with + | some cfg' => .cfg cfg' + | none => .structured annotated_body + let new_proc := { proc with header := new_hdr, spec := new_spec, body := new_body } return (new_proc, finalEnv) diff --git a/Strata/Languages/Core/StatementEval.lean b/Strata/Languages/Core/StatementEval.lean index ce2b35a975..cab6c0459b 100644 --- a/Strata/Languages/Core/StatementEval.lean +++ b/Strata/Languages/Core/StatementEval.lean @@ -249,52 +249,34 @@ def Statements.containsAsserts (ss : Statements) : Bool := (fun c => match c with | .assert _ _ _ => true | _ => false) ss mutual -/-- -Collect all `cover` commands from a statement `s` with their labels and metadata. --/ -def Statement.collectCovers (s : Statement) : List (String × Imperative.MetaData Expression) := +def Statement.collectCmds (f : Imperative.Cmd Expression → Option α) (s : Statement) : List α := match s with - | .cmd (.cmd (.cover label _expr md)) => [(label, md)] + | .cmd (.cmd c) => (f c).toList | .cmd _ => [] - | .block _ inner_ss _ => Statements.collectCovers inner_ss - | .ite _ then_ss else_ss _ => Statements.collectCovers then_ss ++ Statements.collectCovers else_ss - | .loop _ _ _ body_ss _ => Statements.collectCovers body_ss - | .funcDecl _ _ | .exit _ _ | .typeDecl _ _ => [] -- Function/type declarations and exits don't contain cover commands + | .block _ inner_ss _ => Statements.collectCmds f inner_ss + | .ite _ then_ss else_ss _ => Statements.collectCmds f then_ss ++ Statements.collectCmds f else_ss + | .loop _ _ _ body_ss _ => Statements.collectCmds f body_ss + | .funcDecl _ _ | .exit _ _ | .typeDecl _ _ => [] termination_by Imperative.Stmt.sizeOf s -/-- -Collect all `cover` commands from statements `ss` with their labels and metadata. --/ -def Statements.collectCovers (ss : Statements) : List (String × Imperative.MetaData Expression) := +def Statements.collectCmds (f : Imperative.Cmd Expression → Option α) (ss : Statements) : List α := match ss with | [] => [] | s :: ss => - Statement.collectCovers s ++ Statements.collectCovers ss + Statement.collectCmds f s ++ Statements.collectCmds f ss termination_by Imperative.Block.sizeOf ss end -mutual -/-- -Collect all `assert` commands from a statement `s` with their labels and metadata. --/ +def Statement.collectCovers (s : Statement) : List (String × Imperative.MetaData Expression) := + Statement.collectCmds (fun | .cover label _expr md => some (label, md) | _ => none) s + +def Statements.collectCovers (ss : Statements) : List (String × Imperative.MetaData Expression) := + Statements.collectCmds (fun | .cover label _expr md => some (label, md) | _ => none) ss + def Statement.collectAsserts (s : Statement) : List (String × Imperative.MetaData Expression) := - match s with - | .cmd (.cmd (.assert label _expr md)) => [(label, md)] - | .cmd _ => [] - | .block _ inner_ss _ => Statements.collectAsserts inner_ss - | .ite _ then_ss else_ss _ => Statements.collectAsserts then_ss ++ Statements.collectAsserts else_ss - | .loop _ _ _ body_ss _ => Statements.collectAsserts body_ss - | .funcDecl _ _ | .exit _ _ | .typeDecl _ _ => [] -- Function/type declarations and exits don't contain assert commands - termination_by Imperative.Stmt.sizeOf s -/-- -Collect all `assert` commands from statements `ss` with their labels and metadata. --/ + Statement.collectCmds (fun | .assert label _expr md => some (label, md) | _ => none) s + def Statements.collectAsserts (ss : Statements) : List (String × Imperative.MetaData Expression) := - match ss with - | [] => [] - | s :: ss => - Statement.collectAsserts s ++ Statements.collectAsserts ss - termination_by Imperative.Block.sizeOf ss -end + Statements.collectCmds (fun | .assert label _expr md => some (label, md) | _ => none) ss /-- Create cover obligations for covers in an unreachable (dead) branch, including @@ -762,6 +744,36 @@ Interpret a single procedure call. Importantly, this creates a separate Env to execute the body of the procedure with, which initially only contains input/output variables. + +Execute a CFG by following control flow from the entry block. + Returns the list of commands executed (as statements) for compatibility + with the structured interpreter. -/ +private def runCFG (cfg : Core.DetCFG) (fuel : Nat) (env : Env) + (ops : Imperative.RunOps Expression Command Env) : Env := + go cfg.entry fuel env +where + go (label : String) (fuel : Nat) (env : Env) : Env := + match fuel with + | 0 => CmdEval.updateError env (.Misc s!"runCFG: fuel exhausted (possible infinite loop)") + | fuel' + 1 => + match cfg.blocks.lookup label with + | none => CmdEval.updateError env (.Misc s!"runCFG: block '{label}' not found in CFG") + | some blk => + let cmdStmts := blk.cmds.map (Imperative.Stmt.cmd ·) + match Imperative.runStmt ops fuel' (.stmts cmdStmts env) with + | .terminal env' => + match blk.transfer with + | .finish _ => env' + | .condGoto cond lt lf _ => + match ops.evalExpr env' cond with + | some (.boolConst _ true) => go lt fuel' env' + | some (.boolConst _ false) => go lf fuel' env' + | _ => CmdEval.updateError env' + (.Misc s!"runCFG: branch condition in block '{label}' did not evaluate to a boolean") + | _ => CmdEval.updateError env + (.Misc s!"runCFG: block '{label}' did not reach terminal (possibly inner-loop fuel exhaustion or unexpected exit)") + +/-- The resulting Env is the original passed in Env with the output variables copied back into it. -/ def Command.runCall (lhs : List Expression.Ident) (procName : String) (args : List Expression.Expr) @@ -772,7 +784,7 @@ def Command.runCall (lhs : List Expression.Ident) (procName : String) (args : Li match Program.Procedure.find? E.program ⟨procName, ()⟩ with | none => CmdEval.updateError E (.Misc s!"procedure '{procName}' not found") | some proc => - if proc.body.isEmpty then CmdEval.updateError E (.Misc s!"procedure '{proc.header.name}' has no body") + if proc.body.isAbstract then CmdEval.updateError E (.Misc s!"procedure '{proc.header.name}' has no body") else match args.mapM (LExpr.run E.exprEnv) with | .error s => CmdEval.updateError E (.Misc s) @@ -812,10 +824,15 @@ def Command.runCall (lhs : List Expression.Ident) (procName : String) (args : Li hasError := fun E => E.error.isSome addError := fun E msg => CmdEval.updateError E (.Misc msg) } - let config : Imperative.RunConfig Expression Command Env := - .stmts proc.body callEnv - let configAfter := Imperative.runStmt ops fuel' config - match configAfter with + let callEnvAfter := match proc.body with + | .structured ss => + let config : Imperative.RunConfig Expression Command Env := + .stmts ss callEnv + Imperative.runStmt ops fuel' config + | .cfg cfgBody => + -- Interpret CFG by following control flow from the entry block. + .terminal (runCFG cfgBody fuel' callEnv ops) + match callEnvAfter with | .terminal callEnv' => match callEnv'.error with | some _ => { E with error := callEnv'.error } @@ -842,5 +859,3 @@ end Statement end Core end -- public section - ---------------------------------------------------------------------- diff --git a/Strata/Languages/Core/StatementSemantics.lean b/Strata/Languages/Core/StatementSemantics.lean index 233cffd42d..e0ee78c235 100644 --- a/Strata/Languages/Core/StatementSemantics.lean +++ b/Strata/Languages/Core/StatementSemantics.lean @@ -8,6 +8,7 @@ module public import Strata.DL.Lambda.LExpr public import Strata.DL.Lambda.LExprWF public import Strata.DL.Imperative.StmtSemantics +public import Strata.DL.Imperative.CFGSemantics public import Strata.Languages.Core.CoreGen public import Strata.Languages.Core.Procedure @@ -285,6 +286,46 @@ inductive CoreStepStar ---- CoreStepStar π φ c₁ c₃ +/-- Reflexive-transitive closure of CFG steps for the Core language. + Each step looks up a block by label and evaluates it using the generic + `Imperative.EvalDetBlock` instantiated with `EvalCommand`. This works + because `EvalDetBlock` has a `_enableNesting` constructor that directly + references `EvalCmd`, satisfying the Lean kernel's nested inductive + requirement. See `StrataTest/Languages/Core/Tests/NestedInductiveRestriction.lean`. -/ +inductive CoreCFGStepStar + (π : String → Option Procedure) + (φ : CoreEval → PureFunc Expression → CoreEval) : + DetCFG → CFGConfig String Expression → + CFGConfig String Expression → Prop where + | refl : CoreCFGStepStar π φ cfg c c + | step : + List.lookup t cfg.blocks = .some b → + Imperative.EvalDetBlock Expression (EvalCommand π φ) (EvalPureFunc φ) σ b config → + CoreCFGStepStar π φ cfg (updateFailure config failed) c₃ → + ---- + CoreCFGStepStar π φ cfg (.cont t σ failed) c₃ + +/-- Execution of a procedure body: either structured (via `CoreStepStar`) + or unstructured CFG (via `CoreCFGStepStar`). + + The `cfg` constructor passes through the initial eval `δ` as terminal eval + because `CoreCFGStepStar` does not track eval changes. If CFG execution + ever needs `funcDecl` support, `CoreCFGStepStar` would need enrichment. -/ +inductive CoreBodyExec + (π : String → Option Procedure) + (φ : CoreEval → PureFunc Expression → CoreEval) : + Procedure.Body → CoreStore → CoreEval → CoreStore → CoreEval → Bool → Prop where + | structured : + CoreStepStar π φ + (.stmts ss ⟨σ, δ, false⟩) + (.terminal ρ') → + CoreBodyExec π φ (.structured ss) σ δ ρ'.store ρ'.eval ρ'.hasFailure + | cfg : + CoreCFGStepStar π φ cfg + (.cont cfg.entry σ false) + (.terminal σ' failed) → + CoreBodyExec π φ (.cfg cfg) σ δ σ' δ failed + inductive EvalCommand (π : String → Option Procedure) (φ : CoreEval → PureFunc Expression → CoreEval) : CoreEval → CoreStore → Command → CoreStore → Bool → Prop where | cmd_sem {δ σ c σ' f} : @@ -295,7 +336,7 @@ inductive EvalCommand (π : String → Option Procedure) (φ : CoreEval → Pure /-- Arguments are matched positionally: `inArgs` (from `getInputExprs`) aligns with `p.header.inputs`, and `lhs` (from `getLhs`) aligns with `p.header.outputs`. -/ - | call_sem {δ σ₀ σ inArgs vals oVals σA σAO n p modvals callArgs σ' ρ' md} : + | call_sem {δ σ₀ σ inArgs vals oVals σA σAO n p modvals callArgs σ' σ_final δ_final failed md} : π n = .some p → -- inArg exprs + fvar refs for inoutArg ids CallArg.getInputExprs callArgs = inArgs → @@ -317,13 +358,11 @@ inductive EvalCommand (π : String → Option Procedure) (φ : CoreEval → Pure (∀ pre, (Procedure.Spec.getCheckExprs p.spec.preconditions).contains pre → isDefinedOver (HasVarsPure.getVars) σAO pre ∧ δ σAO pre = .some HasBool.tt) → - CoreStepStar π φ - (.stmts p.body ⟨σAO, δ, false⟩) - (.terminal ρ') → + CoreBodyExec π φ p.body σAO δ σ_final δ_final failed → (∀ post, (Procedure.Spec.getCheckExprs p.spec.postconditions).contains post → isDefinedOver (HasVarsPure.getVars) σAO post ∧ - δ ρ'.store post = .some HasBool.tt) → - ReadValues ρ'.store (ListMap.keys (p.header.outputs)) modvals → + δ_final σ_final post = .some HasBool.tt) → + ReadValues σ_final (ListMap.keys (p.header.outputs)) modvals → -- positional: modvals[i] written back to lhs[i] UpdateStates σ lhs modvals σ' → ---- diff --git a/Strata/Languages/Core/WF.lean b/Strata/Languages/Core/WF.lean index 0b5f655441..16783a4efe 100644 --- a/Strata/Languages/Core/WF.lean +++ b/Strata/Languages/Core/WF.lean @@ -137,16 +137,22 @@ structure WFAxiomDeclarationProp (p : Program) (f : Axiom) : Prop where structure WFDistinctDeclarationProp (p : Program) (l : Expression.Ident) (es : List (Expression.Expr)) : Prop where +-- NOTE: For CFG procedures, the structured-body fields (`wfstmts`, `wfloclnd`, +-- `bodyExitsCovered`) are vacuously satisfied. CFG-specific well-formedness +-- (e.g., label uniqueness, reachability) is not yet captured here: +-- * verify block labels are unique +-- * all variables used are declared/initialized +-- * target labels of transfer commands exist structure WFProcedureProp (p : Program) (d : Procedure) : Prop where - wfstmts : WFStatementsProp p d.body - wfloclnd : (HasVarsImp.definedVars (P:=Expression) d.body).Nodup + wfstmts : ∀ ss, d.body = .structured ss → WFStatementsProp p ss + wfloclnd : ∀ ss, d.body = .structured ss → (HasVarsImp.definedVars (P:=Expression) ss).Nodup inputsNodup : (ListMap.keys d.header.inputs).Nodup outputsNodup : (ListMap.keys d.header.outputs).Nodup ioNotOld : ∀ id ∈ ListMap.keys d.header.inputs ++ ListMap.keys d.header.outputs, ∀ x, id ≠ CoreIdent.mkOld x wfspec : WFSpecProp p d.spec d - -- There is no exit statement that cannot be caught by any block in the procedure. - bodyExitsCovered : Stmt.exitsCoveredByBlocks.Block.exitsCoveredByBlocks [] d.body + bodyExitsCovered : ∀ ss, d.body = .structured ss → + Stmt.exitsCoveredByBlocks.Block.exitsCoveredByBlocks [] ss structure WFFunctionProp (p : Program) (f : Function) : Prop where structure WFRecFuncBlockProp (p : Program) (fs : List Function) : Prop where diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean index beb50ad9b0..c4a1c9cf8b 100644 --- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean +++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean @@ -581,7 +581,7 @@ def translateProcedure (proc : Procedure) : TranslateM Core.Procedure := do -- Wrap body in a labeled block so early returns (exit) work correctly. let body : List Core.Statement := [.block "$body" bodyStmts mdWithUnknownLoc] let spec : Core.Procedure.Spec := { preconditions, postconditions } - return { header, spec, body } + return { header, spec, body := .structured body } def translateInvokeOnAxiom (proc : Procedure) (trigger : StmtExprMd) : TranslateM (Option Core.Decl) := do diff --git a/Strata/Languages/Python/PythonToCore.lean b/Strata/Languages/Python/PythonToCore.lean index 5641277d32..541f68b7c0 100644 --- a/Strata/Languages/Python/PythonToCore.lean +++ b/Strata/Languages/Python/PythonToCore.lean @@ -790,7 +790,7 @@ def translateFunctions (a : Array (Python.stmt SourceRange)) (translation_ctx: T inputs := [], outputs := [("maybe_except", (.tcons "ExceptOrNone" []))]}, spec := default, - body := varDecls ++ [.block "end" ((ArrPyStmtToCore translation_ctx body.val).fst) .empty] + body := .structured (varDecls ++ [.block "end" ((ArrPyStmtToCore translation_ctx body.val).fst) .empty]) } some (.proc proc .empty) | _ => none) @@ -821,7 +821,7 @@ def pythonFuncToCore (name : String) (args: List (String × String)) (body: Arra inputs, outputs}, spec, - body + body := .structured body } def unpackPyArguments (args: Python.arguments SourceRange) : List (String × String) := diff --git a/Strata/Transform/ANFEncoder.lean b/Strata/Transform/ANFEncoder.lean index 39390bb321..4269eb1840 100644 --- a/Strata/Transform/ANFEncoder.lean +++ b/Strata/Transform/ANFEncoder.lean @@ -217,8 +217,14 @@ def anfEncodeProgram (p : Program) : Bool × Program := let (revDecls, _, changed) := p.decls.foldl (fun (acc, idx, changed) decl => match decl with | .proc proc md => - let (body', idx') := anfEncodeBody proc.body idx - (.proc { proc with body := body' } md :: acc, idx', changed || idx' > idx) + match proc.body with + | .structured ss => + let (body', idx') := anfEncodeBody ss idx + (.proc { proc with body := .structured body' } md :: acc, idx', changed || idx' > idx) + | .cfg _ => + -- CSE on CFGs would require dominator analysis to determine where to + -- place hoisted var declarations. Skipped for now. + (.proc proc md :: acc, idx, changed) | other => (other :: acc, idx, changed) ) ([], 0, false) (changed, { decls := revDecls.reverse }) diff --git a/Strata/Transform/CoreSpecification.lean b/Strata/Transform/CoreSpecification.lean index aef7675338..7cd9833088 100644 --- a/Strata/Transform/CoreSpecification.lean +++ b/Strata/Transform/CoreSpecification.lean @@ -39,6 +39,47 @@ open Core Imperative Imperative.Specification.Lang.imperative Expression Command (EvalCommand π φ) (EvalPureFunc φ) coreIsAtAssert +/-! ## Core CFG `Lang` bundle -/ + +/-- Configuration for CFG specification: pairs a `CFGConfig` with the eval + function so that `getEnv` can reconstruct a full `Env Expression`. -/ +structure CoreCFGSpecConfig where + cfgConfig : CFGConfig String Expression + eval : CoreEval + +/-- Extract an `Env Expression` from a CFG specification config. -/ +def CoreCFGSpecConfig.toEnv (c : CoreCFGSpecConfig) : Env Expression := + match c.cfgConfig with + | .cont _ σ f => ⟨σ, c.eval, f⟩ + | .terminal σ f => ⟨σ, c.eval, f⟩ + +/-- Assert detection in a CFG: an assert is reachable if the current block + (looked up by the continuation label in a given CFG) contains an assert + command with the matching label and expression. -/ +def coreCFGIsAtAssert (cfg : DetCFG) : CoreCFGSpecConfig → AssertId Expression → Prop + | ⟨.cont lbl _ _, _⟩, aid => + match cfg.blocks.lookup lbl with + | some blk => blk.cmds.any fun + | .cmd (.assert l e _) => l == aid.label && e == aid.expr + | _ => false + | none => False + | ⟨.terminal _ _, _⟩, _ => False + +/-- The `Lang Expression` bundle for Core CFG small-step semantics. -/ +@[expose] def Lang.coreCFG + (π : String → Option Procedure) + (φ : CoreEval → PureFunc Expression → CoreEval) + (cfg : DetCFG) : + Imperative.Specification.Lang Expression where + StmtT := DetCFG + CfgT := CoreCFGSpecConfig + star := fun c₁ c₂ => CoreCFGStepStar π φ cfg c₁.cfgConfig c₂.cfgConfig + stmtCfg := fun _ ρ => ⟨.cont cfg.entry ρ.store false, ρ.eval⟩ + terminalCfg := fun ρ => ⟨.terminal ρ.store ρ.hasFailure, ρ.eval⟩ + exitingCfg := fun _ ρ => ⟨.terminal ρ.store ρ.hasFailure, ρ.eval⟩ + isAtAssert := coreCFGIsAtAssert cfg + getEnv := CoreCFGSpecConfig.toEnv + /-! ## Well-formed program state at the entry of procedure -/ /-- The list of variables that must have been declared, @@ -83,8 +124,13 @@ variable (φ : CoreEval → PureFunc Expression → CoreEval) @[expose] def AssertValidInProcedure (proc : Procedure) (a : Imperative.AssertId Expression) : Prop := - Imperative.Specification.AssertValidWhen (Specification.Lang.core π φ) - (ProcEnvWF proc) (Stmt.block "" proc.body #[]) a + match proc.body with + | .structured ss => + Imperative.Specification.AssertValidWhen (Specification.Lang.core π φ) + (ProcEnvWF proc) (Stmt.block "" ss #[]) a + | .cfg cfg => + Imperative.Specification.AssertValidWhen (Specification.Lang.coreCFG π φ cfg) + (ProcEnvWF proc) cfg a /-- A procedure is correct with respect to its specification. @@ -140,16 +186,21 @@ variable (φ : CoreEval → PureFunc Expression → CoreEval) structure ProcedureCorrect (proc : Procedure) (p : Program) : Prop where /-- (1) The asserts in the body of proc are valid. -/ assertsValid : ∀ a, AssertValidInProcedure π φ proc a - /-- (2) The postconditions hold on termination. -/ + /-- (2) The postconditions hold on termination. + Uses `CoreBodyExec` to abstract over both structured and CFG bodies. + For structured bodies, the terminal eval `δ'` comes from the terminal + `Env` (may differ from `δ` due to `funcDecl` extensions). For CFG + bodies, `δ' = δ` since `CoreCFGStepStar` does not track eval changes. -/ postconditionsValid : WF.WFProcedureProp p proc → - ∀ (ρ₀ ρ' : Env Expression), + ∀ (ρ₀ : Env Expression), ProcEnvWF proc ρ₀ → - CoreStepStar π φ (.stmts proc.body ρ₀) (.terminal ρ') → - (∀ (label : CoreLabel) (check : Procedure.Check), - (label, check) ∈ proc.spec.postconditions.toList → - check.attr = Procedure.CheckAttr.Default → - ρ'.eval ρ'.store check.expr = some HasBool.tt) ∧ - ρ'.hasFailure = Bool.false + ∀ (σ' : CoreStore) (δ' : CoreEval) (failed : Bool), + CoreBodyExec π φ proc.body ρ₀.store ρ₀.eval σ' δ' failed → + (∀ (label : CoreLabel) (check : Procedure.Check), + (label, check) ∈ proc.spec.postconditions.toList → + check.attr = Procedure.CheckAttr.Default → + δ' σ' check.expr = some HasBool.tt) ∧ + failed = Bool.false end Core.Specification diff --git a/Strata/Transform/CoreTransform.lean b/Strata/Transform/CoreTransform.lean index d621676ee0..0cb66a3fde 100644 --- a/Strata/Transform/CoreTransform.lean +++ b/Strata/Transform/CoreTransform.lean @@ -332,10 +332,20 @@ def runProgram currentProcedureName := .some proc.header.name.1 }) - let (changed, new_body) ← runStmtsRec f proc.body + -- TODO: A `runCFGRec` counterpart could be added to apply command-level + -- transforms to CFG bodies. Since `f` returns `Option (List Statement)` + -- and a CFG block holds `List Command`, each returned statement would + -- need to be unwrapped as `.cmd`. If `f` returns nested structures + -- (blocks, if-then-else, loops), those can't be represented in a basic + -- block, so such cases would need to be rejected or left untransformed. + let bodyStmts ← match proc.body with + | .structured ss => pure ss + | .cfg _ => throw (Strata.DiagnosticModel.fromMessage + s!"runProgram: cannot apply statement-level transform to CFG body (procedure '{proc.header.name.1}')") + let (changed, new_body) ← runStmtsRec f bodyStmts if changed then - newDecls := newDecls.set i (Decl.proc { proc with body := new_body } md) + newDecls := newDecls.set i (Decl.proc { proc with body := .structured new_body } md) anyChanged := true modify (fun σ => { σ with currentProgram := .some { decls := newDecls } diff --git a/Strata/Transform/LoopElim.lean b/Strata/Transform/LoopElim.lean index efbee4a8cd..887e1e6cf0 100644 --- a/Strata/Transform/LoopElim.lean +++ b/Strata/Transform/LoopElim.lean @@ -241,8 +241,12 @@ def loopElim (p : Program) : Program × Statistics := let (decls, stats) := p.decls.foldl (fun (acc, stats) d => match d with | .proc proc md => - let (body, st) := StateT.run (Block.removeLoopsM proc.body) {} - ((.proc { proc with body := body } md) :: acc, stats.merge st.statistics) + match proc.body with + | .structured ss => + let (body, st) := StateT.run (Block.removeLoopsM ss) {} + ((.proc { proc with body := .structured body } md) :: acc, stats.merge st.statistics) + -- CFG bodies have no structured loops; pass through unchanged. + | .cfg _ => ((.proc proc md) :: acc, stats) | other => (other :: acc, stats)) ([], {}) ({ decls := decls.reverse }, stats) diff --git a/Strata/Transform/PrecondElim.lean b/Strata/Transform/PrecondElim.lean index ee77df3440..8b1b8bb2af 100644 --- a/Strata/Transform/PrecondElim.lean +++ b/Strata/Transform/PrecondElim.lean @@ -88,9 +88,9 @@ so expression-level metadata carries no source location. We therefore inherit the enclosing statement's `md` (with `propertySummary` stripped to prevent user-facing messages from leaking into generated checks). -/ -def collectPrecondAsserts (F : @Lambda.Factory CoreLParams) (e : Expression.Expr) +def collectPrecondAssertCmds (F : @Lambda.Factory CoreLParams) (e : Expression.Expr) (labelPrefix : String) (md : Imperative.MetaData Expression) -: List Statement := +: List (Imperative.Cmd Expression) := let wfObs := Lambda.collectWFObligations F e -- Strip propertySummary: the enclosing statement's user-facing message -- (e.g., a Python assert message) should not propagate to generated @@ -100,7 +100,7 @@ def collectPrecondAsserts (F : @Lambda.Factory CoreLParams) (e : Expression.Expr -- For nested calls like SafeSDiv(SafeSDiv(x,y),z), obligations arrive as -- [inner-0, inner-1, outer-0, outer-1] with the same funcName throughout. -- Without modulo, the index would be 0,1,2,3 instead of 0,1,0,1. - let (_, _, result) := wfObs.foldl (init := ("", 0, ([] : List Statement))) + let (_, _, result) := wfObs.foldl (init := ("", 0, ([] : List (Imperative.Cmd Expression)))) fun (prevFunc, prevIdx, acc) ob => let rawIdx := if ob.funcName == prevFunc then prevIdx + 1 else 0 let precondCount := F[ob.funcName]?.map (·.preconditions.length) |>.getD 1 @@ -109,32 +109,52 @@ def collectPrecondAsserts (F : @Lambda.Factory CoreLParams) (e : Expression.Expr let md' := match classifyPrecondition ob.funcName precondIdx with | some pt => md.pushElem Imperative.MetaData.propertyType (.msg pt) | none => md - let stmt := Statement.assert + let cmd := Imperative.Cmd.assert s!"{labelPrefix}_calls_{ob.funcName}_{globalIdx}" ob.obligation md' - (ob.funcName, rawIdx, stmt :: acc) + (ob.funcName, rawIdx, cmd :: acc) result.reverse +private def cmdsToStatements (cs : List (Imperative.Cmd Expression)) : List Statement := + cs.map (fun c => Imperative.Stmt.cmd (CmdExt.cmd c)) + +private def cmdsToCommands (cs : List (Imperative.Cmd Expression)) : List Command := + cs.map CmdExt.cmd + +def collectPrecondAsserts (F : @Lambda.Factory CoreLParams) (e : Expression.Expr) +(labelPrefix : String) (md : Imperative.MetaData Expression) +: List Statement := + cmdsToStatements (collectPrecondAssertCmds F e labelPrefix md) + /-- Collect assertions for all expressions in a command. -/ -def collectCmdPrecondAsserts (F : @Lambda.Factory CoreLParams) - (cmd : Imperative.Cmd Expression) : List Statement := +def collectCmdPrecondAssertCmds (F : @Lambda.Factory CoreLParams) + (cmd : Imperative.Cmd Expression) : List (Imperative.Cmd Expression) := match cmd with - | .init _ _ (.det e) md => collectPrecondAsserts F e "init" md + | .init _ _ (.det e) md => collectPrecondAssertCmds F e "init" md | .init _ _ .nondet _ => [] - | .set x (.det e) md => collectPrecondAsserts F e s!"set_{x.name}" md + | .set x (.det e) md => collectPrecondAssertCmds F e s!"set_{x.name}" md | .set _ .nondet _ => [] - | .assert l e md => collectPrecondAsserts F e s!"assert_{l}" md - | .assume l e md => collectPrecondAsserts F e s!"assume_{l}" md - | .cover l e md => collectPrecondAsserts F e s!"cover_{l}" md + | .assert l e md => collectPrecondAssertCmds F e s!"assert_{l}" md + | .assume l e md => collectPrecondAssertCmds F e s!"assume_{l}" md + | .cover l e md => collectPrecondAssertCmds F e s!"cover_{l}" md + +def collectCmdPrecondAsserts (F : @Lambda.Factory CoreLParams) + (cmd : Imperative.Cmd Expression) : List Statement := + cmdsToStatements (collectCmdPrecondAssertCmds F cmd) /-- Collect assertions for call arguments. -/ +def collectCallPrecondAssertCmds (F : @Lambda.Factory CoreLParams) (pname : String) + (args : List Expression.Expr) (md : Imperative.MetaData Expression) + : List (Imperative.Cmd Expression) := + args.flatMap fun arg => collectPrecondAssertCmds F arg s!"call_{pname}_arg" md + def collectCallPrecondAsserts (F : @Lambda.Factory CoreLParams) (pname : String) (args : List Expression.Expr) (md : Imperative.MetaData Expression) : List Statement := - args.flatMap fun arg => collectPrecondAsserts F arg s!"call_{pname}_arg" md + cmdsToStatements (collectCallPrecondAssertCmds F pname args md) /-! ## Processing contract conditions -/ @@ -175,7 +195,7 @@ def mkContractWFProc (F : @Lambda.Factory CoreLParams) (proc : Procedure) some <| .proc { header := { proc.header with name := ⟨wfProcName name, ()⟩, noFilter := true } spec := { preconditions := [], postconditions := [] } - body := body + body := .structured body } md else none @@ -231,7 +251,7 @@ def mkFuncWFProc (F : @Lambda.Factory CoreLParams) (func : Function) noFilter := true } spec := { preconditions := [], postconditions := [] } - body := wfStmts + body := .structured wfStmts } md) /-! ## Statement transformation -/ @@ -341,6 +361,46 @@ def transformStmt (s : Statement) decreasing_by all_goals term_by_mem end +/-! ## CFG transformation -/ + +/-- Transform a single command in a CFG block, prepending precondition asserts. -/ +def transformCFGCmd (F : @Lambda.Factory CoreLParams) (cmd : Command) + : Bool × List Command := + match cmd with + | .cmd c => + let asserts := collectCmdPrecondAssertCmds F c + (!asserts.isEmpty, cmdsToCommands asserts ++ [.cmd c]) + | .call pname callArgs md => + let asserts := collectCallPrecondAssertCmds F pname (CallArg.getInputExprs callArgs) md + (!asserts.isEmpty, cmdsToCommands asserts ++ [.call pname callArgs md]) + +/-- Transform all commands in a CFG block. -/ +def transformCFGCmds (F : @Lambda.Factory CoreLParams) (cmds : List Command) + : Bool × List Command := + cmds.foldl (fun (changed, acc) cmd => + let (c, cmds') := transformCFGCmd F cmd + (changed || c, acc ++ cmds')) (false, []) + +/-- Transform a DetBlock: transform commands and add asserts for the transfer condition. -/ +def transformDetBlock (F : @Lambda.Factory CoreLParams) + (blk : Imperative.DetBlock String Command Expression) + : Bool × Imperative.DetBlock String Command Expression := + let (changed, cmds') := transformCFGCmds F blk.cmds + let (transferChanged, transferAsserts) := match blk.transfer with + | .condGoto cond _ _ md => + let asserts := collectPrecondAssertCmds F cond "branch_cond" md + (!asserts.isEmpty, cmdsToCommands asserts) + | .finish _ => (false, []) + (changed || transferChanged, ⟨cmds' ++ transferAsserts, blk.transfer⟩) + +/-- Transform an entire DetCFG. -/ +def transformDetCFG (F : @Lambda.Factory CoreLParams) (cfg : DetCFG) + : Bool × DetCFG := + let (changed, blocks') := cfg.blocks.foldl (fun (changed, acc) (label, blk) => + let (c, blk') := transformDetBlock F blk + (changed || c, acc ++ [(label, blk')])) (false, []) + (changed, { cfg with blocks := blocks' }) + /-! ## Main transformation -/ /-- Add a precondition-WF procedure as a leaf node in the cached call graph. @@ -382,7 +442,13 @@ where return (changed, d :: rest') else let F ← getFactory - let (changed, body') ← transformStmts proc.body + let (changed, body') ← match proc.body with + | .structured ss => do + let (c, ss') ← transformStmts ss + pure (c, Procedure.Body.structured ss') + | .cfg cfg => + let (c, cfg') := transformDetCFG F cfg + pure (c, Procedure.Body.cfg cfg') setFactory F let proc' := { proc with body := body' } let procDecl := Decl.proc proc' md @@ -391,7 +457,7 @@ where | some wfDecl => do incrementStat s!"{Stats.wfProceduresGenerated}" incrementStat s!"{Stats.wfProcedureBodyStmtsEmitted}" - (match wfDecl with | .proc p _ => p.body.length | _ => 0) + (match wfDecl with | .proc p _ => p.body.structuredLength | _ => 0) addWFProcToCallGraph (wfProcName (CoreIdent.toPretty proc.header.name)) return (true, wfDecl :: procDecl :: rest') @@ -411,7 +477,7 @@ where | some wfDecl => do incrementStat s!"{Stats.wfProceduresGenerated}" incrementStat s!"{Stats.wfProcedureBodyStmtsEmitted}" - (match wfDecl with | .proc p _ => p.body.length | _ => 0) + (match wfDecl with | .proc p _ => p.body.structuredLength | _ => 0) addWFProcToCallGraph (wfProcName (CoreIdent.toPretty func.name)) return (true, wfDecl :: funcDecl :: rest') @@ -436,7 +502,7 @@ where | some wfDecl => do incrementStat s!"{Stats.wfProceduresGenerated}" incrementStat s!"{Stats.wfProcedureBodyStmtsEmitted}" - (match wfDecl with | .proc p _ => p.body.length | _ => 0) + (match wfDecl with | .proc p _ => p.body.structuredLength | _ => 0) addWFProcToCallGraph (wfProcName (CoreIdent.toPretty func.name)) return some wfDecl diff --git a/Strata/Transform/ProcBodyVerify.lean b/Strata/Transform/ProcBodyVerify.lean index aa68c38a96..64503b9f71 100644 --- a/Strata/Transform/ProcBodyVerify.lean +++ b/Strata/Transform/ProcBodyVerify.lean @@ -88,8 +88,13 @@ open Core Imperative Transform -- Convert preconditions to assumes let assumes := requiresToAssumes proc.spec.preconditions + -- ProcBodyVerify expects a structured body: the prefix (inits + assumes) and + -- suffix (postcondition asserts) are statement-level constructs that embed + -- around the body. Unstructured CFG bodies require a different verification + -- strategy (e.g., encoding the contract directly in the CFG). + let bodyStmts ← proc.body.getStructured.mapError Strata.DiagnosticModel.fromMessage -- Wrap body in labeled block - let bodyBlock := Stmt.block bodyLabel proc.body #[] + let bodyBlock := Stmt.block bodyLabel bodyStmts #[] -- Convert postconditions to asserts let asserts := ensuresToAsserts proc.spec.postconditions diff --git a/Strata/Transform/ProcBodyVerifyCorrect.lean b/Strata/Transform/ProcBodyVerifyCorrect.lean index 515f44dee2..3e8ac3d73f 100644 --- a/Strata/Transform/ProcBodyVerifyCorrect.lean +++ b/Strata/Transform/ProcBodyVerifyCorrect.lean @@ -447,6 +447,17 @@ private theorem mapM_stateT_pure_eq {α β : Type} {σ : Type} {ε : Type} /-! ## Verification Statement Structure -/ +/-- if `procToVerifyStmt` succeeds, then the input procedure has `.structured` body -/ +theorem procToVerifyStmt_is_structured + (h : (procToVerifyStmt proc).run st = (Except.ok verifyStmt, st')) : + ∃ ss, proc.body = .structured ss := by + simp [ExceptT.run, procToVerifyStmt] at h + cases hb: proc.body with + | structured ss => simp + | cfg blk => + simp [hb] at h + cases h + /-- Structure: the output of `procToVerifyStmt` is a block `prefix ++ [bodyBlock] ++ postAsserts`, and all prefix statements are `.cmd` (init/assume commands). @@ -459,16 +470,19 @@ theorem procToVerifyStmt_structure (π : String → Option Procedure) (φ : CoreEval → PureFunc Expression → CoreEval) (h_wf_proc : WF.WFProcedureProp p proc) : - ∃ (prefixStmts : List Statement), + ∃ (prefixStmts ss : List Statement), + proc.body = .structured ss ∧ verifyStmt = Stmt.block s!"verify_{proc.header.name.name}" - (prefixStmts ++ [Stmt.block s!"body_{proc.header.name.name}" proc.body #[]] ++ + (prefixStmts ++ [Stmt.block s!"body_{proc.header.name.name}" ss #[]] ++ ensuresToAsserts proc.spec.postconditions) #[] ∧ (∀ s ∈ prefixStmts, ∃ c, s = Stmt.cmd c) ∧ (∀ ρ₀, Core.Specification.ProcEnvWF proc ρ₀ → ∃ ρ_init, Imperative.StepStmtStar Expression (EvalCommand π φ) (EvalPureFunc φ) (.stmts prefixStmts ρ_init) (.terminal ρ₀)) := by + obtain ⟨ss, h_body_eq⟩ := procToVerifyStmt_is_structured h unfold procToVerifyStmt at h + rw [h_body_eq] at h simp only [bind, ExceptT.bind, ExceptT.mk, ExceptT.run, ExceptT.bindCont, pure, ExceptT.pure, StateT.bind] at h rw [mapM_stateT_pure_eq] at h @@ -483,7 +497,8 @@ theorem procToVerifyStmt_structure (.det (LExpr.fvar () id none)) #[] let assumes := requiresToAssumes proc.spec.preconditions let prefixStmts := inputInits ++ outputOnlyInits ++ oldInoutInits ++ assumes - refine ⟨prefixStmts, h_eq.symm, ?_, ?_⟩ + rw [h_body_eq] + refine ⟨prefixStmts, ss, rfl, h_eq.symm, ?_, ?_⟩ · intro s hs simp only [prefixStmts, List.mem_append] at hs rcases hs with ((hs | hs) | hs) | hs @@ -643,9 +658,13 @@ theorem procBodyVerify_procedureCorrect (h_wf_proc : WF.WFProcedureProp p proc) : -- Conclusion: ProcedureCorrect holds. Core.Specification.ProcedureCorrect π φ proc p := by - - obtain ⟨prefixStmts, h_eq, h_prefix_cmd, h_prefix_trace⟩ := + obtain ⟨ss, h_body_eq⟩ := procToVerifyStmt_is_structured h_transform + obtain ⟨prefixStmts, ss', h_body, h_eq, h_prefix_cmd, h_prefix_trace⟩ := procToVerifyStmt_structure proc p st st' verifyStmt h_transform π φ h_wf_proc + have h_ss_eq : ss = ss' := by + have := h_body_eq.symm.trans h_body + exact Procedure.Body.structured.inj this + subst h_ss_eq let verifyLabel := s!"verify_{proc.header.name.name}" let bodyLabel := s!"body_{proc.header.name.name}" let postAsserts := ensuresToAsserts proc.spec.postconditions @@ -656,7 +675,7 @@ theorem procBodyVerify_procedureCorrect verifyStmt context (block verifyLabel > seq > block bodyLabel). -/ have h_embed_body : ∀ ρ₀ (h_wf : Specification.ProcEnvWF proc ρ₀) (cfg : CoreConfig), - CoreStepStar π φ (.stmts proc.body ρ₀) cfg → + CoreStepStar π φ (.stmts ss ρ₀) cfg → ∃ ρ_init, StepStmtStar Expression (EvalCommand π φ) (EvalPureFunc φ) (.stmt verifyStmt ρ_init) @@ -712,7 +731,7 @@ theorem procBodyVerify_procedureCorrect -- Unified helper: all asserts reachable from proc.body are valid have body_asserts_valid : ∀ ρ₀ (h_wf : Specification.ProcEnvWF proc ρ₀) (a : AssertId Expression) (cfg : CoreConfig), - CoreStepStar π φ (.stmts proc.body ρ₀) cfg → + CoreStepStar π φ (.stmts ss ρ₀) cfg → coreIsAtAssert cfg a → cfg.getEval cfg.getStore a.expr = some HasBool.tt := by intro ρ₀ h_wf a cfg h_body h_assert @@ -727,23 +746,25 @@ theorem procBodyVerify_procedureCorrect · ----- Part 1: All asserts in proc.body are valid ----- intro a - unfold Specification.AssertValidInProcedure Specification.AssertValidWhen + unfold Specification.AssertValidInProcedure + rw [h_body_eq] + unfold Specification.AssertValidWhen simp only [Specification.Lang.core, Specification.Lang.imperative] intro ρ₀ cfg (h_wf : Specification.ProcEnvWF proc ρ₀) (h_body : StepStmtStar Expression (EvalCommand π φ) (EvalPureFunc φ) - (.stmt (Stmt.block "" proc.body #[]) ρ₀) cfg) + (.stmt (Stmt.block "" ss #[]) ρ₀) cfg) (h_assert : coreIsAtAssert cfg a) -- Extract first step: .stmt (block "" body #[]) ρ₀ → .block (.some "") ρ₀.store (.stmts body ρ₀) have h_block_star : StepStmtStar Expression (EvalCommand π φ) (EvalPureFunc φ) - (.block (.some "") ρ₀.store (.stmts proc.body ρ₀)) cfg := by + (.block (.some "") ρ₀.store (.stmts ss ρ₀)) cfg := by cases h_body with | refl => simp [coreIsAtAssert] at h_assert | step _ _ _ hstep hrest => cases hstep; exact hrest -- Body never exits (from WFProcedureProp.bodyExitsCovered) have h_no_exit : ∀ lbl ρ', ¬ StepStmtStar Expression (EvalCommand π φ) (EvalPureFunc φ) - (.stmts proc.body ρ₀) (.exiting lbl ρ') := - block_exitsCoveredByBlocks_noEscape Expression (EvalCommand π φ) (EvalPureFunc φ) - proc.body h_wf_proc.bodyExitsCovered ρ₀ + (.stmts ss ρ₀) (.exiting lbl ρ') := + have hcov := h_wf_proc.bodyExitsCovered ss h_body_eq + block_exitsCoveredByBlocks_noEscape Expression (EvalCommand π φ) (EvalPureFunc φ) ss hcov ρ₀ -- cfg is not terminal or exiting (has an assert) have h_nt : ∀ ρ', cfg ≠ .terminal ρ' := by intro ρ' heq; subst heq; exact coreIsAtAssert_not_terminal ρ' a h_assert @@ -761,22 +782,39 @@ theorem procBodyVerify_procedureCorrect simpa [Config.getEval, Config.getStore] using h_valid · ----- Part 2: Postconditions + hasFailure on termination ----- - intro h_wf_proc ρ₀ ρ' h_wf h_term + -- The unified field uses CoreBodyExec. Since procToVerifyStmt only + -- succeeds for structured bodies, we invert the CoreBodyExec to get + -- a CoreStepStar witness. + intro _ ρ₀ h_wf σ' δ' failed h_body_exec + -- Invert CoreBodyExec: since proc.body = .structured ss, the only + -- matching constructor is .structured, giving us a CoreStepStar witness. + rw [h_body_eq] at h_body_exec + -- Invert: the .structured constructor builds the initial env as + -- ⟨σ, δ, false⟩. ProcEnvWF gives us ρ₀.hasFailure = false, so + -- ⟨ρ₀.store, ρ₀.eval, false⟩ = ρ₀. + have h_env_eq : (⟨ρ₀.store, ρ₀.eval, false⟩ : Env Expression) = ρ₀ := by + have := h_wf.noFailure; cases ρ₀; simp_all + obtain ⟨ρ', h_term⟩ : ∃ ρ' : Env Expression, + CoreStepStar π φ (.stmts ss ρ₀) (.terminal ρ') ∧ + σ' = ρ'.store ∧ δ' = ρ'.eval ∧ failed = ρ'.hasFailure := by + cases h_body_exec with + | structured h_step => exact ⟨_, h_env_eq ▸ h_step, rfl, rfl, rfl⟩ + obtain ⟨h_term, rfl, rfl, rfl⟩ := h_term obtain ⟨ρ_init, h_prefix⟩ := h_prefix_trace ρ₀ h_wf -- h_valid: all asserts in body from ρ₀ evaluate to true have h_valid : ∀ (a : AssertId Expression) (cfg : CoreConfig), - CoreStepStar π φ (.stmts proc.body ρ₀) cfg → + CoreStepStar π φ (.stmts ss ρ₀) cfg → coreIsAtAssert cfg a → cfg.getEval cfg.getStore a.expr = some HasBool.tt := fun a cfg h h' => body_asserts_valid ρ₀ h_wf a cfg h h' -- hasFailure = false have h_nf' : ρ'.hasFailure = Bool.false := Core.core_noFailure_preserved π φ - (.stmts proc.body ρ₀) (.terminal ρ') h_valid h_wf.noFailure h_term + (.stmts ss ρ₀) (.terminal ρ') h_valid h_wf.noFailure h_term -- wfBool preservation have h_wfb_term : WellFormedSemanticEvalBool ρ'.eval := Core.core_wfBool_preserved π φ h_wf_ext - (.stmts proc.body ρ₀) (.terminal ρ') h_wf.wfBool h_term + (.stmts ss ρ₀) (.terminal ρ') h_wf.wfBool h_term -- After the body block terminates via step_block_done, the store is projected. -- We define the projected env. @@ -815,13 +853,13 @@ theorem procBodyVerify_procedureCorrect have h_proj_hasFailure : ρ_proj.hasFailure = ρ'.hasFailure := rfl have h_wfVar_term : WellFormedSemanticEvalVar ρ'.eval := Core.core_wfVar_preserved π φ h_wf_ext - (.stmts proc.body ρ₀) (.terminal ρ') h_wf.wfVar h_term + (.stmts ss ρ₀) (.terminal ρ') h_wf.wfVar h_term have h_wfCong_term : Core.WellFormedCoreEvalCong ρ'.eval := Core.core_wfCong_preserved π φ h_wf_ext - (.stmts proc.body ρ₀) (.terminal ρ') h_wf.wfCong h_term + (.stmts ss ρ₀) (.terminal ρ') h_wf.wfCong h_term have h_wfExprCongr_term : WellFormedSemanticEvalExprCongr ρ'.eval := Core.core_wfExprCongr_preserved π φ h_wf_ext - (.stmts proc.body ρ₀) (.terminal ρ') h_wf.wfExprCongr h_term + (.stmts ss ρ₀) (.terminal ρ') h_wf.wfExprCongr h_term have h_all_post_valid : ∀ s ∈ postAsserts, ∀ l e md, s = Statement.assert l e md → ρ'.eval ρ'.store e = some HasBool.tt := by diff --git a/Strata/Transform/ProcedureInlining.lean b/Strata/Transform/ProcedureInlining.lean index 752e626aa6..728727d661 100644 --- a/Strata/Transform/ProcedureInlining.lean +++ b/Strata/Transform/ProcedureInlining.lean @@ -93,14 +93,17 @@ private def renameAllLocalNames (c:Procedure) let var_map: Map Expression.Ident Expression.Ident := [] let proc_name := c.header.name.name - -- Make a map for renaming local variables - let lhs_vars := List.flatMap (fun (s:Statement) => s.definedVars) c.body + -- Extract local names from the body. Although ProcedureInlining only supports + -- structured bodies for inlining, extracting defined variables is a generic + -- facility that supports both structured and CFG bodies. + let lhs_vars : List Expression.Ident := Imperative.HasVarsImp.definedVars c.body + let bodyStmts := match c.body with | .structured ss => ss | .cfg _ => [] let lhs_vars := lhs_vars ++ c.header.inputs.unzip.fst ++ c.header.outputs.unzip.fst let var_map <- genOldToFreshIdMappings lhs_vars var_map proc_name -- Make a map for renaming label names - let labels := List.flatMap (fun s => Statement.labels s) c.body + let labels := List.flatMap (fun s => Statement.labels s) bodyStmts -- Reuse genOldToFreshIdMappings by introducing dummy data to Identifier let label_ids:List Expression.Ident := labels.map (fun s => { name:=s, metadata := () }) @@ -112,12 +115,17 @@ private def renameAllLocalNames (c:Procedure) -- by genOldToFreshIdMappings (counter-based), so a fresh new_id cannot collide with -- a later old_id. The iteration is intentionally sequential because each step also -- renames LHS variables and labels. - let new_body := List.map (fun (s0:Statement) => - var_map.foldl (fun (s:Statement) (old_id,new_id) => - let s := Statement.substFvar s old_id (.fvar () new_id .none) - let s := Statement.renameLhs s old_id new_id - Statement.replaceLabels s label_map) - s0) c.body + let new_body : Procedure.Body ← match c.body with + | .structured bodyStmts => + pure <| .structured (List.map (fun (s0:Statement) => + var_map.foldl (fun (s:Statement) (old_id,new_id) => + let s := Statement.substFvar s old_id (.fvar () new_id .none) + let s := Statement.renameLhs s old_id new_id + Statement.replaceLabels s label_map) + s0) bodyStmts) + | .cfg _ => + throw (Strata.DiagnosticModel.fromMessage + "renameAllLocalNames: CFG body renaming not yet implemented") let new_header := { c.header with inputs := c.header.inputs.map (fun (id,ty) => match var_map.find? id with @@ -269,9 +277,17 @@ def inlineCallCmd Statement.set lhs_var (.fvar () out_var (.none)) md) outs_lhs_and_sig + -- Cannot inline unstructured (CFG) bodies into structured code. + -- CFG-level inlining is a separate, more complex pass that operates + -- entirely in the CFG domain (graph splicing). + let procBodyStmts ← match proc.body with + | .cfg _ => throw (Strata.DiagnosticModel.fromMessage + "cannot inline procedure with CFG body into structured code") + | .structured ss => pure ss + let stmts:List (Imperative.Stmt Core.Expression Core.Command) := inputInits ++ outputInits - ++ Block.setCallSiteMetadata proc.body md + ++ Block.setCallSiteMetadata procBodyStmts md ++ outputSetStmts -- Update CallGraph if available diff --git a/Strata/Transform/StructuredToUnstructured.lean b/Strata/Transform/StructuredToUnstructured.lean index 94b345d25f..8782fff782 100644 --- a/Strata/Transform/StructuredToUnstructured.lean +++ b/Strata/Transform/StructuredToUnstructured.lean @@ -68,7 +68,7 @@ match ss with | .typeDecl _ _ :: rest => do -- Not yet supported, so just continue with `rest`. stmtsToBlocks k rest exitConts accum -| .block l bss _md :: rest => do +| .block l bss md :: rest => do -- Process rest first let (kNext, bsNext) ← stmtsToBlocks k rest exitConts [] -- Process block body, extending the list of exit continuations. @@ -80,9 +80,9 @@ match ss with -- Empty accumulated block pure (accumEntry, accumBlocks ++ bbs ++ bsNext) else - let b := (l, { cmds := [], transfer := .goto bl }) + let b := (l, { cmds := [], transfer := .goto bl md }) pure (l, accumBlocks ++ [b] ++ bbs ++ bsNext) -| .ite c tss fss _md :: rest => do +| .ite c tss fss md :: rest => do -- Process rest first let (kNext, bsNext) ← stmtsToBlocks k rest exitConts [] -- Create ite block @@ -98,9 +98,9 @@ match ss with let initCmd := HasInit.init ident HasBool.boolTy .nondet synthesizedMd pure (HasFvar.mkFvar ident, [initCmd]) let (accumEntry, accumBlocks) ← flushCmds "ite$" (accum ++ extraCmds) - (.some (.condGoto condExpr tl fl)) l + (.some (.condGoto condExpr tl fl md)) l pure (accumEntry, accumBlocks ++ tbs ++ fbs ++ bsNext) -| .loop c m is bss _md :: rest => do +| .loop c m is bss md :: rest => do -- Process rest first let (kNext, bsNext) ← stmtsToBlocks k rest exitConts [] -- Create loop entry block @@ -135,10 +135,18 @@ match ss with if srcLabel.isEmpty then StringGenState.gen "inv$" else pure srcLabel pure (HasPassiveCmds.assert assertLabel i synthesizedMd)) + -- Attach loop contract (invariants + measure) to the transfer metadata so + -- downstream CFG passes can recover the original spec without relying on the + -- lowered assert commands alone. + let contractMd := is.foldl (fun md (_, inv) => + md.pushElem MetaData.specLoopInvariant (.expr inv)) md + let contractMd := match m with + | some mExpr => contractMd.pushElem MetaData.specDecreases (.expr mExpr) + | none => contractMd -- For nondet guards, introduce a fresh boolean variable match c with | .det e => - let b := (lentry, { cmds := invCmds ++ measureCmds, transfer := .condGoto e bl kNext }) + let b := (lentry, { cmds := invCmds ++ measureCmds, transfer := .condGoto e bl kNext contractMd }) let (accumEntry, accumBlocks) ← flushCmds "before_loop$" accum .none lentry pure (accumEntry, accumBlocks ++ [b] ++ bbs ++ decreaseBlocks ++ bsNext) | .nondet => do @@ -146,10 +154,10 @@ match ss with let ident := HasIdent.ident (P := P) freshName let initCmd := HasInit.init ident HasBool.boolTy .nondet synthesizedMd let b := (lentry, { cmds := [initCmd] ++ invCmds ++ measureCmds, - transfer := .condGoto (HasFvar.mkFvar ident) bl kNext }) + transfer := .condGoto (HasFvar.mkFvar ident) bl kNext contractMd }) let (accumEntry, accumBlocks) ← flushCmds "before_loop$" accum .none lentry pure (accumEntry, accumBlocks ++ [b] ++ bbs ++ decreaseBlocks ++ bsNext) -| .exit l _md :: _ => do +| .exit l md :: _ => do -- Find the continuation of the block labeled `l`. let bk := match exitConts.lookup (.some l) with @@ -160,7 +168,7 @@ match ss with -- Flush the accumulated commands, going to the continuation calculated above. -- Any statements after the `.exit` are skipped. let exitName := s!"block${l}$" - flushCmds exitName accum .none bk + flushCmds exitName accum (.some (.goto bk md)) bk def stmtsToCFGM [HasBool P] [HasPassiveCmds P CmdT] [HasInit P CmdT] diff --git a/Strata/Transform/TerminationCheck.lean b/Strata/Transform/TerminationCheck.lean index ddc8065a7c..30b53d0121 100644 --- a/Strata/Transform/TerminationCheck.lean +++ b/Strata/Transform/TerminationCheck.lean @@ -216,7 +216,7 @@ private def mkTermCheckProc (func.preconditions.mapIdx fun i p => (s!"{func.name.name}_requires_{i}", { expr := p.expr, attr := .Free })), postconditions := [] } - body := stmts + body := .structured stmts } md, obligations.length) /-- Add a termination-check procedure as a leaf node in the cached call graph. -/ diff --git a/StrataTest/Backends/CBMC/GOTO/E2E_CFGPipeline.lean b/StrataTest/Backends/CBMC/GOTO/E2E_CFGPipeline.lean new file mode 100644 index 0000000000..93f540876b --- /dev/null +++ b/StrataTest/Backends/CBMC/GOTO/E2E_CFGPipeline.lean @@ -0,0 +1,296 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +import Strata.Backends.CBMC.CollectSymbols +import Strata.Backends.CBMC.GOTO.CoreCFGToGOTOPipeline +import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline + +/-! ## Equivalence tests: direct path vs. CFG path + +Run both `procedureToGotoCtx` (direct) and `procedureToGotoCtxViaCFG` (CFG) +on the same programs and compare outputs. + +The CFG path produces additional GOTO instructions for explicit block-to-block +transfers that the direct path handles implicitly via fall-through. Comparisons +therefore focus on **semantic** instructions (DECL, ASSIGN, ASSERT, ASSUME, +FUNCTION_CALL, END_FUNCTION) and contract annotations, ignoring cosmetic GOTO +and LOCATION differences. +-/ + +open Strata + +private def translateCore (p : Strata.Program) : Core.Program := + (TransM.run Inhabited.default (translateProgram p)).fst + +/-! ### Instruction-level comparison helpers -/ + +private def isSemanticInst (inst : CProverGOTO.Instruction) : Bool := + match inst.type with + | .DECL | .ASSIGN | .ASSERT | .ASSUME | .FUNCTION_CALL + | .SET_RETURN_VALUE | .END_FUNCTION => true + | _ => false + +private def compareSemanticInstructions + (directInsts cfgInsts : Array CProverGOTO.Instruction) + : Except String Unit := do + let dSemantic := directInsts.filter isSemanticInst + let cSemantic := cfgInsts.filter isSemanticInst + if dSemantic.size != cSemantic.size then + throw s!"Semantic instruction count mismatch: direct={dSemantic.size} cfg={cSemantic.size}" + for i in List.range dSemantic.size do + if dSemantic[i]!.type != cSemantic[i]!.type then + throw s!"Semantic instruction type mismatch at index {i}: \ + direct={dSemantic[i]!.type} cfg={cSemantic[i]!.type}" + return () + +/-! ### Pipeline runners -/ + +private def runDirectPipeline (cprog : Core.Program) (procName : String := "main") + : Except Std.Format (CoreToGOTO.CProverGOTO.Context × List Core.Function) := do + let Env := Lambda.TEnv.default + let procs := cprog.decls.filterMap fun d => d.getProc? + let axioms := cprog.decls.filterMap fun d => d.getAxiom? + let distincts := cprog.decls.filterMap fun d => match d with + | .distinct name es _ => some (name, es) | _ => none + let some proc := procs.find? (fun p => Core.CoreIdent.toPretty p.header.name == procName) + | .error f!"procedure {procName} not found" + procedureToGotoCtx Env proc (axioms := axioms) (distincts := distincts) + +private def runCFGPipeline (cprog : Core.Program) (procName : String := "main") + : Except Std.Format (CoreToGOTO.CProverGOTO.Context × List Core.Function) := do + let Env := Lambda.TEnv.default + let procs := cprog.decls.filterMap fun d => d.getProc? + let axioms := cprog.decls.filterMap fun d => d.getAxiom? + let distincts := cprog.decls.filterMap fun d => match d with + | .distinct name es _ => some (name, es) | _ => none + let some proc := procs.find? (fun p => Core.CoreIdent.toPretty p.header.name == procName) + | .error f!"procedure {procName} not found" + procedureToGotoCtxViaCFG Env proc (axioms := axioms) (distincts := distincts) + +private def toJson (ctx : CoreToGOTO.CProverGOTO.Context) (pname : String) + : Except Std.Format (Lean.Json × Lean.Json) := do + let json ← (CoreToGOTO.CProverGOTO.Context.toJson pname ctx).mapError (fun e => f!"{e}") + return (json.symtab, json.goto) + +/-- Run both pipelines and compare semantic instructions + contracts + JSON validity. -/ +private def testEquivalence (prog : Strata.Program) (procName : String := "main") + : IO Unit := do + let cprog := translateCore prog + let directResult := runDirectPipeline cprog procName + let cfgResult := runCFGPipeline cprog procName + match directResult, cfgResult with + | .error e, _ => IO.throwServerError s!"Direct pipeline failed: {e}" + | _, .error e => IO.throwServerError s!"CFG pipeline failed: {e}" + | .ok (dctx, _), .ok (cctx, _) => + -- Instruction-level: compare semantic instructions (ignoring GOTO/LOCATION) + match compareSemanticInstructions dctx.program.instructions cctx.program.instructions with + | .error e => IO.throwServerError s!"Instruction mismatch: {e}" + | .ok () => pure () + -- Contract annotations must match + if dctx.contracts.length != cctx.contracts.length then + IO.throwServerError s!"Contract count mismatch: direct={dctx.contracts.length} cfg={cctx.contracts.length}" + for (dk, dv) in dctx.contracts do + match cctx.contracts.find? (·.1 == dk) with + | some (_, cv) => + if dv != cv then + IO.throwServerError s!"Contract value mismatch for {dk}" + | none => + IO.throwServerError s!"Contract key {dk} missing from CFG path" + -- JSON-level: both produce valid, non-null output + let pname := "main" + match toJson dctx pname, toJson cctx pname with + | .error e, _ => IO.throwServerError s!"Direct JSON failed: {e}" + | _, .error e => IO.throwServerError s!"CFG JSON failed: {e}" + | .ok (dSym, dGoto), .ok (cSym, cGoto) => + assert! dSym != Lean.Json.null + assert! cSym != Lean.Json.null + assert! dGoto != Lean.Json.null + assert! cGoto != Lean.Json.null + +------------------------------------------------------------------------------- + +-- Test 1: Simple assert +def CFGEq_SimpleAssert := +#strata +program Core; +procedure main(x : int) { + assert (x > 0); +}; +#end + +#eval testEquivalence CFGEq_SimpleAssert + +------------------------------------------------------------------------------- + +-- Test 2: Variable declaration and assignment +def CFGEq_VarDeclAssign := +#strata +program Core; +procedure main(x : int) { + var z : int := x + 1; + assert (z > 0); +}; +#end + +#eval testEquivalence CFGEq_VarDeclAssign + +------------------------------------------------------------------------------- + +-- Test 3: If-then-else +def CFGEq_IfThenElse := +#strata +program Core; +procedure main(x : int) { + var r : int; + if (x > 0) { + r := 1; + } else { + r := 0; + } + assert (r >= 0); +}; +#end + +#eval testEquivalence CFGEq_IfThenElse + +------------------------------------------------------------------------------- + +-- Test 4: Preconditions and postconditions +def CFGEq_Contracts := +#strata +program Core; +procedure main(x : int) +spec { + requires (x > 0); + ensures (x >= 0); +} { + assert (x > 0); +}; +#end + +#eval testEquivalence CFGEq_Contracts + +------------------------------------------------------------------------------- + +-- Test 5: Axioms and distinct declarations +def CFGEq_AxiomDistinct := +#strata +program Core; +const a : int; +const b : int; +axiom [ax1]: (a > 0); +distinct [ab]: [a, b]; +procedure main() { + assert (a != b); +}; +#end + +#eval testEquivalence CFGEq_AxiomDistinct + +------------------------------------------------------------------------------- + +-- Test 6: Free specs are skipped (same in both paths) +def CFGEq_FreeSpecs := +#strata +program Core; +procedure main(x : int) +spec { + free requires (x > 10); + requires (x >= 0); + free ensures (x > 5); + ensures (x >= 0); +} { + assert (x >= 0); +}; +#end + +#eval testEquivalence CFGEq_FreeSpecs + +------------------------------------------------------------------------------- + +-- Test 7: Cover command +def CFGEq_Cover := +#strata +program Core; +procedure main(x : int) { + cover (x > 0); +}; +#end + +#eval testEquivalence CFGEq_Cover + +------------------------------------------------------------------------------- + +-- Test 8: Bitvector operations +def CFGEq_BVOps := +#strata +program Core; +procedure main(x : bv32, y : bv32) { + var z : bv32 := x + y; + assert (z > bv{32}(0)); +}; +#end + +#eval testEquivalence CFGEq_BVOps + +------------------------------------------------------------------------------- + +-- Test 9: Assume command +def CFGEq_Assume := +#strata +program Core; +procedure main(x : int) { + assume (x > 0); + assert (x > 0); +}; +#end + +#eval testEquivalence CFGEq_Assume + +------------------------------------------------------------------------------- + +-- Test 10: Multiple sequential commands +def CFGEq_MultipleCommands := +#strata +program Core; +procedure main(x : int) { + var a : int := x + 1; + var b : int := a + 2; + assert (b > x); +}; +#end + +#eval testEquivalence CFGEq_MultipleCommands + +------------------------------------------------------------------------------- + +-- Test 11: CFG path only — verify the CFG-only pipeline produces valid output +-- (no direct path comparison since .cfg bodies aren't supported by the direct path) +#eval do + let prog := + #strata + program Core; + procedure main(x : int) { + var r : int; + if (x > 0) { + r := 1; + } else { + r := 0; + } + assert (r >= 0); + }; + #end + let cprog := translateCore prog + match runCFGPipeline cprog with + | .error e => IO.throwServerError s!"CFG pipeline failed: {e}" + | .ok (ctx, _) => + match toJson ctx "main" with + | .error e => IO.throwServerError s!"JSON failed: {e}" + | .ok (symtab, goto) => + assert! symtab != Lean.Json.null + assert! goto != Lean.Json.null + let gotoStr := goto.pretty + assert! (gotoStr.splitOn "GOTO").length > 1 + assert! (gotoStr.splitOn "ASSERT").length > 1 diff --git a/StrataTest/Backends/CBMC/GOTO/E2E_CoreToGOTO.lean b/StrataTest/Backends/CBMC/GOTO/E2E_CoreToGOTO.lean index a33056b01b..cca938708b 100644 --- a/StrataTest/Backends/CBMC/GOTO/E2E_CoreToGOTO.lean +++ b/StrataTest/Backends/CBMC/GOTO/E2E_CoreToGOTO.lean @@ -344,13 +344,18 @@ private def injectPropertySummary (stmts : List Core.Statement) (msg : String) .cmd (.cmd (.assert label b (md.withPropertySummary msg))) | other => other +-- TODO: This could be split into a two-stage transformation: +-- 1. structured → cfg (via StructuredToUnstructured) +-- 2. cfg → CProverGOTO (always operates on CFG, no pattern matching needed) +-- For now, unstructured bodies are not supported in this test helper. private def coreToGotoJsonWithSummary (p : Strata.Program) (summary : String) : Except Std.Format (Lean.Json × Lean.Json) := do let cprog := translateCore p let Env := Lambda.TEnv.default let procs := cprog.decls.filterMap fun d => d.getProc? let p := procs[0]! - let p' : Core.Procedure := { p with body := injectPropertySummary p.body summary } + let bodyStmts ← p.body.getStructured.mapError fun s => f!"{s}" + let p' : Core.Procedure := { p with body := .structured (injectPropertySummary bodyStmts summary) } let pname := Core.CoreIdent.toPretty p'.header.name let ctx ← procedureToGotoCtx Env p' let json ← (CoreToGOTO.CProverGOTO.Context.toJson pname ctx.1).mapError (fun e => f!"{e}") diff --git a/StrataTest/Languages/Boole/global_readonly_call.lean b/StrataTest/Languages/Boole/global_readonly_call.lean index a0445f8753..a76a23812a 100644 --- a/StrataTest/Languages/Boole/global_readonly_call.lean +++ b/StrataTest/Languages/Boole/global_readonly_call.lean @@ -66,7 +66,9 @@ private def callHelper (p : Strata.Program) : Except String (List String) := do return cp.decls.filterMap fun d => match d with | .proc p _ => - p.body.findSome? fun + -- CFG bodies: call extraction not yet implemented for unstructured programs. + let stmts := match p.body with | .structured ss => ss | .cfg _ => [] + stmts.findSome? fun | .block _ stmts _ => stmts.findSome? fun | .cmd (.call pname args _) => some s!"call {pname}({", ".intercalate (args.map fmtCallArg)})" @@ -141,41 +143,41 @@ spec { VCs: -Label: inc_ensures_1_2418 +Label: inc_ensures_1_2576 Property: assert Assumptions: -inc_requires_0_2400: z@1 > 0 +inc_requires_0_2558: z@1 > 0 Obligation: true -Label: callElimAssert_inc_requires_0_2400_6 +Label: callElimAssert_inc_requires_0_2558_6 Property: assert Assumptions: -main_caller_requires_2_2534: z@3 == 10 -main_caller_requires_3_2554: g@3 == 0 +main_caller_requires_2_2692: z@3 == 10 +main_caller_requires_3_2712: g@3 == 0 Obligation: z@3 > 0 -Label: main_caller_ensures_4_2573 +Label: main_caller_ensures_4_2731 Property: assert Assumptions: -main_caller_requires_2_2534: z@3 == 10 -main_caller_requires_3_2554: g@3 == 0 -callElimAssume_inc_ensures_1_2418_7: g@5 == g@3 + 5 + z@5 +main_caller_requires_2_2692: z@3 == 10 +main_caller_requires_3_2712: g@3 == 0 +callElimAssume_inc_ensures_1_2576_7: g@5 == g@3 + 5 + z@5 Obligation: g@5 == 15 --- info: -Obligation: inc_ensures_1_2418 +Obligation: inc_ensures_1_2576 Property: assert Result: ✅ pass -Obligation: callElimAssert_inc_requires_0_2400_6 +Obligation: callElimAssert_inc_requires_0_2558_6 Property: assert Result: ✅ pass -Obligation: main_caller_ensures_4_2573 +Obligation: main_caller_ensures_4_2731 Property: assert Result: ❓ unknown Model: diff --git a/StrataTest/Languages/Core/Examples/Exit.lean b/StrataTest/Languages/Core/Examples/Exit.lean index 53dedb039d..f33cccc1aa 100644 --- a/StrataTest/Languages/Core/Examples/Exit.lean +++ b/StrataTest/Languages/Core/Examples/Exit.lean @@ -116,10 +116,10 @@ Result: ✅ pass info: Entry: l1 l1: - condGoto true block$l1$_2 block$l1$_2 + #[<[provenance]: :387-502>] condGoto true block$l1$_2 block$l1$_2 block$l1$_2: assert [a1]: x == x; - condGoto true l$_1 l$_1 + #[<[provenance]: :426-434>] condGoto true l$_1 l$_1 l$_1: assert [a3]: x == x; condGoto true end$_0 end$_0 @@ -133,29 +133,29 @@ end$_0: info: Entry: l5 l5: - condGoto true l4 l4 + #[<[provenance]: :577-1056>] condGoto true l4 l4 l4: - condGoto true l4_before l4_before + #[<[provenance]: :589-1050>] condGoto true l4_before l4_before l4_before: - condGoto true l3_before l3_before + #[<[provenance]: :603-996>] condGoto true l3_before l3_before l3_before: - condGoto true l1 l1 + #[<[provenance]: :626-933>] condGoto true l1 l1 l1: - condGoto true ite$_5 ite$_5 + #[<[provenance]: :651-835>] condGoto true ite$_5 ite$_5 ite$_5: assert [a4]: x == x; - condGoto x > 0 block$l5$_2 block$l5$_1 + #[<[provenance]: :706-821>] condGoto x > 0 block$l5$_2 block$l5$_1 l2: - condGoto true l$_3 l$_3 + #[<[provenance]: :848-921>] condGoto true l$_3 l$_3 l$_3: assert [a5]: !(x == x); condGoto true block$l5$_2 block$l5$_2 block$l5$_2: assert [a6]: x * 2 > x; - condGoto true end$_0 end$_0 + #[<[provenance]: :978-986>] condGoto true end$_0 end$_0 block$l5$_1: assert [a7]: x <= 0; - condGoto true end$_0 end$_0 + #[<[provenance]: :1034-1042>] condGoto true end$_0 end$_0 end$_0: finish -/ diff --git a/StrataTest/Languages/Core/Examples/Loops.lean b/StrataTest/Languages/Core/Examples/Loops.lean index ddcddd7c62..7881a6d710 100644 --- a/StrataTest/Languages/Core/Examples/Loops.lean +++ b/StrataTest/Languages/Core/Examples/Loops.lean @@ -15,7 +15,9 @@ def singleCFG (p : Program) (n : Nat) : Imperative.CFG String let corePgm : Core.Program := TransM.run Inhabited.default (translateProgram p) |>.fst let proc := match corePgm.decls[n]? with | .some (.proc p _) => p | _ => Inhabited.default - Imperative.stmtsToCFG proc.body + match proc.body with + | .structured ss => Imperative.stmtsToCFG ss + | .cfg cfg => cfg --------------------------------------------------------------------- @@ -52,7 +54,10 @@ loop_entry$_1: var loop_measure$_2 : int; assume [assume_loop_measure$_2]: loop_measure$_2 == n; assert [measure_lb_loop_measure$_2]: !(loop_measure$_2 < 0); - condGoto i < n l$_4 end$_0 + #[<[provenance]: :869-975>, + <[#spec_loop_invariant]: 0 <= i>, + <[#spec_loop_invariant]: i <= n>, + <[#spec_decreases]: n>] condGoto i < n l$_4 end$_0 l$_4: i := i + 1; condGoto true measure_decrease$_3 measure_decrease$_3 @@ -140,7 +145,11 @@ loop_entry$_1: var loop_measure$_2 : int; assume [assume_loop_measure$_2]: loop_measure$_2 == n - i; assert [measure_lb_loop_measure$_2]: !(loop_measure$_2 < 0); - condGoto i < n l$_4 end$_0 + #[<[provenance]: :2590-2746>, + <[#spec_loop_invariant]: 0 <= i>, + <[#spec_loop_invariant]: i <= n>, + <[#spec_loop_invariant]: s == i * (i + 1) / 2>, + <[#spec_decreases]: n - i>] condGoto i < n l$_4 end$_0 l$_4: i := i + 1; s := s + i; @@ -388,7 +397,11 @@ Context: Global scope: var loop_measure$_2 : int; assume [assume_loop_measure$_2]: loop_measure$_2 == n - x; assert [measure_lb_loop_measure$_2]: !(loop_measure$_2 < 0); - condGoto x < n before_loop$_11 end$_0 + #[<[provenance]: :8360-8613>, + <[#spec_loop_invariant]: x >= 0>, + <[#spec_loop_invariant]: x <= n>, + <[#spec_loop_invariant]: n < top>, + <[#spec_decreases]: n - x>] condGoto x < n before_loop$_11 end$_0 before_loop$_11: y := 0; condGoto true loop_entry$_5 loop_entry$_5 @@ -398,7 +411,10 @@ loop_entry$_5: var loop_measure$_6 : int; assume [assume_loop_measure$_6]: loop_measure$_6 == x - y; assert [measure_lb_loop_measure$_6]: !(loop_measure$_6 < 0); - condGoto y < x l$_8 l$_4 + #[<[provenance]: :8480-8593>, + <[#spec_loop_invariant]: y >= 0>, + <[#spec_loop_invariant]: y <= x>, + <[#spec_decreases]: x - y>] condGoto y < x l$_8 l$_4 l$_8: y := y + 1; condGoto true measure_decrease$_7 measure_decrease$_7 diff --git a/StrataTest/Languages/Core/Tests/CFGParseTests.lean b/StrataTest/Languages/Core/Tests/CFGParseTests.lean new file mode 100644 index 0000000000..263040833f --- /dev/null +++ b/StrataTest/Languages/Core/Tests/CFGParseTests.lean @@ -0,0 +1,404 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ +import Strata.DDM.Elab +import Strata.DDM.BuiltinDialects.Init +import Strata.Languages.Core.DDMTransform.Grammar +import Strata.Languages.Core.Verifier +import Strata.SimpleAPI + +/-! # Tests for CFG (unstructured) procedure parsing -/ + +open Strata +open Strata.Elab (parseStrataProgramFromDialect) + +private def parseCoreText (input : String) : IO Core.Program := do + let inputCtx := Strata.Parser.stringInputContext "inline" input + let dialects := Strata.Elab.LoadedDialects.ofDialects! #[initDialect, Strata.Core] + let strataProgram ← parseStrataProgramFromDialect dialects Strata.Core.name inputCtx + match genericToCore strataProgram with + | .ok program => pure program + | .error msg => throw (IO.userError msg) + +private def printCFGProcInfo (prog : Core.Program) : IO Unit := do + for d in prog.decls do + match d with + | .proc p _ => + IO.println s!"Procedure: {Core.CoreIdent.toPretty p.header.name}" + match p.body with + | .cfg c => + IO.println s!" CFG entry: {c.entry}, {c.blocks.length} blocks" + for (lbl, blk) in c.blocks do + let transferDesc := match blk.transfer with + | .condGoto _ l1 l2 _ => if l1 == l2 then s!"goto {l1}" else s!"branch → {l1}/{l2}" + | .finish _ => "return" + IO.println s!" Block '{lbl}': {blk.cmds.length} cmds, {transferDesc}" + | .structured _ => IO.println " ERROR: expected CFG body" + | _ => pure () + +/-! ## Deterministic CFG with conditional branch -/ + +/-- +info: Procedure: Max + CFG entry: entry, 4 blocks + Block 'entry': 0 cmds, branch → then_branch/else_branch + Block 'then_branch': 1 cmds, goto done + Block 'else_branch': 1 cmds, goto done + Block 'done': 0 cmds, return +-/ +#guard_msgs in +#eval do + let prog ← parseCoreText " +procedure Max(x : int, y : int, out m : int) +spec { + ensures (m >= x); + ensures (m >= y); +} +cfg entry { + entry: { + branch (x >= y) goto then_branch else else_branch; + } + then_branch: { + m := x; + goto done; + } + else_branch: { + m := y; + goto done; + } + done: { + return; + } +}; +" + printCFGProcInfo prog + +/-! ## Nondeterministic CFG with multi-target goto -/ + +/-- +info: Procedure: NondetChoice + CFG entry: entry, 4 blocks + Block 'entry': 0 cmds, branch → left/right + Block 'left': 1 cmds, goto done + Block 'right': 1 cmds, goto done + Block 'done': 0 cmds, return +-/ +#guard_msgs in +#eval do + let prog ← parseCoreText " +procedure NondetChoice(out y : int) +cfg entry { + entry: { + goto left, right; + } + left: { + y := 1; + goto done; + } + right: { + y := 2; + goto done; + } + done: { + return; + } +}; +" + printCFGProcInfo prog + +/-! ## CFG loop pattern -/ + +/-- +info: Procedure: CountUp + CFG entry: entry, 4 blocks + Block 'entry': 1 cmds, goto loop + Block 'loop': 0 cmds, branch → body/done + Block 'body': 1 cmds, goto loop + Block 'done': 0 cmds, return +-/ +#guard_msgs in +#eval do + let prog ← parseCoreText " +procedure CountUp(n : int, out y : int) +spec { + requires (n >= 0); +} +cfg entry { + entry: { + y := 0; + goto loop; + } + loop: { + branch (y < n) goto body else done; + } + body: { + y := y + 1; + goto loop; + } + done: { + return; + } +}; +" + printCFGProcInfo prog + +/-! ## Empty block (just a transfer) -/ + +/-- +info: Procedure: Trivial + CFG entry: start, 1 blocks + Block 'start': 0 cmds, return +-/ +#guard_msgs in +#eval do + let prog ← parseCoreText " +procedure Trivial() +cfg start { + start: { + return; + } +}; +" + printCFGProcInfo prog + +/-! ## End-to-end: type-checking accepts well-formed CFG procedures -/ + +/-- +info: type-check accepted CFG procedure +-/ +#guard_msgs in +#eval do + let prog ← parseCoreText " +procedure Trivial() +cfg start { + start: { + return; + } +}; +" + match Core.typeCheck .quiet prog with + | .error dm => IO.println s!"ERROR: type-check rejected CFG procedure: {dm.message}" + | .ok _ => IO.println "type-check accepted CFG procedure" + +/-! ## End-to-end: type-checking accepts Max (branches + assignments) -/ + +/-- +info: type-check accepted Max with CFG body preserved (4 blocks) +-/ +#guard_msgs in +#eval do + let prog ← parseCoreText " +procedure Max(x : int, y : int, out m : int) +spec { + ensures (m >= x); + ensures (m >= y); +} +cfg entry { + entry: { + branch (x >= y) goto then_branch else else_branch; + } + then_branch: { + m := x; + goto done; + } + else_branch: { + m := y; + goto done; + } + done: { + return; + } +}; +" + match Core.typeCheck .quiet prog with + | .error dm => IO.println s!"ERROR: {dm.message}" + | .ok prog' => + for d in prog'.decls do + match d with + | .proc p _ => + match p.body with + | .cfg c => + IO.println s!"type-check accepted Max with CFG body preserved ({c.blocks.length} blocks)" + | .structured ss => + IO.println s!"ERROR: body collapsed to .structured with {ss.length} statements" + | _ => pure () + +/-! ## End-to-end: type-checking accepts CountUp (loop pattern with init) -/ + +/-- +info: type-check accepted CountUp +-/ +#guard_msgs in +#eval do + let prog ← parseCoreText " +procedure CountUp(n : int, out y : int) +spec { + requires (n >= 0); +} +cfg entry { + entry: { + y := 0; + goto loop; + } + loop: { + branch (y < n) goto body else done; + } + body: { + y := y + 1; + goto loop; + } + done: { + return; + } +}; +" + match Core.typeCheck .quiet prog with + | .error dm => IO.println s!"ERROR: {dm.message}" + | .ok _ => IO.println "type-check accepted CountUp" + +/-! ## Error: duplicate block labels -/ + +/-- +info: rejected: Duplicate block labels in CFG +-/ +#guard_msgs in +#eval do + let prog ← parseCoreText " +procedure Bad() +cfg start { + start: { return; } + start: { return; } +}; +" + match Core.typeCheck .quiet prog with + | .error dm => + if dm.message.contains "Duplicate block labels" then + IO.println "rejected: Duplicate block labels in CFG" + else + IO.println s!"ERROR: unexpected message: {dm.message}" + | .ok _ => IO.println "ERROR: expected type-check to fail" + +/-! ## Error: unknown target label -/ + +/-- +info: rejected: branches to unknown label +-/ +#guard_msgs in +#eval do + let prog ← parseCoreText " +procedure Bad(out y : int) +cfg start { + start: { + y := 0; + goto nonexistent; + } +}; +" + match Core.typeCheck .quiet prog with + | .error dm => + if dm.message.contains "branches to unknown label" then + IO.println "rejected: branches to unknown label" + else + IO.println s!"ERROR: unexpected message: {dm.message}" + | .ok _ => IO.println "ERROR: expected type-check to fail" + +/-! ## Error: type mismatch in CFG command -/ + +/-- +info: rejected: type error in CFG command +-/ +#guard_msgs in +#eval do + let prog ← parseCoreText " +procedure Bad(x : bool, out y : int) +cfg start { + start: { + y := x; + return; + } +}; +" + match Core.typeCheck .quiet prog with + | .error _ => + IO.println "rejected: type error in CFG command" + | .ok _ => IO.println "ERROR: expected type-check to fail" + +/-! ## Error: modification rights violation in CFG -/ + +/-- +info: rejected: modifies disallowed variable +-/ +#guard_msgs in +#eval do + let prog ← parseCoreText " +procedure Bad(x : int) +cfg start { + start: { + x := 42; + return; + } +}; +" + match Core.typeCheck .quiet prog with + | .error dm => + if dm.message.contains "modifies variables" then + IO.println "rejected: modifies disallowed variable" + else + IO.println s!"ERROR: unexpected message: {dm.message}" + | .ok _ => IO.println "ERROR: expected type-check to fail" + +/-! ## Multiple nondet gotos get distinct condition variables -/ + +open Std (format) in +private def getTransferCondStr (blk : Imperative.DetBlock String Core.Command Core.Expression) + : Option String := + match blk.transfer with + | .condGoto cond l1 l2 _ => + if l1 != l2 then some (toString (format cond)) else none + | _ => none + +/-- +info: nondet condition names are distinct across blocks +-/ +#guard_msgs in +#eval do + let prog ← parseCoreText " +procedure MultiNondet(out y : int) +cfg entry { + entry: { + goto a, b; + } + a: { + goto c, d; + } + b: { + y := 1; + goto done; + } + c: { + y := 2; + goto done; + } + d: { + y := 3; + goto done; + } + done: { + return; + } +}; +" + for d in prog.decls do + match d with + | .proc p _ => + match p.body with + | .cfg cfg => + let condNames := cfg.blocks.filterMap fun (pair : String × _) => getTransferCondStr pair.2 + if condNames.length == 2 && condNames.Nodup then + IO.println "nondet condition names are distinct across blocks" + else + IO.println s!"ERROR: expected 2 distinct nondet conditions, got {condNames}" + | .structured _ => IO.println "ERROR: expected CFG body" + | _ => pure () diff --git a/StrataTest/Languages/Core/Tests/NestedInductiveRestriction.lean b/StrataTest/Languages/Core/Tests/NestedInductiveRestriction.lean new file mode 100644 index 0000000000..ed6760400b --- /dev/null +++ b/StrataTest/Languages/Core/Tests/NestedInductiveRestriction.lean @@ -0,0 +1,68 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +/-! # Lean 4 Nested Inductive Restriction in Mutual Blocks + +This file demonstrates why `CoreEvalDetBlock` and `CoreEvalCmds` in +`StatementSemantics.lean` cannot directly reuse the generic +`Imperative.EvalDetBlock` and `Imperative.EvalCmds`. + +## The Rule + +Passing a mutual inductive (partially applied) as a parameter to an external +inductive works IF that external inductive uses the parameter **directly** in +its own constructors. It FAILS if the external inductive delegates to yet +another inductive parameterized by the same slot. + +## Application to CFG Semantics + +- `Imperative.StepStmt` uses `EvalCmd` directly → `CoreStepStar` can use + `StepStmt Expression (EvalCommand π φ)` ✓ +- `Imperative.EvalDetBlock` delegates to `Imperative.EvalCmds` (another + inductive) → cannot use `EvalDetBlock Expression (EvalCommand π φ)` ✗ + +This forces us to duplicate `EvalDetBlock`/`EvalCmds` as `CoreEvalDetBlock`/ +`CoreEvalCmds` inside the mutual block. +-/ + +-- External inductive that uses EvalCmd DIRECTLY in its own constructor +inductive DirectUse (α : Type) (EvalCmd : α → Nat → Nat → Prop) : Nat → Nat → Prop where + | mk : EvalCmd a σ σ' → DirectUse α EvalCmd σ σ' + +-- External inductive that DELEGATES to another inductive (EvalList) +inductive EvalList (α : Type) (EvalCmd : α → Nat → Nat → Prop) : Nat → Nat → Prop where + | nil : EvalCmd a σ σ' → EvalList α EvalCmd σ σ + | cons : EvalList α EvalCmd σ σ' → EvalList α EvalCmd σ σ' + +inductive EvalList' (α : Type) (EvalCmd : α → Nat → Nat → Prop) : Nat → Nat → Prop where + -- EvalList' is not directly using EvalCmd (the commented-out nil constructor directly uses it), so can't be nested in BadStar + -- | nil : EvalCmd a σ σ' → EvalList' α EvalCmd σ σ' + | cons : EvalList α EvalCmd σ σ' → EvalList' α EvalCmd σ σ' + +-- ✓ WORKS: DirectUse uses EvalCmd in its own constructor only +mutual +inductive GoodStar (n : Nat) : Nat → Nat → Prop where + | refl : GoodStar n c c + | step : DirectUse Nat (GoodCmd n) c₁ c₂ → GoodStar n c₂ c₃ → GoodStar n c₁ c₃ + +inductive GoodCmd (n : Nat) : Nat → Nat → Nat → Prop where + | call : GoodStar n σ σ' → GoodCmd n x σ σ' +end + +-- ✗ FAILS: EvalList' references EvalList internally, creating a nested +-- inductive chain. Uncomment to see the error: +-- "(kernel) invalid nested inductive datatype 'EvalList'', +-- nested inductive datatypes parameters cannot contain local variables." +/- +mutual +inductive BadStar (n : Nat) : Nat → Nat → Prop where + | refl : BadStar n c c + | step : EvalList' Nat (BadCmd n) c₁ c₂ → BadStar n c₂ c₃ → BadStar n c₁ c₃ + +inductive BadCmd (n : Nat) : Nat → Nat → Nat → Prop where + | call : BadStar n σ σ' → BadCmd n x σ σ' +end +-/ diff --git a/StrataTest/Languages/Core/Tests/ProcedureEvalCFGTests.lean b/StrataTest/Languages/Core/Tests/ProcedureEvalCFGTests.lean new file mode 100644 index 0000000000..6cbc99b177 --- /dev/null +++ b/StrataTest/Languages/Core/Tests/ProcedureEvalCFGTests.lean @@ -0,0 +1,257 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.Core.ProcedureEval + +namespace Core + +section CFGEvalTests + +open Std (ToFormat Format format) +open Procedure Statement Lambda Lambda.LTy.Syntax Lambda.LExpr.SyntaxMono Core.Syntax +open Imperative + +private def cfgEval (p : Procedure) : String := + let E := Env.init (empty_factory := true) + let (E, _stats) := eval E p + toString (format E) + +/-! ## Trivial CFG: single block with finish, no parameters -/ + +/-- +info: Error: +none +Subst Map: + +Expression Env: +State: + + +Evaluation Config: +Eval Depth: 200 +Factory Functions: + + + +Datatypes: + +Path Conditions: + + +Warnings: +[] +Deferred Proof Obligations: +-/ +#guard_msgs in +#eval IO.println (cfgEval + { header := {name := "Trivial", typeArgs := [], inputs := [], outputs := [] }, + spec := { preconditions := [], postconditions := [] }, + body := .cfg { entry := "start", + blocks := [("start", { cmds := [], transfer := .finish })] } }) + +/-! ## Linear CFG: assignment via goto, postcondition holds -/ + +/-- +info: Error: +none +Subst Map: + +Expression Env: +State: + + +Evaluation Config: +Eval Depth: 200 +Factory Functions: + + + +Datatypes: + +Path Conditions: + + +Warnings: +[] +Deferred Proof Obligations: +Label: y_eq_42 +Property: assert +Assumptions: + +Proof Obligation: +true +-/ +#guard_msgs in +#eval IO.println (cfgEval + { header := {name := "Linear", typeArgs := [], + inputs := [], outputs := [("y", mty[int])] }, + spec := { preconditions := [], + postconditions := [("y_eq_42", ⟨eb[y == #42], .Default, #[]⟩)] }, + body := .cfg { entry := "entry", + blocks := [ + ("entry", { cmds := [CmdExt.cmd (Cmd.set "y" (.det eb[#42]) .empty)], + transfer := .goto "done" }), + ("done", { cmds := [], transfer := .finish }) + ] } }) + +/-! ## Missing block error -/ + +/-- +info: Error: +some [ERROR] evalCFG: block 'nonexistent' not found in CFG +Subst Map: + +Expression Env: +State: +[] + +Evaluation Config: +Eval Depth: 200 +Factory Functions: + + + +Datatypes: + +Path Conditions: + + + +Warnings: +[] +Deferred Proof Obligations: +-/ +#guard_msgs in +#eval IO.println (cfgEval + { header := {name := "MissingBlock", typeArgs := [], inputs := [], outputs := [] }, + spec := { preconditions := [], postconditions := [] }, + body := .cfg { entry := "start", + blocks := [("start", { cmds := [], + transfer := .goto "nonexistent" })] } }) + +/-! ## Fuel exhaustion: loop back-edge -/ + +/-- +info: has error: true +-/ +#guard_msgs in +#eval do + let E := Env.init (empty_factory := true) + let p : Procedure := + { header := {name := "Loop", typeArgs := [], + inputs := [], outputs := [("y", mty[int])] }, + spec := { preconditions := [], postconditions := [] }, + body := .cfg { entry := "loop", + blocks := [ + ("loop", { cmds := [CmdExt.cmd (Cmd.set "y" (.det eb[#1]) .empty)], + transfer := .goto "loop" }) + ] } } + let (E, _stats) := eval E p + IO.println s!"has error: {E.error.isSome}" + +/-! ## Postcondition failure: non-trivial proof obligation -/ + +/-- +info: Error: +none +Subst Map: + +Expression Env: +State: + + +Evaluation Config: +Eval Depth: 200 +Factory Functions: + + + +Datatypes: + +Path Conditions: + + +Warnings: +[] +Deferred Proof Obligations: +Label: y_eq_0 +Property: assert +Assumptions: + +Proof Obligation: +false +-/ +#guard_msgs in +#eval IO.println (cfgEval + { header := {name := "PostFail", typeArgs := [], + inputs := [], outputs := [("y", mty[int])] }, + spec := { preconditions := [], + postconditions := [("y_eq_0", ⟨eb[y == #0], .Default, #[]⟩)] }, + body := .cfg { entry := "entry", + blocks := [ + ("entry", { cmds := [CmdExt.cmd (Cmd.set "y" (.det eb[#42]) .empty)], + transfer := .finish }) + ] } }) + +/-! ## Diamond CFG: symbolic branch produces two proof obligations -/ + +/-- +info: Error: +none +Subst Map: + +Expression Env: +State: + + +Evaluation Config: +Eval Depth: 200 +Factory Functions: + + + +Datatypes: + +Path Conditions: + + +Warnings: +[] +Deferred Proof Obligations: +Label: y_ge_0 +Property: assert +Assumptions: +(= 0>, x@1 >= 0) +Proof Obligation: +x@1 >= 0 + +Label: y_ge_0 +Property: assert +Assumptions: +(= 0)>, if x@1 >= 0 then false else true) +Proof Obligation: +0 - x@1 >= 0 +-/ +#guard_msgs in +#eval IO.println (cfgEval + { header := {name := "Diamond", typeArgs := [], + inputs := [("x", mty[int])], + outputs := [("y", mty[int])] }, + spec := { preconditions := [], + postconditions := [("y_ge_0", ⟨eb[((~Int.Ge y) #0)], .Default, #[]⟩)] }, + body := .cfg { entry := "entry", + blocks := [ + ("entry", { cmds := [], + transfer := .condGoto eb[((~Int.Ge x) #0)] "pos" "neg" }), + ("pos", { cmds := [CmdExt.cmd (Cmd.set "y" (.det eb[x]) .empty)], + transfer := .goto "done" }), + ("neg", { cmds := [CmdExt.cmd (Cmd.set "y" (.det eb[((~Int.Sub #0) x)]) .empty)], + transfer := .goto "done" }), + ("done", { cmds := [], transfer := .finish }) + ] } }) + +end CFGEvalTests +end Core diff --git a/StrataTest/Languages/Core/Tests/ProcedureTypeTests.lean b/StrataTest/Languages/Core/Tests/ProcedureTypeTests.lean index f970ca1270..fe3912e4f0 100644 --- a/StrataTest/Languages/Core/Tests/ProcedureTypeTests.lean +++ b/StrataTest/Languages/Core/Tests/ProcedureTypeTests.lean @@ -36,7 +36,7 @@ info: ok: (procedure P (x : int, out y : int) outputs := [("y", mty[int])] }, spec := { preconditions := [("0_lt_x", ⟨eb[((~Int.Lt #0) x)], .Default, #[]⟩)], postconditions := [("ret_y_lt_0", ⟨eb[((~Int.Lt y) #0)], .Default, #[]⟩)] }, - body := [ + body := .structured [ Statement.set "y" eb[((~Int.Sub #0) x)] .empty ] } diff --git a/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean b/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean index 51d905cbd8..3728d1c3f9 100644 --- a/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean +++ b/StrataTest/Languages/Core/Tests/ProgramEvalTests.lean @@ -404,7 +404,7 @@ Proof Obligation: spec := { preconditions := [("0_lt_x", ⟨eb[((~Int.Lt #0) x)], .Default, #[]⟩)], postconditions := [("ret_y_lt_0", ⟨eb[((~Int.Lt y) #0)], .Default, #[]⟩)] }, - body := [ + body := .structured [ Statement.set "y" eb[(~Int.Neg x)] .empty ] } diff --git a/StrataTest/Languages/Core/Tests/ProgramTypeTests.lean b/StrataTest/Languages/Core/Tests/ProgramTypeTests.lean index ea9c591c50..9a56d40530 100644 --- a/StrataTest/Languages/Core/Tests/ProgramTypeTests.lean +++ b/StrataTest/Languages/Core/Tests/ProgramTypeTests.lean @@ -30,7 +30,7 @@ def bad_prog : Program := { decls := [ spec := { preconditions := [], postconditions := [] }, - body := [ + body := .structured [ Statement.assert "test" eb[(~fooAliasVal == ~fooVal)] .empty ] } .empty @@ -60,7 +60,7 @@ def good_prog : Program := { decls := [ spec := { preconditions := [], postconditions := [] }, - body := [ + body := .structured [ Statement.assert "test" eb[(~fooAliasVal == ~fooVal)] .empty ] } .empty @@ -102,7 +102,7 @@ def outOfScopeVarProg : Program := { decls := [ spec := { preconditions := [], postconditions := [] }, - body := [ + body := .structured [ Statement.set "y" eb[((~Bool.Or x) x)] .empty, .ite (.det eb[(x == #true)]) [Statement.init "q" t[int] (.det eb[#0]) .empty, @@ -146,7 +146,7 @@ def polyFuncProg : Program := { decls := [ outputs := [] }, spec := { preconditions := [], postconditions := [] }, - body := [ + body := .structured [ -- var m : Map int bool; Statement.init "m" (.forAll [] (.tcons "Map" [.tcons "int" [], .tcons "bool" []])) Imperative.ExprOrNondet.nondet .empty, -- m := makePair(identity(42), identity(true)); diff --git a/StrataTest/Languages/Core/Tests/StatementTypeTests.lean b/StrataTest/Languages/Core/Tests/StatementTypeTests.lean index c635fb2184..489ec6e6e5 100644 --- a/StrataTest/Languages/Core/Tests/StatementTypeTests.lean +++ b/StrataTest/Languages/Core/Tests/StatementTypeTests.lean @@ -253,7 +253,7 @@ private def testProc : Procedure := inputs := [(⟨"x", ()⟩, .int)], outputs := [(⟨"x", ()⟩, .int), (⟨"y", ()⟩, .int)] }, spec := { preconditions := [], postconditions := [] }, - body := [] } + body := .structured [] } private def testProgram : Program := { decls := [.proc testProc .empty] } diff --git a/StrataTest/Transform/ProcedureInlining.lean b/StrataTest/Transform/ProcedureInlining.lean index a7c7c08f4a..abaa58e3e4 100644 --- a/StrataTest/Transform/ProcedureInlining.lean +++ b/StrataTest/Transform/ProcedureInlining.lean @@ -211,19 +211,56 @@ def alphaEquivStatement (s1 s2: Core.Statement) (map:IdMap) end -private def alphaEquiv (p1 p2:Core.Procedure):Except Format Bool := do - if p1.body.length ≠ p2.body.length then - .error (s!"# statements do not match: in {p1.header.name}, " - ++ s!"inlined fn one has {p1.body.length}" - ++ s!" whereas the answer has {p2.body.length}") +private def alphaEquivCmds (cmds1 cmds2 : List Core.Command) (map : IdMap) + : Except Format IdMap := do + if cmds1.length ≠ cmds2.length then + .error f!"CFG block command count mismatch: {cmds1.length} vs {cmds2.length}" else + (cmds1.zip cmds2).foldlM (fun map (c1, c2) => + alphaEquivStatement (.cmd c1) (.cmd c2) map) map + +private def alphaEquivTransfer (t1 t2 : Imperative.DetTransferCmd String Core.Expression) + (map : IdMap) : Except Format IdMap := do + match t1, t2 with + | .condGoto c1 lt1 lf1 _, .condGoto c2 lt2 lf2 _ => + if ¬ alphaEquivExprs c1 c2 map then + .error f!"CFG transfer condition mismatch" + else + let map ← IdMap.updateLabel map lt1 lt2 + IdMap.updateLabel map lf1 lf2 + | .finish _, .finish _ => .ok map + | _, _ => .error "CFG transfer type mismatch" + +private def alphaEquivCFG (cfg1 cfg2 : Core.DetCFG) (map : IdMap) + : Except Format IdMap := do + let map ← IdMap.updateLabel map cfg1.entry cfg2.entry + if cfg1.blocks.length ≠ cfg2.blocks.length then + .error f!"CFG block count mismatch: {cfg1.blocks.length} vs {cfg2.blocks.length}" + else + (cfg1.blocks.zip cfg2.blocks).foldlM (fun map ((lbl1, blk1), (lbl2, blk2)) => do + let map ← IdMap.updateLabel map lbl1 lbl2 + let map ← alphaEquivCmds blk1.cmds blk2.cmds map + alphaEquivTransfer blk1.transfer blk2.transfer map) map + +private def alphaEquiv (p1 p2:Core.Procedure):Except Format Bool := do + match p1.body, p2.body with + | .structured ss1, .structured ss2 => + if ss1.length ≠ ss2.length then + .error (s!"# statements do not match: in {p1.header.name}, " + ++ s!"inlined fn one has {ss1.length}" + ++ s!" whereas the answer has {ss2.length}") + else + let newmap:IdMap := IdMap.mk ([], []) [] + let m ← List.foldlM (fun (map:IdMap) (s1,s2) => + alphaEquivStatement s1 s2 map) + newmap (ss1.zip ss2) + return ((p1.header.outputs.zip p2.header.outputs).map (fun ((x, _), (y, _)) => alphaEquivIdents x y m)).all id + | .cfg cfg1, .cfg cfg2 => let newmap:IdMap := IdMap.mk ([], []) [] - let stmts := (p1.body.zip p2.body) - let m ← List.foldlM (fun (map:IdMap) (s1,s2) => - alphaEquivStatement s1 s2 map) - newmap stmts - -- The corresponding outputs should be pairwise α-equivalent + let m ← alphaEquivCFG cfg1 cfg2 newmap return ((p1.header.outputs.zip p2.header.outputs).map (fun ((x, _), (y, _)) => alphaEquivIdents x y m)).all id + | .structured _, .cfg _ => .error "body type mismatch: structured vs cfg" + | .cfg _, .structured _ => .error "body type mismatch: cfg vs structured" diff --git a/StrataTest/Transform/StructuredToUnstructuredTests.lean b/StrataTest/Transform/StructuredToUnstructuredTests.lean new file mode 100644 index 0000000000..872923fb28 --- /dev/null +++ b/StrataTest/Transform/StructuredToUnstructuredTests.lean @@ -0,0 +1,152 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Transform.StructuredToUnstructured +import Strata.DL.Lambda.Lambda + +/-! ## Tests for loop contract metadata preservation in StructuredToUnstructured -/ + +section +open Std (ToFormat Format format) +open Lambda.LTy.Syntax +open Imperative (MetaData MetaDataElem) + +private abbrev TP : Lambda.LExprParams := ⟨Unit, Unit⟩ + +private abbrev P : Imperative.PureExpr := + { Ident := TP.Identifier, + Expr := Lambda.LExprT TP.mono, + Ty := Lambda.LMonoTy, + ExprMetadata := TP.Metadata, + TyEnv := @Lambda.TEnv TP.IDMeta, + TyContext := @Lambda.LContext TP, + EvalEnv := Lambda.LState TP + EqIdent := inferInstanceAs (DecidableEq TP.Identifier) } + +private abbrev mdB : Lambda.Typed Unit := { underlying := (), type := mty[bool] } + +instance : Imperative.HasBool P where + tt := .const mdB (.boolConst true) + ff := .const mdB (.boolConst false) + tt_is_not_ff := by simp + boolTy := mty[bool] + +instance : Imperative.HasIdent P where + ident s := ⟨s, ()⟩ + +instance : Imperative.HasFvar P where + mkFvar := (.fvar mdB · none) + getFvar | .fvar _ v _ => some v | _ => none + +instance : Imperative.HasIntOrder P where + eq e1 e2 := .eq mdB e1 e2 + lt e1 e2 := .app mdB (.app mdB (.op mdB ⟨"Int.Lt", ()⟩ none) e1) e2 + zero := .intConst mdB 0 + intTy := mty[int] + +instance : Imperative.HasNot P where + not e := .app mdB (.op mdB ⟨"Bool.Not", ()⟩ none) e + +instance : Imperative.HasPassiveCmds P (Imperative.Cmd P) where + assert l e md := .assert l e md + assume l e md := .assume l e md + +instance : Imperative.HasInit P (Imperative.Cmd P) where + init i ty e md := .init i ty e md + +private def mkFvar (name : String) : P.Expr := .fvar mdB ⟨name, ()⟩ none +private def trueExpr : P.Expr := .const mdB (.boolConst true) + +private abbrev Stmt' := Imperative.Stmt P (Imperative.Cmd P) +private abbrev CFG' := Imperative.CFG String (Imperative.DetBlock String (Imperative.Cmd P) P) + +private def toCFG (ss : List Stmt') : CFG' := Imperative.stmtsToCFG ss + +private def findLoopEntry (cfg : CFG') : + Option (Imperative.DetBlock String (Imperative.Cmd P) P) := + cfg.blocks.find? (fun (lbl, _) => lbl.startsWith "loop_entry$") |>.map (·.2) + +private def getTransferMd (blk : Imperative.DetBlock String (Imperative.Cmd P) P) : + MetaData P := + match blk.transfer with + | .condGoto _ _ _ md => md + | .finish md => md + +private def countField (md : MetaData P) (fld : MetaDataElem.Field P) : Nat := + md.filter (fun e => e.fld == fld) |>.size + +private def loopEntryMd (ss : List Stmt') : MetaData P := + match findLoopEntry (toCFG ss) with + | some blk => getTransferMd blk + | none => .empty + +private def setCmd (name : String) : Imperative.Cmd P := + .set ⟨name, ()⟩ (.det (mkFvar name)) .empty + +/-! ### Simple loop with one invariant: specLoopInvariant in transfer metadata -/ + +#guard countField (loopEntryMd [ + .loop (.det trueExpr) none [("inv0", mkFvar "x")] [.cmd (setCmd "x")] .empty + ]) MetaData.specLoopInvariant == 1 + +/-! ### Loop with multiple invariants: one entry per invariant -/ + +#guard countField (loopEntryMd [ + .loop (.det trueExpr) none [("inv_a", mkFvar "a"), ("inv_b", mkFvar "b")] + [.cmd (setCmd "x")] .empty + ]) MetaData.specLoopInvariant == 2 + +/-! ### Loop with decreases measure: specDecreases in metadata -/ + +#guard countField (loopEntryMd [ + .loop (.det trueExpr) (some (mkFvar "n")) [("inv", mkFvar "x")] + [.cmd (setCmd "x")] .empty + ]) MetaData.specDecreases == 1 + +/-! ### Loop with both invariants and decreases -/ + +#guard + let md := loopEntryMd [ + .loop (.det trueExpr) (some (mkFvar "n")) [("inv_a", mkFvar "a"), ("inv_b", mkFvar "b")] + [.cmd (setCmd "x")] .empty + ] + countField md MetaData.specLoopInvariant == 2 && + countField md MetaData.specDecreases == 1 + +/-! ### Loop without contract: no spec metadata in transfer -/ + +#guard + let md := loopEntryMd [ + .loop (.det trueExpr) none [] [.cmd (setCmd "x")] .empty + ] + countField md MetaData.specLoopInvariant == 0 && + countField md MetaData.specDecreases == 0 + +/-! ### Invariant assert commands still emitted (both behaviors coexist) -/ + +#guard + let cfg := toCFG [ + .loop (.det trueExpr) none [("my_inv", mkFvar "x")] + [.cmd (setCmd "x")] .empty + ] + match findLoopEntry cfg with + | some blk => blk.cmds.any (fun cmd => + match cmd with + | .assert label _ _ => label == "my_inv" + | _ => false) + | none => false + +/-! ### Nondet loop guard: contract metadata still present -/ + +#guard + let md := loopEntryMd [ + .loop .nondet (some (mkFvar "n")) [("inv", mkFvar "x")] + [.cmd (setCmd "x")] .empty + ] + countField md MetaData.specLoopInvariant == 1 && + countField md MetaData.specDecreases == 1 + +end diff --git a/editors/emacs/core-st-mode.el b/editors/emacs/core-st-mode.el index f2cffc48e1..7501a1dc53 100644 --- a/editors/emacs/core-st-mode.el +++ b/editors/emacs/core-st-mode.el @@ -8,8 +8,8 @@ '( "var" "assume" "assert" "cover" "if" "else" "havoc" "invariant" "decreases" "while" "out" "inout" "call" "exit" "free" "ensures" "requires" "spec" "procedure" "type" "const" "function" "inline" - "rec" "axiom" "distinct" "datatype" "old" "forall" "exists" - "program")) + "rec" "axiom" "distinct" "datatype" "goto" "cfg" "old" "forall" + "exists" "program")) (defvar core-st-types '( "bool" "int" "string" "regex" "real" "bv1" "bv8" "bv16" "bv32" diff --git a/editors/vscode/syntaxes/core-st.tmLanguage.json b/editors/vscode/syntaxes/core-st.tmLanguage.json index 8a1dd9e289..5084e50e1d 100644 --- a/editors/vscode/syntaxes/core-st.tmLanguage.json +++ b/editors/vscode/syntaxes/core-st.tmLanguage.json @@ -57,7 +57,7 @@ }, "keyword": { "name": "keyword.core-st", - "match": "\\b(var|assume|assert|cover|if|else|havoc|invariant|decreases|while|out|inout|call|exit|free|ensures|requires|spec|procedure|type|const|function|inline|rec|axiom|distinct|datatype|old|forall|exists|program)\\b" + "match": "\\b(var|assume|assert|cover|if|else|havoc|invariant|decreases|while|out|inout|call|exit|free|ensures|requires|spec|procedure|type|const|function|inline|rec|axiom|distinct|datatype|goto|cfg|old|forall|exists|program)\\b" }, "type": { "name": "support.type.core-st",