Module KildallComp


Require Import Coqlib.
Require Import Iteration.
Require Import Maps.
Require Import Lattice.
Require Import Kildall.
Require Import Classical.

Section CORRECTNESS.

Lemma add_successors_correct2:
  forall tolist from pred n s,
    ~ (In n pred!!!s) -> (~In s tolist \/ n<>from) ->
    ~ In n (add_successors pred from tolist)!!!s.
Proof.
  induction tolist; simpl; intros.
  - tauto.
  - apply IHtolist.
    * intro.
      unfold successors_list at 1 in H1.
      { case_eq ((PTree.set a (from :: pred !!! a) pred) ! s);
        [ intros l Hl | intros Hl]; rewrite Hl in *.
        - (* normal case *)
          destruct (peq a s); subst.
          rewrite PTree.gss in Hl. inv Hl. inv H1.
          destruct H0. elim H0. intuition. congruence.
                       elim H0. auto.
                       elim H. auto.
          rewrite PTree.gso in Hl ; auto.
          unfold successors_list in H.
          rewrite Hl in *. intuition.
        - (* error case *) inv H1.
      }
    * destruct H0. left.
      intro. elim H0. intuition.
      intuition.
Qed.
          
Context {A: Type}.
Variable code: PTree.t A.
Variable successors: A -> list positive.

Definition make_preds : PTree.t (list positive) :=
  make_predecessors code successors.

Lemma make_predecessors_correct2_aux :
  forall n i s,
    code ! n = Some i ->
    ~In s (successors i) ->
    ~In n make_preds!!!s.
Proof.
  intros until s. intros Hcode.
  set (P := fun (m:PTree.t A) preds =>
              ~In s (successors i) -> ~In n preds!!!s) in *.
  apply PTree_Properties.fold_rec with (P := P).
 extensionality *)  unfold P; intros.
  apply H0; auto.
 base case *)  red ; unfold successors_list. repeat rewrite PTree.gempty. auto.
 inductive case *)  unfold P; intros.
  eapply add_successors_correct2; eauto.
  destruct (peq n k).
  - inv e.
    left ; auto.
    rewrite Hcode in *. congruence.
  - auto.
Qed.

Lemma make_predecessors_correct2 :
  forall n i s,
    code ! n = Some i ->
    In n make_preds!!!s ->
    In s (successors i).
Proof.
  generalize make_predecessors_correct2_aux ; intro.
  intros.
  assert (Hdecpos:forall (p1 p2: positive), {p1 = p2}+{p1 <> p2}) by decide equality.
  assert (Hin := In_dec Hdecpos s (successors i)).
  destruct Hin; auto.
  exploit H ; eauto. intuition.
Qed.

Lemma make_predecessors_some : forall s l,
  make_preds ! s = Some l ->
  forall p, In p l -> exists i, code ! p = Some i.
Proof.
  unfold make_preds, make_predecessors.
  apply PTree_Properties.fold_rec; intros.
  - rewrite <- H. eapply H0; eauto.
  - rewrite PTree.gempty in H. inv H.
  - destruct (peq k p).
    * subst. rewrite PTree.gss. eauto.
    * rewrite PTree.gso; auto.
      destruct (classic (In p a !!! s \/ p = k /\ In s (successors v))).
      {
        destruct H4 as [Hcase1 | Hcase2].
        - unfold successors_list in *.
          case_eq (a ! s) ; intros.
          * rewrite H4 in *. eapply (H1 s); eauto.
          * rewrite H4 in *. inv Hcase1.
        - inv Hcase2. congruence.
      }
      {
        eelim add_successors_correct2 with (tolist := (successors v)); eauto.
        unfold successors_list. rewrite H2.
        auto.
      }
Qed.


Section make_preds_NoDup.

Lemma add_successors_complete : forall tolist from pred n s,
  In n (add_successors pred from tolist) !!! s ->
  In n pred !!! s \/ n = from /\ In s tolist.
Proof.
  intros tolist. induction tolist; intros.
  - simpl in H. left; assumption.
  - simpl in H. apply IHtolist in H.
    destruct H as [H | [H H0]].
    + unfold successors_list at 1 in H. rewrite PTree.gsspec in H.
      destruct (peq s a).
      * subst. destruct H.
        -- right. split; [|left]; congruence.
        -- left; assumption.
      * fold (pred !!! s) in H. left; assumption.
    + right. split; [|right]; congruence.
Qed.

Definition once {A : Type} eq_dec (x : A) l :=
  (count_occ eq_dec l x = 1)%nat.

Lemma add_successors_NoDup : forall preds from tos s,
  NoDup (preds !!! s) ->
  (In s tos -> ~ In from (preds !!! s) /\ once peq s tos) ->
  NoDup ((add_successors preds from tos) !!! s).
Proof.
  intros. revert dependent preds. induction tos; intros.
  - simpl. assumption.
  - simpl. apply IHtos.
    + unfold successors_list at 1. rewrite PTree.gsspec.
      destruct (peq s a).
      * subst. constructor; [|assumption]. apply H0. left; reflexivity.
      * fold (preds !!! s). assumption.
    + intros. destruct H0 as (H01 & H02); [right; assumption|].
      split.
      * unfold successors_list at 1. rewrite PTree.gso.
        -- fold (preds !!! s). assumption.
        -- intros contra. subst. unfold once in H02. simpl in H02.
           rewrite peq_true in H02. apply (count_occ_In peq) in H1. xomega.
      * unfold once in H02. unfold once. simpl in H02.
        destruct (peq a s).
        -- subst. apply (count_occ_In peq) in H1. xomega.
        -- xomega.
