Add Concrete Syntax for Unstructured Programs in Strata Core#1196

Open

PROgram52bc wants to merge 67 commits into

main2from

htd/unstructured-procedure

Commits on May 5, 2026

add CFG to procedure body, no error handling, tests pass
David Deng
committed
eliminate toStmts and use pattern matching/error handling
David Deng
committed

Commits on May 6, 2026

add parser support for user-facing syntax with examples and tests
David Deng
committed
Add TODO comments for two-stage GOTO pipeline refactor
David Deng
committed
add DetCFG abbrev, add obligation extraction and call extraction for DetCFGs
David Deng
committed
refactor ObligationExtraction
David Deng
committed
Address PR review: getCfg, CBMC error, CFG eval, grammar comment
David Deng
committed
integrate semantics for Call statements which could invoke procedures with CFG as body
David Deng
committed
CST support for unstructured programs
David Deng
committed
add explicit comments on funcDecl extraction for unstructured program
David Deng
committed
add ANF comment
David Deng
committed
alphaEquiv for CFG
David Deng
committed
no-op when inlining unstructured procedures
David Deng
committed
add more support for CFG handling
David Deng
committed
simplify StatementEval
David Deng
committed
indent
David Deng
committed
Address PR review: remove .stmts, refine Body interface, cleanup
David Deng
committed

Commits on May 7, 2026

Regenerate editor syntax files for new CFG keywords (goto, cfg)
David Deng
committed
StatementEval returns error on nonexisting label
David Deng
committed
Refine unstructured procedure cases, add comments
David Deng
committed
define variable infrastructures
David Deng
committed
refactor
David Deng
committed
Precond Elim for CFGs
David Deng
committed
add error branch for renameAllLocalNames in ProcedureInlining
David Deng
committed
intermediate proof fix
David Deng
committed
fix proof
David Deng
committed
comment
David Deng
committed
fix WFProcedure
David Deng
committed
restore comments
David Deng
committed
run out of fuel warning
David Deng
committed
better comments on WF
David Deng
committed
error on goto with 2+ targets
David Deng
committed
refine type checker for CFG
David Deng
committed
simplify
David Deng
committed
refine comments
David Deng
committed

Commits on May 11, 2026

fix: propagate error in runCFG fallthrough and clarify ObligationExtraction comment

David Deng
and
claude
committed
test: add end-to-end CFG verification and body preservation tests

David Deng
and
claude
committed
fix: wrap Procedure.body assignment in TerminationCheck.lean for Body type

David Deng
and
claude
committed

Commits on May 12, 2026

fix: split postconditionsValid into structured/CFG fields and add CoreBodyExec TODOs

David Deng
and
claude
committed
refactor: enrich CoreBodyExec with terminal eval and unify postconditionsValid

David Deng
and
claude
committed
Merge branch 'main' into htd/unstructured-procedure
PROgram52bc
authored
implement type checking for CFG
David Deng
committed
Implement symbolic executor for CFG
David Deng
committed
abstract collectCmds
David Deng
committed
add more documentation/better abstraction
David Deng
committed
add metadata to unstructured programs
David Deng
committed
feat: preserve loop contracts in CFG transfer metadata

David Deng
and
claude
committed
fix: split transfer_goto grammar to enforce 1 or 2 targets at parse time

David Deng
and
claude
committed
fix: increment var_def counter when generating nondet goto fvar

David Deng
and
claude
committed
Fix binding bug in CFG Parser
David Deng
committed
fix comments
David Deng
committed
refactor: use Procedure.Body.getStructured instead of raw match

David Deng
and
claude
committed

Commits on May 13, 2026

simplify CFG Eval
David Deng
committed
feat: add CFG-based Core-to-GOTO pipeline alongside direct path

David Deng
and
claude
committed

Commits on May 14, 2026

fix comments
David Deng
committed
Elimiate unnecessary constructor
David Deng
committed
Add PR template warning about repository split (#1166)
atomb
authored

Commits on May 15, 2026

Commits on May 18, 2026