Add support for unstructured programs

[atomb]

Add Control-Flow Graph (CFG) Support to Imperative Dialect

This PR introduces unstructured control-flow graph representation to the
Imperative dialect, enabling transformation from structured statements to
basic blocks with explicit control flow.

Key Changes

New Core Components:

• BasicBlock.lean - Defines CFG structure with deterministic and non-
  deterministic basic blocks

  • DetTransferCmd - Conditional jumps and finish commands
  • NondetTransferCmd - Non-deterministic goto with multiple targets
  • CFG type - Entry label + labeled blocks

• CFGSemantics.lean - Small-step operational semantics for CFGs

  • EvalDetBlock / EvalNondetBlock - Block evaluation relations
  • StepCFG / StepCFGStar - Single-step and multi-step execution

Transformation:

• StructuredToUnstructured.lean - Converts structured statements to CFGs
  • Handles block, ite, loop, and exit constructs
  • Generates labeled basic blocks with explicit control flow
  • Coalesces contiguous blocks during construction

Testing:

• Extended Exit.lean and Loops.lean tests with CFG generation examples
• Added #guard_msgs tests verifying CFG structure for various programs

Implementation Details

• Basic blocks consist of command lists + transfer command
• Labels are generic (currently String, can be Fin n for total functions)
• Command accumulation during translation minimizes block count
• Exit statements properly resolve to labeled block continuations
• Loop invariants preserved as assertions in loop entry blocks

By submitting this pull request, I confirm that you can use, modify, copy,
and redistribute this contribution, under the terms of your choice.

[tautschnig]

What will be the semantics of jumping into a block while skipping over a declaration? In C one can do:

goto lab;
int x = 42;
lab: ++x; // x is considered declared, but is uninitialised

I believe programs like the above can now be represented, but we also need to be clear on their semantics.

[atomb]

What will be the semantics of jumping into a block while skipping over a declaration? In C one can do:

goto lab;
int x = 42;
lab: ++x; // x is considered declared, but is uninitialised

I believe programs like the above can now be represented, but we also need to be clear on their semantics.

You caught one of the key reasons I hadn't moved this from a draft yet! My current plan is to require that declarations be procedure-level when translating to CFG, but I haven't yet decided how best to enforce that. As you've probably noticed, the example you commented on with the errant comma has an init command in a later block.

[atomb]

What will be the semantics of jumping into a block while skipping over a declaration? In C one can do:

goto lab;
int x = 42;
lab: ++x; // x is considered declared, but is uninitialised

I believe programs like the above can now be represented, but we also need to be clear on their semantics.

On further thought, I'm happy with how the semantics for this work out (as specified in the new CFGSemantics.lean). If you were to do that, evaluation would be stuck, because ++x would be translated into something that would require x to have a value already, and it wouldn't. In a structured program, the type checker won't allow that to happen. If you were to create an unstructured program directly, you could encode the above, and it would have no semantics. We could write a type checker for unstructured programs that would rule out such an issue, too.

[MikaelMayer]

A few things that could make our life easier down the road. My strong recommendation to have only non deterministic blocks since deterministic blocks are a subset of them.

I love to see that there are semantics as well, haven't checked them though.