Add CFG-to-CProverGOTO translation

Strata/Backends/CBMC/GOTO/Instruction.lean

@@ -108,9 +108,13 @@ structure Instruction where
 
 instance : ToString Instruction where
   toString instr :=
-    let code_str := f!" {instr.code}"
+    let payload := match instr.type with
+      | .GOTO => match instr.target with
+        | some t => s!" {t}"
+        | none   => ""
+      | _ => s!" {Std.format instr.code}"
     let guard_str := if Expr.beq instr.guard Expr.true then "" else s!" [{Std.format instr.guard}]"
-    s!"{instr.type}{code_str}{guard_str}"
+    s!"{instr.type}{payload}{guard_str}"
 
 -------------------------------------------------------------------------------
 

Strata/DL/Imperative/CFGToCProverGOTO.lean

@@ -0,0 +1,140 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.DL.Imperative.BasicBlock
+import Strata.DL.Imperative.ToCProverGOTO
+
+/-! # CFG to CProverGOTO Translation
+
+Translates an Imperative dialect CFG (deterministic basic blocks with string
+labels) into a flat array of CProverGOTO instructions.
+
+The existing `Stmt.toGotoInstructions` path translates structured statements
+directly to GOTO instructions, interleaving control-flow lowering (emitting
+conditional jumps, patching forward references) with CBMC-specific concerns
+(source locations, instruction encoding). This module separates those two
+responsibilities: `StructuredToUnstructured.stmtsToCFG` handles the
+control-flow lowering once, producing a backend-agnostic CFG, and this module
+handles only the straightforward mapping from CFG blocks to GOTO instructions.
+
+This separation makes it easier to target additional backends (each only needs
+to consume the CFG) and to reason about the control-flow lowering independently
+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`.
+-/
+
+namespace Imperative
+
+open CProverGOTO
+open Std (Format format)
+
+/-- Translate a deterministic CFG to CProverGOTO instructions.
+
+    The translation processes blocks in the order they appear in `cfg.blocks`.
+    The entry block must appear first; the function returns an error otherwise.
+    For each block:
+    1. Record the current location number as the block's entry point
+    2. Translate each command using `Cmd.toGotoInstructions`
+    3. Translate the transfer command:
+       - `condGoto c lt lf` → GOTO [!c] lf; GOTO lt (conditional + fallthrough)
+       - `finish` → no instruction (handled by END_FUNCTION in the caller)
+
+    After all blocks are emitted, a second pass patches GOTO targets using the
+    label-to-location map built during the first pass.
+-/
+def detCFGToGotoTransform {P} [G : ToGoto P] [BEq P.Ident]
+    (T : P.TyEnv) (functionName : String)
+    (cfg : CFG String (DetBlock String (Cmd P) P))
+    (loc : Nat := 0)
+    (sourceText : Option String := none)
+    : Except Format (GotoTransform P.TyEnv) := do
+  -- Verify the entry block is listed first so that GOTO execution starts at
+  -- the right location. The caller (e.g., CoreToGOTOPipeline) relies on the
+  -- first instruction being the entry point.
+  match cfg.blocks with
+  | (firstLabel, _) :: _ =>
+    if firstLabel != cfg.entry then
+      throw f!"[detCFGToGotoTransform] Entry label '{cfg.entry}' does not match \
+               first block label '{firstLabel}'. The entry block must be listed first."
+  | [] => pure ()
+  -- First pass: emit instructions and build label→locationNum map
+  let mut trans : GotoTransform P.TyEnv :=
+    { instructions := #[], nextLoc := loc, T := T, sourceText := sourceText }
+  -- Pending GOTO patches: (instruction array index, target label)
+  let mut pendingPatches : Array (Nat × String) := #[]
+  let mut labelMap : Std.HashMap String Nat := {}
+  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 =>
+      let cond_expr ← G.toGotoExpr cond
+      -- Emit: GOTO [!cond] lf
+      let (trans', falseIdx) := emitCondGoto (Expr.not cond_expr) srcLoc trans
+      trans := trans'
+      pendingPatches := pendingPatches.push (falseIdx, lf)
+      -- Emit: GOTO lt (unconditional)
+      let (trans', trueIdx) := emitUncondGoto srcLoc 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
+  let mut resolvedPatches : List (Nat × Nat) := []
+  for (idx, label) in pendingPatches do
+    match labelMap[label]? with
+    | some targetLoc => resolvedPatches := (idx, targetLoc) :: resolvedPatches
+    | none =>
+      throw f!"[detCFGToGotoTransform] Unresolved label '{label}' referenced \
+               by GOTO at instruction index {idx}."
+  return patchGotoTargets trans resolvedPatches
+
+end Imperative

StrataTest/Backends/CBMC/GOTO/ToCProverGOTO.lean

@@ -174,9 +174,9 @@ info: ok: #[DECL (decl (x : unsignedbv[32])),
  ASSIGN (assign (x : unsignedbv[32]) (0 : unsignedbv[32])),
  DECL (decl (y : unsignedbv[32])),
  ASSIGN (assign (y : unsignedbv[32]) (0 : unsignedbv[32])),
- GOTO skip [((not(true : bool)) : bool)],
+ GOTO 7 [((not(true : bool)) : bool)],
  ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])),
- GOTO skip,
+ GOTO 9,
  LOCATION skip,
  ASSIGN (assign (y : unsignedbv[32]) (20 : unsignedbv[32])),
  LOCATION skip]
@@ -203,9 +203,9 @@ def ExampleStmt3 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
 info: ok: #[DECL (decl (i : unsignedbv[32])),
  ASSIGN (assign (i : unsignedbv[32]) (0 : unsignedbv[32])),
  LOCATION skip,
- GOTO skip [((not(true : bool)) : bool)],
+ GOTO 6 [((not(true : bool)) : bool)],
  ASSIGN (assign (i : unsignedbv[32]) (((i : unsignedbv[32]) + (1 : unsignedbv[32])) : unsignedbv[32])),
- GOTO skip,
+ GOTO 2,
  LOCATION skip]
 -/
 #guard_msgs in
@@ -229,9 +229,9 @@ def ExampleStmt4 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
 info: ok: #[LOCATION skip,
  DECL (decl (x : unsignedbv[32])),
  ASSIGN (assign (x : unsignedbv[32]) (0 : unsignedbv[32])),
- GOTO skip [((not(true : bool)) : bool)],
+ GOTO 6 [((not(true : bool)) : bool)],
  ASSIGN (assign (x : unsignedbv[32]) (100 : unsignedbv[32])),
- GOTO skip,
+ GOTO 7,
  LOCATION skip,
  LOCATION skip,
  LOCATION skip]
@@ -254,7 +254,7 @@ def ExampleStmt5 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
 /--
 info: ok: #[DECL (decl (x : unsignedbv[32])),
  ASSIGN (assign (x : unsignedbv[32]) (0 : unsignedbv[32])),
- GOTO skip,
+ GOTO 6,
  ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])),
  LOCATION skip,
  ASSIGN (assign (x : unsignedbv[32]) (20 : unsignedbv[32])),
@@ -292,14 +292,14 @@ info: ok: #[DECL (decl (i : unsignedbv[32])),
  DECL (decl (sum : unsignedbv[32])),
  ASSIGN (assign (sum : unsignedbv[32]) (0 : unsignedbv[32])),
  LOCATION skip,
- GOTO skip [((not(true : bool)) : bool)],
- GOTO skip [((not(true : bool)) : bool)],
+ GOTO 13 [((not(true : bool)) : bool)],
+ GOTO 9 [((not(true : bool)) : bool)],
  ASSIGN (assign (sum : unsignedbv[32]) (((sum : unsignedbv[32]) + (i : unsignedbv[32])) : unsignedbv[32])),
- GOTO skip,
+ GOTO 10,
  LOCATION skip,
  LOCATION skip,
  ASSIGN (assign (i : unsignedbv[32]) (((i : unsignedbv[32]) + (1 : unsignedbv[32])) : unsignedbv[32])),
- GOTO skip,
+ GOTO 4,
  LOCATION skip]
 -/
 #guard_msgs in
@@ -354,8 +354,8 @@ def ExampleStmt8 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
 /--
 info: ok: #[DECL (decl (x : unsignedbv[32])),
  ASSIGN (assign (x : unsignedbv[32]) (0 : unsignedbv[32])),
- GOTO skip [((not(true : bool)) : bool)],
- GOTO skip,
+ GOTO 4 [((not(true : bool)) : bool)],
+ GOTO 6,
  LOCATION skip,
  ASSIGN (assign (x : unsignedbv[32]) (100 : unsignedbv[32])),
  LOCATION skip]
@@ -376,7 +376,7 @@ def ExampleStmt9 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
      {}]
 
 /--
-info: ok: #[LOCATION skip, GOTO skip [((not(false : bool)) : bool)], GOTO skip, LOCATION skip]
+info: ok: #[LOCATION skip, GOTO 3 [((not(false : bool)) : bool)], GOTO 0, LOCATION skip]
 -/
 #guard_msgs in
 #eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test9" ExampleStmt9
@@ -398,11 +398,11 @@ def ExampleStmt10 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) :=
 /--
 info: ok: #[DECL (decl (x : unsignedbv[32])),
  ASSIGN (assign (x : unsignedbv[32]) (5 : unsignedbv[32])),
- GOTO skip [((not(true : bool)) : bool)],
+ GOTO 7 [((not(true : bool)) : bool)],
  ASSUME skip,
  ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])),
  ASSERT skip,
- GOTO skip,
+ GOTO 8,
  LOCATION skip,
  LOCATION skip]
 -/
@@ -459,9 +459,9 @@ def ExampleLoopInvariant : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP
 info: ok: #[DECL (decl (i : unsignedbv[32])),
  ASSIGN (assign (i : unsignedbv[32]) (0 : unsignedbv[32])),
  LOCATION skip,
- GOTO skip [((not(true : bool)) : bool)],
+ GOTO 6 [((not(true : bool)) : bool)],
  ASSIGN (assign (i : unsignedbv[32]) (((i : unsignedbv[32]) + (1 : unsignedbv[32])) : unsignedbv[32])),
- GOTO skip,
+ GOTO 2,
  LOCATION skip]
 -/
 #guard_msgs in