Blocks, incl. DSL

LeanBoogie/BoogieDsl.lean

@@ -3,6 +3,7 @@ import Std
 import Qq
 -- import LeanBoogie.Boog
 import LeanBoogie.ITree
+import LeanBoogie.ITree.Blocks
 
 namespace Boogie
 open Lean Elab Meta Qq
@@ -19,18 +20,49 @@ open Std (HashSet HashMap)
 structure BoogieElab where
   /-- Mapping of mutable variable names to their ids. Later: Also remember their type. -/
   vars : Std.HashSet Name := {}
+  nextBlockId : Nat := 0
+  /-- Mapping of block name to its internal id. If this is a metavariable, the block is being
+    referred to, but has not been declared. -/
+  blocks : Std.HashMap Name Q(Nat) := {}
 
 abbrev BoogieElabM := StateT BoogieElab TermElabM
 
 def declareVar (x : Name) : BoogieElabM Unit := do
-  if (<- getThe BoogieElab).vars.contains x then
-    throwError "Mutable variable {x} has already been declared"
+  if (<- getThe BoogieElab).vars.contains x then throwError "Mutable variable {x} has already been declared"
+  else modifyThe BoogieElab (fun s => { s with vars := s.vars.insert x })
+
+def allocBlockId : BoogieElabM Nat
+  := modifyGetThe BoogieElab fun st => (st.nextBlockId, {st with nextBlockId := st.nextBlockId + 1})
+
+def needBlock (x : Name) : BoogieElabM Q(Nat) := do
+  if let some id := (<- getThe BoogieElab).blocks.get? x then
+    return q($id)
   else
-    modifyThe BoogieElab (fun s => { s with vars := s.vars.insert x })
+    -- We need this block, but it hasn't been declared yet.
+    let mvar : Q(Nat) <- mkFreshExprMVarQ q(Nat)
+    modifyThe BoogieElab fun st => { st with blocks := st.blocks.insert x mvar}
+    return mvar
+
+def declareBlock (x : Name) : BoogieElabM Nat := do
+  if let some id := (<- getThe BoogieElab).blocks.get? x then
+    let id <- instantiateMVars id
+    if ¬ id.hasMVar then
+      throwError "Duplicate block name {x}"
+    else
+      -- known block, but not declared yet. So instantiate its mvar using `isDefEq`.
+      let freshId : Nat <- allocBlockId
+      if !(<- isDefEq q($freshId) id) then throwError "delcareBlock: bug"
+      return freshId
+  else -- entirely new block
+    let id : Nat <- allocBlockId
+    modifyThe BoogieElab (fun s => { s with blocks := s.blocks.insert x q($id) })
+    return id
 
 -- ## Syntax
 
 section Syntax
+  -- syntax BoogieIdent := ("$" noWs)? ident
+
   declare_syntax_cat BoogieType
   syntax "unit" : BoogieType
   syntax "int" : BoogieType
@@ -64,15 +96,32 @@ section Syntax
   syntax:20 "∀" ident ": " BoogieType ", " BoogieFormula : BoogieFormula
 
   declare_syntax_cat BoogieCommand
-  syntax "var " BoogieVarBinder "; " : BoogieCommand
-  syntax "assume " BoogieFormula "; " : BoogieCommand
   syntax ident " := " BoogieExpr "; " : BoogieCommand
-  syntax "return " BoogieExpr "; " : BoogieCommand
   syntax "if " BoogieExpr " { " BoogieCommand* " }" ("else" " { " BoogieCommand* " }")? : BoogieCommand
   syntax "while " BoogieExpr " { " BoogieCommand* " }" : BoogieCommand
+  -- syntax "var " BoogieVarBinder "; " : BoogieCommand
+  -- syntax "assume " BoogieFormula "; " : BoogieCommand
+  -- syntax "return " BoogieExpr "; " : BoogieCommand
+
+  declare_syntax_cat BoogieAssume
+  syntax "assume " BoogieFormula "; " : BoogieAssume
+  declare_syntax_cat BoogieGoto
+  syntax "goto " ident,+ "; " : BoogieGoto
+  declare_syntax_cat BoogieReturn
+  syntax "return" "; " : BoogieReturn
+
+  declare_syntax_cat BoogieBlock
+  syntax ident ": " BoogieAssume* BoogieCommand* (BoogieGoto <|> BoogieReturn) : BoogieBlock
+
+  declare_syntax_cat BoogieVarCmd
+  syntax "var " BoogieVarBinder "; " : BoogieVarCmd
 
   declare_syntax_cat BoogieProc
