From 7b8e91f5ef1eeef8c04bdd6a4eeebc3c5680ca57 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 22 Dec 2025 12:54:58 +0100 Subject: [PATCH 1/4] Extend Cmds.toGotoTransform to handle all Stmt types Extended transformation to handle all `Stmt` constructors (`.block`, `.ite`, `.loop`, `.goto` in addition to `.cmd`, which was already being handled). Ten new tests cover basic, nested, and edge-case scenarios. --- Strata/DL/Imperative/ToCProverGOTO.lean | 232 +++++++++++++++++ StrataTest/Backends/CBMC/ToCProverGOTO.lean | 275 +++++++++++++++++++- 2 files changed, 504 insertions(+), 3 deletions(-) diff --git a/Strata/DL/Imperative/ToCProverGOTO.lean b/Strata/DL/Imperative/ToCProverGOTO.lean index 675c7f1dc..1627a2603 100644 --- a/Strata/DL/Imperative/ToCProverGOTO.lean +++ b/Strata/DL/Imperative/ToCProverGOTO.lean @@ -15,6 +15,8 @@ open Std (ToFormat Format format) namespace Imperative +open CProverGOTO + class ToGoto (P : PureExpr) where -- NOTE: `lookupType` and `updateType` correspond to the functions `lookup` -- and `update` in the `Imperative.TypeContext` class. @@ -129,3 +131,233 @@ def Cmds.toGotoTransform {P} [G: ToGoto P] (T : P.TyEnv) go { instructions := #[], nextLoc := loc, T := T } cs ------------------------------------------------------------------------------- + +/-! ## Imperative's Statements to CProverGOTO's Instructions -/ + +-- Mutual recursion between Stmt.toGotoInstructions and Block.toGotoInstructions: +-- Statements can contain blocks (e.g., in .ite and .loop), and blocks contain statements. +-- This mutual dependency requires both functions to be defined in a mutual block. +mutual + +/-- +Convert an `Imperative.Stmt` to one or more `CProverGOTO.Instruction`s. + +This function handles all statement types including control flow constructs like +blocks, conditionals, and loops. +-/ +def Stmt.toGotoInstructions {P} [G: ToGoto P] + (T : P.TyEnv) (functionName : String) (s : Stmt P (Cmd P)) (trans : GotoTransform P.TyEnv) : + Except Format (GotoTransform P.TyEnv) := do + match s with + | .cmd c => + -- Atomic command - delegate to existing Cmd transformation + Cmd.toGotoInstructions trans.T functionName c trans + + | .block label body _md => + -- Block with label - emit a LOCATION instruction with the label, then process body + let label_inst : Instruction := + { type := .LOCATION, + locationNum := trans.nextLoc, + sourceLoc := { SourceLocation.nil with function := functionName }, + labels := [label], + code := Code.skip } + let trans := { trans with + instructions := trans.instructions.push label_inst, + nextLoc := trans.nextLoc + 1 } + Block.toGotoInstructions trans.T functionName body trans + + | .ite cond thenb elseb _md => + -- Conditional: if cond then thenb else elseb + -- Structure: + -- GOTO [!cond] else_label ; jump to else branch if condition is false + -- + -- GOTO end_label ; skip else branch + -- LOCATION else_label ; else branch starts here + -- + -- LOCATION end_label ; after conditional + + let else_label := s!"else_{trans.nextLoc}" + let end_label := s!"end_if_{trans.nextLoc}" + + -- Negate condition and create conditional GOTO to else branch + let cond_expr ← G.toGotoExpr cond + let neg_cond := Expr.not cond_expr + let goto_else_inst : Instruction := + { type := .GOTO, + locationNum := trans.nextLoc, + sourceLoc := { SourceLocation.nil with function := functionName }, + guard := neg_cond, + target := .none } -- Will be filled with actual location later + + let trans := { trans with + instructions := trans.instructions.push goto_else_inst, + nextLoc := trans.nextLoc + 1 } + let goto_else_loc := trans.nextLoc - 1 -- Remember location of GOTO for patching + + -- Process then branch + let trans ← Block.toGotoInstructions trans.T functionName thenb trans + + -- Add unconditional GOTO to skip else branch + let goto_end_inst : Instruction := + { type := .GOTO, + locationNum := trans.nextLoc, + sourceLoc := { SourceLocation.nil with function := functionName }, + guard := Expr.true, + target := .none } -- Will be filled later + let trans := { trans with + instructions := trans.instructions.push goto_end_inst, + nextLoc := trans.nextLoc + 1 } + let goto_end_loc := trans.nextLoc - 1 -- Remember location for patching + + -- Mark else branch start with LOCATION + let else_loc := trans.nextLoc + let else_label_inst : Instruction := + { type := .LOCATION, + locationNum := else_loc, + sourceLoc := { SourceLocation.nil with function := functionName }, + labels := [else_label], + code := Code.skip } + let trans := { trans with + instructions := trans.instructions.push else_label_inst, + nextLoc := trans.nextLoc + 1 } + + -- Process else branch + let trans ← Block.toGotoInstructions trans.T functionName elseb trans + + -- Mark end of conditional with LOCATION + let end_loc := trans.nextLoc + let end_label_inst : Instruction := + { type := .LOCATION, + locationNum := end_loc, + sourceLoc := { SourceLocation.nil with function := functionName }, + labels := [end_label], + code := Code.skip } + let trans := { trans with + instructions := trans.instructions.push end_label_inst, + nextLoc := trans.nextLoc + 1 } + + -- Patch GOTO targets + let insts := trans.instructions + let insts := insts.set! goto_else_loc + { insts[goto_else_loc]! with target := .some else_loc } + let insts := insts.set! goto_end_loc + { insts[goto_end_loc]! with target := .some end_loc } + + return { trans with instructions := insts } + + | .loop guard _measure _invariant body _md => + -- Loop: while guard do body + -- Structure: + -- LOCATION loop_start ; loop entry point + -- GOTO [!guard] loop_end ; exit loop if guard false + -- + -- GOTO loop_start ; back edge + -- LOCATION loop_end ; after loop + + let loop_start_label := s!"loop_start_{trans.nextLoc}" + let loop_end_label := s!"loop_end_{trans.nextLoc}" + + -- Mark loop start with LOCATION + let loop_start_loc := trans.nextLoc + let loop_start_inst : Instruction := + { type := .LOCATION, + locationNum := loop_start_loc, + sourceLoc := { SourceLocation.nil with function := functionName }, + labels := [loop_start_label], + code := Code.skip } + let trans := { trans with + instructions := trans.instructions.push loop_start_inst, + nextLoc := trans.nextLoc + 1 } + + -- Add conditional GOTO to exit loop + let guard_expr ← G.toGotoExpr guard + let neg_guard := Expr.not guard_expr + let goto_end_inst : Instruction := + { type := .GOTO, + locationNum := trans.nextLoc, + sourceLoc := { SourceLocation.nil with function := functionName }, + guard := neg_guard, + target := .none } -- Will be filled later + let trans := { trans with + instructions := trans.instructions.push goto_end_inst, + nextLoc := trans.nextLoc + 1 } + let goto_end_loc := trans.nextLoc - 1 + + -- Process loop body + let trans ← Block.toGotoInstructions trans.T functionName body trans + + -- Add unconditional GOTO back to loop start + let goto_start_inst : Instruction := + { type := .GOTO, + locationNum := trans.nextLoc, + sourceLoc := { SourceLocation.nil with function := functionName }, + guard := Expr.true, + target := .some loop_start_loc } + let trans := { trans with + instructions := trans.instructions.push goto_start_inst, + nextLoc := trans.nextLoc + 1 } + + -- Mark loop end with LOCATION + let loop_end_loc := trans.nextLoc + let loop_end_inst : Instruction := + { type := .LOCATION, + locationNum := loop_end_loc, + sourceLoc := { SourceLocation.nil with function := functionName }, + labels := [loop_end_label], + code := Code.skip } + let trans := { trans with + instructions := trans.instructions.push loop_end_inst, + nextLoc := trans.nextLoc + 1 } + + -- Patch GOTO to loop end + let insts := trans.instructions + let insts := insts.set! goto_end_loc + { insts[goto_end_loc]! with target := .some loop_end_loc } + + return { trans with instructions := insts } + + | .goto label _md => + -- Goto statement - creates an incomplete GOTO (target will be resolved later) + -- Note: In a full implementation, we would need a second pass to resolve labels + let goto_inst : Instruction := + { type := .INCOMPLETE_GOTO, + locationNum := trans.nextLoc, + sourceLoc := { SourceLocation.nil with function := functionName }, + code := Code.goto label } + return { trans with + instructions := trans.instructions.push goto_inst, + nextLoc := trans.nextLoc + 1, + T := trans.T } +termination_by Stmt.sizeOf s +decreasing_by all_goals sorry + +/-- +Convert a block (list of statements) to GOTO instructions. +-/ +def Block.toGotoInstructions {P} [G: ToGoto P] + (T : P.TyEnv) (functionName : String) (stmts : Block P (Cmd P)) (trans : GotoTransform P.TyEnv) : + Except Format (GotoTransform P.TyEnv) := do + let rec go (trans : GotoTransform P.TyEnv) (stmts' : List (Stmt P (Cmd P))) : + Except Format (GotoTransform P.TyEnv) := + match stmts' with + | [] => .ok trans + | s :: rest => do + let new_trans ← Stmt.toGotoInstructions trans.T functionName s trans + go new_trans rest + termination_by Block.sizeOf stmts' + decreasing_by all_goals simp [*] at * <;> omega + go trans stmts +termination_by Block.sizeOf stmts +decreasing_by all_goals sorry +end + +/-- +Transform a block of statements to a GotoTransform structure. +This is the main entry point for statement transformation. +-/ +def Stmts.toGotoTransform {P} [G: ToGoto P] (T : P.TyEnv) + (functionName : String) (stmts : List (Stmt P (Cmd P))) (loc : Nat := 0) : + Except Format (GotoTransform P.TyEnv) := do + Block.toGotoInstructions T functionName stmts { instructions := #[], nextLoc := loc, T := T } + +------------------------------------------------------------------------------- diff --git a/StrataTest/Backends/CBMC/ToCProverGOTO.lean b/StrataTest/Backends/CBMC/ToCProverGOTO.lean index 4ba14958f..2d54d46bb 100644 --- a/StrataTest/Backends/CBMC/ToCProverGOTO.lean +++ b/StrataTest/Backends/CBMC/ToCProverGOTO.lean @@ -67,7 +67,7 @@ info: ok: #[DECL (decl (s : unsignedbv[32])), ASSIGN (assign (s : unsignedbv[32]) (100 : unsignedbv[32]))] -/ #guard_msgs in -#eval do let ans ← Imperative.Cmds.toGotoTransform Lambda.TEnv.default "one" ExampleProgram1 +#eval! do let ans ← Imperative.Cmds.toGotoTransform Lambda.TEnv.default "one" ExampleProgram1 return format ans.instructions ------------------------------------------------------------------------------- @@ -90,7 +90,7 @@ info: ok: #[DECL (decl (s : unsignedbv[32])), ASSIGN (assign (s : unsignedbv[32]) (((100 : unsignedbv[32]) + (200 : unsignedbv[32])) : unsignedbv[32]))] -/ #guard_msgs in -#eval do let ans ← Imperative.Cmds.toGotoTransform Lambda.TEnv.default "two" ExampleProgram2 +#eval! do let ans ← Imperative.Cmds.toGotoTransform Lambda.TEnv.default "two" ExampleProgram2 return format ans.instructions ------------------------------------------------------------------------------- @@ -115,7 +115,276 @@ info: ok: #[DECL (decl (x : unsignedbv[32])), ASSIGN (assign (z : unsignedbv[32]) (((x : unsignedbv[32]) + (y : unsignedbv[32])) : unsignedbv[32]))] -/ #guard_msgs in -#eval do let ans ← Imperative.Cmds.toGotoTransform Lambda.TEnv.default "three" ExampleProgram3 +#eval! do let ans ← Imperative.Cmds.toGotoTransform Lambda.TEnv.default "three" ExampleProgram3 + return format ans.instructions + +------------------------------------------------------------------------------- + +/-! ## Tests for Statement Transformation -/ + +/-- Test block statement transformation -/ +def ExampleStmt1 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) := + [.block "test_block" + [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10))), + .cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 20)))] + {}] + +/-- +info: ok: #[LOCATION skip, + DECL (decl (x : unsignedbv[32])), + ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])), + ASSIGN (assign (x : unsignedbv[32]) (20 : unsignedbv[32]))] +-/ +#guard_msgs in +#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test1" ExampleStmt1 + return format ans.instructions + +------------------------------------------------------------------------------- + +/-- Test if-then-else (ite) statement transformation -/ +def ExampleStmt2 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) := + [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))), + .cmd (.init (Lambda.Identifier.mk "y" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))), + .ite + (.const { underlying := (), type := mty[bool] } (.boolConst true)) + [.cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10)))] + [.cmd (.set (Lambda.Identifier.mk "y" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 20)))] + {}] + +/-- +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)], + ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])), + GOTO skip, + LOCATION skip, + ASSIGN (assign (y : unsignedbv[32]) (20 : unsignedbv[32])), + LOCATION skip] +-/ +#guard_msgs in +#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test2" ExampleStmt2 + return format ans.instructions + +------------------------------------------------------------------------------- + +/-- Test loop statement transformation -/ +def ExampleStmt3 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) := + [.cmd (.init (Lambda.Identifier.mk "i" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))), + .loop + (.const { underlying := (), type := mty[bool] } (.boolConst true)) + none + none + [.cmd (.set (Lambda.Identifier.mk "i" ()) (addBV32LExpr + (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "i" ()) (some mty[bv32])) + (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 1))))] + {}] + +/-- +info: ok: #[DECL (decl (i : unsignedbv[32])), + ASSIGN (assign (i : unsignedbv[32]) (0 : unsignedbv[32])), + LOCATION skip, + GOTO skip [((not(true : bool)) : bool)], + ASSIGN (assign (i : unsignedbv[32]) (((i : unsignedbv[32]) + (1 : unsignedbv[32])) : unsignedbv[32])), + GOTO skip, + LOCATION skip] +-/ +#guard_msgs in +#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test3" ExampleStmt3 + return format ans.instructions + +------------------------------------------------------------------------------- + +/-- Test nested control flow: if inside block -/ +def ExampleStmt4 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) := + [.block "outer" + [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))), + .ite + (.const { underlying := (), type := mty[bool] } (.boolConst true)) + [.cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 100)))] + [] + {}] + {}] + +/-- +info: ok: #[LOCATION skip, + DECL (decl (x : unsignedbv[32])), + ASSIGN (assign (x : unsignedbv[32]) (0 : unsignedbv[32])), + GOTO skip [((not(true : bool)) : bool)], + ASSIGN (assign (x : unsignedbv[32]) (100 : unsignedbv[32])), + GOTO skip, + LOCATION skip, + LOCATION skip] +-/ +#guard_msgs in +#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test4" ExampleStmt4 + return format ans.instructions + +------------------------------------------------------------------------------- + +/-- Test goto statement transformation -/ +def ExampleStmt5 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) := + [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))), + .goto "target_label" {}, + .cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10))), + .block "target_label" + [.cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 20)))] + {}] + +/-- +info: ok: #[DECL (decl (x : unsignedbv[32])), + ASSIGN (assign (x : unsignedbv[32]) (0 : unsignedbv[32])), + INCOMPLETE_GOTO goto target_label, + ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])), + LOCATION skip, + ASSIGN (assign (x : unsignedbv[32]) (20 : unsignedbv[32]))] +-/ +#guard_msgs in +#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test5" ExampleStmt5 + return format ans.instructions + +------------------------------------------------------------------------------- + +/-- Test complex nested control flow: loop with if inside -/ +def ExampleStmt6 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) := + [.cmd (.init (Lambda.Identifier.mk "i" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))), + .cmd (.init (Lambda.Identifier.mk "sum" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))), + .loop + (.const { underlying := (), type := mty[bool] } (.boolConst true)) + none + none + [.ite + (.const { underlying := (), type := mty[bool] } (.boolConst true)) + [.cmd (.set (Lambda.Identifier.mk "sum" ()) (addBV32LExpr + (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "sum" ()) (some mty[bv32])) + (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "i" ()) (some mty[bv32]))))] + [] + {}, + .cmd (.set (Lambda.Identifier.mk "i" ()) (addBV32LExpr + (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "i" ()) (some mty[bv32])) + (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 1))))] + {}] + +/-- +info: ok: #[DECL (decl (i : unsignedbv[32])), + ASSIGN (assign (i : unsignedbv[32]) (0 : 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)], + ASSIGN (assign (sum : unsignedbv[32]) (((sum : unsignedbv[32]) + (i : unsignedbv[32])) : unsignedbv[32])), + GOTO skip, + LOCATION skip, + LOCATION skip, + ASSIGN (assign (i : unsignedbv[32]) (((i : unsignedbv[32]) + (1 : unsignedbv[32])) : unsignedbv[32])), + GOTO skip, + LOCATION skip] +-/ +#guard_msgs in +#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test6" ExampleStmt6 + return format ans.instructions + +------------------------------------------------------------------------------- + +/-- Test multiple blocks in sequence -/ +def ExampleStmt7 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) := + [.block "block1" + [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10)))] + {}, + .block "block2" + [.cmd (.init (Lambda.Identifier.mk "y" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 20)))] + {}, + .block "block3" + [.cmd (.set (Lambda.Identifier.mk "x" ()) + (addBV32LExpr + (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "x" ()) (some mty[bv32])) + (.fvar { underlying := (), type := mty[bv32] } (Lambda.Identifier.mk "y" ()) (some mty[bv32]))))] + {}] + +/-- +info: ok: #[LOCATION skip, + DECL (decl (x : unsignedbv[32])), + ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])), + LOCATION skip, + DECL (decl (y : unsignedbv[32])), + ASSIGN (assign (y : unsignedbv[32]) (20 : unsignedbv[32])), + LOCATION skip, + ASSIGN (assign (x : unsignedbv[32]) (((x : unsignedbv[32]) + (y : unsignedbv[32])) : unsignedbv[32]))] +-/ +#guard_msgs in +#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test7" ExampleStmt7 + return format ans.instructions + +------------------------------------------------------------------------------- + +/-- Test empty branches in if-then-else -/ +def ExampleStmt8 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) := + [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 0))), + .ite + (.const { underlying := (), type := mty[bool] } (.boolConst true)) + [] + [.cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 100)))] + {}] + +/-- +info: ok: #[DECL (decl (x : unsignedbv[32])), + ASSIGN (assign (x : unsignedbv[32]) (0 : unsignedbv[32])), + GOTO skip [((not(true : bool)) : bool)], + GOTO skip, + LOCATION skip, + ASSIGN (assign (x : unsignedbv[32]) (100 : unsignedbv[32])), + LOCATION skip] +-/ +#guard_msgs in +#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test8" ExampleStmt8 + return format ans.instructions + +------------------------------------------------------------------------------- + +/-- Test loop with empty body -/ +def ExampleStmt9 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) := + [.loop + (.const { underlying := (), type := mty[bool] } (.boolConst false)) + none + none + [] + {}] + +/-- +info: ok: #[LOCATION skip, GOTO skip [((not(false : bool)) : bool)], GOTO skip, LOCATION skip] +-/ +#guard_msgs in +#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test9" ExampleStmt9 + return format ans.instructions + +------------------------------------------------------------------------------- + +/-- Test assertions and assumptions within control flow -/ +def ExampleStmt10 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) := + [.cmd (.init (Lambda.Identifier.mk "x" ()) mty[bv32] (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 5))), + .ite + (.const { underlying := (), type := mty[bool] } (.boolConst true)) + [.cmd (.assume "precond" (.const { underlying := (), type := mty[bool] } (.boolConst true))), + .cmd (.set (Lambda.Identifier.mk "x" ()) (.const { underlying := (), type := mty[bv32] } (.bitvecConst 32 10))), + .cmd (.assert "postcond" (.const { underlying := (), type := mty[bool] } (.boolConst true)))] + [] + {}] + +/-- +info: ok: #[DECL (decl (x : unsignedbv[32])), + ASSIGN (assign (x : unsignedbv[32]) (5 : unsignedbv[32])), + GOTO skip [((not(true : bool)) : bool)], + ASSUME skip, + ASSIGN (assign (x : unsignedbv[32]) (10 : unsignedbv[32])), + ASSERT skip, + GOTO skip, + LOCATION skip, + LOCATION skip] +-/ +#guard_msgs in +#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test10" ExampleStmt10 return format ans.instructions ------------------------------------------------------------------------------- From 79613eae1fe48625e24c547945002872f59ae95a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 22 Dec 2025 22:29:44 +0100 Subject: [PATCH 2/4] Address some comments --- Strata/DL/Imperative/ToCProverGOTO.lean | 134 ++++++++++-------------- 1 file changed, 57 insertions(+), 77 deletions(-) diff --git a/Strata/DL/Imperative/ToCProverGOTO.lean b/Strata/DL/Imperative/ToCProverGOTO.lean index 1627a2603..f7869c877 100644 --- a/Strata/DL/Imperative/ToCProverGOTO.lean +++ b/Strata/DL/Imperative/ToCProverGOTO.lean @@ -134,9 +134,11 @@ def Cmds.toGotoTransform {P} [G: ToGoto P] (T : P.TyEnv) /-! ## Imperative's Statements to CProverGOTO's Instructions -/ --- Mutual recursion between Stmt.toGotoInstructions and Block.toGotoInstructions: --- Statements can contain blocks (e.g., in .ite and .loop), and blocks contain statements. --- This mutual dependency requires both functions to be defined in a mutual block. +/- +Mutual recursion between Stmt.toGotoInstructions and Block.toGotoInstructions: +Statements can contain blocks (e.g., in .ite and .loop), and blocks contain statements. +This mutual dependency requires both functions to be defined in a mutual block. +-/ mutual /-- @@ -167,56 +169,50 @@ def Stmt.toGotoInstructions {P} [G: ToGoto P] Block.toGotoInstructions trans.T functionName body trans | .ite cond thenb elseb _md => - -- Conditional: if cond then thenb else elseb - -- Structure: - -- GOTO [!cond] else_label ; jump to else branch if condition is false - -- - -- GOTO end_label ; skip else branch - -- LOCATION else_label ; else branch starts here - -- - -- LOCATION end_label ; after conditional - + /- + Conditional: if cond then thenb else elseb + Structure: + GOTO [!cond] else_label ; jump to else branch if condition is false + + GOTO end_label ; skip else branch + LOCATION else_label ; else branch starts here + + LOCATION end_label ; after conditional + -/ let else_label := s!"else_{trans.nextLoc}" let end_label := s!"end_if_{trans.nextLoc}" - -- Negate condition and create conditional GOTO to else branch + -- Emit conditional GOTO to else branch let cond_expr ← G.toGotoExpr cond let neg_cond := Expr.not cond_expr let goto_else_inst : Instruction := - { type := .GOTO, - locationNum := trans.nextLoc, + { type := .GOTO, locationNum := trans.nextLoc, sourceLoc := { SourceLocation.nil with function := functionName }, - guard := neg_cond, - target := .none } -- Will be filled with actual location later - + guard := neg_cond, target := .none } let trans := { trans with instructions := trans.instructions.push goto_else_inst, nextLoc := trans.nextLoc + 1 } - let goto_else_loc := trans.nextLoc - 1 -- Remember location of GOTO for patching + let goto_else_loc := trans.nextLoc - 1 -- Process then branch let trans ← Block.toGotoInstructions trans.T functionName thenb trans - -- Add unconditional GOTO to skip else branch + -- Emit unconditional GOTO to end let goto_end_inst : Instruction := - { type := .GOTO, - locationNum := trans.nextLoc, + { type := .GOTO, locationNum := trans.nextLoc, sourceLoc := { SourceLocation.nil with function := functionName }, - guard := Expr.true, - target := .none } -- Will be filled later + guard := Expr.true, target := .none } let trans := { trans with instructions := trans.instructions.push goto_end_inst, nextLoc := trans.nextLoc + 1 } - let goto_end_loc := trans.nextLoc - 1 -- Remember location for patching + let goto_end_loc := trans.nextLoc - 1 - -- Mark else branch start with LOCATION + -- Emit else branch label let else_loc := trans.nextLoc let else_label_inst : Instruction := - { type := .LOCATION, - locationNum := else_loc, + { type := .LOCATION, locationNum := else_loc, sourceLoc := { SourceLocation.nil with function := functionName }, - labels := [else_label], - code := Code.skip } + labels := [else_label], code := Code.skip } let trans := { trans with instructions := trans.instructions.push else_label_inst, nextLoc := trans.nextLoc + 1 } @@ -224,14 +220,12 @@ def Stmt.toGotoInstructions {P} [G: ToGoto P] -- Process else branch let trans ← Block.toGotoInstructions trans.T functionName elseb trans - -- Mark end of conditional with LOCATION + -- Emit end label let end_loc := trans.nextLoc let end_label_inst : Instruction := - { type := .LOCATION, - locationNum := end_loc, + { type := .LOCATION, locationNum := end_loc, sourceLoc := { SourceLocation.nil with function := functionName }, - labels := [end_label], - code := Code.skip } + labels := [end_label], code := Code.skip } let trans := { trans with instructions := trans.instructions.push end_label_inst, nextLoc := trans.nextLoc + 1 } @@ -242,42 +236,38 @@ def Stmt.toGotoInstructions {P} [G: ToGoto P] { insts[goto_else_loc]! with target := .some else_loc } let insts := insts.set! goto_end_loc { insts[goto_end_loc]! with target := .some end_loc } - return { trans with instructions := insts } | .loop guard _measure _invariant body _md => - -- Loop: while guard do body - -- Structure: - -- LOCATION loop_start ; loop entry point - -- GOTO [!guard] loop_end ; exit loop if guard false - -- - -- GOTO loop_start ; back edge - -- LOCATION loop_end ; after loop - + /- + Loop: while guard do body + Structure: + LOCATION loop_start ; loop entry point + GOTO [!guard] loop_end ; exit loop if guard false + + GOTO loop_start ; back edge + LOCATION loop_end ; after loop + -/ let loop_start_label := s!"loop_start_{trans.nextLoc}" let loop_end_label := s!"loop_end_{trans.nextLoc}" - -- Mark loop start with LOCATION + -- Emit loop start label let loop_start_loc := trans.nextLoc let loop_start_inst : Instruction := - { type := .LOCATION, - locationNum := loop_start_loc, + { type := .LOCATION, locationNum := loop_start_loc, sourceLoc := { SourceLocation.nil with function := functionName }, - labels := [loop_start_label], - code := Code.skip } + labels := [loop_start_label], code := Code.skip } let trans := { trans with instructions := trans.instructions.push loop_start_inst, nextLoc := trans.nextLoc + 1 } - -- Add conditional GOTO to exit loop + -- Emit conditional GOTO to exit loop let guard_expr ← G.toGotoExpr guard let neg_guard := Expr.not guard_expr let goto_end_inst : Instruction := - { type := .GOTO, - locationNum := trans.nextLoc, + { type := .GOTO, locationNum := trans.nextLoc, sourceLoc := { SourceLocation.nil with function := functionName }, - guard := neg_guard, - target := .none } -- Will be filled later + guard := neg_guard, target := .none } let trans := { trans with instructions := trans.instructions.push goto_end_inst, nextLoc := trans.nextLoc + 1 } @@ -286,25 +276,21 @@ def Stmt.toGotoInstructions {P} [G: ToGoto P] -- Process loop body let trans ← Block.toGotoInstructions trans.T functionName body trans - -- Add unconditional GOTO back to loop start + -- Emit unconditional GOTO back to loop start let goto_start_inst : Instruction := - { type := .GOTO, - locationNum := trans.nextLoc, + { type := .GOTO, locationNum := trans.nextLoc, sourceLoc := { SourceLocation.nil with function := functionName }, - guard := Expr.true, - target := .some loop_start_loc } + guard := Expr.true, target := .some loop_start_loc } let trans := { trans with instructions := trans.instructions.push goto_start_inst, nextLoc := trans.nextLoc + 1 } - -- Mark loop end with LOCATION + -- Emit loop end label let loop_end_loc := trans.nextLoc let loop_end_inst : Instruction := - { type := .LOCATION, - locationNum := loop_end_loc, + { type := .LOCATION, locationNum := loop_end_loc, sourceLoc := { SourceLocation.nil with function := functionName }, - labels := [loop_end_label], - code := Code.skip } + labels := [loop_end_label], code := Code.skip } let trans := { trans with instructions := trans.instructions.push loop_end_inst, nextLoc := trans.nextLoc + 1 } @@ -313,7 +299,6 @@ def Stmt.toGotoInstructions {P} [G: ToGoto P] let insts := trans.instructions let insts := insts.set! goto_end_loc { insts[goto_end_loc]! with target := .some loop_end_loc } - return { trans with instructions := insts } | .goto label _md => @@ -329,7 +314,7 @@ def Stmt.toGotoInstructions {P} [G: ToGoto P] nextLoc := trans.nextLoc + 1, T := trans.T } termination_by Stmt.sizeOf s -decreasing_by all_goals sorry +decreasing_by all_goals simp [*] at * <;> omega /-- Convert a block (list of statements) to GOTO instructions. @@ -337,18 +322,13 @@ Convert a block (list of statements) to GOTO instructions. def Block.toGotoInstructions {P} [G: ToGoto P] (T : P.TyEnv) (functionName : String) (stmts : Block P (Cmd P)) (trans : GotoTransform P.TyEnv) : Except Format (GotoTransform P.TyEnv) := do - let rec go (trans : GotoTransform P.TyEnv) (stmts' : List (Stmt P (Cmd P))) : - Except Format (GotoTransform P.TyEnv) := - match stmts' with - | [] => .ok trans - | s :: rest => do - let new_trans ← Stmt.toGotoInstructions trans.T functionName s trans - go new_trans rest - termination_by Block.sizeOf stmts' - decreasing_by all_goals simp [*] at * <;> omega - go trans stmts + match stmts with + | [] => return trans + | s :: rest => do + let new_trans ← Stmt.toGotoInstructions T functionName s trans + Block.toGotoInstructions T functionName rest new_trans termination_by Block.sizeOf stmts -decreasing_by all_goals sorry +decreasing_by all_goals simp [*] at * <;> omega end /-- From 6d3d2a4ccb28c6ff200d727bfc756a3c8f094989 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 22 Dec 2025 22:32:17 +0100 Subject: [PATCH 3/4] eval! no longer needed --- StrataTest/Backends/CBMC/ToCProverGOTO.lean | 26 ++++++++++----------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/StrataTest/Backends/CBMC/ToCProverGOTO.lean b/StrataTest/Backends/CBMC/ToCProverGOTO.lean index 2d54d46bb..470b9ea90 100644 --- a/StrataTest/Backends/CBMC/ToCProverGOTO.lean +++ b/StrataTest/Backends/CBMC/ToCProverGOTO.lean @@ -67,7 +67,7 @@ info: ok: #[DECL (decl (s : unsignedbv[32])), ASSIGN (assign (s : unsignedbv[32]) (100 : unsignedbv[32]))] -/ #guard_msgs in -#eval! do let ans ← Imperative.Cmds.toGotoTransform Lambda.TEnv.default "one" ExampleProgram1 +#eval do let ans ← Imperative.Cmds.toGotoTransform Lambda.TEnv.default "one" ExampleProgram1 return format ans.instructions ------------------------------------------------------------------------------- @@ -90,7 +90,7 @@ info: ok: #[DECL (decl (s : unsignedbv[32])), ASSIGN (assign (s : unsignedbv[32]) (((100 : unsignedbv[32]) + (200 : unsignedbv[32])) : unsignedbv[32]))] -/ #guard_msgs in -#eval! do let ans ← Imperative.Cmds.toGotoTransform Lambda.TEnv.default "two" ExampleProgram2 +#eval do let ans ← Imperative.Cmds.toGotoTransform Lambda.TEnv.default "two" ExampleProgram2 return format ans.instructions ------------------------------------------------------------------------------- @@ -115,7 +115,7 @@ info: ok: #[DECL (decl (x : unsignedbv[32])), ASSIGN (assign (z : unsignedbv[32]) (((x : unsignedbv[32]) + (y : unsignedbv[32])) : unsignedbv[32]))] -/ #guard_msgs in -#eval! do let ans ← Imperative.Cmds.toGotoTransform Lambda.TEnv.default "three" ExampleProgram3 +#eval do let ans ← Imperative.Cmds.toGotoTransform Lambda.TEnv.default "three" ExampleProgram3 return format ans.instructions ------------------------------------------------------------------------------- @@ -136,7 +136,7 @@ info: ok: #[LOCATION skip, ASSIGN (assign (x : unsignedbv[32]) (20 : unsignedbv[32]))] -/ #guard_msgs in -#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test1" ExampleStmt1 +#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test1" ExampleStmt1 return format ans.instructions ------------------------------------------------------------------------------- @@ -164,7 +164,7 @@ info: ok: #[DECL (decl (x : unsignedbv[32])), LOCATION skip] -/ #guard_msgs in -#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test2" ExampleStmt2 +#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test2" ExampleStmt2 return format ans.instructions ------------------------------------------------------------------------------- @@ -191,7 +191,7 @@ info: ok: #[DECL (decl (i : unsignedbv[32])), LOCATION skip] -/ #guard_msgs in -#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test3" ExampleStmt3 +#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test3" ExampleStmt3 return format ans.instructions ------------------------------------------------------------------------------- @@ -218,7 +218,7 @@ info: ok: #[LOCATION skip, LOCATION skip] -/ #guard_msgs in -#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test4" ExampleStmt4 +#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test4" ExampleStmt4 return format ans.instructions ------------------------------------------------------------------------------- @@ -241,7 +241,7 @@ info: ok: #[DECL (decl (x : unsignedbv[32])), ASSIGN (assign (x : unsignedbv[32]) (20 : unsignedbv[32]))] -/ #guard_msgs in -#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test5" ExampleStmt5 +#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test5" ExampleStmt5 return format ans.instructions ------------------------------------------------------------------------------- @@ -283,7 +283,7 @@ info: ok: #[DECL (decl (i : unsignedbv[32])), LOCATION skip] -/ #guard_msgs in -#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test6" ExampleStmt6 +#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test6" ExampleStmt6 return format ans.instructions ------------------------------------------------------------------------------- @@ -314,7 +314,7 @@ info: ok: #[LOCATION skip, ASSIGN (assign (x : unsignedbv[32]) (((x : unsignedbv[32]) + (y : unsignedbv[32])) : unsignedbv[32]))] -/ #guard_msgs in -#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test7" ExampleStmt7 +#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test7" ExampleStmt7 return format ans.instructions ------------------------------------------------------------------------------- @@ -338,7 +338,7 @@ info: ok: #[DECL (decl (x : unsignedbv[32])), LOCATION skip] -/ #guard_msgs in -#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test8" ExampleStmt8 +#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test8" ExampleStmt8 return format ans.instructions ------------------------------------------------------------------------------- @@ -356,7 +356,7 @@ def ExampleStmt9 : List (Imperative.Stmt LExprTP (Imperative.Cmd LExprTP)) := info: ok: #[LOCATION skip, GOTO skip [((not(false : bool)) : bool)], GOTO skip, LOCATION skip] -/ #guard_msgs in -#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test9" ExampleStmt9 +#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test9" ExampleStmt9 return format ans.instructions ------------------------------------------------------------------------------- @@ -384,7 +384,7 @@ info: ok: #[DECL (decl (x : unsignedbv[32])), LOCATION skip] -/ #guard_msgs in -#eval! do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test10" ExampleStmt10 +#eval do let ans ← Imperative.Stmts.toGotoTransform Lambda.TEnv.default "test10" ExampleStmt10 return format ans.instructions ------------------------------------------------------------------------------- From 2289ae77cd247f2b7a4b91cfce22b6b50fb2e893 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Jan 2026 12:20:53 +0100 Subject: [PATCH 4/4] Update Strata/DL/Imperative/ToCProverGOTO.lean Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com> --- Strata/DL/Imperative/ToCProverGOTO.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Strata/DL/Imperative/ToCProverGOTO.lean b/Strata/DL/Imperative/ToCProverGOTO.lean index f7869c877..807eabdfe 100644 --- a/Strata/DL/Imperative/ToCProverGOTO.lean +++ b/Strata/DL/Imperative/ToCProverGOTO.lean @@ -311,8 +311,7 @@ def Stmt.toGotoInstructions {P} [G: ToGoto P] code := Code.goto label } return { trans with instructions := trans.instructions.push goto_inst, - nextLoc := trans.nextLoc + 1, - T := trans.T } + nextLoc := trans.nextLoc + 1 } termination_by Stmt.sizeOf s decreasing_by all_goals simp [*] at * <;> omega