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

1 files changed, 316 insertions, 0 deletions

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.
+