path: root/src/hls/DeadBlocksproof.v

(** This file contain the proof of the RTLdfs transformation. We show
both that the transformation ensures that generated functions are
satisfying the predicate [wf_dfs_function] and that the transformation
preserves the semantics. *)

Require Recdef.
Require Import FSets.
Require Import Coqlib.
Require Import Ordered.
Require Import Errors.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import Smallstep.
Require Import DeadBlocks.
Require Import Kildall.
Require Import Conventions.
Require Import Integers.
Require Import Floats.
Require Import Utils.
Require Import Events.
Require Import Gible.
Require Import GibleSeq.
Require Import Relation_Operators.

Unset Allow StrictProp.

(** * The [cfg] predicate *)
Variant cfg (code:code) (i j:node) : Prop :=
  | CFG : forall ins
    (HCFG_ins: code!i = Some ins)
    (HCFG_in : In j (all_successors ins)),
    cfg code i j.

Inductive cfg_star (code:code) (i:node) : node -> Prop :=
| cfg_star0 : cfg_star code i i
| cfg_star1 : forall j k, cfg_star code i j -> cfg code j k -> cfg_star code i k.

Notation "R **" := (@clos_refl_trans _ R) (at level 30).

Lemma Rstar_refl : forall A R (i:A), R** i i.
Proof. constructor 2. Qed.

Lemma Rstar_R : forall A (R:A->A->Prop) (i j:A), R i j -> R** i j.
Proof. constructor 1; auto. Qed.

Lemma Rstar_trans : forall A (R:A->A->Prop) (i j k:A),
  R** i j -> R** j k -> R** i k.
Proof. intros A R i j k; constructor 3 with j; auto. Qed.

Global Hint Resolve Rstar_trans Rstar_refl Rstar_R: core.

Lemma star_eq : forall A (R1 R2:A->A->Prop),
  (forall i j, R1 i j -> R2 i j) ->
  forall i j, R1** i j -> R2** i j.
Proof.
  induction 2.
  econstructor 1; eauto.
  econstructor 2; eauto.
  econstructor 3; eauto.
Qed.

Lemma cfg_star_same_code: forall code1 code2 i,
  (forall k, cfg_star code1 i k -> code1!k = code2!k) ->
  forall j, cfg_star code1 i j -> cfg_star code2 i j.
Proof.
  induction 2.
  constructor 1.
  constructor 2 with j; auto.
  inv H1.
  rewrite H in *; auto.
  econstructor; eauto.
Qed.

Lemma cfg_star_same : forall code i j,
  cfg_star code i j <-> (cfg code)** i j.
Proof.
  split.
  induction 1.
  constructor 2.
  constructor 3 with j; auto.
  assert (forall i j, (cfg code0**) i j -> forall k, cfg_star code0 k i -> cfg_star code0 k j).
    clear i j; induction 1; auto.
    intros.
    constructor 2 with x; auto.
  intros; apply H with i; auto.
  constructor 1.
Qed.

(** * Utility lemmas *)
Section dfs.
Variable entry:node.
Variable code:code.