-  syntax "procedure " ident "(" BoogieVarBinder,* ")" (" returns " "(" BoogieVarBinder ")")? " { " BoogieCommand* " }" : BoogieProc
+  syntax "procedure " ident "(" BoogieVarBinder,* ")" (" returns " "(" BoogieVarBinder ")")?
+    " { "
+      BoogieVarCmd*
+      BoogieBlock*
+    " }" : BoogieProc
 end Syntax
 
 
@@ -221,6 +270,16 @@ where go
 | stx => throwError "elabBoogieFormula: Unknown syntax {stx}"
 
 mutual
+  partial def elabBoogieAssume : TSyntax `BoogieAssume -> BoogieElabM Q(Mem Unit)
+  | `(BoogieAssume| assume $φ:BoogieFormula; ) => do
+    let vars <- collectMutVarsFormula φ
+    withReadMutVars vars.toList q(Unit) do
+      let φ : Q(Prop) <- elabBoogieFormula φ
+      let _dφ <- synthInstanceQ q(Decidable $φ) -- ! Need `Decidable`, or later: Use events
+      -- have : Q(Bool) := q(@decide $φ $dφ)
+      return q(ITree.assume $φ) -- return q(if $φ then ITree.skip else ITree.spin)
+  | stx => throwError "elabBoogieAssume: Unknown syntax {stx}"
+
   partial def elabBoogieCommands (cmds : TSyntaxArray `BoogieCommand) : BoogieElabM Q(Mem Unit) := do
     cmds.foldlM (fun (acc : Q(Mem Unit)) (cmd : TSyntax _) => do
       let cmd : Q(Mem Unit) <- withRef cmd <| elabBoogieCommand cmd
@@ -235,13 +294,6 @@ mutual
     let cmd : Q(Mem Unit) := q(bind $val (fun val => Mem.set $xStr val))
     -- Term.addTermInfo' stx cmd
     return cmd
-  | `(BoogieCommand| assume $φ:BoogieFormula; ) => do
-    let vars <- collectMutVarsFormula φ
-    withReadMutVars vars.toList q(Unit) do
-      let φ : Q(Prop) <- elabBoogieFormula φ
-      let _dφ <- synthInstanceQ q(Decidable $φ) -- ! Need `Decidable`
-      -- have : Q(Bool) := q(@decide $φ $dφ)
-      return q(ITree.assume $φ) -- return q(if $φ then ITree.skip else ITree.spin)
   | `(BoogieCommand| if $cond { $t* } $[else { $e* }]?) => do
     let cond <- withRef cond <| elabBoogieExpr q(Bool) cond
     let t <- elabBoogieCommands t
@@ -264,15 +316,51 @@ def elabBoogieVarBinder : TSyntax `BoogieVarBinder -> BoogieElabM (Name × Q(Typ
   return (id.getId, ty)
 | stx => throwError "elabBoogieVarBinder: Unknown syntax {stx}"
 
+def elabBoogieVarBinders (binders: TSyntaxArray `BoogieVarBinder) : BoogieElabM (Array <| Name × Q(Type)) := do
+  binders.mapM elabBoogieVarBinder
+
+structure BoogieBlock where
+  assumes : List Q(Prop)
+  code : Q(Mem Unit)
+  gotos : List Nat
+
+def elabBoogieBlock : TSyntax `BoogieBlock -> BoogieElabM Q(Block)
+| `(BoogieBlock| $lbl:ident : $asumes:BoogieAssume* $cmds:BoogieCommand* goto $gotos,* ; ) => do
+  let _blockId <- declareBlock lbl.getId
+  -- TODO: assumes
+  let body : Q(Mem Unit) <- elabBoogieCommands cmds
+  let gotos : Q(List Nat) <- gotos.getElems.foldlM (fun acc g => do
+    let gId : Q(Nat) <- needBlock g.getId
+    return q($gId :: $acc)
+  ) q([])
+  let ret : Q(Mem (List Nat)) := q(bind $body (fun _ => pure $gotos))
+  return ret
+| `(BoogieBlock| $lbl:ident : $asumes:BoogieAssume* $cmds:BoogieCommand* return; ) => do
+  throwError "returns not yet supported, just use an empty goto instead."
+| stx => throwError "elabBoogieBlock: Unknown syntax {stx}"
+
+def List.q {A : Q(Type)} : List Q($A) -> Q(List $A)
+| [] => q([])
+| x :: xs => let xs := q xs; q($x :: $xs)
+
 /-- Elaborate a boogie procedure. Returns the procedure name and its body. -/
 def elabBoogieProc : TSyntax `BoogieProc -> BoogieElabM (String × Q(Mem Unit))
-| `(BoogieProc| procedure $proc ( $binders,* ) $[returns ($retBinder)]? { $body* }) => do
+| `(BoogieProc| procedure $proc ( $binders,* ) $[returns ($retBinder)]? { $vars:BoogieVarCmd* $body:BoogieBlock* }) => do
+  -- vars: parameters
   let binders <- binders.getElems.mapM fun (b : TSyntax _) => withRef b <| do elabBoogieVarBinder b
   binders.forM fun (n, _ty) => declareVar n
+  -- vars: ret var
   if let some retBinder := retBinder then
     let (retVarName, _retVarType) <- withRef retBinder <| elabBoogieVarBinder retBinder
     declareVar retVarName
-  return (proc.getId.toString, <- elabBoogieCommands body)
+  -- TODO leading `var` statements inside proc
+
+  let blocks : Array Q(Block) <- body.mapM elabBoogieBlock
+  if blocks.size = 0 then throwError "Need at least one block."
+  let blocks : Q(List Block) := List.q blocks.toList
+
+  let cfg : Q(Cfg) := q(⟨[], $blocks, 0⟩)
+  return (proc.getId.toString, q(Cfg.run $cfg))
 | stx => throwError "elabBoogieProc: Unknown syntax {stx}"
 
 def runBoogieElab' (m : BoogieElabM A) : TermElabM (A × BoogieElab) := StateT.run m { }
@@ -306,7 +394,14 @@ elab stx:BoogieProc : command => do
       addDecl (.defnDecl decl)
       compileDecl (.defnDecl decl)
 
-procedure foo(x: int) { x := x + 10; }
+procedure foo(x: int) {
+  bb0:
+    x := x + 10;
+    goto bb0, bb1;
+  bb1:
+    y := x + 10;
+    goto bb0;
+}
 
 #check ITree.run foo (fun _ => 0) 10
 -- #eval! ITree.run foo (fun _ => 0) 10

LeanBoogie/ITree/Blocks.lean

@@ -0,0 +1,69 @@
+import LeanBoogie.ITree.ITree
+import LeanBoogie.ITree.Eutt
+import LeanBoogie.ITree.Monad
+import LeanBoogie.ITree.Mem
+import LeanBoogie.Boog
+
+namespace Boogie
+
+/-
+  # Basic, Labels, `goto`
+-/
+
+/-- A block is just an ITree which tells us which next block(s) to jump to.
+  - If returned jump list is empty: This cfg (which is usually a procedure) is done, i.e. `return;`.
+  - If returned jump list has two or more elems: Non-deterministic jump.
+    Currently not supported, and we just pick the first label for now, but eventually we'll
+    implement an oracle to choose the jump label via ITree events. -/
+abbrev Block /- (nBlocks : Nat) (Γ : Vars) -/ : Type
+  := ITree (MemEv /- Γ -/) (List Nat)
+
+/-- Control flow graph. Just a bunch of blocks. -/
+structure Cfg : Type where
+  /-- Which Boogie variables we have. Later: Also store their types. -/
+  vars : List Unit := []
+  blocks : List (Block /- vars -/)
+  -- entry : Fin blocks.length := by exact ⟨0, by rw [List.length]; omega⟩
+  entry : Nat := 0
+
+-- ## Example:
+
+def bb0 : Block := do
+  let i0 <- Mem.get "i0"
+  Mem.set "i1" (i0 == 0).toNat
+  return [1, 2]
+
+def bb1 : Block := do
+  let i1 <- Mem.get "i1"
+  ITree.assume (i1 = 0)
+  return [4]
+
+def myCfg : Cfg := {
+  vars := []
+  blocks := [bb0, bb1]
+}
+
+
+
+-- // Reminder: def iter (body : A -> ITree E (Sum A B)) (a : A) : ITree E B
+-- Reminder: def loop (body : Sum C A -> ITree E (Sum C B)) (a : A) : ITree E B
+/-- Run a bunch of blocks until no jump label is returned anymore.
+  ```lean4
+  let mut l : Label := 0 -- or cfg.entry
+
+  -- Then repeat this:
+  let ls : List Label <- cfg.blocks[l] -- run block
+  if ls.length = 0
+    then return
+    else l := choose lbls
+  ```
+-/
+def Cfg.run (cfg : Cfg) : ITree MemEv Unit :=
+  ITree.iter (A := Nat) (B := Unit) (fun a => do
+    let lbls <- cfg.blocks[a]! -- run block -- ! Panic if label is invalid
+    if h : ¬ lbls.length = 0 then
+      return .inl lbls[0]
+    else
+      return .inr () -- we are done
+  )
+  cfg.entry

LeanBoogie/ITree/ITree.lean

@@ -57,13 +57,31 @@ def tau {E A} (t : ITree E A) : ITree E A := @Internal.ITree.tau Ans E A t
 def vis {E A} (e : E) (k : Ans -> ITree E A) := @Internal.ITree.vis E Ans A e k
 
 abbrev Base E A β := Internal.ITree.Base Ans E A β
+abbrev Base.Uncurried : TypeFun 3 := Internal.ITree.Base.Uncurried Ans
 
 def corec {E A β : Type} (f : β → ITree.Base E A β) (b : β) : ITree E A
   := MvQPF.Cofix.corec (n := 2) (α := (Vec.reverse (Vec.nil.append1 A ::: E))) (F := TypeFun.ofCurried (n := 3) (ITree.Base)) f b
 
 def dest {E A : Type} : ITree E A -> ITree.Base E A (ITree E A)
   := MvQPF.Cofix.dest
 
+/-- Just a convenience function. Re-plays a tree within another tree. -/
+def Base.replay (ta : ITree E A₁) (fTree : ITree E A₁ -> C) (fRet : A₁ -> A₂ := by exact id) : ITree.Base E A₂ C :=
+  match ta.dest with
+  | .ret (a : A₁) => .ret (fRet a)
+  | .tau (t : ITree E A₁) => .tau (fTree t)
+  | .vis e k => .vis e (fun x => fTree (k x))
+
+def _root_.TypeVec.ofList : (l : List Type) -> TypeVec l.length
+| [] => Vec.nil
+| t :: l => TypeVec.ofList l |>.append1 t
+
+def Base.Map (f : C -> D) : TypeVec.Arrow (TypeVec.ofList [C, B, E]) (TypeVec.ofList [D, B, E])
+  := TypeVec.appendFun TypeVec.id f
+
+def Base.Inr : TypeVec.Arrow (TypeVec.ofList [ITree E B, B, E]) (TypeVec.ofList [ITree E A ⊕ ITree E B, B, E])
+  := TypeVec.appendFun TypeVec.id Sum.inr
+
 @[cases_eliminator, elab_as_elim]
 def cases {E A : Type} {motive : ITree E A → Sort u}
     (ret : (r : A) → motive (.ret r))
@@ -101,6 +119,8 @@ def run (t : ITree E A) (f : E -> Ans) : Nat -> (List E) × Option A
     let (evs, ret) := run t f n
     exact (e :: evs, ret)
 
+abbrev KTree (E A B : Type) : Type := A -> ITree E B
+
 -- # Experimentation:
 
 namespace WithSigma