Module RTLPaths

Definitions and lemmas related to paths in the CFG of a well-formed function.

Require Import Bool.
Require Import Arith.
Require Import List.
Require Import BinPos.

Require Import Coqlib.
Require Import Maps.
Require Import Registers.
Require Import RTL.
Require Import Errors.

Require Import UtilTacs.
Require Import UtilLemmas.
Require Import UtilBase.
Require Import Utils.
Require Import RTLutils.
Require Import RTLWfFunction.
Require Import RTLReaches.
Require Import RTLReachesproof.

Section FUNCTION.

  Variable f : function.

  Definition succ_node (n s : node) : Prop :=
    exists i, f.(fn_code) ! n = Some i /\ In s (successors_instr i).

  Inductive reaches : node -> node -> Prop :=
  | r_refl : forall n, f_In n f -> reaches n n
  | r_succ : forall n n' n'', reaches n' n'' -> succ_node n n' -> reaches n n''.

End FUNCTION.

Section CHECKER.

Proof of the properties ensured by the checker related to well-formed functions.

  Variable f : function.
  Variable exit_n : node.
  Variable reg_vint : reg.
  Hypothesis WFF: check_wf f = OK (exit_n, reg_vint).

  Ltac PrepareWf WFF :=
    intros;
    unfold check_wf in WFF;
    let CONDS := fresh in
    optDecN WFF CONDS; trim;
    monadInv WFF;
    boolrw;
    destruct CONDS as [[ACC ENTRY] REACH].
  
  Lemma wf_acc:
    forall n s,
      succ_node f n s -> f_In s f.
Proof.
    PrepareWf WFF.
    unfolds in ACC.
    unfold succ_node in H.
    destruct H as [i [INST SUCC]].
    apply ptree_forall with (i := n) (x := i) in ACC; auto.
    rewrite forallb_forall in ACC.
    apply ACC in SUCC.
    unfold Pmem in SUCC.
    unfold f_In.
    intro.
    rewrite H in SUCC; trim.
  Qed.

  Lemma wf_entry:
    forall n,
      ~ succ_node f n f.(fn_entrypoint).
Proof.
    PrepareWf WFF.
    unfolds in ENTRY.
    intro.
    unfold succ_node in H.
    destruct H as [i [INST SUCC]].
    apply ptree_forall with (i := n) (x := i) in ENTRY; auto.
    rewrite forallb_forall in ENTRY.
    apply ENTRY in SUCC.
    rewrite negb_true_iff in SUCC.
    unfolds in SUCC. optDec SUCC; trim.
  Qed.

  Lemma wf_entry_in:
    f_In f.(fn_entrypoint) f.
Proof.
    PrepareWf WFF.
    unfolds in EQ1.
    optDecN EQ1 IN; trim.
  Qed.

  Lemma reaches_app:
    forall n n' n'',
      reaches f n n' ->
      succ_node f n' n'' ->
      reaches f n n''.
Proof.
    induction 1; intros.
    eapply r_succ; eauto.
    apply r_refl.
    eapply wf_acc; eauto.
    apply r_succ with (n' := n'); auto.
  Qed.

  Lemma cfg_star_f_In:
    forall n n',
      f_In n f ->
      cfg_star (fn_code f) n n' ->
      f_In n' f.
Proof.
    induction 2; intros; auto.
    apply wf_acc with (n := j).
    inv H1.
    eexists; eauto.
  Qed.

  Lemma cfg_star_reaches:
    forall n n',
      f_In n f ->
      cfg_star (fn_code f) n n' ->
      reaches f n n'.
