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/Coqlib.v | 19 +--- lib/Iteration.v | 176 ++++++++++++++++++------------- lib/Maps.v | 100 +++++++++++++++++- lib/Postorder.v | 316 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ lib/Wfsimpl.v | 68 ++++++++++++ 5 files changed, 583 insertions(+), 96 deletions(-) create mode 100644 lib/Postorder.v create mode 100644 lib/Wfsimpl.v (limited to 'lib') diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 87b19ca..50535fb 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -23,23 +23,6 @@ Require Export List. Require Export Bool. Require Import Wf_nat. -(*** - -(** * Logical axioms *) - -(** We use two logical axioms that are not provable in Coq but consistent - with the logic: function extensionality and proof irrelevance. - These are used in the memory model to show that two memory states - that have identical contents are equal. *) - -Axiom extensionality: - forall (A B: Type) (f g : A -> B), - (forall x, f x = g x) -> f = g. - -Axiom proof_irrelevance: - forall (P: Prop) (p1 p2: P), p1 = p2. -***) - (** * Useful tactics *) Ltac inv H := inversion H; clear H; subst. @@ -51,7 +34,7 @@ Ltac caseEq name := generalize (refl_equal name); pattern name at -1 in |- *; case name. Ltac destructEq name := - generalize (refl_equal name); pattern name at -1 in |- *; destruct name; intro. + destruct name as []_eqn. Ltac decEq := match goal with diff --git a/lib/Iteration.v b/lib/Iteration.v index 3625845..235b650 100644 --- a/lib/Iteration.v +++ b/lib/Iteration.v @@ -10,65 +10,88 @@ (* *) (* *********************************************************************) -(* Bounded and unbounded iterators *) +(** Bounded and unbounded iterators *) Require Import Axioms. Require Import Coqlib. -Require Import Classical. -Require Import Max. +Require Import Wfsimpl. -Module Type ITER. -Variable iterate - : forall A B : Type, (A -> B + A) -> A -> option B. -Hypothesis iterate_prop - : forall (A B : Type) (step : A -> B + A) (P : A -> Prop) (Q : B -> Prop), - (forall a : A, P a -> - match step a with inl b => Q b | inr a' => P a' end) -> - forall (a : A) (b : B), iterate A B step a = Some b -> P a -> Q b. -End ITER. +(** This modules defines several Coq encodings of a general "while" loop. + The loop is presented in functional style as the iteration + of a [step] function of type [A -> B + A]: +<< + let rec iterate step a = + match step a with + | inl b -> b + | inr a' -> iterate step a' +>> + This iteration cannot be defined directly in Coq using [Fixpoint], + because Coq is a logic of total functions, and therefore we must + guarantee termination of the loop. +*) -Axiom - dependent_description' : - forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop), - (forall x:A, - exists y : B x, R x y /\ (forall y':B x, R x y' -> y = y')) -> - sigT (fun f : forall x:A, B x => (forall x:A, R x (f x))). +(** * Terminating iteration *) -(* A constructive implementation using bounded iteration. *) +(** We first implement the case where termination is guaranteed because + the current state [a] decreases at each iteration. *) -Module PrimIter: ITER. +Module WfIter. Section ITERATION. Variables A B: Type. Variable step: A -> B + A. +Variable ord: A -> A -> Prop. +Hypothesis ord_wf: well_founded ord. +Hypothesis step_decr: forall a a', step a = inr _ a' -> ord a' a. -(** The [step] parameter represents one step of the iteration. From a - current iteration state [a: A], it either returns a value of type [B], - meaning that iteration is over and that this [B] value is the final - result of the iteration, or a value [a' : A] which is the next state - of the iteration. +Definition step_info (a: A) : {b | step a = inl _ b} + {a' | step a = inr _ a' & ord a' a}. +Proof. + caseEq (step a); intros. left; exists b; auto. right; exists a0; auto. +Qed. - The naive way to define the iteration is: -<< -Fixpoint iterate (a: A) : B := - match step a with - | inl b => b - | inr a' => iterate a' +Definition iterate_F (a: A) (rec: forall a', ord a' a -> B) : B := + match step_info a with + | inl (exist b P) => b + | inr (exist2 a' P Q) => rec a' Q end. ->> - However, this is a general recursion, not guaranteed to terminate, - and therefore not expressible in Coq. The standard way to work around - this difficulty is to use Noetherian recursion (Coq module [Wf]). - This requires that we equip the type [A] with a well-founded ordering [<] - (no infinite ascending chains) and we demand that [step] satisfies - [step a = inr a' -> a < a']. For the types [A] that are of interest to us - in this development, it is however very painful to define adequate - well-founded orderings, even though we know our iterations always - terminate. - - Instead, we choose to bound the number of iterations by an arbitrary - constant. [iterate] then becomes a function that can fail, + +Definition iterate (a: A) : B := Fix ord_wf iterate_F a. + +(** We now prove an invariance property [iterate_prop], similar to the Hoare + logic rule for "while" loops. *) + +Variable P: A -> Prop. +Variable Q: B -> Prop. + +Hypothesis step_prop: + forall a : A, P a -> + match step a with inl b => Q b | inr a' => P a' end. + +Lemma iterate_prop: + forall a, P a -> Q (iterate a). +Proof. + intros a0. pattern a0. apply well_founded_ind with (R := ord). auto. + intros. unfold iterate; rewrite unroll_Fix. unfold iterate_F. + destruct (step_info x) as [[b U] | [a' U V]]. + exploit step_prop; eauto. rewrite U; auto. + apply H. auto. exploit step_prop; eauto. rewrite U; auto. +Qed. + +End ITERATION. + +End WfIter. + +(** * Bounded iteration *) + +(** The presentation of iteration shown above is predicated on the existence + of a well-founded ordering that decreases at each step of the iteration. + In several parts of the CompCert development, it is very painful to define + such a well-founded ordering and to prove decrease, even though we know our + iterations always terminate. + + In the presentation below, we choose instead to bound the number of iterations + by an arbitrary constant. [iterate] then becomes a function that can fail, of type [A -> option B]. The [None] result denotes failure to reach a result in the number of iterations prescribed, or, in other terms, failure to find a solution to the dataflow problem. The compiler @@ -82,6 +105,13 @@ Fixpoint iterate (a: A) : B := course our proofs also cover the failure case and show that nothing bad happens in this hypothetical case either. *) +Module PrimIter. + +Section ITERATION. + +Variables A B: Type. +Variable step: A -> B + A. + Definition num_iterations := 1000000000000%positive. (** The simple definition of bounded iteration is: @@ -117,19 +147,7 @@ Definition iter_step (x: positive) end end. -Definition iter: positive -> A -> option B := - Fix Plt_wf (fun _ => A -> option B) iter_step. - -(** We then prove the expected unrolling equations for [iter]. *) - -Remark unroll_iter: - forall x, iter x = iter_step x (fun y _ => iter y). -Proof. - unfold iter; apply (Fix_eq Plt_wf (fun _ => A -> option B) iter_step). - intros. unfold iter_step. apply extensionality. intro s. - case (peq x xH); intro. auto. - rewrite H. auto. -Qed. +Definition iter: positive -> A -> option B := Fix Plt_wf iter_step. (** The [iterate] function is defined as [iter] up to [num_iterations] through the loop. *) @@ -150,11 +168,12 @@ Lemma iter_prop: Proof. apply (well_founded_ind Plt_wf (fun p => forall a b, P a -> iter p a = Some b -> Q b)). - intros until b. intro. rewrite unroll_iter. - unfold iter_step. case (peq x 1); intro. congruence. - generalize (step_prop a H0). - case (step a); intros. congruence. - apply H with (Ppred x) a0. apply Ppred_Plt; auto. auto. auto. + intros. unfold iter in H1. rewrite unroll_Fix in H1. unfold iter_step in H1. + destruct (peq x 1). discriminate. + specialize (step_prop a H0). + destruct (step a) as [b'|a']_eqn. + inv H1. auto. + apply H with (Ppred x) a'. apply Ppred_Plt; auto. auto. auto. Qed. Lemma iterate_prop: @@ -167,11 +186,21 @@ End ITERATION. End PrimIter. +(** * General iteration *) + (* An implementation using classical logic and unbounded iteration, in the style of Yves Bertot's paper, "Extending the Calculus - of Constructions with Tarski's fix-point theorem". *) + of Constructions with Tarski's fix-point theorem". -Module GenIter: ITER. + As in the bounded case, the [iterate] function returns an option type. + [None] means that iteration does not terminate. + [Some b] means that iteration terminates with the result [b]. *) + +Require Import Classical. +Require Import ClassicalDescription. +Require Import Max. + +Module GenIter. Section ITERATION. @@ -249,30 +278,29 @@ Proof. Qed. Lemma converges_to_exists_uniquely: - forall a, exists b, converges_to a b /\ forall b', converges_to a b' -> b = b'. + forall a, exists! b, converges_to a b . Proof. intro. destruct (converges_to_exists a) as [b CT]. exists b. split. assumption. exact (converges_to_unique _ _ CT). Qed. -Definition exists_iterate := - dependent_description' A (fun _ => option B) - converges_to converges_to_exists_uniquely. - -Definition iterate : A -> option B := - match exists_iterate with existT f P => f end. +Definition iterate (a: A) : option B := + proj1_sig (constructive_definite_description (converges_to a) (converges_to_exists_uniquely a)). Lemma converges_to_iterate: forall a b, converges_to a b -> iterate a = b. Proof. - intros. unfold iterate. destruct exists_iterate as [f P]. - apply converges_to_unique with a. apply P. auto. + intros. unfold iterate. + destruct (constructive_definite_description (converges_to a) (converges_to_exists_uniquely a)) as [b' P]. + simpl. apply converges_to_unique with a; auto. Qed. Lemma iterate_converges_to: forall a, converges_to a (iterate a). Proof. - intros. unfold iterate. destruct exists_iterate as [f P]. apply P. + intros. unfold iterate. + destruct (constructive_definite_description (converges_to a) (converges_to_exists_uniquely a)) as [b' P]. + simpl; auto. Qed. (** Invariance property. *) diff --git a/lib/Maps.v b/lib/Maps.v index f8d1bd5..255ce44 100644 --- a/lib/Maps.v +++ b/lib/Maps.v @@ -77,6 +77,9 @@ Module Type TREE. Hypothesis grspec: forall (A: Type) (i j: elt) (m: t A), get i (remove j m) = if elt_eq i j then None else get i m. + Hypothesis set2: + forall (A: Type) (i: elt) (m: t A) (v1 v2: A), + set i v2 (set i v1 m) = set i v2 m. (** Extensional equality between trees. *) Variable beq: forall (A: Type), (A -> A -> bool) -> t A -> t A -> bool. @@ -302,8 +305,15 @@ Module PTree <: TREE. rewrite (IHi m1 v H); congruence. Qed. - Lemma rleaf : forall (A : Type) (i : positive), remove i (Leaf : t A) = Leaf. - Proof. destruct i; simpl; auto. Qed. + Theorem set2: + forall (A: Type) (i: elt) (m: t A) (v1 v2: A), + set i v2 (set i v1 m) = set i v2 m. + Proof. + induction i; intros; destruct m; simpl; try (rewrite IHi); auto. + Qed. + + Lemma rleaf : forall (A : Type) (i : positive), remove i (Leaf : t A) = Leaf. + Proof. destruct i; simpl; auto. Qed. Theorem grs: forall (A: Type) (i: positive) (m: t A), get i (remove i m) = None. @@ -1116,6 +1126,13 @@ Module PMap <: MAP. unfold option_map. destruct (PTree.get i (snd m)); auto. Qed. + Theorem set2: + forall (A: Type) (i: elt) (x y: A) (m: t A), + set i y (set i x m) = set i y m. + Proof. + intros. unfold set. simpl. decEq. apply PTree.set2. + Qed. + End PMap. (** * An implementation of maps over any type that injects into type [positive] *) @@ -1178,6 +1195,13 @@ Module IMap(X: INDEXED_TYPE). intros. unfold map, get. apply PMap.gmap. Qed. + Lemma set2: + forall (A: Type) (i: elt) (x y: A) (m: t A), + set i y (set i x m) = set i y m. + Proof. + intros. unfold set. apply PMap.set2. + Qed. + End IMap. Module ZIndexed. @@ -1378,6 +1402,76 @@ Qed. End TREE_FOLD_IND. +(** A nonnegative measure over trees *) + +Section MEASURE. + +Variable V: Type. + +Definition cardinal (x: T.t V) : nat := List.length (T.elements x). + +Remark list_incl_length: + forall (A: Type) (l1: list A), list_norepet l1 -> + forall (l2: list A), List.incl l1 l2 -> (List.length l1 <= List.length l2)%nat. +Proof. + induction 1; simpl; intros. + omega. + exploit (List.in_split hd l2). auto with coqlib. intros [l3 [l4 EQ]]. subst l2. + assert (length tl <= length (l3 ++ l4))%nat. + apply IHlist_norepet. red; intros. + exploit (H1 a); auto with coqlib. + repeat rewrite in_app_iff. simpl. intuition. subst. contradiction. + repeat rewrite app_length in *. simpl. omega. +Qed. + +Remark list_length_incl: + forall (A: Type) (l1: list A), list_norepet l1 -> + forall l2, List.incl l1 l2 -> List.length l1 = List.length l2 -> List.incl l2 l1. +Proof. + induction 1; simpl; intros. + destruct l2; simpl in *. auto with coqlib. discriminate. + exploit (List.in_split hd l2). auto with coqlib. intros [l3 [l4 EQ]]. subst l2. + assert (incl (l3 ++ l4) tl). + apply IHlist_norepet. red; intros. + exploit (H1 a); auto with coqlib. + repeat rewrite in_app_iff. simpl. intuition. subst. contradiction. + repeat rewrite app_length in *. simpl in H2. omega. + red; simpl; intros. rewrite in_app_iff in H4; simpl in H4. intuition. +Qed. + +Remark list_strict_incl_length: + forall (A: Type) (l1 l2: list A) (x: A), + list_norepet l1 -> List.incl l1 l2 -> ~In x l1 -> In x l2 -> + (List.length l1 < List.length l2)%nat. +Proof. + intros. exploit list_incl_length; eauto. intros. + assert (length l1 = length l2 \/ length l1 < length l2)%nat by omega. + destruct H4; auto. elim H1. eapply list_length_incl; eauto. +Qed. + +Remark list_norepet_map: + forall (A B: Type) (f: A -> B) (l: list A), + list_norepet (List.map f l) -> list_norepet l. +Proof. + induction l; simpl; intros. + constructor. + inv H. constructor; auto. red; intros; elim H2. apply List.in_map; auto. +Qed. + +Theorem cardinal_remove: + forall x m y, T.get x m = Some y -> (cardinal (T.remove x m) < cardinal m)%nat. +Proof. + unfold cardinal; intros. apply list_strict_incl_length with (x := (x, y)). + apply list_norepet_map with (f := @fst T.elt V). apply T.elements_keys_norepet. + red; intros. destruct a as [x' y']. exploit T.elements_complete; eauto. + rewrite T.grspec. destruct (T.elt_eq x' x); intros; try discriminate. + apply T.elements_correct; auto. + red; intros. exploit T.elements_complete; eauto. rewrite T.grspec. rewrite dec_eq_true. congruence. + apply T.elements_correct; auto. +Qed. + +End MEASURE. + End Tree_Properties. Module PTree_Properties := Tree_Properties(PTree). @@ -1386,5 +1480,3 @@ Module PTree_Properties := Tree_Properties(PTree). Notation "a ! b" := (PTree.get b a) (at level 1). Notation "a !! b" := (PMap.get b a) (at level 1). - -(* $Id: Maps.v,v 1.12.4.4 2006/01/07 11:46:55 xleroy Exp $ *) diff --git a/lib/Postorder.v b/lib/Postorder.v new file mode 100644 index 0000000..fe06da7 --- /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. + diff --git a/lib/Wfsimpl.v b/lib/Wfsimpl.v new file mode 100644 index 0000000..1ed6326 --- /dev/null +++ b/lib/Wfsimpl.v @@ -0,0 +1,68 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Defining recursive functions by Noetherian induction. This is a simplified + interface to the [Wf] module of Coq's standard library, where the functions + to be defined have non-dependent types, and function extensionality is assumed. *) + +Require Import Axioms. +Require Import Wf. +Require Import Wf_nat. + +Set Implicit Arguments. + +Section FIX. + +Variables A B: Type. +Variable R: A -> A -> Prop. +Hypothesis Rwf: well_founded R. +Variable F: forall (x: A), (forall (y: A), R y x -> B) -> B. + +Definition Fix (x: A) : B := Wf.Fix Rwf (fun (x: A) => B) F x. + +Theorem unroll_Fix: + forall x, Fix x = F (fun (y: A) (P: R y x) => Fix y). +Proof. + unfold Fix; intros. apply Wf.Fix_eq with (P := fun (x: A) => B). + intros. assert (f = g). apply functional_extensionality_dep; intros. + apply functional_extensionality; intros. auto. + subst g; auto. +Qed. + +End FIX. + +(** Same, with a nonnegative measure instead of a well-founded ordering *) + +Section FIXM. + +Variables A B: Type. +Variable measure: A -> nat. +Variable F: forall (x: A), (forall (y: A), measure y < measure x -> B) -> B. + +Definition Fixm (x: A) : B := Wf.Fix (well_founded_ltof A measure) (fun (x: A) => B) F x. + +Theorem unroll_Fixm: + forall x, Fixm x = F (fun (y: A) (P: measure y < measure x) => Fixm y). +Proof. + unfold Fixm; intros. apply Wf.Fix_eq with (P := fun (x: A) => B). + intros. assert (f = g). apply functional_extensionality_dep; intros. + apply functional_extensionality; intros. auto. + subst g; auto. +Qed. + +End FIXM. + + + -- cgit v1.2.3