Lemma not_seen_sons_aux0 : forall l0 l1 l2 seen_set seen_set',
  fold_left
  (fun (ns : prod (list node) (PTree.t unit)) (j : positive) =>
    let (new, seen) := ns in
      match seen ! j with
        | Some _ => ns
        | None => (j :: new, PTree.set j tt seen)
      end) l0 (l1, seen_set) = (l2, seen_set') ->
  forall x, In x l1 -> In x l2.
Proof.
  induction l0; simpl; intros.
  inv H; auto.
  destruct (seen_set!a); inv H; eauto with datatypes.
Qed.

Lemma not_seen_sons_prop1 : forall i j seen_set seen_set' l,
  not_seen_sons code i seen_set = (l,seen_set') ->
  cfg code i j -> In j l \/ seen_set ! j = Some tt.
Proof.
  unfold not_seen_sons; intros.
  inv H0.
  rewrite HCFG_ins in *.
  assert (
   forall l0 l1 l2 seen_set seen_set',
   fold_left
     (fun (ns : prod (list node) (PTree.t unit)) (j0 : positive) =>
      let (new, seen) := ns in
      match seen ! j0 with
      | Some _ => ns
      | None => (j0 :: new, PTree.set j0 tt seen)
      end) l0 (l1, seen_set) = (l2, seen_set') ->
   In j l0 -> In j l2 \/ seen_set ! j = Some tt).
  induction l0; simpl; intros.
  intuition.
  destruct (peq a j).
  subst.
  case_eq (seen_set0!j); intros.
  destruct u; auto.
  rewrite H2 in *.
  left; eapply not_seen_sons_aux0; eauto with datatypes.
  destruct H1.
  intuition.
  destruct (seen_set0!a); eauto.
  elim IHl0 with (1:=H0); auto.
  rewrite PTree.gso; auto.
  eauto.
Qed.

Lemma not_seen_sons_prop8 : forall i j seen_set seen_set' l,
  not_seen_sons code i seen_set = (l,seen_set') ->
  In j l -> cfg code i j.
Proof.
  unfold not_seen_sons; intros.
  assert (
   forall l0 l1 l2 seen_set seen_set',
   fold_left
     (fun (ns : prod (list node) (PTree.t unit)) (j0 : positive) =>
      let (new, seen) := ns in
      match seen ! j0 with
      | Some _ => ns
      | None => (j0 :: new, PTree.set j0 tt seen)
      end) l0 (l1, seen_set) = (l2, seen_set') ->
   In j l2 -> In j l0 \/ In j l1).
  induction l0; simpl; intros.
  inv H1; auto.
  case_eq (seen_set0!a); intros; rewrite H3 in *.
  elim IHl0 with (1:=H1); auto.
  elim IHl0 with (1:=H1); auto.
  simpl; destruct 1; auto.
  case_eq (code!i); intros; rewrite H2 in H.
  apply H1 in H; auto; clear H1.
  destruct H as [H|H]; try (elim H; fail).
  econstructor; eauto.
  inv H; elim H0.
Qed.

Lemma not_seen_sons_prop2 : forall i j seen_set,
  In j (fst (not_seen_sons code i seen_set)) ->
  seen_set ! j = None.
Proof.
  unfold not_seen_sons; intros.
  case_eq (code!i); [intros ins Hi|intros Hi]; rewrite Hi in *.
  assert (forall l l0 seen_set,
    In j
        (fst
           (fold_left
              (fun (ns : prod (list node) (PTree.t unit)) (j : positive) =>
               let (new, seen) := ns in
               match seen ! j with
               | Some _ => ns
               | None => (j :: new, PTree.set j tt seen)
               end) l (l0, seen_set))) ->
        In j l0\/ seen_set ! j = None).
  induction l; simpl; auto.
  intros.
  case_eq (seen_set0 ! a); intros; rewrite H1 in *; eauto.
  elim IHl with (1:=H0); auto.
  simpl; destruct 1; subst; auto.
  rewrite PTree.gsspec; destruct peq; auto.
  intros; congruence.
  elim H0 with (1:=H); auto.
  simpl; intuition.
  simpl in H; intuition.
Qed.

Lemma not_seen_sons_prop5 : forall i seen_set,
  list_norepet (fst (not_seen_sons code i seen_set)).
Proof.
  unfold not_seen_sons; intros.
  destruct (code ! i); simpl; try constructor.
  assert (forall l l0 seen_set l1 seen_set',
    (fold_left
      (fun (ns : prod (list node) (PTree.t unit)) (j : positive) =>
        let (new, seen) := ns in
          match seen ! j with
            | Some _ => ns
            | None => (j :: new, PTree.set j tt seen)
          end) l (l0, seen_set)) = (l1,seen_set') ->
    (forall x, In x l0 -> seen_set!x = Some tt) ->
    list_norepet l0 ->
    (forall x, In x l1 -> seen_set'!x = Some tt) /\ list_norepet l1).
  induction l; simpl; intros.
  inv H ;auto.
  case_eq (seen_set0!a); intros; rewrite H2 in *; auto.
  elim IHl with (1:=H); auto.
  elim IHl with (1:=H); auto.
  simpl; destruct 1; auto.
  subst; rewrite PTree.gss; auto.
  rewrite PTree.gsspec; destruct peq; auto.
  constructor; auto.
  intro; rewrite (H0 a) in H2; auto; congruence.
  generalize (H (all_successors t) nil seen_set).
  destruct (fold_left
      (fun (ns : prod (list node) (PTree.t unit)) (j : positive) =>
        let (new, seen) := ns in
          match seen ! j with
            | Some _ => ns
            | None => (j :: new, PTree.set j tt seen)
          end) (all_successors t) (nil, seen_set)); intuition.
  eelim H0; eauto.
  simpl; intuition.
  constructor.
Qed.

Lemma not_seen_sons_prop3_aux : forall l i l0 seen_set l1 seen_set',
    seen_set!i = Some tt ->
    (fold_left
      (fun (ns : prod (list node) (PTree.t unit)) (j : positive) =>
        let (new, seen) := ns in
          match seen ! j with
            | Some _ => ns
            | None => (j :: new, PTree.set j tt seen)
          end) l (l0, seen_set)) = (l1,seen_set') ->
    seen_set'!i = Some tt.
Proof.
 induction l; simpl; intros.
 inv H0; auto.
 destruct (seen_set!a).
 rewrite (IHl _ _ _ _ _ H H0); auto.
 assert ((PTree.set a tt seen_set)! i = Some tt).
 rewrite PTree.gsspec; destruct peq; auto.
 rewrite (IHl _ _ _ _ _ H1 H0); auto.
Qed.

Lemma not_seen_sons_prop3 : forall i seen_set seen_set' l,
  not_seen_sons code i seen_set = (l,seen_set') ->
  forall i, seen_set!i = Some tt -> seen_set'!i = Some tt.
Proof.
  unfold not_seen_sons; intros.
  destruct (code!i); inv H; auto.
  apply not_seen_sons_prop3_aux with (2:=H2); auto.
Qed.


Lemma not_seen_sons_prop4 : forall i seen_set seen_set' l,
  not_seen_sons code i seen_set = (l,seen_set') ->
  forall i, In i l -> seen_set'!i = Some tt.
Proof.
  unfold not_seen_sons; intros.
  destruct (code!i); inv H; auto.
  assert (forall l i l0 seen_set l1 seen_set',
    In i l1 ->
    (forall i, In i l0 -> seen_set !i = Some tt) ->
    (fold_left
      (fun (ns : prod (list node) (PTree.t unit)) (j : positive) =>
        let (new, seen) := ns in
          match seen ! j with
            | Some _ => ns
            | None => (j :: new, PTree.set j tt seen)
          end) l (l0, seen_set)) = (l1,seen_set') ->
    seen_set'!i = Some tt).
  induction l0; simpl; intros.
  inv H3; auto.
  case_eq (seen_set0 ! a); intros; rewrite H4 in *; inv H3.
  apply IHl0 with (3:= H6); auto.
  apply IHl0 with (3:= H6); auto.
  simpl; destruct 1; subst.
  rewrite PTree.gss; auto.
  rewrite PTree.gsspec; destruct peq; auto.
  apply H with (3:=H2); auto.
  simpl; intuition.
  elim H0.
Qed.

Lemma not_seen_sons_prop6 : forall i seen_set seen_set' l,
  not_seen_sons code i seen_set = (l,seen_set') ->
  forall i, seen_set'!i = Some tt -> seen_set!i = Some tt \/ In i l.
Proof.
  unfold not_seen_sons; intros.
  destruct (code!i); inv H; auto.
  assert (forall l i l0 seen_set l1 seen_set',
    (fold_left
      (fun (ns : prod (list node) (PTree.t unit)) (j : positive) =>
        let (new, seen) := ns in
          match seen ! j with
            | Some _ => ns
            | None => (j :: new, PTree.set j tt seen)
          end) l (l0, seen_set)) = (l1,seen_set') ->
    seen_set'!i = Some tt ->
    seen_set !i = Some tt \/ In i l1).
  induction l0; simpl; intros.
  inv H; auto.
  case_eq (seen_set0 ! a); intros; rewrite H3 in *; inv H.
  apply IHl0 with (1:= H5); auto.
  elim IHl0 with (1:= H5) (i:=i1); auto; intros.
  rewrite PTree.gsspec in H; destruct peq; auto.
  subst.
  right.
  eapply not_seen_sons_aux0; eauto with datatypes.
  apply H with (1:=H2); auto.
Qed.

Lemma iter_hh7 :  forall seen_list stack
  (HH7: forall i j, In i seen_list -> cfg code i j -> In j seen_list \/ In j stack),
  forall i j, (cfg code)** i j -> In i seen_list -> In j seen_list \/
    exists k, (cfg code)** i k /\ (cfg code)** k j /\ In k stack.
Proof.
  induction 2; intros; auto.
  edestruct HH7; eauto.
  right; exists y; repeat split; auto.
  edestruct IHclos_refl_trans1; eauto.
  edestruct IHclos_refl_trans2; eauto.
  destruct H3 as [k [T1 [T2 T3]]].
  right; exists k; repeat split; eauto.
  destruct H2 as [k [T1 [T2 T3]]].
  right; exists k; repeat split; eauto.
Qed.

Lemma acc_succ_prop : forall workl seen_set seen_list stack seen code'
  (HH1: In entry seen_list)
  (HH2: list_norepet stack)
  (HH3: forall i, In i stack -> seen_set ! i = Some  tt)
  (HH4: forall i, In i seen_list -> seen_set ! i = Some  tt)
  (HH5: forall i, In i seen_list -> In i stack -> False)
  (HH6: forall i, seen_set ! i = Some tt -> In i seen_list \/ In i stack)
  (HH7: forall i j, In i seen_list -> cfg code i j -> In j seen_list \/ In j stack)
  (HH8: forall i, In i seen_list -> (cfg code)** entry i)
  (HH11: forall i, In i stack -> (cfg code)** entry i)
  (HH9: acc_succ code workl (OK (seen_set,seen_list,stack)) = OK (seen, code'))
  (HH10: list_norepet seen_list),
  (forall j, (cfg code)** entry j -> In j seen /\ code ! j = code' !j)
  /\ (forall j ins, code'!j = Some ins -> In j seen)
  /\ list_norepet seen
  /\ (forall j, In j seen -> code!j = code'!j)
  /\ (forall i j, In i seen -> cfg code i j -> In j seen)
  /\ (forall j, In j seen -> (cfg code)** entry j).
Proof.
  induction workl; simpl; intros until 11.
  destruct stack; inv HH9.
  assert (forall j : node, (cfg code **) entry j -> In j seen); intros.
  elim (iter_hh7 seen nil HH7 entry j); auto.
  destruct 1; intuition.
  split; auto.
  intros.
  rewrite PTree.gcombine; auto.
  rewrite HH4; auto.
  split; intros.
  rewrite PTree.gcombine in H0; auto.
  unfold remove_dead in *.
  case_eq (seen_set!j); intros; rewrite H1 in *; try congruence.
  elim HH6 with j; intros; auto.
  destruct u; auto.
  split; auto.
  split; auto.
  intros.
  rewrite PTree.gcombine; simpl; auto.
  rewrite HH4; auto.
  split.
  intros; exploit HH7; eauto; destruct 1; simpl; auto.
  assumption.

  destruct stack; inv HH9.
  assert (forall j : node, (cfg code **) entry j -> In j seen); intros.
  elim (iter_hh7 seen nil HH7 entry j); auto.
  destruct 1; intuition.
  split; auto.
  intros.
  rewrite PTree.gcombine; auto.
  rewrite HH4; auto.
  split; intros.
  rewrite PTree.gcombine in H0; unfold remove_dead in *.
  case_eq (seen_set!j); intros; rewrite H1 in *; try congruence.
  elim HH6 with j; intros; auto.
  destruct u; auto.
  auto.
  split; auto.
  split; auto.
  intros; rewrite PTree.gcombine; auto.
  rewrite HH4; auto.
  split.
  intros; exploit HH7; eauto; destruct 1; auto.
  assumption.

  case_eq (not_seen_sons code p (PTree.set p tt seen_set)); intros new seen_set' Hn.
  rewrite Hn in *.

  apply IHworkl with (10:=H0); auto with datatypes; clear H0.

  apply list_norepet_append; auto.
  generalize (not_seen_sons_prop5 p (PTree.set p tt seen_set)); rewrite Hn; auto.
  inv HH2; auto.
  unfold list_disjoint; red; intros; subst.
  assert (seen_set!y=None).
  generalize (not_seen_sons_prop2 p y (PTree.set p tt seen_set)); rewrite Hn; simpl; intros.
  apply H1 in H.
  rewrite PTree.gsspec in H; destruct peq; try congruence.
  rewrite HH3 in H1; auto with datatypes; congruence.

  simpl; intros i Hi.
  rewrite in_app in Hi; destruct Hi; auto.
  eapply not_seen_sons_prop4; eauto.
  eapply not_seen_sons_prop3; eauto.
  rewrite PTree.gsspec; destruct peq; auto with datatypes.

simpl; intros i Hi.
  destruct Hi; subst.
  eapply not_seen_sons_prop3; eauto.
  rewrite PTree.gss; auto.
  eapply not_seen_sons_prop3; eauto.
  rewrite PTree.gsspec; destruct peq; auto.

simpl; intros i Hi1 Hi2.
  rewrite in_app in Hi2.
  destruct Hi2.
  generalize (not_seen_sons_prop2 p i (PTree.set p tt seen_set)); rewrite Hn; simpl; intros.
  apply H0 in H; clear H0.
  rewrite PTree.gsspec in H; destruct peq; try congruence.
  destruct Hi1; subst; try congruence.
  rewrite HH4 in H; congruence.
  destruct Hi1; subst.
  inv HH2; intuition.
  elim HH5 with i; auto with datatypes.

intros i Hi.
  elim not_seen_sons_prop6 with (1:=Hn) (2:=Hi); intros.
  rewrite PTree.gsspec in H; destruct peq; auto.
  left; left; auto.
  elim HH6 with i; auto with datatypes.
  simpl; destruct 1; auto.
  right; rewrite in_app; auto.
  right; rewrite in_app; auto.

intros i j Hi1 Hi2.
  simpl in Hi1; destruct Hi1; subst.
  elim not_seen_sons_prop1 with i j (PTree.set i tt seen_set) seen_set' new; auto; intros.
  right; eauto with datatypes.
  rewrite PTree.gsspec in H; destruct peq; auto.
  left; left; auto.
  elim HH6 with j; auto with datatypes.
  simpl; destruct 1; auto with datatypes.
  elim HH7 with i j; auto with datatypes.
  simpl; destruct 1; auto with datatypes.

simpl; intros i Hi.
  destruct Hi; auto with datatypes.
  subst; auto with datatypes.

simpl; intros i Hi.
  rewrite in_app in Hi.
  destruct Hi; auto with datatypes.
  exploit not_seen_sons_prop8; eauto with datatypes.

  constructor; auto.
  intro HI; elim HH5 with p; auto with arith datatypes.
Qed.

End dfs.

(** * Proof of the well-formedness of generated functions *)
Lemma dfs_prop_aux : forall tf seen code',
  dfs tf = OK (seen, code') ->
  (forall j, (cfg (fn_code tf))** (fn_entrypoint tf) j ->
    In j seen /\  (fn_code tf) ! j = code' ! j)
  /\ (forall j ins, code'!j = Some ins -> In j seen)
  /\ list_norepet seen
  /\ (forall j, In j seen -> (fn_code tf)!j = code'!j)
  /\ (forall i j, In i seen -> cfg (fn_code tf) i j -> In j seen)
  /\ (forall i, In i seen -> (cfg (fn_code tf))** (fn_entrypoint tf) i).
Proof.
  unfold dfs; intros tf seen.
  destruct (map (@fst node SeqBB.t) (PTree.elements (fn_code tf))); simpl.
  intros; congruence.
  case_eq (not_seen_sons (fn_code tf) (fn_entrypoint tf)
           (PTree.set (fn_entrypoint tf) tt (PTree.empty unit)));
  intros new seen_set TT.
  intros code' T; monadInv T.
  assert (
 (forall j : node,
    (cfg (fn_code tf) **) (fn_entrypoint tf) j ->
    In j x /\ (fn_code tf) ! j = code' ! j) /\
   (forall (j : positive) (ins : SeqBB.t),
    code' ! j = Some ins -> In j x) /\ list_norepet x /\
   (forall j, In j x -> (fn_code tf)!j = code'!j) /\
   (forall i j, In i x -> cfg (fn_code tf) i j -> In j x) /\
   (forall j : positive, In j x -> (cfg (fn_code tf) **) (fn_entrypoint tf) j)
   ).
  apply acc_succ_prop with (entry:=(fn_entrypoint tf)) (10:=EQ); auto with datatypes.

  apply list_norepet_append; auto with datatypes.
  generalize (not_seen_sons_prop5 (fn_code tf) (fn_entrypoint tf)
         (PTree.set (fn_entrypoint tf) tt (PTree.empty unit))); rewrite TT; simpl; auto.
  constructor.
  intro; simpl; intuition.

  intros.
  rewrite in_app in H; destruct H.
  generalize (not_seen_sons_prop4 (fn_code tf) (fn_entrypoint tf)
         (PTree.set (fn_entrypoint tf) tt (PTree.empty unit))); rewrite TT; simpl; eauto.
  elim H.

  simpl; intuition.
  subst.
  generalize (not_seen_sons_prop3 (fn_code tf) (fn_entrypoint tf)
         (PTree.set (fn_entrypoint tf) tt (PTree.empty unit))); rewrite TT; simpl; intros.
  eapply H; eauto.
  rewrite PTree.gss; auto.

  simpl; intuition; subst.
  rewrite in_app in H0; destruct H0.
  generalize (not_seen_sons_prop2 (fn_code tf) (fn_entrypoint tf)
    (fn_entrypoint tf)
    (PTree.set (fn_entrypoint tf) tt (PTree.empty unit))); rewrite TT; simpl.
  rewrite PTree.gss; intros.
  apply H0 in H; congruence.
  elim H.

  intros.
  elim not_seen_sons_prop6 with (1:=TT) (i0:=i); auto with datatypes.
  rewrite PTree.gsspec; destruct peq; subst; intros; auto with datatypes.
  rewrite PTree.gempty in H0; congruence.

  simpl; intuition.
  elim not_seen_sons_prop1 with (j:=j) (1:=TT); auto with datatypes.
  rewrite PTree.gsspec; destruct peq; subst; intros; auto with datatypes.
  rewrite PTree.gempty in H; congruence.
  rewrite H1; auto.

  simpl; destruct 1; subst.
  constructor 2.
  elim H.

  intros i; rewrite in_app; destruct 1.
  exploit not_seen_sons_prop8; eauto.
  elim H.

  repeat constructor.
  intro H; elim H.

  destruct H.
  destruct H0.
  destruct H1.
  destruct H2.
  destruct H3 as [H3 H5].
  repeat split; intros.
  rewrite <- rev_alt; rewrite <- In_rev; eauto.
  elim H with j; auto.
  elim H with j; auto.
  rewrite <- rev_alt; rewrite <- In_rev; eauto.
  rewrite <- rev_alt; auto.
  apply list_norepet_rev; auto.
  rewrite <- rev_alt in H4; rewrite <- In_rev in H4; eauto.
  rewrite <- rev_alt in *; rewrite <- In_rev in *; eauto.
  rewrite <- rev_alt in *; rewrite <- In_rev in *; eauto.
Qed.

  (** Lemmas derived from the main lemma.*)
Lemma transf_function_fn_entrypoint : forall f tf,
  transf_function f = OK tf ->
  fn_entrypoint tf = fn_entrypoint f.
Proof.
  intros.
  unfold transf_function in H.
  destruct (dfs f); simpl in H; try congruence.
  destruct p; inv H.
  reflexivity.
Qed.

Lemma transf_function_ppoints1 : forall f tf,
  transf_function f = OK tf ->
  (forall j, (cfg (fn_code f))** (fn_entrypoint f) j ->
             (fn_code f) ! j = (fn_code tf) ! j).
Proof.
  intros.
  monadInv H.
  exploit dfs_prop_aux ; eauto.
  intuition.
  eelim H1; eauto.
Qed.

Lemma transf_function_ppoints1' : forall f tf,
  transf_function f = OK tf ->
  (forall j, (cfg (fn_code f))** (fn_entrypoint f) j ->
    (cfg (fn_code tf))** (fn_entrypoint tf) j).
Proof.
  intros.
  rewrite <- cfg_star_same.
  assert (fn_entrypoint tf = fn_entrypoint f)
    by (eapply transf_function_fn_entrypoint; eauto).
  apply cfg_star_same_code with (fn_code f).
  - intros.
    rewrite cfg_star_same in *.
    clear H0.
    rewrite H1 in H2.
    exploit transf_function_ppoints1; eauto.
  - intuition.
    rewrite cfg_star_same; rewrite H1; auto.
Qed.

(* Lemma transf_function_ppoints2 : forall f tf, *)
(*     transf_function f = OK tf -> *)
(*     (forall j ins, (fn_code tf)!j = Some ins -> In j (fn_dfs tf)). *)
(* Proof. *)
(*   intros. *)
(*   monadInv H ; simpl in *. *)
(*   exploit dfs_prop_aux ; eauto; intuition eauto. *)
(* Qed. *)


(* Lemma transf_function_ppoints3 : forall f tf, *)
(*   transf_function f = OK tf -> *)
(*   list_norepet (fn_dfs tf). *)
(* Proof. *)
(*   intros. *)
(*   monadInv H. *)
(*   eapply dfs_prop_aux ; eauto. *)
(* Qed. *)

(* Lemma transf_function_ppoints6 : forall f tf, *)
(*   transf_function f = OK tf -> *)
(*   (forall i, In i (fn_dfs tf) -> (cfg (RTLdfs.fn_code tf))** (RTLdfs.fn_entrypoint tf) i). *)
(* Proof. *)
(*   intros. *)
(*   eapply transf_function_ppoints1'; eauto. *)
(*   monadInv H. *)
(*   eapply dfs_prop_aux ; eauto. *)
(* Qed. *)

(* Lemma transf_function_wf_dfs : forall f tf, *)
(*    transf_function f = OK tf -> *)
(*    wf_dfs_function tf. *)
(* Proof. *)
(*   constructor. *)
(*   eapply transf_function_ppoints2 ; eauto. *)
(*   eapply transf_function_ppoints6 ; eauto. *)
(*   eapply transf_function_ppoints3 ; eauto. *)
(* Qed. *)

(** All generated functions satisfy the [wf_dfs] predicate. *)
Require Import Linking.

Definition match_prog (p: program) (tp: program) :=
  match_program (fun ctx f tf => transf_fundef f = OK tf) eq p tp.

Lemma transf_program_match:
  forall p tp, transf_program p = OK tp -> match_prog p tp.
Proof.
  intros. apply match_transform_partial_program; auto.
Qed.

(* Lemma match_prog_wf_dfs : forall p tp, *)
(*   match_prog p tp -> *)
(*   wf_dfs_program tp. *)
(* Proof. *)
(*   intros. *)
(*   red. intros. *)
(*   inv H. intuition. *)
(*   revert H1 H0. clear. *)
(*   generalize (prog_defs tp). *)
(*   induction 1; intros. *)
(*   - inv H0. *)
(*   - inv H0. *)
(*     + clear H1 IHlist_forall2. *)
(*       inv H. inv H1. *)
(*       destruct f1 ; simpl in * ; try constructor; auto. *)
(*       * monadInv H4. *)
(*         exploit transf_function_wf_dfs; eauto. *)
(*         intros. *)
(*         econstructor; eauto. *)
(*       * monadInv H4. *)
(*         constructor. *)
(*     + eapply IHlist_forall2; eauto. *)
(* Qed. *)

(** * Semantics preservation *)
Section PRESERVATION.

Variable prog: program.
Variable tprog: program.
Hypothesis TRANSF_PROG: match_prog prog tprog.

Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma symbols_preserved:
  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof.
  intro.
  eapply Genv.find_symbol_transf_partial; eauto.
Qed.

Lemma functions_translated:
  forall (v: val) (f: fundef),
  Genv.find_funct ge v = Some f ->
  exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
Proof.
  eapply Genv.find_funct_transf_partial; eauto.
Qed.

Lemma function_ptr_translated:
  forall (b: block) (f: fundef),
  Genv.find_funct_ptr ge b = Some f ->
  exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
Proof.
  eapply Genv.find_funct_ptr_transf_partial ; eauto.
Qed.

Lemma instr_at:
  forall f tf pc ins,
  transf_function f = OK tf ->
  (cfg (fn_code f) **) (fn_entrypoint f) pc ->
  (fn_code f)!pc = Some ins ->
  (fn_code tf)!pc = Some ins.
Proof.
  intros. inv H.
  monadInv  H3; simpl.
  inv EQ.
  elim dfs_prop_aux with f x x0; auto; intros.
  elim H with pc; auto.
  congruence.
Qed.

Lemma sig_fundef_translated:
  forall f tf,
  transf_fundef f = OK tf ->
  funsig tf = funsig f.
Proof.
  intros f tf. destruct f; simpl; intros.
  monadInv H; auto.
  monadInv EQ; auto.
  inv H. simpl; auto.
Qed.

Lemma find_function_preserved_same : forall r rs f f',
  find_function ge (inl ident r) rs = Some f ->
  find_function tge (inl ident r) rs = Some f' ->
  funsig f = funsig f'.
Proof.
  intros. simpl in *.
  exploit (functions_translated rs#r) ; eauto.
  intros.
  destruct H1 as [tf [Htf Oktf]].
  symmetry.
  eapply sig_fundef_translated; eauto.
  rewrite Htf in H0. inv H0; auto.
Qed.

Lemma spec_ros_r_find_function:
  forall rs f r,
  find_function ge (inl _ r) rs = Some f ->
  exists tf,
     find_function tge (inl _ r) rs = Some tf
  /\ transf_fundef f = OK tf.
Proof.
  intros.
  eapply functions_translated; eauto.
Qed.

Lemma spec_ros_id_find_function:
  forall rs f id,
  find_function ge (inr _ id) rs = Some f ->
  exists tf,
     find_function tge (inr _ id) rs = Some tf
  /\ transf_fundef f = OK tf.
Proof.
  intros.
  simpl in *.
  case_eq (Genv.find_symbol ge id) ; intros.
  rewrite H0 in H.
  rewrite symbols_preserved in * ; eauto ; rewrite H0 in *.
  exploit function_ptr_translated; eauto.
  rewrite H0 in H ; inv H.
Qed.

Inductive match_stackframes : list stackframe -> list stackframe -> Prop :=
| match_stackframes_nil: match_stackframes nil nil
| match_stackframes_cons:
  forall res f sp pc ps rs s tf ts
    (STACK : (match_stackframes s ts))
    (SPEC: (transf_function f = OK tf))
    (HCFG: (cfg (fn_code f) **) (fn_entrypoint f) pc),
    match_stackframes
    ((Stackframe res f sp pc ps rs) :: s)
    ((Stackframe res tf sp pc ps rs) :: ts)
    .
Hint Constructors match_stackframes: core.

Variant match_states: state -> state -> Prop :=
  | match_states_intro:
      forall s ts sp pc rs m f tf ps
        (SPEC: transf_function f = OK tf)
        (HCFG: (cfg (fn_code f) ** ) (fn_entrypoint f) pc)
        (STACK: match_stackframes s ts ),
        match_states (State s f sp pc rs ps m) (State ts tf sp pc rs ps m)
  | match_states_call:
      forall s ts f tf args m
        (SPEC: transf_fundef f = OK tf)
        (STACK: match_stackframes s ts ),
        match_states (Callstate s f args m) (Callstate ts tf args m)
  | match_states_return:
      forall s ts v m
        (STACK: match_stackframes s ts ),
        match_states (Returnstate s v m) (Returnstate ts v m).
Hint Constructors match_states: core.

Lemma transf_initial_states:
  forall st1, initial_state prog st1 ->
    exists st2, initial_state tprog st2 /\ match_states st1 st2.
Proof.
  intros. inversion H.
  exploit function_ptr_translated ; eauto. intros [tf [Hfind Htrans]].
  assert (MEM: (Genv.init_mem tprog) = Some m0)
    by (eapply (Genv.init_mem_transf_partial TRANSF_PROG); eauto).
  exists (Callstate nil tf nil m0); split.
  - econstructor; eauto.
    + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved; eauto.
      symmetry; eapply match_program_main; eauto.
    + rewrite <- H3. apply sig_fundef_translated; auto.
  - eapply match_states_call  ; eauto.
Qed.

Lemma transf_final_states:
  forall st1 st2 r,
  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
Proof.
  intros. inv H0. inv H.
  inv STACK.
  constructor.
Qed.

Lemma stacksize_preserved: forall f tf,
  transf_function f = OK tf ->
  fn_stacksize f = fn_stacksize tf.
Proof.
  intros.
  monadInv H. auto.
Qed.

Lemma senv_preserved:
  Senv.equiv (Genv.to_senv ge) (Genv.to_senv tge).
Proof.
  eapply Genv.senv_transf_partial; eauto.
Qed.

Create HintDb valagree.
Hint Resolve find_function_preserved_same: valagree.
Hint Resolve symbols_preserved : valagree.
Hint Resolve eval_addressing_preserved : valagree.
Hint Resolve eval_operation_preserved : valagree.
Hint Resolve sig_fundef_translated : valagree.
Hint Resolve senv_preserved : valagree.
Hint Resolve stacksize_preserved: valagree.

Ltac try_succ f pc pc' :=
  try (eapply Rstar_trans ; eauto) ; constructor ;
    (eapply (CFG (fn_code f) pc pc'); eauto;  simpl; auto).

Lemma transl_step_correct:
  forall s1 t s2,
  step ge s1 t s2 ->
  forall s1' (MS: match_states s1 s1'),
  exists s2', step tge s1' t s2' /\ match_states s2 s2'.
Proof.
  induction 1; intros; inv MS; auto.

  (* inop *)
  exploit instr_at; eauto; intros.
  destruct state0.
  exists (State stack f0 sp0 pc0 rs0 pr0 m0); split ; eauto.
  econstructor; auto. eauto. admit. admit.
  constructor; auto. admit.
  try_succ f pc pc'.

  (* iop *)
  exploit instr_at; eauto; intros.
  exists (RTLdfs.State ts tf sp pc' (rs#res<- v) m); split ; eauto.
  eapply RTLdfs.exec_Iop ; eauto.
  rewrite <- H0 ; eauto with valagree.
  constructor; auto.
  try_succ f pc pc'.

  (* iload *)
  exploit instr_at; eauto; intros.
  exists (RTLdfs.State ts tf sp pc' (rs#dst <- v) m); split ; eauto.
  eapply RTLdfs.exec_Iload ; eauto.
  try solve [rewrite <- H0 ; eauto with valagree].
  econstructor ; eauto.
  try_succ f pc pc'.

  (* istore *)
  exploit instr_at; eauto; intros.
  exists (RTLdfs.State ts tf sp pc' rs m'); split ; eauto.
  eapply RTLdfs.exec_Istore ; eauto.
  try solve [rewrite <- H0 ; eauto with valagree].
  constructor ; eauto.
  try_succ f pc pc'.

  (* icall *)
  destruct ros.
  exploit spec_ros_r_find_function ; eauto.
  intros. destruct H1 as [tf' [Hfind OKtf']].

  exploit instr_at; eauto; intros.
  exists (RTLdfs.Callstate (RTLdfs.Stackframe res tf sp pc' rs :: ts) tf' rs ## args m) ; split ; eauto.
  eapply RTLdfs.exec_Icall ; eauto.
  eauto with valagree.
  constructor; auto.
  constructor; auto.
  try_succ f pc pc'.

  exploit spec_ros_id_find_function ; eauto.
  intros. destruct H1 as [tf' [Hfind OKtf']].

  exploit instr_at; eauto; intros.
  exists (RTLdfs.Callstate (RTLdfs.Stackframe res tf sp pc' rs :: ts) tf' rs ## args m) ; split ; eauto.
  eapply RTLdfs.exec_Icall ; eauto.
  eauto with valagree.
  constructor; auto.
  constructor ; eauto.
  try_succ f pc pc'.

  (* itailcall *)
  destruct ros.
  exploit spec_ros_r_find_function ; eauto.
  intros. destruct H1 as [tf' [Hfind OKtf']].

  exploit instr_at; eauto; intros.
  exploit find_function_preserved_same ; eauto.
  intros.
  exists (RTLdfs.Callstate ts tf' rs##args m');  split ; eauto.
  eapply RTLdfs.exec_Itailcall ; eauto with valagree.
  replace (RTLdfs.fn_stacksize tf) with (fn_stacksize f); eauto with valagree.

  exploit spec_ros_id_find_function ; eauto.
  intros. destruct H1 as [tf' [Hfind OKtf']].

  exploit instr_at; eauto; intros.
  exists (RTLdfs.Callstate ts tf' rs##args m');  split ; eauto.
  eapply RTLdfs.exec_Itailcall ; eauto with valagree.
  replace (RTLdfs.fn_stacksize tf) with (fn_stacksize f); eauto with valagree.

  (* ibuiltin *)
  exploit instr_at; eauto; intros.
  exists (RTLdfs.State ts tf sp pc' (regmap_setres res vres rs) m') ; split ; eauto.
  eapply RTLdfs.exec_Ibuiltin with (vargs:= vargs) ; eauto.
  eapply eval_builtin_args_preserved with (2:= H0); eauto with valagree.
  eapply external_call_symbols_preserved; eauto with valagree.

  constructor; auto. try_succ f pc pc'.

  (* ifso *)

  exploit instr_at; eauto; intros.
  destruct b.
  exists (RTLdfs.State ts tf sp ifso rs m); split ; eauto.
  eapply RTLdfs.exec_Icond ; eauto.
  constructor; auto.
  try_succ f pc ifso.

  (* ifnot *)
  exploit instr_at; eauto; intros.
  exists (RTLdfs.State ts tf sp ifnot rs m); split ; eauto.
  eapply RTLdfs.exec_Icond ; eauto.
  constructor; auto.
  try_succ f pc ifnot.

  (* ijump *)
  exploit instr_at; eauto; intros.
  exists (RTLdfs.State ts tf sp pc' rs m); split ; eauto.
  eapply RTLdfs.exec_Ijumptable ; eauto.
  constructor; auto.
  try_succ f pc pc'.
  eapply list_nth_z_in; eauto.

  (* ireturn *)
  exploit instr_at; eauto; intros.
  exists (RTLdfs.Returnstate ts (regmap_optget or Vundef rs) m'); split ; eauto.
  eapply RTLdfs.exec_Ireturn ; eauto.
  rewrite <- H0 ; eauto with valagree.
  rewrite stacksize_preserved with f tf ; eauto.

  (* internal *)
  simpl in SPEC. monadInv SPEC. simpl in STACK.
  exists (RTLdfs.State ts x
    (Vptr stk Ptrofs.zero)
    x.(RTLdfs.fn_entrypoint)
    (init_regs args x.(RTLdfs.fn_params))
    m').
  split.
  eapply RTLdfs.exec_function_internal; eauto.
  rewrite stacksize_preserved with f x in H ; auto.
  replace (RTL.fn_entrypoint f) with (RTLdfs.fn_entrypoint x).
  replace (RTL.fn_params f) with (RTLdfs.fn_params x).

  econstructor ; eauto.
  replace (RTLdfs.fn_entrypoint x) with (fn_entrypoint f).
  eapply Rstar_refl ; eauto.
  monadInv EQ. auto.
  monadInv EQ. auto.
  monadInv EQ. auto.

  (* external *)
  inv SPEC.
  exists (RTLdfs.Returnstate ts res m'). split.
  eapply RTLdfs.exec_function_external; eauto.
  eapply external_call_symbols_preserved; eauto with valagree.
  econstructor ; eauto.

  (* return state *)
  inv STACK.
  exists (RTLdfs.State ts0 tf sp pc (rs# res <- vres) m);
    split; ( try constructor ; eauto).
Qed.

Theorem transf_program_correct:
  forward_simulation (RTL.semantics prog) (RTLdfs.semantics tprog).
Proof.
  eapply forward_simulation_step.
  eapply senv_preserved.
  eexact transf_initial_states.
  eexact transf_final_states.
  exact transl_step_correct.
Qed.

End PRESERVATION.