Add support for unstructured programs

Strata/DL/Imperative/BasicBlock.lean

@@ -0,0 +1,120 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.DL.Imperative.MetaData
+import Strata.DL.Imperative.PureExpr
+
+namespace Imperative
+
+/-! # Imperative dialect: unstructured control-flow graphs
+
+A control-flow graph consists of a list of labeled blocks paired with a
+distinguished entry label. Each basic block consists of a label, a list of
+commands, and a transfer command. The types of each of these components are
+parameters, and the type of control flow can be deterministic or
+non-deterministic based on the type of transfer command.
+
+Note: basic block labels could just be `String`, like they are for `Stmt`.
+However, when processing CFGs later, it'll be helpful to be able to create total
+functions over labels, in which case it'll be nice to have `Label` be `Fin n`,
+where `n` is the total number of blocks in the graph.
+-/
+
+
+/-- A `DetTransfer` command terminates a deterministic basic block, indicating
+where execution should proceed next, if anywhere. -/
+inductive DetTransferCmd (Label : Type) (P : PureExpr) where
+  /-- Transfer to `lt` if `p` is true, or `lf` is `p` is false. -/
+  | cgoto (p : P.Expr) (lt lf : Label) (md : MetaData P := .empty)
+  /-- Stop execution of the current unstructured program. If in a procedure
+  body, this can be interpreted as returning to the caller. -/
+  | finish (md : MetaData P := .empty)
+
+/-- For the moment, we don't have an unconditional jump in the language, and
+model it instead using `cgoto`. 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 :=
+  .cgoto HasBool.tt l l
+
+/-- A `NondetTransfer` command terminates a non-deterministic basic block,
+indicating the list of possible blocks where execution could proceed next, if
+anywhere. -/
+inductive NondetTransferCmd (Label : Type) (P : PureExpr) where
+  /-- Transfer to any one of a list of labels, non-deterministically. `goto`
+  with no labels is equivalent to `finish` in `DetTransferCmd` -/
+  | goto (ls : List Label) (md : MetaData P := .empty)
+  deriving Inhabited
+
+def NondetTransferCmd.targets : NondetTransferCmd Label P → List Label
+| .goto ls _ => ls
+
+/-- A basic block consists of a label, a list of body commands, and a transfer
+command that indicates where to go next. It can be deterministic or
+non-deterministic depending on the type of transfer command. -/
+structure BasicBlock (Label TransferCmd Cmd : Type) where
+  label : Label
+  cmds : List Cmd
+  transfer : TransferCmd
+
+def DetBlock (Label Cmd : Type) (P : PureExpr) :=
+  BasicBlock Label (DetTransferCmd Label P) Cmd
+
+def NondetBlock (Label Cmd : Type) (P : PureExpr) :=
+  BasicBlock Label (NondetTransferCmd Label P) Cmd
+
+/-- A control flow graph is a list of blocks paired with a label indicating
+where execution should start. -/
+structure CFG (Label Block : Type) where
+  entry : Label
+  blocks : List Block -- TODO: it would be very nice to have Label → Block
+
+--------
+
+open Std (ToFormat Format format)
+
+def formatDetTransferCmd (P : PureExpr) (c : DetTransferCmd Label P)
+  [ToFormat Label] [ToFormat P.Ident] [ToFormat P.Expr] [ToFormat P.Ty] : Format :=
+  match c with
+  | .cgoto c lt lf md => f!"{md}cgoto {c} {lt} {lf}"
+  | .finish md => f!"{md}finish"
+
+def formatNondetTransferCmd (P : PureExpr) (c : NondetTransferCmd Label P)
+  [ToFormat Label] [ToFormat P.Ident] [ToFormat P.Expr] [ToFormat P.Ty] : Format :=
+  match c with
+  | .goto ls md => f!"{md}goto {ls}"
+
+def formatBasicBlock (b : BasicBlock Label TransferCmd TCmd)
+  [ToFormat Label] [ToFormat TransferCmd] [ToFormat TCmd] : Format :=
+  f!"{b.label}:{Format.line}  {b.cmds}{Format.line}  {b.transfer}"
+
+def formatCFG (cfg : CFG Label Blk)
+  [ToFormat Label] [ToFormat Blk] : Format :=
+  f!"Entry: {cfg.entry}{Format.line}{Format.line}{cfg.blocks}"
+
+instance [ToFormat Label] [ToFormat P.Ident] [ToFormat P.Expr] [ToFormat P.Ty]
+    : ToFormat (DetTransferCmd Label P) where
+  format c := formatDetTransferCmd P c
+
+instance [ToFormat Label] [ToFormat P.Ident] [ToFormat P.Expr] [ToFormat P.Ty]
+    : ToFormat (NondetTransferCmd Label P) where
+  format c := formatNondetTransferCmd P c
+
+instance [ToFormat Label] [ToFormat TransferCmd] [ToFormat TCmd]
+    : ToFormat (BasicBlock Label TransferCmd TCmd) where
+  format b := formatBasicBlock b
+
+instance [ToFormat P.Expr] [ToFormat P.Ident] [ToFormat P.Ty] [ToFormat Label] [ToFormat TCmd]
+    : ToFormat (DetBlock Label TCmd P) where
+  format b := formatBasicBlock b
+
+instance [ToFormat P.Expr] [ToFormat P.Ident] [ToFormat P.Ty] [ToFormat Label] [ToFormat TCmd]
+    : ToFormat (NondetBlock Label TCmd P) where
+  format b := formatBasicBlock b
+
+instance [ToFormat Label] [ToFormat Blk]
+    : ToFormat (CFG Label Blk) where
+  format cfg := formatCFG cfg

