Require Import Coqlib. Require Import Maps. Require Import Classical. Require Import Utils. Require Import Relation_Operators. Require Import Relations.Relation_Definitions. Require Import DLib. (** * Formalization of Dominators *) Section Graph. Context {node : Type}. Variable peq : forall x y:node, {x=y}+{x<>y}. Variable cfg : node -> node -> Prop. Variable exit : node -> Prop. Variable entry : node. (** [reached pc] holds if node [pc] is reachable from [entry] *) Definition reached (pc: node) : Prop := (cfg **) entry pc. (** Definition of paths in the CFG of a function *) Inductive pstate : Type := | PState: forall (pc: node), pstate | PStop: pstate. Inductive path_step : pstate -> node -> pstate -> Prop := | step_i: forall pc pc' (CFG : reached pc) (STEP: cfg pc pc'), path_step (PState pc) pc (PState pc') | step_stop: forall pc (CFG : reached pc) (NOSTEP : exit pc), path_step (PState pc) pc PStop. Inductive path : pstate -> list node -> pstate -> Prop := | path_refl : forall s, path s nil s | path_cons : forall s1 t s2 pc s3 (STEP: path_step s1 pc s2) (PATH: path s2 t s3), path s1 (pc::t) s3. Hint Constructors path_step path. (** Useful lemmas about [path] *) Lemma path_app : forall p1 s1 s2 s3 p2, path s1 p1 s2 -> path s2 p2 s3 -> path s1 (p1++p2) s3. Proof. induction p1; intros. inv H. simpl ; auto. simpl. inv H. econstructor ; eauto. Qed. Lemma path_from_ret_nil : forall p s, path PStop p s -> p = nil. Proof. induction p ; intros. auto. inv H ; auto. inv STEP. Qed. Lemma path_from_ret_ret : forall p s, path PStop p s -> s = PStop. Proof. intros. exploit path_from_ret_nil ; eauto. intros. inv H0. inv H. auto. Qed. Lemma in_path_split : forall (pc pc' pc'' : node) (p : list node), path (PState pc) p (PState pc') -> In pc'' p -> exists p' : list node, exists p'' : list node, path (PState pc) p' (PState pc'') /\ ~ In pc'' p' /\ path (PState pc'') (pc'' :: p'') (PState pc'). Proof. induction 1 ; intros. inv H. inv STEP. destruct (peq pc'' pc0). inv e. exists nil ; exists t ; split ; (econstructor ; eauto). inv H0. congruence. exploit IHpath ; eauto. intros [p' [p'' [Hp' [Hnotin Hp'']]]]. exists (pc0::p'). exists p''. split. econstructor 2 ; eauto. econstructor ; eauto. intro Hcont ; inv Hcont ; intuition. exploit path_from_ret_nil ; eauto. intros Heq. inv Heq. inv H0. inv H. exists nil; exists nil. split; (econstructor ; eauto). inv H2. Qed. Lemma in_path_split_app : forall pc pc' pc'' p, path (PState pc) p (PState pc') -> In pc'' p -> exists p', exists p'', path (PState pc) p' (PState pc'') /\ ~ In pc'' p' /\ p = p'++(pc''::p''). Proof. induction 1 ; intros. inv H. inv STEP. destruct (peq pc'' pc0). inv e. clear H0. exists nil. exists t ; split ; econstructor ; eauto. inv H0. congruence. exploit IHpath ; eauto. intros [p' [p'' [Hp' [Hnotin Happ]]]]. rewrite Happ. exists (pc0::p'). exists p''. split. econstructor 2 ; eauto. split. intro Hcont. inv Hcont. elim n ; auto. elim Hnotin ; auto. simpl ; auto. exploit path_from_ret_nil ; eauto. intros. inv H1. inv H. inv H0. exists nil. exists nil. split. econstructor ; eauto. split ; auto. elim H. Qed. Lemma path_first : forall p pc pc', path (PState pc) p (PState pc') -> pc <> pc' -> exists pc'', exists p', path (PState pc) p' (PState pc'') /\ ~ In pc' p' /\ pc'' <> pc' /\ path_step (PState pc'') pc'' (PState pc'). Proof. induction p ; intros; inv H. congruence. assert (a = pc) by (inv STEP; auto). inv H. destruct s2. destruct (peq pc0 pc'). (* peq *) inv e. exists pc. exists nil. split; auto. (* diff *) exploit IHp ; eauto. intros [pc'' [p' [Hp' [Hpc'' [Hdiff Hnotin]]]]]. exists pc''. exists (pc::p'). split ; auto. econstructor ; eauto. split ; auto. intro Hcont. inv Hcont. congruence. elim Hpc'' ; auto. exploit path_from_ret_nil ; eauto. intros Heq ; inv Heq. inv PATH. Qed. Lemma cfg_path : forall pc pc', cfg** pc pc' -> reached pc -> exists p, path (PState pc) p (PState pc'). Proof. intros pc pc' HCFG. eapply (clos_refl_trans_ind node) with (P := fun a b => reached a -> exists p, path (PState a) p (PState b)) ; eauto; intros. clear pc pc' HCFG. exploit H0; eauto; intros [pxy Hpxy]. assert (reached y). eapply rt_trans ; eauto. exploit H2 ; eauto ; intros [pyz Hpyz]. exists (pxy++pyz). eapply path_app; eauto. Qed. Lemma reached_path : forall pc', reached pc' -> exists p, path (PState entry) p (PState pc'). Proof. intros. apply cfg_path; auto. eapply rt_refl ; eauto. Qed. (** Dominance relation: [dom pc pc'] holds if node [pc'] dominates node [pc] *) Inductive dom : node -> node -> Prop := | dom_eq : forall pc, dom pc pc | dom_path : forall pc pc' (RPC' : reached pc') (PATH : forall p, path (PState entry) p (PState pc') -> In pc p), dom pc pc'. Hint Constructors dom. (** Dominance relation is reflexive *) Lemma dom_refl : forall pc, dom pc pc. Proof. intros ; eauto. Qed. (** Dominance relation is transitive *) Lemma dom_trans : forall pc1 pc2 pc3, dom pc1 pc2 -> dom pc2 pc3 -> dom pc1 pc3. Proof. intros; inv H; auto. inv H0. econstructor ; eauto. econstructor ; eauto ; intros. exploit PATH0 ; eauto ; intros. destruct (peq entry pc2). inv e. eelim (PATH nil) ; eauto. exploit in_path_split_app ; eauto. intros. destruct H1 as [p1 [p2 [Hpath [Htrace Happ]]]]. inv Happ. exploit PATH ; eauto. intros. eapply in_app ; eauto. Qed. (** Strict dominance [sdom pc pc'] holds if [pc'] strictly dominates [pc] *) Inductive sdom (pc pc' : node) : Prop := | sdom_intro : forall (DOM : (dom pc pc')) (NEQ : pc <> pc'), sdom pc pc'. (* Useful lemmas about [sdom] and [dom] *) Lemma sdom_spec : forall pc1 pc2, sdom pc1 pc2 -> (dom pc1 pc2) /\ pc1 <> pc2. Proof. intros. inv H ; auto. Qed. Lemma not_sdom_spec : forall pc1 pc2, ~ sdom pc1 pc2 -> (pc1 = pc2) \/ (~ dom pc1 pc2). Proof. intros. destruct (peq pc1 pc2). auto. right. intro Hcont. elim H ; auto. econstructor ; eauto. Qed. Lemma sdom_not_dom : forall pc pc', sdom pc pc' -> ~ dom pc' pc. Proof. intros pc pc' SDOM. inv SDOM. generalize DOM ; inv DOM ; intros DOM. congruence. exploit reached_path ; eauto. intros [ppc' Hppc']. exploit PATH ; eauto. intros. exploit in_path_split ; eauto. intros [p' [p'' [Hp' [Hnotin Happ]]]]. destruct (In_dec peq pc' p'). exploit (in_path_split_app entry pc); eauto. intros [p2 [p3 [Hp'' [Hnotin' Happ']]]]. inv Happ'. exploit PATH ; eauto. intros. elim Hnotin. eapply in_app ; eauto. intro Hcont. inv Hcont. congruence. exploit PATH0 ; eauto. Qed. (** Dominance relation is antisymmetric *) Lemma dom_antisym : forall pc pc', dom pc pc' -> dom pc' pc -> pc = pc'. Proof. intros. case (peq pc pc') ; intros. auto. exploit sdom_not_dom ; eauto. split ; auto. intuition. Qed. (** Strict dominance is transitive *) Lemma sdom_trans : forall pc1 pc2 pc3, sdom pc1 pc2 -> sdom pc2 pc3 -> sdom pc1 pc3. Proof. intros. inv H. inv H0. econstructor ; eauto. eapply dom_trans; eauto. intro Hcont. inv Hcont. exploit dom_antisym ; eauto. Qed. Lemma dom_sdom_trans : forall pc1 pc2 pc3, dom pc1 pc2 -> sdom pc2 pc3 -> sdom pc1 pc3. Proof. intros. destruct (peq pc1 pc2). inv e. auto. eapply sdom_trans; eauto. econstructor ; eauto. Qed. (** Dominance relation is an order *) Lemma dom_order : order node dom. Proof. constructor. exact dom_refl. exact dom_trans. exact dom_antisym. Qed. (** Other utility lemmas about (strict) dominance *) Lemma sdom_dom_pred : forall pc pc' pc'', sdom pc pc'' -> reached pc' -> cfg pc' pc'' -> dom pc pc'. Proof. intros. destruct (peq pc pc'). - inv e ; econstructor ; eauto. - econstructor ; eauto. intros. inv H. inv DOM; try congruence. exploit (PATH (p++(pc'::nil))). + eapply path_app; eauto. + rewrite in_app_iff; destruct 1; auto. simpl in H; destruct H; intuition. Qed. Lemma dom_eq_sdom : forall pc pc', dom pc pc' -> pc = pc' \/ sdom pc pc'. Proof. intros. destruct (peq pc pc'). inv e ; auto. right. inv H. congruence. constructor ; auto. Qed. Lemma entry_dom : forall pc, reached pc -> dom entry pc. Proof. intros. destruct (peq pc entry). inv e ; constructor ; auto. constructor; auto. intros. inv H0. congruence. inv STEP ; eauto. Qed. Lemma dom_entry : forall pc, dom pc entry -> pc = entry. Proof. intros. destruct (peq pc entry). inv e ; constructor ; auto. inv H. congruence. exploit (PATH nil) ; eauto. intros. inv H. Qed. Lemma entry_sdom : forall pc, ~ sdom pc entry. Proof. intros. intro Hcont. inv Hcont. exploit dom_entry ; eauto. Qed. Lemma not_dom_path_wo : forall pc pc', ~ dom pc pc' -> reached pc' -> (exists p, path (PState entry) p (PState pc') /\ ~ In pc p). Proof. intros. destruct (peq pc pc'). inv e. elim H ; econstructor ; eauto. eelim (classic (exists p, path (PState entry) p (PState pc') /\ ~ In pc p)); intros. eauto. elim H. econstructor ; eauto. intros. destruct (In_dec peq pc p); auto. eelim H1. exists p ; eauto. Qed. Lemma sdom_dom_trans : forall pc1 pc2 pc3, sdom pc1 pc2 -> dom pc2 pc3 -> sdom pc1 pc3. Proof. intros. destruct (peq pc2 pc3). - go. - eapply sdom_trans; go. Qed. Lemma elim_sdom_sdom : forall pc1 pc2, sdom pc1 pc2 -> sdom pc2 pc1 -> False. Proof. intros; repeat invh sdom. exploit dom_antisym; eauto. Qed. End Graph.