From 0053b1aa1d26da5d1f995a603b127daf799c2da9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 21 May 2012 16:26:30 +0000 Subject: Merge of the newmem branch: - Revised memory model with Max and Cur permissions, but without bounds - Constant propagation of 'const' globals - Function inlining at RTL level - (Unprovable) elimination of unreferenced static definitions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1899 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Postorder.v | 316 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 316 insertions(+) create mode 100644 lib/Postorder.v (limited to 'lib/Postorder.v') diff --git a/lib/Postorder.v b/lib/Postorder.v new file mode 100644 index 00000000..fe06da77 --- /dev/null +++ b/lib/Postorder.v @@ -0,0 +1,316 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Postorder numbering of a directed graph. *) + +Require Import Wellfounded. +Require Import Coqlib. +Require Import Maps. +Require Import Iteration. + +(** The graph is presented as a finite map from nodes (of type [positive]) + to the lists of their successors. *) + +Definition node: Type := positive. + +Definition graph: Type := PTree.t (list node). + +(** The traversal is presented as an iteration that modifies the following state. *) + +Record state : Type := mkstate { + gr: graph; (**r current graph, without already-visited nodes *) + wrk: list (node * list node); (**r worklist *) + map: PTree.t positive; (**r current mapping node -> postorder number *) + next: positive (**r number to use for next numbering *) +}. + +Definition init_state (g: graph) (root: node) := + match g!root with + | Some succs => + {| gr := PTree.remove root g; + wrk := (root, succs) :: nil; + map := PTree.empty positive; + next := 1%positive |} + | None => + {| gr := g; + wrk := nil; + map := PTree.empty positive; + next := 1%positive |} + end. + +Definition transition (s: state) : PTree.t positive + state := + match s.(wrk) with + | nil => + inl _ s.(map) + | (x, nil) :: l => + inr _ {| gr := s.(gr); wrk := l; map := PTree.set x s.(next) s.(map); next := Psucc s.(next) |} + | (x, y :: succs_x) :: l => + match s.(gr)!y with + | None => + inr _ {| gr := s.(gr); wrk := (x, succs_x) :: l; map := s.(map); next := s.(next) |} + | Some succs_y => + inr _ {| gr := PTree.remove y s.(gr); wrk := (y, succs_y) :: (x, succs_x) :: l; map := s.(map); next := s.(next) |} + end + end. + +Section POSTORDER. + +Variable ginit: graph. +Variable root: node. + +Inductive invariant (s: state) : Prop := + Invariant + (* current graph is a subset of ginit *) + (SUB: forall x y, s.(gr)!x = Some y -> ginit!x = Some y) + (* root is not in current graph *) + (ROOT: s.(gr)!root = None) + (* mapped nodes have their numbers below next *) + (BELOW: forall x y, s.(map)!x = Some y -> Plt y s.(next)) + (* mapping is injective *) + (INJ: forall x1 x2 y, s.(map)!x1 = Some y -> s.(map)!x2 = Some y -> x1 = x2) + (* nodes not yet visited have no number *) + (REM: forall x y, s.(gr)!x = Some y -> s.(map)!x = None) + (* black nodes have no white son *) + (COLOR: forall x succs n y, + ginit!x = Some succs -> s.(map)!x = Some n -> + In y succs -> s.(gr)!y = None) + (* worklist is well-formed *) + (WKLIST: forall x l, In (x, l) s.(wrk) -> + s.(gr)!x = None /\ + exists l', ginit!x = Some(l' ++ l) + /\ forall y, In y l' -> s.(gr)!y = None) + (* all grey nodes are on the worklist *) + (GREY: forall x, ginit!x <> None -> s.(gr)!x = None -> s.(map)!x = None -> + exists l, In (x,l) s.(wrk)). + +Inductive postcondition (map: PTree.t positive) : Prop := + Postcondition + (INJ: forall x1 x2 y, map!x1 = Some y -> map!x2 = Some y -> x1 = x2) + (ROOT: ginit!root <> None -> map!root <> None) + (SUCCS: forall x succs y, ginit!x = Some succs -> map!x <> None -> In y succs -> ginit!y <> None -> map!y <> None). + +Lemma transition_spec: + forall s, invariant s -> + match transition s with inr s' => invariant s' | inl m => postcondition m end. +Proof. + intros. inv H. unfold transition. destruct (wrk s) as [ | [x succ_x] l]. + (* finished *) + constructor; intros. + eauto. + caseEq (s.(map)!root); intros. congruence. exploit GREY; eauto. intros [? ?]; contradiction. + destruct (s.(map)!x) as []_eqn; try congruence. + destruct (s.(map)!y) as []_eqn; try congruence. + exploit COLOR; eauto. intros. exploit GREY; eauto. intros [? ?]; contradiction. + (* not finished *) + destruct succ_x as [ | y succ_x ]. + (* all children of x were traversed *) + constructor; simpl; intros. + (* sub *) + eauto. + (* root *) + eauto. + (* below *) + rewrite PTree.gsspec in H. destruct (peq x0 x). inv H. + apply Plt_succ. + apply Plt_trans_succ. eauto. + (* inj *) + rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0. + destruct (peq x1 x); destruct (peq x2 x); subst. + auto. + inv H. exploit BELOW; eauto. intros. eelim Plt_strict; eauto. + inv H0. exploit BELOW; eauto. intros. eelim Plt_strict; eauto. + eauto. + (* rem *) + intros. rewrite PTree.gso; eauto. red; intros; subst x0. + exploit (WKLIST x nil); auto with coqlib. intros [A B]. congruence. + (* color *) + rewrite PTree.gsspec in H0. destruct (peq x0 x). + inv H0. exploit (WKLIST x nil); auto with coqlib. + intros [A [l' [B C]]]. rewrite app_nil_r in B. + assert (l' = succs) by congruence. subst l'. eauto. + eauto. + (* wklist *) + apply WKLIST. auto with coqlib. + (* grey *) + rewrite PTree.gsspec in H1. destruct (peq x0 x). inv H1. + exploit GREY; eauto. intros [l' A]. simpl in A; destruct A. + congruence. + exists l'; auto. + + (* children y needs traversing *) + destruct ((gr s)!y) as [ succs_y | ]_eqn. + (* y has children *) + constructor; simpl; intros. + (* sub *) + rewrite PTree.grspec in H. destruct (PTree.elt_eq x0 y); eauto. inv H. + (* root *) + rewrite PTree.gro. auto. congruence. + (* below *) + eauto. + (* inj *) + eauto. + (* rem *) + rewrite PTree.grspec in H. destruct (PTree.elt_eq x0 y); eauto. inv H. + (* color *) + rewrite PTree.grspec. destruct (PTree.elt_eq y0 y); eauto. + (* wklist *) + destruct H. + inv H. split. apply PTree.grs. exists (@nil positive); simpl; intuition. + destruct H. + inv H. exploit WKLIST; eauto with coqlib. intros [A [l' [B C]]]. + split. rewrite PTree.grspec. destruct (PTree.elt_eq x0 y); auto. + exists (l' ++ y :: nil); split. rewrite app_ass. auto. + intros. rewrite in_app_iff in H. simpl in H. intuition. + rewrite PTree.grspec. destruct (PTree.elt_eq y0 y); auto. + subst y0. apply PTree.grs. + exploit (WKLIST x0 l0); eauto with coqlib. intros [A [l' [B C]]]. + split. rewrite PTree.grspec. destruct (PTree.elt_eq x0 y); auto. + exists l'; split; auto. intros. + rewrite PTree.grspec. destruct (PTree.elt_eq y0 y); auto. + (* grey *) + rewrite PTree.grspec in H0. destruct (PTree.elt_eq x0 y) in H0. + subst. exists succs_y; auto with coqlib. + exploit GREY; eauto. simpl. intros [l1 A]. destruct A. + inv H2. exists succ_x; auto. + exists l1; auto. + + (* y has no children *) + constructor; simpl; intros; eauto. + (* wklist *) + destruct H. inv H. + exploit (WKLIST x0); eauto with coqlib. intros [A [l' [B C]]]. + split. auto. exists (l' ++ y :: nil); split. rewrite app_ass; auto. + intros. rewrite in_app_iff in H; simpl in H. intuition. congruence. + eapply WKLIST; eauto with coqlib. + (* grey *) + exploit GREY; eauto. intros [l1 A]. simpl in A. destruct A. + inv H2. exists succ_x; auto. + exists l1; auto. +Qed. + +Lemma initial_state_spec: + invariant (init_state ginit root). +Proof. + unfold init_state. destruct (ginit!root) as [succs|]_eqn. + (* root has succs *) + constructor; simpl; intros. + (* sub *) + rewrite PTree.grspec in H. destruct (PTree.elt_eq x root). inv H. auto. + (* root *) + apply PTree.grs. + (* below *) + rewrite PTree.gempty in H; inv H. + (* inj *) + rewrite PTree.gempty in H; inv H. + (* rem *) + apply PTree.gempty. + (* color *) + rewrite PTree.gempty in H0; inv H0. + (* wklist *) + destruct H; inv H. + split. apply PTree.grs. exists (@nil positive); simpl; tauto. + (* grey *) + rewrite PTree.grspec in H0. destruct (PTree.elt_eq x root). + subst. exists succs; auto. + contradiction. + + (* root has no succs *) + constructor; simpl; intros. + (* sub *) + auto. + (* root *) + auto. + (* below *) + rewrite PTree.gempty in H; inv H. + (* inj *) + rewrite PTree.gempty in H; inv H. + (* rem *) + apply PTree.gempty. + (* color *) + rewrite PTree.gempty in H0; inv H0. + (* wklist *) + contradiction. + (* grey *) + contradiction. + +Qed. + +(** Termination criterion. *) + +Fixpoint size_worklist (w: list (positive * list positive)) : nat := + match w with + | nil => 0%nat + | (x, succs) :: w' => (S (List.length succs) + size_worklist w')%nat + end. + +Definition lt_state (s1 s2: state) : Prop := + lex_ord lt lt (PTree_Properties.cardinal s1.(gr), size_worklist s1.(wrk)) + (PTree_Properties.cardinal s2.(gr), size_worklist s2.(wrk)). + +Lemma lt_state_wf: well_founded lt_state. +Proof. + set (f := fun s => (PTree_Properties.cardinal s.(gr), size_worklist s.(wrk))). + change (well_founded (fun s1 s2 => lex_ord lt lt (f s1) (f s2))). + apply wf_inverse_image. + apply wf_lex_ord. + apply lt_wf. apply lt_wf. +Qed. + +Lemma transition_decreases: + forall s s', transition s = inr _ s' -> lt_state s' s. +Proof. + unfold transition, lt_state; intros. + destruct (wrk s) as [ | [x succs] l]. + discriminate. + destruct succs as [ | y succs ]. + inv H. simpl. apply lex_ord_right. omega. + destruct ((gr s)!y) as [succs'|]_eqn. + inv H. simpl. apply lex_ord_left. eapply PTree_Properties.cardinal_remove; eauto. + inv H. simpl. apply lex_ord_right. omega. +Qed. + +End POSTORDER. + +Definition postorder (g: graph) (root: node) := + WfIter.iterate _ _ transition lt_state lt_state_wf transition_decreases (init_state g root). + +Inductive reachable (g: graph) (root: positive) : positive -> Prop := + | reachable_root: + reachable g root root + | reachable_succ: forall x succs y, + reachable g root x -> g!x = Some succs -> In y succs -> + reachable g root y. + +Theorem postorder_correct: + forall g root, + let m := postorder g root in + (forall x1 x2 y, m!x1 = Some y -> m!x2 = Some y -> x1 = x2) + /\ (forall x, reachable g root x -> g!x <> None -> m!x <> None). +Proof. + intros. + assert (postcondition g root m). + unfold m. unfold postorder. + apply WfIter.iterate_prop with (P := invariant g root). + apply transition_spec. + apply initial_state_spec. + inv H. + split. auto. + induction 1; intros. + (* root case *) + apply ROOT; auto. + (* succ case *) + eapply SUCCS; eauto. apply IHreachable. congruence. +Qed. + -- cgit