Regalloc single bb

SSA.lean

@@ -20,6 +20,7 @@ import SSA.Projects.DCE.DCE
 import SSA.Projects.CSE.CSE
 import SSA.Projects.PaperExamples.PaperExamples
 import SSA.Projects.Scf.ScfFunctor
+import SSA.Projects.Regalloc.Regalloc
 import SSA.Projects.LeanMlirCommon.LeanMlirCommon
 
 

SSA/Core/ErasedContext.lean

@@ -119,6 +119,24 @@ theorem succ_eq_toSnoc {Γ : Ctxt Ty} {t : Ty} {w} (h : (Γ.snoc t).get? (w+1) =
     ⟨w+1, h⟩ = toSnoc ⟨w, h⟩ :=
   rfl
 
+@[simp]
+theorem Ctxt.Var.toSnoc_neq_last {Γ : Ctxt Ty} {t : Ty} {v : Γ.Var t} :
+    v.toSnoc ≠ Ctxt.Var.last Γ t := by
+  unfold Ctxt.Var.toSnoc Ctxt.Var.last
+  rcases v with ⟨v, hv⟩
+  simp only []
+  have heq : v + 1 ≠ 0 := by omega
+  simp [heq]
+  intros hcontra
+  unfold last at hcontra
+  obtain ⟨h₁, h₂⟩ := hcontra
+
+@[simp]
+theorem Ctxt.Var.last_neq_toSnoc {Γ : Ctxt Ty} {t : Ty} {v : Γ.Var t} :
+    Ctxt.Var.last Γ t ≠ v.toSnoc := by
+  symm
+  simp
+
 /-- Transport a variable from `Γ` to any mapped context `Γ.map f` -/
 def toMap : Var Γ t → Var (Γ.map f) (f t)
   | ⟨i, h⟩ => ⟨i, by
@@ -401,9 +419,45 @@ theorem Valuation.reassignVar_eq_of_lookup [DecidableEq Ty]
   subst x
   rfl
 
-
 end Valuation
 
+section CoValuation
+
+variable [TyDenote Ty]
+
+/-- A Covaluation for a context. Provide a value for some type in the context. -/
+structure CoValuation (Γ : Ctxt Ty) where
+  t : Ty
+  var : Γ.Var t
+  val : toType t
+
+/-- Eliminate a CoValuation of an empty context. -/
+@[simp]
+def CoValuation.elim_nil (V : CoValuation (∅ : Ctxt Ty)) : False :=
+  V.var.emptyElim
+
+/-- Build a covaluation for a single type context. -/
+def CoValuation.singleton (t : Ty) (v : toType t) : CoValuation [t] :=
+  ⟨t, Var.last _ _, v⟩
+
+/-- Build a CoValuation from a variable and a value. -/
+def CoValuation.ofVar {Γ : Ctxt Ty} (v : Γ.Var α) (a : toType α) : CoValuation Γ :=
+  ⟨α, v, a⟩
+
+/-- transport/pullback a valuation along a context homomorphism. -/
+def CoValuation.comap {Γi Γo : Ctxt Ty} (Γiv: Γi.CoValuation) (hom : Ctxt.Hom Γi Γo) : Γo.CoValuation where
+  t := Γiv.t
+  var := hom Γiv.var
+  val := Γiv.val
+
+  -- fun _to vo => Γiv (hom vo)
+
+/-
+TODO: write helpers to coerce to a from a value of 'toType Γ.Var α'.
+We suspect that this will come up when reasoning about straight line code.
+-/
+
+end CoValuation
 
 /- ## VarSet -/
 

SSA/Core/Framework.lean

@@ -153,7 +153,6 @@ inductive Expr : (Γ : Ctxt d.Ty) → (eff : EffectKind) → (ty : d.Ty) → Typ
     (regArgs : HVector (fun t : Ctxt d.Ty × d.Ty => Com t.1 .impure t.2)
       (DialectSignature.regSig op)) : Expr Γ eff ty
 
-
 /-- A very simple intrinsically typed program: a sequence of let bindings.
 Note that the `EffectKind` is uniform: if a `Com` is `pure`, then the expression and its body are pure,
 and if a `Com` is `impure`, then both the expression and the body are impure!
@@ -2598,3 +2597,18 @@ def Expr.ty : Expr d Γ eff t → d.Ty := fun _ => t
 def Expr.ctxt : Expr d Γ eff t → Ctxt d.Ty := fun _ => Γ
 
 end TypeProjections
+
+section FlatComReprInstance
+/-!
+## Repr instance to convert a FlatCom into a zipper.
+-/
+
+/-- Convert a `FlatCom` to a `Zipper` that is at the end of the `FlatCom` -/
+def FlatCom.toZipperAtRet {Γ : Ctxt d.Ty} {eff : EffectKind} {t : d.Ty}
+    (fc : FlatCom d Γ eff Δ t) : Zipper d Γ eff Δ t := ⟨fc.lets, Com.ret fc.ret⟩
+
+instance [DialectSignature d] [Repr d.Op] [Repr d.Ty] :
+    Repr (FlatCom d Γ eff Γ_out ty) where
+  reprPrec flatCom n := reprPrec flatCom.toZipperAtRet.toCom n
+
+end FlatComReprInstance

SSA/Projects/Regalloc/Chordal.lean

@@ -0,0 +1,26 @@
+/-
+Properties of chordal graphs.
+Proof that a chordal graphs possess a perfect eliminiation ordering.
+This implies that greedy coloring is optimal for chordal graphs.
+We also provide easy lemmas that make the fact that
+the interference graph of a SSA program is chordal.
+
+References:
+- https://compilers.cs.uni-saarland.de/projects/ssara/
+- Optimal register allocation for SSA form programs in polytime:
+    https://www.sciencedirect.com/science/article/pii/S0020019006000196?via%3Dihub
+ -/
+
+ /-
+ TODO: think if this can be written abstractly in terms
+ of a matroid?
+ -/
+import Mathlib.Combinatorics.SimpleGraph.Basic
+import Mathlib.Combinatorics.SimpleGraph.Coloring
+import Mathlib.Combinatorics.SimpleGraph.Finite
+import Mathlib.Combinatorics.SimpleGraph.Operations
+import Mathlib.Combinatorics.SimpleGraph.Maps
+import Mathlib.Combinatorics.SimpleGraph.IncMatrix
+import Mathlib.Data.Matroid.Basic
+import Mathlib.Data.Matroid.IndepAxioms
+import Mathlib.Combinatorics.SimpleGraph.Acyclic -- dominator tree.

SSA/Projects/Regalloc/Regalloc.lean

@@ -0,0 +1,3 @@
+import SSA.Projects.Regalloc.RegallocSingleBB
+import SSA.Projects.Regalloc.Chordal
+-- import SSA.Projects.Regalloc.RegallocMultipleBB

SSA/Projects/Regalloc/RegallocMultipleBB.lean

@@ -0,0 +1,137 @@
+import Init.Data.BitVec.Basic
+import Init.Data.BitVec.Lemmas
+import Init.Data.BitVec.Bitblast
+
+-- 1) RegionTree in Polly, from our work in Polly:
+-- 2) https://github.com/llvm/llvm-project/blob/7b08c2774ca7350b372f70f63135eacc04d739c5/llvm/include/llvm/Analysis/RegionInfo.h#L9-L22
+--      Which is, in turn, based on the program structure Tree: https://en.wikipedia.org/wiki/Program_structure_tree
+-- 3) LLVM's functional API for BB utils,
+--     which we shall provide as a surface level API https://llvm.org/doxygen/BasicBlockUtils_8h.html
+-- import SSA.Core.Framework
+import Lean.Data.HashMap
+import Mathlib.Init.Function
+import Mathlib.CategoryTheory.Category.Basic
+
+import SSA.Core.ErasedContext
+import SSA.Core.HVector
+import SSA.Core.EffectKind
+import Mathlib.Control.Monad.Basic
+import SSA.Core.Framework.Dialect
+import Mathlib.Data.List.AList
+import Mathlib.Data.Finset.Piecewise
+
+open Ctxt (Var VarSet Valuation)
+open TyDenote (toType)
+
+namespace Pure
+
+variable [TyDenote Ty]
+
+/-- A simple term, consisting of variables, operations, pairs, units, and booleans -/
+inductive Term (Γ : Ctxt Ty) : Ty → Type where
+  | var : {α : Ty} → (v : Γ.Var α) → Term Γ α
+  | val : {α : Ty} → (v : toType α) → Term Γ α
+  -- | op : φ → Term φ → Term φ
+  -- | let1 : Term φ → Term φ → Term φ
+  -- | pair : Term φ → Term φ → Term φ
+  -- | unit : Term φ
+  -- | let2 : Term φ → Term φ → Term φ
+  -- | inl : Term φ → Term φ
+  -- | inr : Term φ → Term φ
+  -- | case: Term φ → Term φ → Term φ → Term φ
+  -- | abort : Term φ → Term φ
+
+-- inductive Wf : Ctx α ε → Region φ → LCtx α → Prop
+--   | br : L.Trg n A → a.Wf Γ ⟨A, ⊥⟩ → Wf Γ (br n a) L
+--   | case : a.Wf Γ ⟨Ty.coprod A B, e⟩
+--     → s.Wf (⟨A, ⊥⟩::Γ) L
+--     → t.Wf (⟨B, ⊥⟩::Γ) L
+--     → Wf Γ (case a s t) L
+--   | let1 : a.Wf Γ ⟨A, e⟩ → t.Wf (⟨A, ⊥⟩::Γ) L → (let1 a t).Wf Γ L
+--   | let2 : a.Wf Γ ⟨(Ty.prod A B), e⟩ → t.Wf (⟨B, ⊥⟩::⟨A, ⊥⟩::Γ) L → (let2 a t).Wf Γ L
+--   | cfg (n) {G} (R : LCtx α) :
+--     (hR : R.length = n) → β.Wf Γ (R ++ L) →
+--     (∀i : Fin n, (G i).Wf (⟨R.get (i.cast hR.symm), ⊥⟩::Γ) (R ++ L)) →
+--     Wf Γ (cfg β n G) L
+
+def Term.evaluate [TyDenote Ty] {Γ : Ctxt Ty} {ty : Ty} (t : Term Γ ty) (VΓ : Ctxt.Valuation Γ) : toType ty :=
+  match t with
+  | var v => VΓ v
+  | val v => v
+
+-- def InS.br {Γ : Ctx α ε} {L : LCtx α} (ℓ) (a : Term.InS φ Γ ⟨A, ⊥⟩)
+--   (hℓ : L.Trg ℓ A) : InS φ Γ L
+--   := ⟨Region.br ℓ a, Wf.br hℓ a.2⟩
+
+
+-- | TODO: add a thingie that coerces case into `Bool`.
+-- def InS.case {Γ : Ctx α ε} {L : LCtx α} {A B e}
+--  (a : Term.InS φ Γ ⟨Ty.coprod A B, e⟩) (s : InS φ (⟨A, ⊥⟩::Γ) L) (t : InS φ (⟨B, ⊥⟩::Γ) L) : InS φ Γ L
+
+class TyHasCoprod (Ty : Type) where
+  coprod : Ty → Ty → Ty
+
+class TyHasCoprodDenote (Ty : Type) [TyDenote Ty] [C : TyHasCoprod Ty] where
+  inl : toType α →  toType (C.coprod α β)
+  inr : toType α →  toType (C.coprod α β)
+  elim : (toType α → γ) → (toType β → γ) → toType (C.coprod α β) → γ
+
+/- TODO: implement a thing `left? : toType (C.coprod α β) → Option (toType α)` using `elim`.
+This will allow us to cleanup case_inl by writing `(ha : (l : toType  α) ∈ a.evaluate VΓ |>.left?)`-/
+/-
+TODO: add lawful instance of TyHasCoprodDenote for proving properties about the universal property.
+-/
+
+instance : Append (Ctxt Ty) where
+  append Γ Δ := Γ.append Δ
+
+inductive Region [C : TyHasCoprod Ty] : (Γ : Ctxt Ty) → (L : Ctxt Ty) → Type
+| br (a : Term Γ α) (hl : L.Var α) : Region Γ L
+| case (a : Term Γ (C.coprod α β)) (s : Region (Γ.snoc α) L) (t : Region (Γ.snoc β) L) : Region Γ L
+| let₁ (a : Term Γ α) (t : Region (Γ.snoc α) L) : Region Γ L
+-- | cfg {R L D : Ctxt Ty}
+--     (hD : D = R ++ L)
+--     (t : Region Γ D) -- t for terminator, G for fixpoint graph.
+--     (G : R.Var α → Region (Γ.snoc α) D)
+--    : Region Γ L
+| cfg {Γ R L D : Ctxt Ty}
+    -- (hD : D = R ++ L)
+    (inL : Ctxt.Hom D (R ++ L))
+    (t : Region Γ D) -- t for terminator, G for fixpoint graph.
+    (G : ∀{α}, R.Var α → Region (Γ.snoc α) D)
+   : Region Γ L
+
+def _root_.Ctxt.CoValuation.ofAppend {R L : Ctxt Ty} (VRL : Ctxt.CoValuation (R ++ L)) : (Ctxt.CoValuation R)⊕(Ctxt.CoValuation L) :=
+  sorry
+
+/- Show that CoVal (R++L) splits as (Either (CoVal R) (CoVal L))-/
+/--
+Bigstep operational semantics for evaluation of a control flow graph.
+-/
+inductive Region.Evaluated [C : TyHasCoprod Ty] [CD : TyHasCoprodDenote Ty]  :
+    (Γ : Ctxt Ty) → (VΓ : Ctxt.Valuation Γ) → (L : Ctxt Ty) → (R : Region Γ L) → (VL' : Ctxt.CoValuation L) → Prop
+| br :  Evaluated Γ VL L (Region.br a hl) (Ctxt.CoValuation.ofVar hl (a.evaluate VΓ))
+| case_inl : (ha : a.evaluate VΓ = CD.inl (α := α) l)
+  → Evaluated (Ctxt.snoc Γ α) (Ctxt.Valuation.snoc VΓ l) L t VL
+  → Evaluated Γ VΓ L (Region.case a s t) VL
+| case_inr : (ha : a.evaluate VΓ = CD.inr (β := β) r)
+  → Evaluated (Ctxt.snoc Γ β) (Ctxt.Valuation.snoc VΓ r) L t VL
+  → Evaluated Γ VΓ L (Region.case a s t) VL
+| let₁
+  : Evaluated (Ctxt.snoc Γ α) (Ctxt.Valuation.snoc VΓ (a.evaluate VΓ)) L t VL
+  → Evaluated Γ VΓ L (let₁ a t) VL
+| cfg_sibling {inL : Ctxt.Hom D (R ++ L)}
+  : Evaluated Γ VΓ D t VL
+  → (hVL : (VL.comap inL).ofAppend = Sum.inr S)
+  → Evaluated Γ VΓ L (cfg inL t G) S
+| cfg_child {Γ : Ctxt Ty} {VΓ : Γ.Valuation} {L R D : Ctxt Ty}
+  {VL : L.CoValuation} {VD : D.CoValuation} {inL : Ctxt.Hom D (R ++ L)}
+  {C : Ctxt.CoValuation R}
+  {t : Region Γ D}
+  {G : ∀ {α}, R.Var α → Region (Γ.snoc α) D}
+  : Evaluated Γ VΓ D t VD
+  → (hVL : (VD.comap inL).ofAppend = Sum.inl (α := R.CoValuation) (β := L.CoValuation) C)
+  → Evaluated Γ VΓ L (cfg inL (let₁ (Term.val C.val) (G C.var)) G) VL
+  → Evaluated Γ VΓ L (cfg (Γ := Γ) (R := R) (L := L) (D := D) inL t G) VL
+
+end Pure