From 2ee7552c01a9e42754f9e3c99881b9399958cdda Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 16 Aug 2011 11:52:56 +0000
Subject: New backend pass "RRE": optimize (somewhat) redundant reloads
 introduced by the Reload pass.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1713 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Locations.v |  35 ++-
 backend/RRE.v       | 172 ++++++++++++++
 backend/RREproof.v  | 630 ++++++++++++++++++++++++++++++++++++++++++++++++++++
 backend/RREtyping.v | 109 +++++++++
 4 files changed, 926 insertions(+), 20 deletions(-)
 create mode 100644 backend/RRE.v
 create mode 100644 backend/RREproof.v
 create mode 100644 backend/RREtyping.v

(limited to 'backend')

diff --git a/backend/Locations.v b/backend/Locations.v
index 8a0b5ea..0b538fd 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -301,22 +301,26 @@ Module Loc.
     | l1 :: ls => diff l l1 /\ notin l ls
     end.
 
+  Lemma notin_iff:
+    forall l ll, notin l ll <-> (forall l', In l' ll -> Loc.diff l l').
+  Proof.
+    induction ll; simpl. 
+    tauto.
+    rewrite IHll. intuition. subst a. auto. 
+  Qed.
+
   Lemma notin_not_in:
     forall l ll, notin l ll -> ~(In l ll).
   Proof.
-    unfold not; induction ll; simpl; intros.
-    auto.
-    elim H; intros. elim H0; intro. 
-    subst l. exact (same_not_diff a H1).
-    auto.
+    intros; red; intros. rewrite notin_iff in H.
+    elim (diff_not_eq l l); auto.
   Qed.
 
   Lemma reg_notin:
     forall r ll, ~(In (R r) ll) -> notin (R r) ll.
   Proof.
-    induction ll; simpl; intros. auto. 
-    split. destruct a; auto. intuition congruence.
-    apply IHll. intuition.
+    intros. rewrite notin_iff; intros. 
+    destruct l'; simpl. congruence. auto.
   Qed.
 
 (** [Loc.disjoint l1 l2] is true if the locations in list [l1]
@@ -347,29 +351,20 @@ Module Loc.
   Lemma in_notin_diff:
     forall l1 l2 ll, notin l1 ll -> In l2 ll -> diff l1 l2.
   Proof.
-    induction ll; simpl; intros.
-    elim H0.
-    elim H0; intro. subst a. tauto. apply IHll; tauto.
+    intros. rewrite notin_iff in H. auto. 
   Qed.
 
   Lemma notin_disjoint:
     forall l1 l2,
     (forall x, In x l1 -> notin x l2) -> disjoint l1 l2.
   Proof.
-    unfold disjoint; induction l1; intros.
-    elim H0. 
-    elim H0; intro.
-    subst x1. eapply in_notin_diff. apply H. auto with coqlib. auto.
-    eapply IHl1; eauto. intros. apply H. auto with coqlib.
+    intros; red; intros. exploit H; eauto. rewrite notin_iff; intros. auto. 
   Qed.
 
   Lemma disjoint_notin:
     forall l1 l2 x, disjoint l1 l2 -> In x l1 -> notin x l2.
   Proof.
-    unfold disjoint; induction l2; simpl; intros.
-    auto.
-    split. apply H. auto. tauto.
-    apply IHl2. intros. apply H. auto. tauto. auto.
+    intros; rewrite notin_iff; intros. red in H. auto. 
   Qed.
 
 (** [Loc.norepet ll] holds if the locations in list [ll] are pairwise
diff --git a/backend/RRE.v b/backend/RRE.v
new file mode 100644
index 0000000..95eadce
--- /dev/null
+++ b/backend/RRE.v
@@ -0,0 +1,172 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Redundant Reloads Elimination *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Values.
+Require Import Globalenvs.
+Require Import Op.
+Require Import Locations.
+Require Import Conventions.
+Require Import Linear.
+
+(** * Equations between slots and machine registers *)
+
+(** The RRE pass keeps track of which register holds the value of which
+  stack slot, using sets of equations like the following. *)
+
+Record equation := mkeq { e_reg: mreg; e_slot: slot }.
+
+Definition equations : Type := list equation.
+
+Fixpoint find_reg_containing (s: slot) (eqs: equations) : option mreg :=
+  match eqs with
+  | nil => None
+  | e :: eqs' => if slot_eq (e_slot e) s then Some (e_reg e) else find_reg_containing s eqs'
+  end.
+
+Definition eq_equation (eq1 eq2: equation) : {eq1=eq2} + {eq1<>eq2}.
+Proof.
+  generalize slot_eq mreg_eq. decide equality.
+Qed.
+
+Definition contains_equation (s: slot) (r: mreg) (eqs: equations) : bool :=
+  In_dec eq_equation (mkeq r s) eqs.
+
+(** Remove equations that are invalidated by an assignment to location [l]. *)
+
+Fixpoint kill_loc (l: loc) (eqs: equations) : equations :=
+  match eqs with
+  | nil => nil
+  | e :: eqs' =>
+      if Loc.diff_dec (S (e_slot e)) l && Loc.diff_dec (R (e_reg e)) l
+      then e :: kill_loc l eqs'
+      else kill_loc l eqs'
+  end.
+
+(** Same, for a list of locations [ll]. *)
+
+Definition kill_locs (ll: list loc) (eqs: equations) : equations :=
+  List.fold_left (fun eqs l => kill_loc l eqs) ll eqs.
+
+Definition kill_temps (eqs: equations) : equations :=
+  kill_locs temporaries eqs.
+
+Definition kill_at_move (eqs: equations) : equations :=
+  kill_locs destroyed_at_move eqs.
+
+Definition kill_op (op: operation) (eqs: equations) : equations :=
+  match op with Omove => kill_at_move eqs | _ => kill_temps eqs end.
+
+(** * Safety criterion *)
+
+Definition is_incoming (s: slot) : bool :=
+  match s with
+  | Incoming _ _ => true
+  | _ => false
+  end.
+
+(** Turning a [Lgetstack] into a register-to-register move is not always
+  safe: at least on x86, the move destroys some registers 
+  (those from [destroyed_at_move] list) while the [Lgetstack] does not.
+  Therefore, we perform this transformation only if the destroyed
+  registers are not used before being destroyed by a later
+  [Lop], [Lload], [Lstore], [Lbuiltin], [Lcond] or [Ljumptable] operation. *)
+
+Fixpoint safe_move_insertion (c: code) : bool :=
+  match c with
+  | Lgetstack s r :: c' =>
+      negb(In_dec mreg_eq r destroyed_at_move_regs) && safe_move_insertion c'
+  | Lsetstack r s :: c' =>
+      negb(In_dec mreg_eq r destroyed_at_move_regs)
+  | Lop op args res :: c' =>
+      list_disjoint_dec mreg_eq args destroyed_at_move_regs
+  | Lload chunk addr args res :: c' =>
+      list_disjoint_dec mreg_eq args destroyed_at_move_regs
+  | Lstore chunk addr args src :: c' =>
+      list_disjoint_dec mreg_eq (src :: args) destroyed_at_move_regs
+  | Lbuiltin ef args res :: c' =>
+      list_disjoint_dec mreg_eq args destroyed_at_move_regs
+  | Lcond cond args lbl :: c' =>
+      list_disjoint_dec mreg_eq args destroyed_at_move_regs
+  | Ljumptable arg tbl :: c' =>
+      negb(In_dec mreg_eq arg destroyed_at_move_regs)
+  | _ => false
+  end.
+
+(** * Code transformation *)
+
+(** The following function eliminates [Lgetstack] instructions or turn them
+  into register-to-register move whenever possible.  Simultaneously,
+  it propagates valid (register, slot) equations across basic blocks. *)
+
+Fixpoint transf_code (eqs: equations) (c: code) : code :=
+  match c with
+  | nil => nil
+  | Lgetstack s r :: c =>
+      if is_incoming s then
+        Lgetstack s r :: transf_code (kill_loc (R r) (kill_loc (R IT1) eqs)) c
+      else if contains_equation s r eqs then
+        transf_code eqs c
+      else 
+        match find_reg_containing s eqs with
+        | Some r' => 
+            if safe_move_insertion c then
+              Lop Omove (r' :: nil) r :: transf_code (kill_at_move (mkeq r s :: kill_loc (R r) eqs)) c
+            else
+              Lgetstack s r:: transf_code (mkeq r s :: kill_loc (R r) eqs) c
+        | None =>
+            Lgetstack s r:: transf_code (mkeq r s :: kill_loc (R r) eqs) c
+        end
+  | Lsetstack r s :: c =>
+      Lsetstack r s :: transf_code (kill_at_move (mkeq r s :: kill_loc (S s) eqs)) c
+  | Lop op args res :: c =>
+      Lop op args res :: transf_code (kill_loc (R res) (kill_op op eqs)) c
+  | Lload chunk addr args res :: c =>
+      Lload chunk addr args res :: transf_code (kill_loc (R res) (kill_temps eqs)) c
+  | Lstore chunk addr args src :: c =>
+      Lstore chunk addr args src :: transf_code (kill_temps eqs) c
+  | Lcall sg ros :: c =>
+      Lcall sg ros :: transf_code nil c
+  | Ltailcall sg ros :: c =>
+      Ltailcall sg ros :: transf_code nil c
+  | Lbuiltin ef args res :: c =>
+      Lbuiltin ef args res :: transf_code (kill_loc (R res) (kill_temps eqs)) c
+  | Lannot ef args :: c =>
+      Lannot ef args :: transf_code eqs c
+  | Llabel lbl :: c =>
+      Llabel lbl :: transf_code nil c
+  | Lgoto lbl :: c =>
+      Lgoto lbl :: transf_code nil c
+  | Lcond cond args lbl :: c =>
+      Lcond cond args lbl :: transf_code (kill_temps eqs) c
+  | Ljumptable arg lbls :: c =>
+      Ljumptable arg lbls :: transf_code nil c
+  | Lreturn :: c =>
+      Lreturn :: transf_code nil c
+  end.
+
+Definition transf_function (f: function) : function :=
+  mkfunction
+    (fn_sig f)
+    (fn_stacksize f)
+    (transf_code nil (fn_code f)).
+
+Definition transf_fundef (fd: fundef) : fundef :=
+  transf_fundef transf_function fd.
+
+Definition transf_program (p: program) : program :=
+  transform_program transf_fundef p.
+
diff --git a/backend/RREproof.v b/backend/RREproof.v
new file mode 100644
index 0000000..da959ea
--- /dev/null
+++ b/backend/RREproof.v
@@ -0,0 +1,630 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Correctness proof for the [RRE] pass. *)
+
+Require Import Axioms.
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Values.
+Require Import Globalenvs.
+Require Import Events.
+Require Import Smallstep.
+Require Import Op.
+Require Import Locations.
+Require Import Conventions.
+Require Import Linear.
+Require Import RRE.
+
+(** * Operations over equations *)
+
+Lemma find_reg_containing_sound:
+  forall s r eqs, find_reg_containing s eqs = Some r -> In (mkeq r s) eqs.
+Proof.
+  induction eqs; simpl; intros.
+  congruence.
+  destruct (slot_eq (e_slot a) s). inv H. left; destruct a; auto. right; eauto.
+Qed.
+
+Definition equations_hold (ls: locset) (eqs: equations) : Prop :=
+  forall e, In e eqs -> ls (S (e_slot e)) = ls (R (e_reg e)).
+
+Lemma nil_hold:
+  forall ls, equations_hold ls nil.
+Proof.
+  red; intros; contradiction.
+Qed.
+
+Lemma In_kill_loc:
+  forall e l eqs,
+  In e (kill_loc l eqs) ->
+  In e eqs /\ Loc.diff (S (e_slot e)) l /\ Loc.diff (R (e_reg e)) l.
+Proof.
+  induction eqs; simpl kill_loc; simpl In; intros.
+  tauto.
+  destruct (Loc.diff_dec (S (e_slot a)) l).
+  destruct (Loc.diff_dec (R (e_reg a)) l).
+  simpl in H.  intuition congruence. 
+  simpl in H.  intuition.
+  simpl in H.  intuition.
+Qed.
+
+Lemma kill_loc_hold:
+  forall ls eqs l v,
+  equations_hold ls eqs ->
+  equations_hold (Locmap.set l v ls) (kill_loc l eqs).
+Proof.
+  intros; red; intros. 
+  exploit In_kill_loc; eauto. intros [A [B C]].
+  repeat rewrite Locmap.gso; auto; apply Loc.diff_sym; auto.
+Qed.
+
+Lemma In_kill_locs:
+  forall e ll eqs,
+  In e (kill_locs ll eqs) ->
+  In e eqs /\ Loc.notin (S (e_slot e)) ll /\ Loc.notin (R (e_reg e)) ll.
+Proof.
+Opaque Loc.diff.
+  induction ll; simpl; intros.
+  tauto.
+  exploit IHll; eauto. intros [A [B C]]. exploit In_kill_loc; eauto. intros [D [E F]]. 
+  tauto.
+Qed.
+
+Lemma kill_locs_hold:
+  forall ll ls eqs,
+  equations_hold ls eqs ->
+  equations_hold (Locmap.undef ll ls) (kill_locs ll eqs).
+Proof.
+  intros; red; intros. exploit In_kill_locs; eauto. intros [A [B C]]. 
+  repeat rewrite Locmap.guo; auto. 
+Qed.
+
+Lemma kill_temps_hold:
+  forall ls eqs,
+  equations_hold ls eqs ->
+  equations_hold (LTL.undef_temps ls) (kill_temps eqs).
+Proof.
+  exact (kill_locs_hold temporaries).
+Qed.
+
+Lemma kill_at_move_hold:
+  forall ls eqs,
+  equations_hold ls eqs ->
+  equations_hold (undef_setstack ls) (kill_at_move eqs).
+Proof.
+  exact (kill_locs_hold destroyed_at_move).
+Qed.
+
+Lemma kill_at_op_hold:
+  forall op ls eqs,
+  equations_hold ls eqs ->
+  equations_hold (undef_op op ls) (kill_op op eqs).
+Proof.
+  intros op. 
+  destruct op; exact kill_temps_hold || exact kill_at_move_hold.
+Qed.
+
+Lemma eqs_getstack_hold:
+  forall rs r s eqs,
+  equations_hold rs eqs ->
+  equations_hold (Locmap.set (R r) (rs (S s)) rs)
+                 (mkeq r s :: kill_loc (R r) eqs).
+Proof.
+Transparent Loc.diff.
+  intros; red; intros. simpl in H0; destruct H0.
+  subst e. simpl. rewrite Locmap.gss; rewrite Locmap.gso; auto. red; auto.
+  exploit In_kill_loc; eauto. intros [D [E F]].
+  repeat rewrite Locmap.gso. auto. 
+  apply Loc.diff_sym; auto. apply Loc.diff_sym; auto.
+Qed.
+
+Lemma eqs_movestack_hold:
+  forall rs r s eqs,
+  equations_hold rs eqs ->
+  equations_hold (Locmap.set (R r) (rs (S s)) (undef_setstack rs))
+                 (kill_at_move (mkeq r s :: kill_loc (R r) eqs)).
+Proof.
+  unfold undef_setstack, kill_at_move; intros; red; intros.
+  exploit In_kill_locs; eauto. intros [A [B C]].
+  simpl in A; destruct A.
+  subst e. rewrite Locmap.gss. rewrite Locmap.gso. apply Locmap.guo. auto. 
+  simpl; auto.
+  exploit In_kill_loc; eauto. intros [D [E F]].
+  repeat rewrite Locmap.gso. repeat rewrite Locmap.guo; auto.
+  apply Loc.diff_sym; auto. apply Loc.diff_sym; auto.
+Qed.
+
+Lemma eqs_setstack_hold:
+  forall rs r s eqs,
+  equations_hold rs eqs ->
+  equations_hold (Locmap.set (S s) (rs (R r)) (undef_setstack rs))
+                 (kill_at_move (mkeq r s :: kill_loc (S s) eqs)).
+Proof.
+  unfold undef_setstack, kill_at_move; intros; red; intros.
+  exploit In_kill_locs; eauto. intros [A [B C]].
+  simpl in A; destruct A.
+  subst e. rewrite Locmap.gss. rewrite Locmap.gso. rewrite Locmap.guo. auto. 
+  auto. simpl. destruct s; auto.
+  exploit In_kill_loc; eauto. intros [D [E F]].
+  repeat rewrite Locmap.gso. repeat rewrite Locmap.guo; auto.
+  apply Loc.diff_sym; auto. apply Loc.diff_sym; auto.
+Qed.
+
+Lemma locmap_set_reg_same:
+  forall rs r,
+  Locmap.set (R r) (rs (R r)) rs = rs.
+Proof.
+  intros. apply extensionality; intros. 
+  destruct (Loc.eq x (R r)).
+  subst x. apply Locmap.gss.
+  apply Locmap.gso. apply Loc.diff_reg_right; auto.
+Qed.
+
+(** * Agreement between values of locations *)
+
+(** Values of locations may differ between the original and transformed
+  program: after a [Lgetstack] is optimized to a [Lop Omove], 
+  the values of [destroyed_at_move] temporaries differ.  This
+  can only happen in parts of the code where the [safe_move_insertion]
+  function returns [true].  *)
+
+Definition agree (sm: bool) (rs rs': locset) : Prop :=
+  forall l, sm = false \/ Loc.notin l destroyed_at_move -> rs' l = rs l.
+
+Lemma agree_false:
+  forall rs rs',
+  agree false rs rs' <-> rs' = rs.
+Proof.
+  intros; split; intros.
+  apply extensionality; intros. auto.
+  subst rs'. red; auto. 
+Qed.
+
+Lemma agree_slot:
+  forall sm rs rs' s,
+  agree sm rs rs' -> rs' (S s) = rs (S s).
+Proof.
+Transparent Loc.diff.
+  intros. apply H. right. simpl; destruct s; tauto.
+Qed.
+
+Lemma agree_reg:
+  forall sm rs rs' r,
+  agree sm rs rs' ->
+  sm = false \/ ~In r destroyed_at_move_regs -> rs' (R r) = rs (R r).
+Proof.
+  intros. apply H. destruct H0; auto. right. 
+  simpl in H0; simpl; intuition congruence.
+Qed.
+
+Lemma agree_regs:
+  forall sm rs rs' rl,
+  agree sm rs rs' ->
+  sm = false \/ list_disjoint rl destroyed_at_move_regs -> reglist rs' rl = reglist rs rl.
+Proof.
+  induction rl; intros; simpl. 
+  auto.
+  decEq. apply agree_reg with sm; auto.
+    destruct H0; auto.
+    right. eapply list_disjoint_notin; eauto with coqlib.
+  apply IHrl; auto. destruct H0; auto. right. eapply list_disjoint_cons_left; eauto.
+Qed.
+
+Lemma agree_set:
+  forall sm rs rs' l v,
+  agree sm rs rs' ->
+  agree sm (Locmap.set l v rs) (Locmap.set l v rs').
+Proof.
+  intros; red; intros.
+  unfold Locmap.set. 
+  destruct (Loc.eq l l0). auto. 
+  destruct (Loc.overlap l l0). auto.
+  apply H; auto.
+Qed. 
+
+Lemma agree_undef_move_1:
+  forall sm rs rs',
+  agree sm rs rs' ->
+  agree true rs (undef_setstack rs').
+Proof.
+  intros. unfold undef_setstack. red; intros.
+  destruct H0. congruence. rewrite Locmap.guo; auto.
+Qed.
+
+Remark locmap_undef_equal:
+  forall x ll rs rs',
+  (forall l, Loc.notin l ll -> rs' l = rs l) ->
+  Locmap.undef ll rs' x = Locmap.undef ll rs x.
+Proof.
+  induction ll; intros; simpl.
+  apply H. simpl. auto.
+  apply IHll. intros. unfold Locmap.set. 
+  destruct (Loc.eq a l). auto. destruct (Loc.overlap a l) as []_eqn. auto. 
+  apply H. simpl. split; auto. apply Loc.diff_sym. apply Loc.non_overlap_diff; auto.
+Qed. 
+
+Lemma agree_undef_move_2:
+  forall sm rs rs',
+  agree sm rs rs' ->
+  agree false (undef_setstack rs) (undef_setstack rs').
+Proof.
+  intros. rewrite agree_false.
+  apply extensionality; intros. unfold undef_setstack. apply locmap_undef_equal. auto.
+Qed.
+
+Lemma agree_undef_temps:
+  forall sm rs rs',
+  agree sm rs rs' ->
+  agree false (LTL.undef_temps rs) (LTL.undef_temps rs').
+Proof.
+  intros. rewrite agree_false.
+  apply extensionality; intros. unfold LTL.undef_temps. apply locmap_undef_equal.
+  intros. apply H. right. simpl in H0; simpl; tauto.
+Qed.
+
+Lemma agree_undef_op:
+  forall op sm rs rs',
+  agree sm rs rs' ->
+  agree false (undef_op op rs) (undef_op op rs').
+Proof.
+  intros op.
+  destruct op; exact agree_undef_temps || exact agree_undef_move_2.
+Qed.
+
+Lemma transl_find_label:
+  forall lbl c eqs,
+  find_label lbl (transf_code eqs c) =
+  option_map (transf_code nil) (find_label lbl c).
+Proof.
+  induction c; simpl; intros.
+  auto.
+  destruct a; simpl; auto.
+  destruct (is_incoming s); simpl; auto.
+  destruct (contains_equation s m eqs); auto.
+  destruct (find_reg_containing s eqs); simpl; auto.
+  destruct (safe_move_insertion c); simpl; auto. 
+  destruct (peq lbl l); simpl; auto.
+Qed.
+
+(** * Semantic preservation *)
+
+Section PRESERVATION.
+
+Variable prog: program.
+Let tprog := transf_program prog.
+
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+Lemma functions_translated:
+  forall v f,
+  Genv.find_funct ge v = Some f ->
+  Genv.find_funct tge v = Some (transf_fundef f).
+Proof (@Genv.find_funct_transf _ _ _ transf_fundef prog).
+
+Lemma function_ptr_translated:
+  forall v f,
+  Genv.find_funct_ptr ge v = Some f ->
+  Genv.find_funct_ptr tge v = Some (transf_fundef f).
+Proof (@Genv.find_funct_ptr_transf _ _ _ transf_fundef prog).
+
+Lemma symbols_preserved:
+  forall id,
+  Genv.find_symbol tge id = Genv.find_symbol ge id.
+Proof (@Genv.find_symbol_transf _ _ _ transf_fundef prog).
+
+Lemma varinfo_preserved:
+  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
+Proof (@Genv.find_var_info_transf _ _ _ transf_fundef prog).
+
+Lemma sig_preserved:
+  forall f, funsig (transf_fundef f) = funsig f.
+Proof.
+  destruct f; reflexivity.
+Qed.
+
+Lemma find_function_translated:
+  forall ros rs fd,
+  find_function ge ros rs = Some fd ->
+  find_function tge ros rs = Some (transf_fundef fd).
+Proof.
+  intros. destruct ros; simpl in *. 
+  apply functions_translated; auto.
+  rewrite symbols_preserved. destruct (Genv.find_symbol ge i). 
+  apply function_ptr_translated; auto. 
+  congruence.
+Qed.
+
+Inductive match_frames: stackframe -> stackframe -> Prop :=
+  | match_frames_intro:
+      forall f sp rs c,
+      match_frames (Stackframe f sp rs c)
+                   (Stackframe (transf_function f) sp rs (transf_code nil c)).
+
+Inductive match_states: state -> state -> Prop :=
+  | match_states_regular:
+      forall sm stk f sp c rs m stk' rs' eqs
+        (STK: list_forall2 match_frames stk stk')
+        (EQH: equations_hold rs' eqs)
+        (AG: agree sm rs rs')
+        (SAFE: sm = false \/ safe_move_insertion c = true),
+      match_states (State stk f sp c rs m)
+                   (State stk' (transf_function f) sp (transf_code eqs c) rs' m)
+  | match_states_call:
+      forall stk f rs m stk'
+        (STK: list_forall2 match_frames stk stk'),
+      match_states (Callstate stk f rs m)
+                   (Callstate stk' (transf_fundef f) rs m)
+  | match_states_return:
+      forall stk rs m stk'
+        (STK: list_forall2 match_frames stk stk'),
+      match_states (Returnstate stk rs m)
+                   (Returnstate stk' rs m).
+
+Definition measure (S: state) : nat :=
+  match S with
+  | State s f sp c rs m => List.length c
+  | _ => 0%nat
+  end.
+
+Remark match_parent_locset:
+  forall stk stk',
+  list_forall2 match_frames stk stk' ->
+  return_regs (parent_locset stk') = return_regs (parent_locset stk).
+Proof.
+  intros. inv H; auto. inv H0; auto.
+Qed.
+
+Theorem transf_step_correct:
+  forall S1 t S2, step ge S1 t S2 ->
+  forall S1' (MS: match_states S1 S1'),
+  (exists S2', step tge S1' t S2' /\ match_states S2 S2')
+  \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
+Proof.
+Opaque destroyed_at_move_regs.
+  induction 1; intros; inv MS; simpl.
+(** getstack *)
+  simpl in SAFE. 
+  assert (SAFE': sm = false \/ ~In r destroyed_at_move_regs /\ safe_move_insertion b = true).
+    destruct (in_dec mreg_eq r destroyed_at_move_regs); simpl in SAFE; intuition congruence. 
+  destruct (is_incoming sl) as []_eqn.
+  (* incoming, stays as getstack *)
+  assert (UGS: forall rs, undef_getstack sl rs = Locmap.set (R IT1) Vundef rs).
+    destruct sl; simpl in Heqb0; discriminate || auto.
+  left; econstructor; split. constructor.
+  repeat rewrite UGS.
+  apply match_states_regular with sm; auto.
+  apply kill_loc_hold. apply kill_loc_hold; auto.
+  rewrite (agree_slot _ _ _ sl AG). apply agree_set. apply agree_set. auto.
+  tauto.
+  (* not incoming *)
+  assert (UGS: forall rs, undef_getstack sl rs = rs). 
+    destruct sl; simpl in Heqb0; discriminate || auto.
+  unfold contains_equation. 
+  destruct (in_dec eq_equation (mkeq r sl) eqs); simpl.
+  (* eliminated *)
+  right.  split. omega. split. auto. rewrite UGS.  
+  exploit EQH; eauto. simpl. intro EQ.
+  assert (EQ1: rs' (S sl) = rs (S sl)) by (eapply agree_slot; eauto).
+  assert (EQ2: rs' (R r) = rs (R r)) by (eapply agree_reg; eauto; tauto).
+  rewrite <- EQ1; rewrite EQ; rewrite EQ2. rewrite locmap_set_reg_same.
+  apply match_states_regular with sm; auto. tauto. 
+  (* found an equation *)
+  destruct (find_reg_containing sl eqs) as [r'|]_eqn.
+  exploit EQH. eapply find_reg_containing_sound; eauto. 
+  simpl; intro EQ.
+  (* turned into a move *)
+  destruct (safe_move_insertion b) as []_eqn. 
+  left; econstructor; split. constructor. simpl; eauto. 
+  rewrite UGS. rewrite <- EQ.
+  apply match_states_regular with true; auto. 
+  apply eqs_movestack_hold; auto. 
+  rewrite (agree_slot _ _ _ sl AG). apply agree_set. eapply agree_undef_move_1; eauto.
+  (* left as a getstack *)
+  left; econstructor; split. constructor.
+  repeat rewrite UGS.
+  apply match_states_regular with sm; auto. 
+  apply eqs_getstack_hold; auto. 
+  rewrite (agree_slot _ _ _ sl AG). apply agree_set. auto. 
+  intuition congruence. 
+  (* no equation, left as a getstack *)
+  left; econstructor; split. constructor.
+  repeat rewrite UGS.
+  apply match_states_regular with sm; auto. 
+  apply eqs_getstack_hold; auto. 
+  rewrite (agree_slot _ _ _ sl AG). apply agree_set. auto.
+  tauto.
+
+(* setstack *)
+  left; econstructor; split. constructor.
+  apply match_states_regular with false; auto.
+  apply eqs_setstack_hold; auto.
+  rewrite (agree_reg _ _ _ r AG). apply agree_set. eapply agree_undef_move_2; eauto. 
+  simpl in SAFE. destruct (in_dec mreg_eq r destroyed_at_move_regs); simpl in SAFE; intuition congruence.
+
+(* op *)
+  left; econstructor; split. constructor. 
+  instantiate (1 := v). rewrite <- H.
+  rewrite (agree_regs _ _ _ args AG). 
+  apply eval_operation_preserved. exact symbols_preserved.
+  simpl in SAFE. destruct (list_disjoint_dec mreg_eq args destroyed_at_move_regs); simpl in SAFE; intuition congruence.
+  apply match_states_regular with false; auto.
+  apply kill_loc_hold; apply kill_at_op_hold; auto.
+  apply agree_set. eapply agree_undef_op; eauto.
+
+(* load *)
+  left; econstructor; split.
+  econstructor.  instantiate (1 := a).  rewrite <- H.
+  rewrite (agree_regs _ _ _ args AG). 
+  apply eval_addressing_preserved.  exact symbols_preserved.
+  simpl in SAFE. destruct (list_disjoint_dec mreg_eq args destroyed_at_move_regs); simpl in SAFE; intuition congruence.
+  eauto.
+  apply match_states_regular with false; auto.
+  apply kill_loc_hold; apply kill_temps_hold; auto.
+  apply agree_set. eapply agree_undef_temps; eauto.
+
+(* store *)
+Opaque list_disjoint_dec.
+  simpl in SAFE.
+  assert (sm = false \/ ~In src destroyed_at_move_regs /\ list_disjoint args destroyed_at_move_regs).
+    destruct SAFE. auto. right. 
+    destruct (list_disjoint_dec mreg_eq (src :: args) destroyed_at_move_regs); try discriminate.
+    split. eapply list_disjoint_notin; eauto with coqlib. eapply list_disjoint_cons_left; eauto. 
+  left; econstructor; split.
+  econstructor.  instantiate (1 := a).  rewrite <- H.
+  rewrite (agree_regs _ _ _ args AG). 
+  apply eval_addressing_preserved.  exact symbols_preserved.
+  tauto.
+  rewrite (agree_reg _ _ _ src AG).
+  eauto.
+  tauto.
+  apply match_states_regular with false; auto.
+  apply kill_temps_hold; auto.
+  eapply agree_undef_temps; eauto.
+
+(* call *)
+  simpl in SAFE. assert (sm = false) by intuition congruence. 
+  subst sm. rewrite agree_false in AG. subst rs'. 
+  left; econstructor; split.
+  constructor. eapply find_function_translated; eauto. 
+  symmetry; apply sig_preserved.
+  constructor. constructor; auto. constructor. 
+
+(* tailcall *)
+  simpl in SAFE. assert (sm = false) by intuition congruence. 
+  subst sm. rewrite agree_false in AG. subst rs'. 
+  left; econstructor; split.
+  constructor. eapply find_function_translated; eauto. 
+  symmetry; apply sig_preserved. eauto. 
+  rewrite (match_parent_locset _ _ STK). constructor; auto.
+
+(* builtin *)
+  left; econstructor; split.
+  constructor.
+  rewrite (agree_regs _ _ _ args AG). 
+  eapply external_call_symbols_preserved; eauto. 
+  exact symbols_preserved. exact varinfo_preserved.
+  simpl in SAFE. destruct (list_disjoint_dec mreg_eq args destroyed_at_move_regs); simpl in SAFE; intuition congruence.
+  apply match_states_regular with false; auto.
+  apply kill_loc_hold; apply kill_temps_hold; auto.
+  apply agree_set. eapply agree_undef_temps; eauto.
+
+(* annot *)
+  simpl in SAFE. assert (sm = false) by intuition congruence. 
+  subst sm. rewrite agree_false in AG. subst rs'. 
+  left; econstructor; split.
+  econstructor. eapply external_call_symbols_preserved; eauto. 
+  exact symbols_preserved. exact varinfo_preserved.
+  apply match_states_regular with false; auto.
+  rewrite agree_false; auto. 
+
+(* label *)
+  left; econstructor; split. constructor.
+  apply match_states_regular with false; auto. 
+  apply nil_hold.
+  simpl in SAFE. destruct SAFE. subst sm. auto. congruence.
+
+(* goto *)
+  generalize (transl_find_label lbl (fn_code f) nil).  rewrite H. simpl. intros.
+  left; econstructor; split. constructor; eauto.
+  apply match_states_regular with false; auto. 
+  apply nil_hold.
+  simpl in SAFE. destruct SAFE. subst sm. auto. congruence.
+
+(* cond true *)
+  generalize (transl_find_label lbl (fn_code f) nil).  rewrite H0. simpl. intros.
+  left; econstructor; split.
+  apply exec_Lcond_true; auto.
+  rewrite (agree_regs _ _ _ args AG). auto.
+  simpl in SAFE. destruct (list_disjoint_dec mreg_eq args destroyed_at_move_regs); simpl in SAFE; intuition congruence.
+  eauto.
+  apply match_states_regular with false; auto.
+  apply nil_hold. 
+  eapply agree_undef_temps; eauto.
+
+(* cond false *)
+  left; econstructor; split. apply exec_Lcond_false; auto.
+  rewrite (agree_regs _ _ _ args AG). auto.
+  simpl in SAFE. destruct (list_disjoint_dec mreg_eq args destroyed_at_move_regs); simpl in SAFE; intuition congruence.
+  apply match_states_regular with false; auto.
+  apply kill_temps_hold; auto.
+  eapply agree_undef_temps; eauto.
+
+(* jumptable *)
+  generalize (transl_find_label lbl (fn_code f) nil).  rewrite H1. simpl. intros.
+  left; econstructor; split. econstructor; eauto.
+  rewrite (agree_reg _ _ _ arg AG). auto.
+  simpl in SAFE. destruct (in_dec mreg_eq arg destroyed_at_move_regs); simpl in SAFE; intuition congruence.
+  apply match_states_regular with false; auto.
+  apply nil_hold.
+  eapply agree_undef_temps; eauto.
+
+(* return *)
+  simpl in SAFE. destruct SAFE; try discriminate. subst sm. rewrite agree_false in AG. subst rs'.
+  left; econstructor; split.
+  constructor. simpl. eauto. 
+  rewrite (match_parent_locset _ _ STK). 
+  constructor; auto.
+
+(* internal *)
+  left; econstructor; split.
+  constructor. simpl; eauto.
+  simpl. apply match_states_regular with false; auto. apply nil_hold. rewrite agree_false; auto.
+
+(* external *)
+  left; econstructor; split.
+  econstructor. eapply external_call_symbols_preserved; eauto. 
+  exact symbols_preserved. exact varinfo_preserved. 
+  auto. eauto. 
+  constructor; auto. 
+
+(* return *)
+  inv STK. inv H1. left; econstructor; split. constructor.
+  apply match_states_regular with false; auto.
+  apply nil_hold.
+  rewrite agree_false; auto.
+Qed.
+
+Lemma transf_initial_states:
+  forall st1, initial_state prog st1 ->
+  exists st2, initial_state tprog st2 /\ match_states st1 st2.
+Proof.
+  intros. inversion H.
+  econstructor; split.
+  econstructor.
+  apply Genv.init_mem_transf; eauto.
+  rewrite symbols_preserved. eauto.
+  apply function_ptr_translated; eauto. 
+  rewrite sig_preserved. auto.
+  econstructor; eauto. constructor.
+Qed.
+
+Lemma transf_final_states:
+  forall st1 st2 r, 
+  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
+Proof.
+  intros. inv H0. inv H. inv STK. econstructor. auto.
+Qed.
+
+Theorem transf_program_correct:
+  forward_simulation (Linear.semantics prog) (Linear.semantics tprog).
+Proof.
+  eapply forward_simulation_opt.
+  eexact symbols_preserved.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  eexact transf_step_correct. 
+Qed.
+
+End PRESERVATION.
diff --git a/backend/RREtyping.v b/backend/RREtyping.v
new file mode 100644
index 0000000..2501c7f
--- /dev/null
+++ b/backend/RREtyping.v
@@ -0,0 +1,109 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Proof of type preservation for the [RRE] pass. *)
+
+Require Import Coqlib.
+Require Import AST.
+Require Import Locations.
+Require Import Linear.
+Require Import Lineartyping.
+Require Import Conventions.
+Require Import RRE.
+Require Import RREproof.
+
+Remark wt_cons:
+  forall f c i, wt_instr f i -> wt_code f c -> wt_code f (i::c).
+Proof.
+  intros; red; intros. simpl in H1; destruct H1. congruence. auto.
+Qed.
+
+Hint Constructors wt_instr : linearty.
+Hint Resolve wt_cons: linearty.
+
+Definition wt_eqs (eqs: equations) :=
+  forall e, In e eqs -> slot_type (e_slot e) = mreg_type (e_reg e).
+
+Lemma wt_eqs_nil:
+  wt_eqs nil.
+Proof. red; simpl; tauto. Qed.
+
+Lemma wt_eqs_cons:
+  forall r s eqs,
+  slot_type s = mreg_type r -> wt_eqs eqs -> wt_eqs (mkeq r s :: eqs).
+Proof.
+  intros; red; simpl; intros. destruct H1. subst; simpl; auto. auto.
+Qed.
+  
+Lemma wt_kill_loc:
+  forall l eqs,
+  wt_eqs eqs -> wt_eqs (kill_loc l eqs).
+Proof.
+  intros; red; intros. exploit In_kill_loc; eauto. intros [A B]. auto.
+Qed.
+
+Lemma wt_kill_locs:
+  forall ll eqs,
+  wt_eqs eqs -> wt_eqs (kill_locs ll eqs).
+Proof.
+  intros; red; intros. exploit In_kill_locs; eauto. intros [A B]. auto.
+Qed.
+
+Lemma wt_kill_temps:
+  forall eqs, wt_eqs eqs -> wt_eqs (kill_temps eqs).
+Proof.
+  exact (wt_kill_locs temporaries).
+Qed.
+
+Lemma wt_kill_at_move:
+  forall eqs, wt_eqs eqs -> wt_eqs (kill_at_move eqs).
+Proof.
+  exact (wt_kill_locs destroyed_at_move).
+Qed.
+
+Hint Resolve wt_eqs_nil wt_eqs_cons wt_kill_loc wt_kill_locs
+             wt_kill_temps wt_kill_at_move: linearty.
+
+Lemma wt_kill_op:
+  forall op eqs, wt_eqs eqs -> wt_eqs (kill_op op eqs).
+Proof.
+  intros; destruct op; simpl; apply wt_kill_locs; auto.
+Qed.
+
+Hint Resolve wt_kill_op: linearty.
+
+Lemma wt_transf_code:
+  forall f c eqs, wt_code f c -> wt_eqs eqs ->
+  wt_code (transf_function f) (transf_code eqs c).
+Proof.
+  induction c; intros; simpl.
+  red; simpl; tauto.
+  assert (WI: wt_instr f a) by auto with coqlib.
+  assert (WC: wt_code f c) by (red; auto with coqlib).
+  clear H.
+  inv WI; auto 10 with linearty.
+  destruct (is_incoming s) as []_eqn. auto with linearty.
+  destruct (contains_equation s r eqs). auto with linearty.
+  destruct (find_reg_containing s eqs) as [r'|]_eqn; auto with linearty.
+  assert (mreg_type r' = mreg_type r).
+  exploit H0. eapply find_reg_containing_sound; eauto. simpl. congruence.
+  destruct (safe_move_insertion c); auto 10 with linearty.
+Qed.
+
+Lemma program_typing_preserved:
+  forall p, wt_program p -> wt_program (transf_program p).
+Proof.
+  intros. red; intros. exploit transform_program_function; eauto. 
+  intros [f0 [A B]]. subst f. exploit H; eauto. intros WTFD.
+  inv WTFD; simpl; constructor.  red; simpl. 
+  apply wt_transf_code; auto with linearty.
+Qed.
-- 
cgit v1.2.3