Module Annotagen

Require
  Csharpminorannot.
Import
  Utf8 String
  Coqlib Errors AST Maps
  Integers
  Annotations
  Csharpminorannot.
Require Import Sorting.Mergesort.

Local Coercion is_true : bool >-> Sortclass.

Definition annotation_log : Type :=
  annotation.

Definition annotation_map : Type :=
  PTree.t (list ablock).

Definition collect_annotations (log: list annotation_log) : annotation_map :=
  List.fold_left
    (λ m a,
     let '(i, x) := a in
     PTree.set
       i
       match m ! i with
       | Some nil => nil
       | Some y => match x with nil => x | _ => x ++ y end
       | None => x
       end
       m
    ) log (PTree.empty _).

Module IntPairOrder <: Orders.TotalLeBool' with Definition t := (int * int)%type.
  Definition t : Type := (int * int)%type.

  Definition leb (x x': t) : bool :=
    let '(a, b) := x in
    let '(a', b') := x' in
    match Z.compare (Int.unsigned a) (Int.unsigned a') with
    | Lt => true
    | Gt => false
    | Eq => match Z.compare (Int.unsigned b') (Int.unsigned b) with
            | Lt | Eq => true
            | Gt => false
            end
    end.

  Lemma leb_total (x x': t) : leb x x' ∨ leb x' x.

End IntPairOrder.

Module AblockOrder <: Orders.TotalLeBool' with Definition t := ablock.
  Definition t : Type := ablock.

  Definition leb (x x': ablock) : bool :=
    match x, x' with
    | ABlocal d _ r, ABlocal d' _ r' =>
      match nat_compare d d' with
      | Lt => true | Gt => false | Eq =>
      IntPairOrder.leb r r'
      end
    | ABlocal _ _ _, ABglobal _ _ => true
    | ABglobal _ _, ABlocal _ _ _ => false
    | ABglobal b r, ABglobal b' r' =>
      match Pos.compare b b' with
      | Lt => true | Gt => false | Eq =>
      IntPairOrder.leb r r'
      end
    end.

  Lemma leb_total (x x': t) : leb x x' ∨ leb x' x.

End AblockOrder.

Module AblockSort := Sort AblockOrder.

Definition ablock_leb (x x': ablock) : bool :=
  match x, x' with
  | ABlocal d _ r, ABlocal d' _ r' =>
    match nat_compare d d' with
    | Lt | Gt => false | Eq =>
    range_leb r r'
    end
  | ABlocal _ _ _, ABglobal _ _
  | ABglobal _ _, ABlocal _ _ _ => false
  | ABglobal b r, ABglobal b' r' =>
    match Pos.compare b b' with
    | Lt | Gt => false | Eq =>
    range_leb r r'
    end
  end.

Remark range_leb_refl x : range_leb x x.

Remark ablock_leb_refl x : ablock_leb x x.

Fixpoint remove_stutter_rec a m acc { struct m } :=
  match m with
  | nil => a :: acc
  | b :: m' =>
    if ablock_leb b a
    then remove_stutter_rec a m' acc
    else remove_stutter_rec b m' (a :: acc)
  end.

Definition remove_stutter (m: list ablock) : list ablock :=
  match m with
  | nil => nil
  | a :: m' => remove_stutter_rec a m' nil
  end.

Definition nodup (m: list ablock) : list ablock :=
  remove_stutter (AblockSort.sort m).

Lemma remove_stutter_rec_in m :
  ∀ a acc x, In x m ∨ (∃ y, In y (a :: acc) ∧ ablock_leb x y) → ∃ y, In y (remove_stutter_rec a m acc) ∧ ablock_leb x y.

Lemma remove_stutter_in m :
  ∀ x, In x m → ∃ y, In y (remove_stutter m) ∧ ablock_leb x y.

Lemma nodup_in m :
  ∀ x, In x m → ∃ y, In y (nodup m) ∧ ablock_leb x y.

Definition merge_adjacent_blocks (m: list ablock) : list ablock :=
  let merge x v u :=
      if Int.eq (Int.add (snd u) Int.one) (fst v)
      then Some (x, (fst u, snd v))
      else None
  in
  let same_block x y :=
      match x, y with
      | ABglobal a u, ABglobal b v => if Pos.eqb a b then merge (ABglobal a) u v else None
      | ABlocal a x u, ABlocal b _ v => if NPeano.Nat.eqb a b then merge (ABlocal a x) u v else None
      | _, _ => None
      end
  in
  let fix rec ab m :=
      match m with
      | nil => ab :: m
      | ab' :: m' =>
        match same_block ab ab' with
        | None => ab :: rec ab' m'
        | Some(x, r) => rec (x r) m'
        end
      end
  in
  match m with
  | nil => m
  | ab :: m' => rec ab m'
  end.


Section TRANSF.

Variable am: annotation_map.

Local Open Scope error_monad_scope.
Arguments OK {_} _.

Definition annot (α: annotation) : annotation :=
  let '(i, _) := α in
  match am ! i with
  | None => α
  | Some a => (i, merge_adjacent_blocks (nodup a))
  end.

Fixpoint transl_expr (e: expr) : res expr :=
  match e with
  | Evar _
  | Eaddrof _
  | Econst _
    => OK e
  | Eunop op a => do a' <- transl_expr a; OK (Eunop op a')
  | Ebinop op a b => do a' <- transl_expr a; do b' <- transl_expr b; OK (Ebinop op a' b')
  | Eload α κ a => do a' <- transl_expr a; OK (Eload (annot α) κ a')
  end.

Definition transl_exprlist (el: list expr) : res (list expr) :=
  Errors.mmap transl_expr el.

Fixpoint transl_statement (s: stmt) : res stmt :=
  match s with
  | Sskip => OK s
  | Sset x e => do e' <- transl_expr e; OK (Sset x e')
  | Sstore α κ dst src =>
    do dst' <- transl_expr dst;
    do src' <- transl_expr src;
    OK (Sstore (annot α) κ dst' src')
  | Scall r s f args =>
    do f' <- transl_expr f;
    do args' <- transl_exprlist args;
    OK (Scall r s f' args')
  | Sbuiltin r ef args =>
    do args' <- transl_exprlist args;
    OK (Sbuiltin r ef args')
  | Sseq s₁ s₂ =>
    do s₁' <- transl_statement s₁;
    do s₂' <- transl_statement s₂;
    OK (Sseq s₁' s₂')
  | Sifthenelse c s₁ s₂ =>
    do c' <- transl_expr c;
    do s₁' <- transl_statement s₁;
    do s₂' <- transl_statement s₂;
    OK (Sifthenelse c' s₁' s₂')
  | Sloop body =>
    do body' <- transl_statement body;
    OK (Sloop body')
  | Sblock body =>
    do body' <- transl_statement body;
    OK (Sblock body')
  | Sexit _ => OK s
  | Sswitch b c ls =>
    do c' <- transl_expr c;
    do ls' <- transl_lstatement ls;
    OK (Sswitch b c' ls')
  | Sreturn None => OK s
  | Sreturn (Some a) =>
    do a' <- transl_expr a;
    OK (Sreturn (Some a'))
  | Slabel lbl body =>
    do body' <- transl_statement body;
    OK (Slabel lbl body')
  | Sgoto _ => OK s
  end
with transl_lstatement (ls: lbl_stmt) : res lbl_stmt :=
       match ls with
       | LSnil => OK ls
       | LScons lbl s ls =>
         do s' <- transl_statement s;
         do ls' <- transl_lstatement ls;
         OK (LScons lbl s' ls')
       end.

Definition transl_function (f: function) : res function :=
  do body <- transl_statement (fn_body f);
  OK (mkfunction (fn_sig f) (fn_params f) (fn_vars f) (fn_temps f) body).

Definition transl_fundef (fd: fundef) : res fundef :=
  match fd with
  | Internal f => do f' <- transl_function f; OK (Internal f')
  | _ => OK fd
  end.

Definition transl_globdefs defs : res (list (ident * globdef fundef unit)) :=
  transf_globdefs transl_fundef OK defs.

Definition transl_program (p: program): res program :=
  do tprog_defs <- transl_globdefs p.(prog_defs);
  OK {| prog_defs := tprog_defs;
        prog_public := p.(prog_public);
        prog_main := p.(prog_main)
     |}.

End TRANSF.

Definition doit (log: list annotation_log) : program → res program :=
  let am := collect_annotations log in
  transl_program am.