Module CfgIterator

Require Import DLib.
Require Import AST.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import LatticeSignatures.

Module BWLattice.

  Record t {A:Type} {B:Type} : Type := make {
    leb: A -> A -> bool;
    bot: A;
    top: A;
    join: A -> A -> A;
    widen: A -> A -> A;

    gamma: A -> B -> Prop;
    gamma_monotone: forall {a1} {a2},
      leb a1 a2 = true -> gamma a1 ⊆ gamma a2;
    gamma_top: forall x, gamma top x
  }.

  Implicit Arguments t [].
  Hint Resolve @gamma_monotone @gamma_top.

  Definition from_wlattice {A B:Type} (l:WLattice.t A B) : t (option A) B.

End BWLattice.

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

Module BourdoncleIterator.

Section Lat.
Context {t B: Type}.
Variable lat : BWLattice.t t B.

Definition get_extern_fixpoint
  (f:function)
  (transfer: instruction -> list (node * (t -> t)))
  (init:t) : PMap.t t :=
  extern_iterator
    (BWLattice.leb lat)
    (BWLattice.join lat)
    (BWLattice.widen lat)
    (BWLattice.top lat)
    (BWLattice.bot lat) transfer f init.

Definition check_fixpoint
  (f:function)
  (transfer: instruction -> list (node * (t -> t)))
  (init:t)
  (fxp:PMap.t t) : bool :=
  BWLattice.leb lat init (PMap.get f.(fn_entrypoint) fxp)
    && ptree_forall f.(fn_code)
    (fun n ins =>
      let ab := PMap.get n fxp in
      List.forallb
      (fun x:(node*(t->t)) =>
        let (n',tf) := x in
          BWLattice.leb lat (tf ab) (PMap.get n' fxp))
      (transfer ins)).

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

Definition top_analyze (n:node) := BWLattice.top lat.

Definition analyze
  (f:function)
  (transfer:instruction -> list (node* (t -> t)))
  (init:t) : node -> t :=
  let fxp := get_extern_fixpoint f transfer init in
    if check_fixpoint f transfer init fxp
      then get_fxp fxp
      else top_analyze.

Lemma analyze_entrypoint: forall f transfer init,
  BWLattice.gamma lat init ⊆ BWLattice.gamma lat (analyze f transfer init f.(fn_entrypoint)).

Lemma analyze_entrypoint_value: forall f transfer init,
  BWLattice.leb lat init (analyze f transfer init f.(fn_entrypoint)) = true
  \/
  analyze f transfer init f.(fn_entrypoint) = BWLattice.top lat.

Lemma analyze_postfixpoint: forall f transfer init pc1 ins,
  f.(fn_code)!pc1 = Some ins -> forall pc2 tf,
  In (pc2,tf) (transfer ins) ->
  BWLattice.gamma lat (tf (analyze f transfer init pc1)) ⊆ BWLattice.gamma lat (analyze f transfer init pc2).

End Lat.
End BourdoncleIterator.

Module WProd.
Section lat.
  Context {t1 t2 B: Type}.
  Variable lat1 : WLattice.t t1 B.
  Variable lat2 : WLattice.t t2 B.
  
  Definition A: Type := (t1*t2)%type.
  
  Definition leb: A -> A -> bool :=
    fun x y =>
      let (x1,x2) := x in
      let (y1,y2) := y in
        (WLattice.leb lat1 x1 y1)
        &&
        (WLattice.leb lat2 x2 y2).
  
  Definition top: A :=
    (WLattice.top lat1, WLattice.top lat2).
  
  Definition join: A -> A -> A :=
    fun x y =>
      let (x1,x2) := x in
      let (y1,y2) := y in
        (WLattice.join lat1 x1 y1,
          WLattice.join lat2 x2 y2).
  
  Definition widen: A -> A -> A :=
    fun x y =>
      let (x1,x2) := x in
      let (y1,y2) := y in
        (WLattice.widen lat1 x1 y1,
          WLattice.widen lat2 x2 y2).
  
  Definition gamma: A -> B -> Prop :=
    fun x b =>
      let (x1,x2) := x in
        (WLattice.gamma lat1 x1 b)
        /\ (WLattice.gamma lat2 x2 b).
  
  
  Lemma gamma_monotone: forall a1 a2,
    leb a1 a2 = true -> gamma a1 ⊆ gamma a2.
  
  Lemma gamma_top: forall x, gamma top x.
  
  Definition make : WLattice.t A B :=
   (WLattice.make _ _
    leb
    top
    join
    widen
    gamma
    gamma_monotone
    gamma_top ).

End lat.
End WProd.


Module WPMap.
Section lat.
Context {t0 B: Type}.
Variable lat : WLattice.t t0 B.

Definition A := PTree.t t0.
Definition t := option (PTree.t t0).

Definition bot : t := None.

Definition topA : A := (PTree.empty _).
Definition top : t := Some topA.

Definition getA (m: A) (r: reg) : t0 :=
  match PTree.get r m with
    | None => WLattice.top lat
    | Some i => i
  end.

Definition get (app: t) (r: reg) : option t0 :=
  match app with
    | None => None
    | Some m =>
      match PTree.get r m with
        | None => Some (WLattice.top lat)
        | Some i => Some i
      end
  end.

Definition set (app: t) (r: reg) (i:option t0) : t :=
  match i with
    | None => None
    | Some i =>
      match app with
        | None => Some (PTree.set r i (PTree.empty _))
        | Some m => Some (PTree.set r i m)
      end
  end.

Definition leb0 (m1 m2:A) : bool :=
    ptree_forall m2
    (fun x i2 =>
          match get (Some m1) x with
            | None => true
            | Some i1 => WLattice.leb lat i1 i2
          end).

Definition leb (x y:t) : bool :=
  match x, y with
    | None, _ => true
    | Some x, Some y => leb0 x y
    | _, _ => false
  end.

  Lemma leb_le: forall m1 m2,
    leb m1 m2 = true -> (forall p, BWLattice.leb (BWLattice.from_wlattice lat) (get m1 p) (get m2 p) = true
                                \/ get m2 p = BWLattice.top (BWLattice.from_wlattice lat)).

  Definition joinA : A -> A -> A :=
    PTree.combine
     (fun x y =>
       match x, y with
         | None, _ => None
           |_ , None => None
         | Some x, Some y => Some (WLattice.join lat x y)
       end).

  Definition join (x y: t): t :=
    match x, y with
      | None, _ => y
      |_ , None => x
      | Some x, Some y => Some (joinA x y)
    end.

  Definition widenA: A -> A -> A :=
    PTree.combine
    (fun x y =>
      match x, y with
        | None, _ => None
          |_ , None => None
        | Some x, Some y => Some (WLattice.widen lat x y)
      end).

  Definition widen (x y: t): t :=
    match x, y with
      | None, _ => y
      |_ , None => x
      | Some x, Some y => Some (widenA x y)
    end.

  Definition gamma (m: t) (rs: PMap.t B) : Prop :=
    forall r, BWLattice.gamma (BWLattice.from_wlattice lat) (get m r) rs#r.
  
  Lemma gamma_monotone: forall x y,
    leb x y = true ->
    gamma x ⊆ gamma y.

  Definition make : BWLattice.t t (PMap.t B).


Lemma gamma_set1 : forall app rs ab x,
  gamma app rs ->
  BWLattice.gamma (BWLattice.from_wlattice lat) ab (rs#x) ->
  gamma (set app x ab) rs.

Lemma gamma_set2 : forall app rs ab v x,
  gamma app rs ->
  BWLattice.gamma (BWLattice.from_wlattice lat) ab v ->
  gamma (set app x ab) (rs # x <- v).



End lat.
End WPMap.