Qed.

Lemma make_preds_NoDup : forall s,
  (forall n i, code ! n = Some i -> In s (successors i) -> once peq s (successors i)) ->
  NoDup (make_preds !!! s).
Proof.
  intros s.
 we prove this statement that works better with induction *)  assert (
    ((forall n i, code ! n = Some i -> In s (successors i) -> once peq s (successors i)) ->
      NoDup (make_preds !!! s)
    ) /\ Forall (fun p => code ! p <> None) (make_preds !!! s)) as Ha.
  {
    unfold make_preds, make_predecessors.
    apply PTree_Properties.fold_rec.
    - intros. destruct H0 as (H01 & H02).
      split.
      + intros. apply H01. intros. rewrite H in H1.
        eapply H0; eassumption.
      + rewrite Forall_forall in H02 |- *. intros. rewrite <- H. auto.
    - unfold successors_list. rewrite PTree.gempty.
      split; constructor.
    - intros. destruct H1 as (H11 & H12).
      split.
      + intros. apply add_successors_NoDup.
        * apply H11. intros. apply (H1 n). rewrite PTree.gso by congruence.
          assumption. assumption.
        * intros. split.
          -- intros contra. rewrite Forall_forall in H12. apply H12 in contra.
             contradiction.
          -- apply (H1 k). rewrite PTree.gss. reflexivity. assumption.
      + rewrite Forall_forall. intros. apply add_successors_complete in H1.
        destruct H1 as [H1|[H2 H3]].
        * rewrite Forall_forall in H12. apply H12 in H1.
          rewrite PTree.gso by congruence. assumption.
        * subst. rewrite PTree.gss. discriminate.
  }
  apply Ha.
Qed.

End make_preds_NoDup.

End CORRECTNESS.

Section FOLD_EQ.

Section fold_eq.
  Variable A B: Type.
  Variable f: B -> positive -> A -> B.
  Variable b0: B.
  Variable m1 m2: PTree.t A.
  Variable Heq: forall i, m1!i = m2!i.

  Lemma fold_eq: PTree.fold f m1 b0 = PTree.fold f m2 b0.
Proof.
    repeat rewrite PTree.fold_spec.
    rewrite (PTree.elements_extensional _ _ Heq); auto.
  Qed.

End fold_eq.

End FOLD_EQ.

Section Pred_Succs.

Lemma same_successors_same_predecessors_aux0 {A B} :
  forall f1 (f2:B->list positive) (m1:PTree.t A) t a,
 (forall i, m1! i = None) ->
  PTree.xfold
    (fun pred pc instr => add_successors pred pc (f1 instr)) a m1 t = t.
Proof.
  induction m1; simpl; auto.
  intros a t T.
  generalize (T xH); destruct o; simpl; try congruence.
  intros _.
  rewrite IHm1_2.
  - rewrite IHm1_1; auto.
    intros i; generalize (T (xO i)); auto.
  - intros i; generalize (T (xI i)); auto.
Qed.

Lemma same_successors_same_predecessors_aux1 {A B} :
  forall f1 f2 (m1:PTree.t A) (m2:PTree.t B) t a,
 (forall i,
    (PTree.map1 f1 m1) ! i =
    (PTree.map1 f2 m2) ! i) ->
  PTree.xfold
    (fun pred pc instr => add_successors pred pc (f1 instr)) a m1 t =
  PTree.xfold
    (fun pred pc instr => add_successors pred pc (f2 instr)) a m2 t.
Proof.
  induction m1; simpl; auto; intros.
  - erewrite same_successors_same_predecessors_aux0; eauto.
    intros i; generalize (H i); simpl.
    rewrite PTree.gmap1.
    destruct (m2!i); simpl; auto.
    destruct i; simpl; congruence.
  - destruct m2.
    + erewrite same_successors_same_predecessors_aux0; eauto.
      erewrite same_successors_same_predecessors_aux0; eauto.
      erewrite same_successors_same_predecessors_aux0; eauto.
      generalize (H xH); destruct o; simpl; try congruence.
      destruct i; auto.
      intros i; generalize (H (xI i)); simpl.
      rewrite PTree.gmap1.
      destruct (m1_2!i); simpl; congruence.
      intros i; generalize (H (xO i)); simpl.
      rewrite PTree.gmap1.
      destruct (m1_1!i); simpl; congruence.
    + rewrite IHm1_1 with (m2:=m2_1); eauto.
      rewrite IHm1_2 with (m2:=m2_2); eauto.
      generalize (H xH).
      simpl.
      destruct o; destruct o0; simpl; try congruence.
      intros T; inv T.
      rewrite IHm1_2 with (m2:=m2_2); eauto.
      intros i; generalize (H (xI i)); simpl; auto.
      intros i; generalize (H (xI i)); simpl; auto.
      intros i; generalize (H (xO i)); simpl; auto.
Qed.

Lemma same_successors_same_predecessors {A B} : forall f1 f2 (m1:PTree.t A) (m2:PTree.t B),
 (forall i,
    (PTree.map1 f1 m1) ! i =
    (PTree.map1 f2 m2) ! i) ->
  make_predecessors m1 f1 = make_predecessors m2 f2.
Proof.
  unfold make_predecessors; intros.
  apply same_successors_same_predecessors_aux1; auto.
Qed.

End Pred_Succs.
Generated by coq2html