Proof.
    induction 2; intros.
    apply r_refl; auto.
    assert (FIN: f_In j f).
      apply cfg_star_f_In with (n := n); auto.
    apply reaches_app with (n' := j); auto.
    inv H1; eexists; eauto.
  Qed.

  Lemma wf_entry_acc_allin:
    forall f' seen tf',
      RTLReaches.transf_function f = OK (seen, tf') ->
      forall_ptree (fun p i => TheoryList.mem positive_eq_dec p seen) f'.(fn_code) = true ->
      forall i ins, (fn_code f') ! i = Some ins -> In i seen.
Proof.
    intros.
    apply forall_ptree_true with (i := i) (x := ins) in H0; auto.
    apply mem_iff_In in H0; auto.
  Qed.

  Lemma wf_entry_acc:
    forall n,
      f_In n f -> reaches f f.(fn_entrypoint) n.
Proof.
    PrepareWf WFF.
    unfold wf_entry_acc in REACH.
    optDecN REACH TF; trim.
    destruct p; simpls.
    case_eq ((fn_code f) ! n); introsv INST; trim.
    eapply transf_function_cfg_star in INST; eauto.
    apply cfg_star_reaches in INST; auto.
    apply wf_entry_in.
    intros.
    eapply wf_entry_acc_allin; eauto.
  Qed.

End CHECKER.

Section CHECKED.

  Variable f : function.
  Variable exit_n : node.
  Variable reg_vint : reg.
  Hypothesis WFF: check_wf f = OK (exit_n, reg_vint).
  Notation reaches := (reaches f).
  Notation succ_node' := (succ_node f).

  Lemma succ_f_In:
    forall n n',
      succ_node' n n' -> f_In n f.
Proof.
    unfold succ_node, f_In; intros.
    decs H. intro; trim.
  Qed.

  Lemma succ_f_In':
    forall n n',
      succ_node' n n' -> f_In n' f.
Proof.
    intros.
    eapply wf_acc; eauto.
  Qed.

  Lemma f_In_ex:
    forall n f,
      f_In n f ->
      exists i, f.(fn_code) ! n = Some i.
Proof.
    intros.
    unfolds in H.
    case_eq (fn_code f0) ! n; intros; trim.
    exists i; auto.
  Qed.

  Lemma reaches_f_In:
    forall n n',
      reaches n n' -> f_In n f -> f_In n' f.
Proof.
    induction 1; intros; auto.
    apply IHreaches.
    eapply succ_f_In'; eauto.
  Qed.

  Lemma entry_in:
    f_In f.(fn_entrypoint) f.
Proof.
    eapply wf_entry_in; eauto.
  Qed.

  Inductive path : node -> list node -> node -> Prop :=
  | p_nil : forall n, f_In n f -> path n nil n
  | p_cons : forall nl n n' n'', path n' nl n'' -> succ_node' n n' -> path n (n :: nl) n''.

  Lemma path_f_In:
    forall el n n',
      path n el n' ->
      f_In n f.
Proof.
    intros.
    inv H; trim.
    apply succ_f_In in H1; asmp.
  Qed.

  Lemma path_f_In':
    forall el n n',
      path n el n' ->
      f_In n' f.
Proof.
    induction el; intros.
    inv H; auto.
    inv H; trim.
    eapply IHel; eauto.
  Qed.

  Lemma path_app:
    forall el n n' n'',
      path n el n' ->
      succ_node' n' n'' ->
      f_In n'' f ->
      path n (el ++ n' :: nil) n''.
Proof.
    induction el; intros; simpl.
    inv H.
    eapply p_cons; eauto.
    apply p_nil; auto.
    inv H.
    eapply p_cons; eauto.
  Qed.

  Lemma path_app_split:
    forall el el' n n' n'',
      path n (el ++ n' :: el') n'' ->
      path n el n' /\
      path n' (n' :: el') n''.
Proof.
    induction el; intros; simpls.
    inv H.
    split.
    apply p_nil. apply succ_f_In in H5; auto.
    apply p_cons with (n' := n'0); auto.
    inv H.
    apply IHel in H3. destruct H3.
    split; auto.
    apply p_cons with (n' := n'0); auto.
  Qed.

  Lemma in_path_split:
    forall el n n'
      (PATH: path n el n'),
      forall n'',
        In n'' el ->
        exists el', exists el'',
                      el = el' ++ el'' /\
                      path n el' n'' /\ path n'' el'' n'.
Proof.
    induction el; intros; trim.
    inv_clear PATH.
    subst n''0 n0 nl n.
    destruct H.
    subst n''.
    exists nil.
    exists (a :: el).
    split; auto.
    split.
    apply p_nil. eapply succ_f_In; eauto.
    eapply p_cons; eauto.
    eapply IHel in H; eauto.
    decs H.
    exists (a :: x).
    exists x0.
    split.
    rewrite H0; auto.
    split; auto.
    eapply p_cons; eauto.
  Qed.

  Inductive rev_path : node -> list node -> node -> Prop :=
  | r_nil : forall n, f_In n f -> rev_path n nil n
  | r_cons : forall rl n' n n'', rev_path n' rl n -> succ_node' n' n'' -> rev_path n'' (n' :: rl) n.

  Lemma rev_path_app_last:
    forall el n' n n'',
      rev_path n'' el n' ->
      succ_node' n n' ->
      rev_path n'' (el ++ (n :: nil)) n.
Proof.
    induction el; intros.
    inv H. apply r_cons; auto. apply r_nil. apply succ_f_In in H0; auto.
    inv H. apply IHel with (n := n) in H4; auto.
    simpl. apply r_cons; auto.
  Qed.

  Lemma rev_path_app:
    forall el1 el2 n' n n'',
      rev_path n'' el1 n' ->
      rev_path n' el2 n ->
      rev_path n'' (el1 ++ el2) n.
Proof.
    induction el1; intros; simpl; inv H; auto.
    apply r_cons; auto.
    eapply IHel1; eauto.
  Qed.

  Lemma path_rev_path_1:
    forall el n n',
      path n el n' -> rev_path n' (rev el) n.
Proof.
    induction el; intros.
    inv H. apply r_nil; auto.
    inv H. simpl. apply rev_path_app_last with (n' := n'0); auto.
  Qed.

  Lemma path_rev_path_2:
    forall el n n',
      rev_path n' el n -> path n (rev el) n'.
Proof.
    induction el; intros.
    inv H. simpl. apply p_nil; auto.
    inv H. simpl. apply IHel in H3.
    apply path_app; auto.
    eapply succ_f_In'; eauto.
  Qed.
  
  Lemma path_rev_path:
    forall el n n',
      path n el n' <-> rev_path n' (rev el) n.
Proof.
    intros; split; intros.
    apply path_rev_path_1; auto.
    assert (REV: rev (rev el) = el) by (apply rev_involutive).
    rewrite <- REV.
    apply path_rev_path_2; auto.
  Qed.

  Lemma rev_path_f_In:
    forall rl n n',
      rev_path n' rl n ->
      f_In n f.
Proof.
    intros.
    apply path_rev_path_2 in H.
    apply path_f_In in H; auto.
  Qed.

  Lemma rev_path_f_In':
    forall rl n n',
      rev_path n' rl n ->
      f_In n' f.
Proof.
    intros.
    apply path_rev_path_2 in H.
    apply path_f_In' in H; auto.
  Qed.

  Ltac revPath rl PATH :=
    assert (REV: rev (rev rl) = rl) by (apply rev_involutive); rewrite <- REV in PATH; apply path_rev_path in PATH.
  
  Lemma in_rev_path_split:
    forall rl n n'
      (PATH: rev_path n' rl n),
      forall n'',
        In n'' rl ->
        exists rl', exists rl'',
                      rl = rl'' ++ rl' /\
                      rev_path n'' rl' n /\ rev_path n' rl'' n''.
Proof.
    intros.
    revPath rl PATH.
    apply in_path_split with (n'' := n'') in PATH; auto.
    decs PATH.
    apply path_rev_path in H1.
    apply path_rev_path in H3.
    exists (rev x).
    exists (rev x0).
    split. rewrite <- rev_app_distr. rewrite <- H0; auto.
    split; auto.
    apply in_rev.
    rewrite rev_involutive; auto.
  Qed.

  Lemma rev_path_app_split:
    forall rl rl' a b n n'
      (PATH: rev_path n' (rl' ++ b :: a :: rl) n),
      rev_path n' (rl' ++ b :: nil) b /\
      succ_node f a b /\
      rev_path a rl n.
Proof.
    intros.
    apply path_rev_path_2 in PATH.
    rewrite rev_app_distr in PATH.
    simpls.
    rewrite <- app_assoc in PATH.
    rewrite app_singleton in PATH.
    rewrite app_cons_nil_cons in PATH.
    apply path_app_split in PATH.
    destruct PATH as [P1 P2].
    apply path_rev_path in P1.
    rewrite rev_involutive in P1.
    inv P2.
    assert (n'0 = b).
      inv H0; auto.
    subst n'0.
    apply path_rev_path in H0. simpls.
    rewrite rev_involutive in H0.
    split; auto.
  Qed.

  Lemma rev_path_app_split':
    forall rl rl' a n n'
      (PATH: rev_path n' (rl' ++ a :: rl) n),
      rev_path n' (rl' ++ a :: nil) a /\
      rev_path a rl n.
Proof.
    intros.
    apply path_rev_path_2 in PATH.
    rewrite rev_app_distr in PATH.
    simpls.
    rewrite <- app_assoc in PATH.
    rewrite app_singleton in PATH.
    apply path_app_split in PATH.
    destruct PATH as [P1 P2].
    apply path_rev_path in P1.
    rewrite rev_involutive in P1.
    apply path_rev_path in P2. simpls.
    rewrite rev_involutive in P2.
    split; auto.
  Qed.

  Lemma rev_path_app_split_last:
    forall
      rl' rl n' n def
      (NNIL: rl' <> nil)
      (PATH: rev_path n' (rl' ++ rl) n),
      rev_path n' rl' (last rl' def) /\
      rev_path (last rl' def) rl n.
Proof.
    induction rl'; intros; trim.
    destruct rl'.
    simpls.
    inv_clear PATH; subst n0 n'0 n'' rl0.
    split; auto.
    apply r_cons; auto. apply r_nil.
    apply succ_f_In in H4; auto.
    inv_clear PATH. subst n1 n'0 n'' rl0.
    apply IHrl' with (def := def) in H2; trim.
    destruct H2.
    split; auto.
    apply r_cons; auto.
  Qed.

  Lemma succ_node_in_succs:
    forall n s,
      succ_node f n s ->
      exists i,
        f.(fn_code) ! n = Some i /\
        exists l,
          (successors f) ! n = Some l /\
          In s l.
Proof.
    unfold succ_node.
    intros.
    decs H.
    eexists; intuition; eauto.
    unfold successors.
    rewrite PTree.gmap1.
    unfold option_map.
    rewrite H1.
    eexists; eauto.
  Qed.

  Fixpoint path_edges_aux (src : node) (l : list node) (dst : node) : list (node * node) :=
    match l with
      | nil => (src, dst) :: nil
      | n :: r => (src, n) :: (path_edges_aux n r dst)
    end.

  Definition path_edges (l : list node) (dst : node) : list (node * node) :=
    match l with
      | nil => nil
      | n :: r => path_edges_aux n r dst
    end.

  Lemma path_edges_aux_succ:
    forall l n n',
      path n (n :: l) n' ->
      forall e,
        In e (path_edges_aux n l n') ->
        succ_node' (fst e) (snd e).
Proof.
    induction l; intros.
    inv H.
    simpls. destruct H0; trim.
    inv H; simpl.
    inv H2; trim.
    inv H; simpls.
    destruct H0; subst; simpls.
    inv H2; trim.
    inv H2.
    eapply IHl; eauto.
    eapply p_cons; eauto.
  Qed.

  Lemma in_path_edges_cons:
    forall el n n' n'',
      In (n, n') (path_edges el n'') ->
      forall n''',
        In (n, n') (path_edges (n''' :: el) n'').
Proof.
    induction el; intros; simpls; auto.
  Qed.

  Lemma rev_path_in_split:
    forall rl n n',
      rev_path n rl n' ->
      forall n'',
        In n'' rl ->
        exists rl1, exists rl2,
          rl = rl1 ++ rl2 /\
          rev_path n rl1 n'' /\
          rev_path n'' rl2 n'.
Proof.
    induction rl; intros; trim.
    destruct H0.
    subst.
    inv H.
    exists (n'' :: nil).
    exists rl. intuition.
    apply r_cons; auto. apply r_nil; auto.
    eapply succ_f_In; eauto.
    inv H.
    gen (IHrl _ _ H4 _ H0) as EX.
    decs EX; subst.
    exists (a :: x). exists x0.
    intuition.
    apply r_cons; auto.
  Qed.

  Lemma in_cycle_any:
    forall rl n,
      rev_path n rl n ->
      forall n', In n' rl ->
        exists rl', rev_path n' rl' n' /\ forall n'', In n'' rl <-> In n'' rl'.
Proof.
    intros.
    apply rev_path_in_split with (n'' := n') in H; auto.
    decs H.
    exists (x0 ++ x).
    split.
    eapply rev_path_app; eauto.
    intros.
    subst; split; intros.
    apply in_app in H. destruct H; apply in_app; auto.
    apply in_app in H. destruct H; apply in_app; auto.
  Qed.


  Notation list_prefix := (list_prefix positive).

  Lemma path_prefix_ex:
    forall l n n',
      path n l n' ->
      forall p,
        list_prefix p l ->
        exists n'',
          path n p n''.
Proof.
    induction l; intros.
    apply list_prefix_nil in H0.
    subst; simpl. inv H. exists n'; apply p_nil; auto.
    inv H.
    apply list_prefix_cons_ex in H0. destruct H0; subst; simpls.
    exists a; apply p_nil. eapply succ_f_In; eauto.
    decs H; subst.
    apply IHl with (p := x) in H4; auto.
    decs H4.
    eexists; eapply p_cons; eauto.
  Qed.

  Lemma path_prefix_nnil:
    forall l n n',
      path n l n' ->
      forall p,
        p <> nil ->
        list_prefix p l ->
        forall n'',
          succ_node' (last p n') n'' ->
          path n p n''.
Proof.
    induction l; intros; simpls; trim.
    destruct p; trim.
    destruct p; trim. clear H0.
    inv H.
    simpl in H1; destruct H1.
    subst.
    destruct p0.
    apply p_cons with (n' := n''); auto. apply p_nil. eapply succ_f_In'; eauto.
    assert (NNIL: p :: p0 <> nil) by trim.
    assert (S: succ_node' (last (p :: p0) n') n'') by auto.
    gen (IHl _ _ H5 (p :: p0) NNIL H0 n'' S).
    apply p_cons with (n' := n'0); auto.
  Qed.

  Lemma path_prefix_removelast:
    forall l n n',
      path n l n' ->
      forall p,
        p <> nil ->
        list_prefix p l ->
        path n (removelast p) (last p n').
Proof.
    induction l; intros; simpls; trim.
    destruct p; trim.
    destruct p; trim. clear H0.
    inv H.
    simpl in H1; destruct H1.
    subst.
    destruct p0.
    simpl. apply p_nil. eapply succ_f_In; eauto.
    assert (NNIL: p :: p0 <> nil) by trim.
    gen (IHl _ _ H4 (p :: p0) NNIL H0).
    apply p_cons with (n' := n'0); auto.
  Qed.

  Lemma list_prefix_rev_path:
    forall rl n n',
      rev_path n' rl n ->
      forall sl,
        list_prefix sl rl ->
        rev_path n' sl (last sl n').
Proof.
    induction rl; intros.
    apply list_prefix_nil in H0; subst.
    simpl. apply r_nil. inv H. asmp.
    inv H.
    destruct sl; simpl. apply r_nil. eapply succ_f_In'; eauto.
    inv H0.
    apply IHrl with (sl := sl) in H4; auto.
    apply r_cons; auto.
    destruct sl; simpl.
    apply r_nil. eapply succ_f_In; eauto.
    rewrite last_not_nil with (d' := n') in H4.
    apply H4.
  Qed.

  Lemma reaches_trans:
    forall n n' n'',
      reaches n n' ->
      reaches n' n'' ->
      reaches n n''.
Proof.
    intros.
    generalize dependent n''.
    induction H; intros; auto.
    apply IHreaches in H1.
    apply r_succ with (n' := n'); auto.
  Qed.

End CHECKED.

Generated by coq2html