Strata/Languages/Boogie/Examples/Loops.lean

@@ -5,6 +5,7 @@
 -/
 
 import Strata.Languages.Boogie.Verifier
+import Strata.Transform.StructuredToUnstructured
 
 ---------------------------------------------------------------------
 namespace Strata
@@ -33,6 +34,39 @@ spec {
 };
 #end
 
+def singleCFG (p : Program) : Imperative.CFG String (Imperative.DetBlock String Boogie.Command Boogie.Expression) :=
+  let boogiePgm := TransM.run (translateProgram p) |>.fst
+  let proc := match boogiePgm.decls.filter (λ d => d.kind = .proc) with | (.proc p) :: _ => p | _ => panic!"No procedure!"
+  Imperative.stmtsToCFG proc.body
+
+/--
+info: Entry: l_6
+
+[l_6:
+   [init (i : int) := init_i_0]
+   cgoto #true l_5 l_5,
+ l_5:
+   [i := #0]
+   cgoto #true l_4 l_4,
+ l_4:
+   [s := #0]
+   cgoto #true loop_entry_1 loop_entry_1,
+ loop_entry_1:
+   [assert [inv] (((~Bool.And : (arrow bool (arrow bool bool))) (((~Bool.And : (arrow bool (arrow bool bool))) (((~Int.Le : (arrow int (arrow int bool))) #0) (i : int))) (((~Int.Le : (arrow int (arrow int bool))) (i : int)) (n : int)))) ((s : int) == (((~Int.Div : (arrow int (arrow int int))) (((~Int.Mul : (arrow int (arrow int int))) (i : int)) (((~Int.Add : (arrow int (arrow int int))) (i : int)) #1))) #2)))]
+   cgoto (((~Int.Lt : (arrow int (arrow int bool))) (i : int)) (n : int)) l_3 end_0,
+ l_3:
+   [i := (((~Int.Add : (arrow int (arrow int int))) (i : int)) #1)]
+   cgoto #true l_2 l_2,
+ l_2:
+   [s := (((~Int.Add : (arrow int (arrow int int))) (s : int)) (i : int))]
+   cgoto #true loop_entry_1 loop_entry_1,
+ end_0:
+   []
+   finish]
+-/
+#guard_msgs in
+#eval (Std.format (singleCFG gaussPgm))
+
 /--
 info: [Strata.Boogie] Type checking succeeded.
 
@@ -109,6 +143,40 @@ spec {
 };
 #end
 
+/--
+info: Entry: l_8
+
+[l_8:
+   [init (x : int) := init_x_0]
+   cgoto #true l_7 l_7,
+ l_7:
+   [init (y : int) := init_y_1]
+   cgoto #true l_6 l_6,
+ l_6:
+   [x := #0]
+   cgoto #true loop_entry_1 loop_entry_1,
+ loop_entry_1:
+   [assert [inv] (((~Bool.And : (arrow bool (arrow bool bool))) (((~Bool.And : (arrow bool (arrow bool bool))) (((~Int.Ge : (arrow int (arrow int bool))) (x : int)) #0)) (((~Int.Le : (arrow int (arrow int bool))) (x : int)) (n : int)))) (((~Int.Lt : (arrow int (arrow int bool))) (n : int)) (~top : int)))]
+   cgoto (((~Int.Lt : (arrow int (arrow int bool))) (x : int)) (n : int)) l_5 end_0,
+ l_5:
+   [y := #0]
+   cgoto #true loop_entry_3 loop_entry_3,
+ loop_entry_3:
+   [assert [inv] (((~Bool.And : (arrow bool (arrow bool bool))) (((~Int.Ge : (arrow int (arrow int bool))) (y : int)) #0)) (((~Int.Le : (arrow int (arrow int bool))) (y : int)) (x : int)))]
+   cgoto (((~Int.Lt : (arrow int (arrow int bool))) (y : int)) (x : int)) l_4 l_2,
+ l_4:
+   [y := (((~Int.Add : (arrow int (arrow int int))) (y : int)) #1)]
+   cgoto #true loop_entry_3 loop_entry_3,
+ l_2:
+   [x := (((~Int.Add : (arrow int (arrow int int))) (x : int)) #1)]
+   cgoto #true loop_entry_1 loop_entry_1,
+ end_0:
+   []
+   finish]
+-/
+#guard_msgs in
+#eval (Std.format (singleCFG nestedPgm))
+
 /--
 info:
 Obligation: entry_invariant_0

Strata/Transform/StructuredToUnstructured.lean

@@ -0,0 +1,85 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.DL.Imperative.PureExpr
+import Strata.DL.Imperative.BasicBlock
+import Strata.DL.Imperative.Cmd
+import Strata.DL.Imperative.Stmt
+import Strata.DL.Lambda.LExpr
+import Strata.DL.Util.LabelGen
+
+namespace Imperative
+
+abbrev DetBlocks (Label CmdT : Type) (P : PureExpr) := List (DetBlock Label CmdT P)
+
+def detCmdBlock [HasBool P] (l : Label) (c : CmdT) (k : Label) :
+  DetBlock Label CmdT P :=
+  { label := l, cmds := [c], transfer := .goto k }
+
+open LabelGen
+
+mutual
+
+/-- Translate a structured statement to an unstructured list of basic blocks
+along with an entry label. -/
+def stmtToBlocks
+  [HasBool P] [HasPassiveCmds P CmdT]
+  (k : String) (s : Stmt P CmdT) :
+  StringGenM (String × DetBlocks String CmdT P) :=
+match s with
+| .cmd c => do
+  let l ← StringGenState.gen "l"
+  -- TODO: this introduces a separate block for every command
+  pure (l, [detCmdBlock l c k])
+| .block l ⟨ bss ⟩  _md => do
+  let (bl, bbs) ← stmtsToBlocks k bss
+  -- TODO: this introduces another unnecessary block
+  let b := { label := l, cmds := [], transfer := .goto bl }
+  pure (l, b :: bbs)
+| .ite c ⟨ tss ⟩ ⟨ fss ⟩ _md => do
+  let l ← StringGenState.gen "ite"
+  let (tl, tbs) ← stmtsToBlocks k tss
+  let (fl, fbs) ← stmtsToBlocks k fss
+  let b := { label := l, cmds := [], transfer := .cgoto c tl fl }
+  pure (l, [b] ++ tbs ++ fbs)
+| .loop c _m i? ⟨ bss ⟩ _md => do
+  let lentry ← StringGenState.gen "loop_entry"
+  let (bl, bbs) ← stmtsToBlocks lentry bss
+  let cmds : List CmdT :=
+    match i? with
+    | .some i => [HasPassiveCmds.assert "inv" i]
+    | .none => []
+  let b := { label := lentry, cmds := cmds, transfer := .cgoto c bl k }
+  pure (lentry, [b] ++ bbs)
+| .goto l _md => pure (l, [])
+
+def stmtsToBlocks
+  [HasBool P] [HasPassiveCmds P CmdT]
+  (k : String) (ss : List (Stmt P CmdT)) :
+  StringGenM (String × DetBlocks String CmdT P) :=
+match ss with
+| [] => pure (k, [])
+| s :: ss => do
+  let (l, bs) ← stmtsToBlocks k ss
+  let (l', bs') ← stmtToBlocks l s
+  pure (l', bs' ++ bs)
+
+end
+
+def stmtsToCFGM
+  [HasBool P] [HasPassiveCmds P CmdT]
+  (ss : List (Stmt P CmdT)) :
+  StringGenM (CFG String (DetBlock String CmdT P)) := do
+  let lend ← StringGenState.gen "end"
+  let bend := { label := lend, cmds := [], transfer := .finish }
+  let (l, bs) ← stmtsToBlocks lend ss
+  pure { entry := l, blocks := bs ++ [bend] }
+
+def stmtsToCFG
+  [HasBool P] [HasPassiveCmds P CmdT]
+  (ss : List (Stmt P CmdT)) :
+  CFG String (DetBlock String CmdT P) :=
+  (stmtsToCFGM ss StringGenState.emp).fst