Module CfgIterator

Require Import Coqlib DLib.
Require Import AST.
Require Import Op.
Require Import Registers Maps.
Require Import BinPos.
Require Import LatticeSignatures.

Local Notation node := positive.

Parameter extern_iterator : forall {A:Type} {instruction:Type},
  (A -> A -> bool) ->
  (A -> A -> A) ->
  (A -> A -> A) ->
  A ->
  A ->
  (node -> instruction -> list (node* (A -> A))) ->
  node ->
  PTree.t instruction ->
  A ->
  PMap.t A.

Module BourdoncleIterator.

Section lat.
Context {t0 B instruction: Type}.
Definition t := t0+⊥.
Variable ab : adom t B.

Definition get_extern_fixpoint
  (entrypoint:node) (code:PTree.t instruction)
  (transfer:node -> instruction -> list (node* (t -> t)))
  (init:t) : PMap.t t :=
  extern_iterator leb join widen top (bot ab) transfer entrypoint code init.

Definition check_fxp
  (entrypoint:node) (code:PTree.t instruction)
  (transfer:node -> instruction -> list (node* (t -> t)))
  (init:t)
  (fxp:PMap.t t) : bool :=
  init ⊑ (PMap.get entrypoint fxp)
    && ptree_forall code
    (fun n ins =>
      let ab := PMap.get n fxp in
      List.forallb
      (fun x:(node*(t->t)) =>
        let (n',tf) := x in
          (tf ab) ⊑ (PMap.get n' fxp))
      (transfer n ins)).

Definition get_fxp (fxp:PMap.t t) (n:node) : t := fxp!!n.

Definition top_solve_pfp (n:node) := ⊤.

Definition solve_pfp
  (entrypoint:node) (code:PTree.t instruction)
  (transfer:node -> instruction -> list (node* (t -> t)))
  (init:t) : node -> t :=
  let fxp := get_extern_fixpoint entrypoint code transfer init in
    if check_fxp entrypoint code transfer init fxp
      then get_fxp fxp
      else top_solve_pfp.

Lemma solve_pfp_entrypoint: forall entrypoint code transfer init,
  γ init ⊆ γ (solve_pfp entrypoint code transfer init entrypoint).

Lemma solve_pfp_postfixpoint: forall entrypoint code transfer init pc1 ins,
  code!pc1 = Some ins -> forall pc2 tf,
  In (pc2,tf) (transfer pc1 ins) ->
  γ (tf (solve_pfp entrypoint code transfer init pc1)) ⊆ γ (solve_pfp entrypoint code transfer init pc2).

End lat.
End BourdoncleIterator.