Fusion des modifications faites sur les branches "tailcalls" et "smallstep".

En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 496 insertions, 1475 deletions

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index f0b2968..1b5a415 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -1,16 +1,17 @@
 (** Correctness proof for the [Allocation] pass (translation from
   RTL to LTL). *)
 
-Require Import Relations.
 Require Import FSets.
 Require Import SetoidList.
 Require Import Coqlib.
+Require Import Errors.
 Require Import Maps.
 Require Import AST.
 Require Import Integers.
 Require Import Values.
 Require Import Mem.
 Require Import Events.
+Require Import Smallstep.
 Require Import Globalenvs.
 Require Import Op.
 Require Import Registers.
@@ -20,7 +21,6 @@ Require Import Locations.
 Require Import Conventions.
 Require Import Coloring.
 Require Import Coloringproof.
-Require Import Parallelmove.
 Require Import Allocation.
 
 (** * Semantic properties of calling conventions *)
@@ -53,9 +53,27 @@ Proof.
   auto.
   case (In_dec Loc.eq (R (loc_result sig)) destroyed_at_call); intro.
   auto.
-  elim n0. apply loc_result_acceptable.
+  elim n0. apply loc_result_caller_save.
 Qed.
 
+(** Function arguments for a tail call are preserved by a
+    [return_regs] operation. *)
+
+Lemma return_regs_arguments:
+  forall sig caller callee,
+  tailcall_possible sig ->
+  map (LTL.return_regs caller callee) (loc_arguments sig) =
+  map callee (loc_arguments sig).
+Proof.
+  intros. apply list_map_exten; intros.
+  generalize (H x H0). destruct x; intro.
+  unfold LTL.return_regs.
+  destruct (In_dec Loc.eq (R m) temporaries). auto.
+  destruct (In_dec Loc.eq (R m) destroyed_at_call). auto.
+  elim n0. eapply arguments_caller_save; eauto.
+  contradiction.
+Qed. 
+
 (** Acceptable locations that are not destroyed at call keep
   their values across a call. *)
 
@@ -73,31 +91,22 @@ Proof.
   auto.
 Qed.
 
-(** * Correctness condition for the liveness analysis *)
-
-(** The liveness information computed by the dataflow analysis is
-  correct in the following sense: all registers live ``before''
-  an instruction are live ``after'' all of its predecessors. *)
+(** Characterization of parallel assignments. *)
 
-Lemma analyze_correct:
-  forall (f: function) (live: PMap.t Regset.t) (n s: node),
-  analyze f = Some live ->
-  f.(fn_code)!n <> None ->
-  f.(fn_code)!s <> None ->
-  In s (successors f n) ->
-  RegsetLat.ge live!!n (transfer f s live!!s).
+Lemma parmov_spec:
+  forall ls srcs dsts,
+  Loc.norepet dsts -> List.length srcs = List.length dsts ->
+  List.map (LTL.parmov srcs dsts ls) dsts = List.map ls srcs /\
+  (forall l, Loc.notin l dsts -> LTL.parmov srcs dsts ls l = ls l).
 Proof.
-  intros.
-  eapply DS.fixpoint_solution.
-  unfold analyze in H. eexact H.
-  elim (fn_code_wf f n); intro. auto. contradiction.
-  elim (fn_code_wf f s); intro. auto. contradiction.
+  induction srcs; destruct dsts; simpl; intros; try discriminate.
   auto.
+  inv H. inv H0. destruct (IHsrcs _ H4 H1). split.
+  f_equal. apply Locmap.gss. rewrite <- H. apply list_map_exten; intros.
+  symmetry. apply Locmap.gso. eapply Loc.in_notin_diff; eauto. 
+  intros x [A B]. rewrite Locmap.gso; auto. apply Loc.diff_sym; auto.
 Qed.
 
-Definition live0 (f: RTL.function) (live: PMap.t Regset.t) :=
-  transfer f f.(RTL.fn_entrypoint) live!!(f.(RTL.fn_entrypoint)).
-
 (** * Properties of allocated locations *)
 
 (** We list here various properties of the locations [alloc r],
@@ -112,19 +121,6 @@ Variable live: PMap.t Regset.t.
 Variable alloc: reg -> loc.
 Hypothesis ALLOC: regalloc f live (live0 f live) env = Some alloc.
 
-Lemma loc_acceptable_noteq_diff:
-  forall l1 l2,
-  loc_acceptable l1 -> l1 <> l2 -> Loc.diff l1 l2.
-Proof.
-  unfold loc_acceptable, Loc.diff; destruct l1; destruct l2;
-  try (destruct s); try (destruct s0); intros; auto; try congruence.
-  case (zeq z z0); intro. 
-  compare t t0; intro.
-  subst z0; subst t0; tauto.
-  tauto. tauto.
-  contradiction. contradiction.
-Qed.
-
 Lemma regalloc_noteq_diff:
   forall r1 l2,
   alloc r1 <> l2 -> Loc.diff (alloc r1) l2.
@@ -134,18 +130,6 @@ Proof.
   auto.
 Qed.   
 
-Lemma loc_acceptable_notin_notin:
-  forall r ll,
-  loc_acceptable r ->
-  ~(In r ll) -> Loc.notin r ll.
-Proof.
-  induction ll; simpl; intros.
-  auto.
-  split. apply loc_acceptable_noteq_diff. assumption. 
-  apply sym_not_equal. tauto. 
-  apply IHll. assumption. tauto. 
-Qed.
-
 Lemma regalloc_notin_notin:
   forall r ll,
   ~(In (alloc r) ll) -> Loc.notin (alloc r) ll.
@@ -153,6 +137,15 @@ Proof.
   intros. apply loc_acceptable_notin_notin. 
   eapply regalloc_acceptable; eauto. auto.
 Qed.
+
+Lemma regalloc_notin_notin_2:
+  forall l rl,
+  ~(In l (map alloc rl)) -> Loc.notin l (map alloc rl).
+Proof.
+  induction rl; simpl; intros. auto. 
+  split. apply Loc.diff_sym. apply regalloc_noteq_diff. tauto.
+  apply IHrl. tauto.
+Qed.
   
 Lemma regalloc_norepet_norepet:
   forall rl,
@@ -215,7 +208,7 @@ Hypothesis REGALLOC: regalloc f flive (live0 f flive) env = Some assign.
   of [assign r] can be arbitrary. *)
 
 Definition agree (live: Regset.t) (rs: regset) (ls: locset) : Prop :=
-  forall (r: reg), Regset.In r live -> ls (assign r) = rs#r.
+  forall (r: reg), Regset.In r live -> Val.lessdef (rs#r) (ls (assign r)).
 
 (** What follows is a long list of lemmas expressing properties
   of the [agree_live_regs] predicate that are useful for the 
@@ -232,6 +225,24 @@ Proof.
   apply H0. apply H. auto.
 Qed.
 
+Lemma agree_succ:
+  forall n s rs ls live,
+  analyze f = Some live ->
+  In s (RTL.successors f n) ->
+  agree live!!n rs ls ->
+  agree (transfer f s live!!s) rs ls.
+Proof.
+  intros.
+  elim (RTL.fn_code_wf f n); intro.
+  elim (RTL.fn_code_wf f s); intro.
+  apply agree_increasing with (live!!n).
+  eapply DS.fixpoint_solution. unfold analyze in H; eauto.
+  auto. auto. auto. auto.
+  unfold transfer. rewrite H3.
+  red; intros. elim (Regset.empty_1 _ H4).
+  unfold RTL.successors in H0; rewrite H2 in H0; elim H0.
+Qed.
+

 (** Some useful special cases of [agree_increasing]. *)
 
 
@@ -266,7 +277,7 @@ Qed.
 
 Lemma agree_eval_reg:
   forall r live rs ls,
-  agree (reg_live r live) rs ls -> ls (assign r) = rs#r.
+  agree (reg_live r live) rs ls -> Val.lessdef (rs#r) (ls (assign r)).
 Proof.
   intros. apply H. apply Regset.add_1. auto. 
 Qed.
@@ -276,11 +287,11 @@ Qed.
 Lemma agree_eval_regs:
   forall rl live rs ls,
   agree (reg_list_live rl live) rs ls ->
-  List.map ls (List.map assign rl) = rs##rl.
+  Val.lessdef_list (rs##rl) (List.map ls (List.map assign rl)).
 Proof.
   induction rl; simpl; intros.
-  reflexivity.
-  apply (f_equal2 (@cons val)). 
+  constructor.
+  constructor.
   apply agree_eval_reg with live. 
   apply agree_reg_list_live with rl. auto.
   eapply IHrl. eexact H.
@@ -322,21 +333,18 @@ Qed.
   are mapped to locations other than that of [r]. *)
 
 Lemma agree_assign_live:
-  forall live r rs ls ls' v,
+  forall live r rs ls v v',
   (forall s,
      Regset.In s live -> s <> r -> assign s <> assign r) ->
-  ls' (assign r) = v ->
-  (forall l, Loc.diff l (assign r) -> Loc.notin l temporaries -> ls' l = ls l) ->
+  Val.lessdef v v' ->
   agree (reg_dead r live) rs ls ->
-  agree live (rs#r <- v) ls'.
+  agree live (rs#r <- v) (Locmap.set (assign r) v' ls).
 Proof.
-  unfold agree; intros.
-  case (Reg.eq r r0); intro.
-  subst r0. rewrite Regmap.gss. assumption.
-  rewrite Regmap.gso; auto.
-  rewrite H1. apply H2. apply Regset.remove_2; auto. 
-  eapply regalloc_noteq_diff. eauto. apply H. auto.  auto.
-  eapply regalloc_not_temporary; eauto.
+  unfold agree; intros. rewrite Regmap.gsspec.
+  destruct (peq r0 r).
+  subst r0. rewrite Locmap.gss. auto.
+  rewrite Locmap.gso. apply H1. apply Regset.remove_2; auto.
+  eapply regalloc_noteq_diff. eauto. apply sym_not_equal. apply H. auto.  auto.
 Qed.
 
 (** This is a special case of the previous lemma where the value [v]
@@ -347,30 +355,47 @@ Qed.
   are mapped to locations other than that of [res]. *)
 
 Lemma agree_move_live:
-  forall live arg res rs (ls ls': locset),
+  forall live arg res rs (ls: locset),
   (forall r,
      Regset.In r live -> r <> res -> r <> arg -> 
      assign r <> assign res) ->
-  ls' (assign res) = ls (assign arg) ->
-  (forall l, Loc.diff l (assign res) -> Loc.notin l temporaries -> ls' l = ls l) ->
   agree (reg_live arg (reg_dead res live)) rs ls ->
-  agree live (rs#res <- (rs#arg)) ls'.
+  agree live (rs#res <- (rs#arg)) (Locmap.set (assign res) (ls (assign arg)) ls).
 Proof.
-  unfold agree; intros. 
-  case (Reg.eq res r); intro.
-  subst r. rewrite Regmap.gss. rewrite H0. apply H2.
+  unfold agree; intros. rewrite Regmap.gsspec. destruct (peq r res). 
+  subst r. rewrite Locmap.gss. apply H0.
   apply Regset.add_1; auto.
-  rewrite Regmap.gso; auto.
-  case (Loc.eq (assign r) (assign res)); intro.
-  rewrite e. rewrite H0.
-  case (Reg.eq arg r); intro.
-  subst r. apply H2. apply Regset.add_1; auto.
-  elim (H r); auto.
-  rewrite H1. apply H2. 
-  case (Reg.eq arg r); intro. subst r. apply Regset.add_1; auto.
-  apply Regset.add_2. apply Regset.remove_2. auto. auto. 
-  eapply regalloc_noteq_diff; eauto.
-  eapply regalloc_not_temporary; eauto.
+  destruct (Reg.eq r arg).
+  subst r.
+  replace (Locmap.set (assign res) (ls (assign arg)) ls (assign arg))
+     with (ls (assign arg)).
+  apply H0. apply Regset.add_1. auto.
+  symmetry. destruct (Loc.eq (assign arg) (assign res)).
+  rewrite <- e. apply Locmap.gss.
+  apply Locmap.gso. eapply regalloc_noteq_diff; eauto.
+
+  rewrite Locmap.gso. apply H0. apply Regset.add_2. apply Regset.remove_2. auto. auto.
+  eapply regalloc_noteq_diff; eauto. apply sym_not_equal. apply H; auto.
+Qed.
+
+(** Yet another special case corresponding to the case of 
+  a redundant move. *)
+
+Lemma agree_redundant_move_live:
+  forall live arg res rs (ls: locset),
+  (forall r,
+     Regset.In r live -> r <> res -> r <> arg -> 
+     assign r <> assign res) ->
+  agree (reg_live arg (reg_dead res live)) rs ls ->
+  assign res = assign arg ->
+  agree live (rs#res <- (rs#arg)) ls.
+Proof.
+  intros. 
+  apply agree_exten with (Locmap.set (assign res) (ls (assign arg)) ls).
+  eapply agree_move_live; eauto. 
+  intros. symmetry. rewrite H1. destruct (Loc.eq l (assign arg)).
+  subst l. apply Locmap.gss.
+  apply Locmap.gso. eapply regalloc_noteq_diff; eauto. 
 Qed.
 
 (** This complicated lemma states agreement between the states after
@@ -384,7 +409,7 @@ Lemma agree_call:
     ~(In (assign r) Conventions.destroyed_at_call)) ->
   (forall r,
     Regset.In r live -> r <> res -> assign r <> assign res) ->
-  ls' (assign res) = v ->
+  Val.lessdef v (ls' (assign res)) ->
   (forall l,
     Loc.notin l destroyed_at_call -> loc_acceptable l -> Loc.diff l (assign res) ->
     ls' l = ls l) ->
@@ -413,757 +438,33 @@ Lemma agree_init_regs:
   (forall r1 r2,
     In r1 rl -> Regset.In r2 live -> r1 <> r2 ->
     assign r1 <> assign r2) ->
-  List.map ls (List.map assign rl) = vl ->
-  agree (reg_list_dead rl live) (Regmap.init Vundef) ls ->
+  Val.lessdef_list vl (List.map ls (List.map assign rl)) ->
   agree live (init_regs vl rl) ls.
 Proof.
   induction rl; simpl; intros.
-  assumption.
-  destruct vl. discriminate. 
-  assert (agree (reg_dead a live) (init_regs vl rl) ls).
-  apply IHrl. intros. apply H. tauto.
-  eapply Regset.remove_3; eauto.
-  auto. congruence. assumption.
+  red; intros. rewrite Regmap.gi. auto.
+  inv H0. 
+  assert (agree live (init_regs vl1 rl) ls).
+  apply IHrl. intros. apply H. tauto. auto. auto. auto.
   red; intros. case (Reg.eq a r); intro.
-  subst r. rewrite Regmap.gss. congruence. 
-  rewrite Regmap.gso; auto. apply H2.
-  apply Regset.remove_2; auto. 
+  subst r. rewrite Regmap.gss. auto.
+  rewrite Regmap.gso; auto.
 Qed.
 
 Lemma agree_parameters:
   forall vl ls,
   let params := f.(RTL.fn_params) in
-  List.map ls (List.map assign params) = vl ->
-  (forall r,
-     Regset.In r (reg_list_dead params (live0 f flive)) ->
-     ls (assign r) = Vundef) ->
-  agree (live0 f flive) (init_regs vl params) ls.
+  Val.lessdef_list vl (List.map ls (List.map assign params)) ->
+  agree (live0 f flive)
+        (init_regs vl params) 
+        ls.
 Proof.
   intros. apply agree_init_regs. 
   intros. eapply regalloc_correct_3; eauto.
-  assumption. 
-  red; intros. rewrite Regmap.gi. auto.
-Qed.
-
-End AGREE.
-
-(** * Correctness of the LTL constructors *)
-
-(** This section proves theorems that establish the correctness of the
-  LTL constructor functions such as [add_op].  The theorems are of
-  the general form ``the generated LTL instructions execute and
-  modify the location set in the expected way: the result location(s)
-  contain the expected values and other, non-temporary locations keep
-  their values''. *)
-
-Section LTL_CONSTRUCTORS.
-
-Variable ge: LTL.genv.
-Variable sp: val.
-
-Lemma reg_for_spec:
-  forall l,
-  R(reg_for l) = l \/ In (R (reg_for l)) temporaries.
-Proof.
-  intros. unfold reg_for. destruct l. tauto.
-  case (slot_type s); simpl; tauto.
-Qed.
-
-Lemma add_reload_correct:
-  forall src dst k rs m,
-  exists rs',
-  exec_instrs ge sp (add_reload src dst k) rs m E0 k rs' m /\
-  rs' (R dst) = rs src /\
-  forall l, Loc.diff (R dst) l -> rs' l = rs l.
-Proof.
-  intros. unfold add_reload. destruct src.
-  case (mreg_eq m0 dst); intro.
-  subst dst. exists rs. split. apply exec_refl. tauto.
-  exists (Locmap.set (R dst) (rs (R m0)) rs).
-  split. apply exec_one; apply exec_Bop.  reflexivity. 
-  split. apply Locmap.gss. 
-  intros; apply Locmap.gso; auto.
-  exists (Locmap.set (R dst) (rs (S s)) rs).
-  split. apply exec_one; apply exec_Bgetstack. 
-  split. apply Locmap.gss. 
-  intros; apply Locmap.gso; auto.
-Qed.
-
-Lemma add_spill_correct:
-  forall src dst k rs m,
-  exists rs',
-  exec_instrs ge sp (add_spill src dst k) rs m E0 k rs' m /\
-  rs' dst = rs (R src) /\
-  forall l, Loc.diff dst l -> rs' l = rs l.
-Proof.
-  intros. unfold add_spill. destruct dst.
-  case (mreg_eq src m0); intro.
-  subst src. exists rs. split. apply exec_refl. tauto.
-  exists (Locmap.set (R m0) (rs (R src)) rs).
-  split. apply exec_one. apply exec_Bop. reflexivity.
-  split. apply Locmap.gss.
-  intros; apply Locmap.gso; auto.
-  exists (Locmap.set (S s) (rs (R src)) rs).
-  split. apply exec_one. apply exec_Bsetstack. 
-  split. apply Locmap.gss.
-  intros; apply Locmap.gso; auto.
-Qed.
-
-Lemma add_reloads_correct_rec:
-  forall srcs itmps ftmps k rs m,
-  (List.length srcs <= List.length itmps)%nat ->
-  (List.length srcs <= List.length ftmps)%nat ->
-  (forall r, In (R r) srcs -> In r itmps -> False) ->
-  (forall r, In (R r) srcs -> In r ftmps -> False) ->
-  list_disjoint itmps ftmps ->
-  list_norepet itmps ->
-  list_norepet ftmps ->
-  exists rs',
-  exec_instrs ge sp (add_reloads srcs (regs_for_rec srcs itmps ftmps) k) rs m E0 k rs' m /\
-  reglist (regs_for_rec srcs itmps ftmps) rs' = map rs srcs /\
-  (forall r, ~(In r itmps) -> ~(In r ftmps) -> rs' (R r) = rs (R r)) /\
-  (forall s, rs' (S s) = rs (S s)).
-Proof.
-  induction srcs; simpl; intros.
-  (* base case *)
-  exists rs. split. apply exec_refl. tauto.
-  (* inductive case *)
-  destruct itmps; simpl in H. omegaContradiction.
-  destruct ftmps; simpl in H0. omegaContradiction.
-  assert (R1: (length srcs <= length itmps)%nat). omega.
-  assert (R2: (length srcs <= length ftmps)%nat). omega.
-  assert (R3: forall r, In (R r) srcs -> In r itmps -> False).
-    intros. apply H1 with r. tauto. auto with coqlib. 
-  assert (R4: forall r, In (R r) srcs -> In r ftmps -> False).
-    intros. apply H2 with r. tauto. auto with coqlib.
-  assert (R5: list_disjoint itmps ftmps).
-    eapply list_disjoint_cons_left.
-    eapply list_disjoint_cons_right. eauto.
-  assert (R6: list_norepet itmps).
-    inversion H4; auto.
-  assert (R7: list_norepet ftmps).
-    inversion H5; auto.
-  destruct a.
-  (* a is a register *)
-  generalize (IHsrcs itmps ftmps k rs m R1 R2 R3 R4 R5 R6 R7).
-  intros [rs' [EX [RES [OTH1 OTH2]]]].
-  exists rs'. split.
-  unfold add_reload. case (mreg_eq m2 m2); intro; tauto.
-  split. simpl. apply (f_equal2 (@cons val)). 
-  apply OTH1. 
-  red; intro; apply H1 with m2. tauto. auto with coqlib.
-  red; intro; apply H2 with m2. tauto. auto with coqlib.
-  assumption.
-  split. intros. apply OTH1. simpl in H6; tauto. simpl in H7; tauto.
-  auto.
-  (* a is a stack location *)
-  set (tmp := match slot_type s with Tint => m0 | Tfloat => m1 end).
-  assert (NI: ~(In tmp itmps)).
-    unfold tmp; case (slot_type s).
-    inversion H4; auto. 
-    apply list_disjoint_notin with (m1 :: ftmps). 
-    apply list_disjoint_sym. apply list_disjoint_cons_left with m0.
-    auto. auto with coqlib.
-  assert (NF: ~(In tmp ftmps)).
-    unfold tmp; case (slot_type s).
-    apply list_disjoint_notin with (m0 :: itmps). 
-    apply list_disjoint_cons_right with m1.
-    auto. auto with coqlib.
-    inversion H5; auto. 
-  generalize
-    (add_reload_correct (S s) tmp
-       (add_reloads srcs (regs_for_rec srcs itmps ftmps) k) rs m).
-  intros [rs1 [EX1 [RES1 OTH]]].     
-  generalize (IHsrcs itmps ftmps k rs1 m R1 R2 R3 R4 R5 R6 R7).
-  intros [rs' [EX [RES [OTH1 OTH2]]]].
-  exists rs'.
-  split. eapply exec_trans; eauto. traceEq.
-  split. simpl. apply (f_equal2 (@cons val)). 
-  rewrite OTH1; auto.
-  rewrite RES. apply list_map_exten. intros.
-  symmetry. apply OTH. 
-  destruct x; try exact I. simpl. red; intro; subst m2.
-  generalize H6; unfold tmp. case (slot_type s).
-  intro. apply H1 with m0. tauto. auto with coqlib.
-  intro. apply H2 with m1. tauto. auto with coqlib.
-  split. intros. simpl in H6; simpl in H7.
-  rewrite OTH1. apply OTH. 
-  simpl. unfold tmp. case (slot_type s); tauto.
-  tauto. tauto.
-  intros. rewrite OTH2. apply OTH. exact I.
-Qed.
-
-Lemma add_reloads_correct:
-  forall srcs k rs m,
-  (List.length srcs <= 3)%nat ->
-  Loc.disjoint srcs temporaries ->
-  exists rs',
-  exec_instrs ge sp (add_reloads srcs (regs_for srcs) k) rs m E0 k rs' m /\
-  reglist (regs_for srcs) rs' = List.map rs srcs /\
-  forall l, Loc.notin l temporaries -> rs' l = rs l.
-Proof.
-  intros.
-  pose (itmps := IT1 :: IT2 :: IT3 :: nil).
-  pose (ftmps := FT1 :: FT2 :: FT3 :: nil).
-  assert (R1: (List.length srcs <= List.length itmps)%nat).
-    unfold itmps; simpl; assumption.
-  assert (R2: (List.length srcs <= List.length ftmps)%nat).
-    unfold ftmps; simpl; assumption.
-  assert (R3: forall r, In (R r) srcs -> In r itmps -> False).
-    intros. assert (In (R r) temporaries). 
-    simpl in H2; simpl; intuition congruence.
-    generalize (H0 _ _ H1 H3). simpl. tauto.
-  assert (R4: forall r, In (R r) srcs -> In r ftmps -> False).
-    intros. assert (In (R r) temporaries). 
-    simpl in H2; simpl; intuition congruence.
-    generalize (H0 _ _ H1 H3). simpl. tauto.
-  assert (R5: list_disjoint itmps ftmps).
-    red; intros r1 r2; simpl; intuition congruence.
-  assert (R6: list_norepet itmps).
-    unfold itmps. NoRepet.
-  assert (R7: list_norepet ftmps).
-    unfold ftmps. NoRepet.
-  generalize (add_reloads_correct_rec srcs itmps ftmps k rs m
-                R1 R2 R3 R4 R5 R6 R7).
-  intros [rs' [EX [RES [OTH1 OTH2]]]].
-  exists rs'. split. exact EX. 
-  split. exact RES.
-  intros. destruct l. apply OTH1.
-  generalize (Loc.notin_not_in _ _ H1). simpl. intuition congruence.
-  generalize (Loc.notin_not_in _ _ H1). simpl. intuition congruence.
-  apply OTH2.
-Qed.
-
-Lemma add_move_correct:
-  forall src dst k rs m,
-  exists rs',
-  exec_instrs ge sp (add_move src dst k) rs m E0 k rs' m /\
-  rs' dst = rs src /\
-  forall l, Loc.diff l dst -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> rs' l = rs l.
-Proof.
-  intros; unfold add_move.
-  case (Loc.eq src dst); intro.
-  subst dst. exists rs. split. apply exec_refl. tauto.
-  destruct src.
-  (* src is a register *)
-  generalize (add_spill_correct m0 dst k rs m); intros [rs' [EX [RES OTH]]].
-  exists rs'; intuition. apply OTH; apply Loc.diff_sym; auto.
-  destruct dst.
-  (* src is a stack slot, dst a register *)
-  generalize (add_reload_correct (S s) m0 k rs m); intros [rs' [EX [RES OTH]]].
-  exists rs'; intuition. apply OTH; apply Loc.diff_sym; auto.
-  (* src and dst are stack slots *)
-  set (tmp := match slot_type s with Tint => IT1 | Tfloat => FT1 end).
-  generalize (add_reload_correct (S s) tmp (add_spill tmp (S s0) k) rs m);
-  intros [rs1 [EX1 [RES1 OTH1]]].
-  generalize (add_spill_correct tmp (S s0) k rs1 m);
-  intros [rs2 [EX2 [RES2 OTH2]]].
-  exists rs2. split.
-  eapply exec_trans; eauto. traceEq.
-  split. congruence.
-  intros. rewrite OTH2. apply OTH1. 
-  apply Loc.diff_sym. unfold tmp; case (slot_type s); auto.
-  apply Loc.diff_sym; auto.
-Qed.
-
-Lemma effect_move_sequence:
-  forall k moves rs m,
-  let k' := List.fold_right (fun p k => add_move (fst p) (snd p) k) k moves in
-  exists rs',
-  exec_instrs ge sp k' rs m E0 k rs' m /\
-  effect_seqmove moves rs rs'.
-Proof.
-  induction moves; intros until m; simpl.
-  exists rs; split. constructor. constructor.
-  destruct a as [src dst]; simpl.
-  set (k1 := fold_right
-              (fun (p : loc * loc) (k : block) => add_move (fst p) (snd p) k)
-              k moves) in *.
-  destruct (add_move_correct src dst k1 rs m) as [rs1 [A [B C]]].
-  destruct (IHmoves rs1 m) as [rs' [D E]].
-  exists rs'; split. 
-  eapply exec_trans; eauto. traceEq.
-  econstructor; eauto. red. tauto. 
-Qed.
-
-Theorem parallel_move_correct:
-  forall srcs dsts k rs m,
-  List.length srcs = List.length dsts ->
-  Loc.no_overlap srcs dsts ->
-  Loc.norepet dsts ->
-  Loc.disjoint srcs temporaries ->
-  Loc.disjoint dsts temporaries ->
-  exists rs',
-  exec_instrs ge sp (parallel_move srcs dsts k) rs m E0 k rs' m /\
-  List.map rs' dsts = List.map rs srcs /\
-  rs' (R IT3) = rs (R IT3) /\
-  forall l, Loc.notin l dsts -> Loc.notin l temporaries -> rs' l = rs l.
-Proof.
-  intros. 
-  generalize (effect_move_sequence k (parmove srcs dsts) rs m).
-  intros [rs' [EXEC EFFECT]].
-  exists rs'. split. exact EXEC. 
-  apply effect_parmove; auto.
-Qed.
- 
-Lemma add_op_correct:
-  forall op args res s rs m v,
-  (List.length args <= 3)%nat ->
-  Loc.disjoint args temporaries ->
-  eval_operation ge sp op (List.map rs args) = Some v ->
-  exists rs',
-  exec_block ge sp (add_op op args res s) rs m E0 (Cont s) rs' m /\
-  rs' res =  v /\
-  forall l, Loc.diff l res -> Loc.notin l temporaries -> rs' l = rs l.
-Proof.
-  intros. unfold add_op. 
-  caseEq (is_move_operation op args).
-  (* move *)
-  intros arg IMO. 
-  generalize (is_move_operation_correct op args IMO). 
-  intros [EQ1 EQ2]. subst op; subst args.   
-  generalize (add_move_correct arg res (Bgoto s) rs m).
-  intros [rs' [EX [RES OTHER]]].
-  exists rs'. split. 
-  apply exec_Bgoto. exact EX. 
-  split. simpl in H1. congruence.
-  intros. unfold temporaries in H3; simpl in H3. 
-  apply OTHER. assumption. tauto. tauto. 
-  (* other ops *)
-  intros.
-  set (rargs := regs_for args). set (rres := reg_for res).
-  generalize (add_reloads_correct args
-                (Bop op rargs rres (add_spill rres res (Bgoto s)))
-                rs m H H0).
-  intros [rs1 [EX1 [RES1 OTHER1]]].
-  pose (rs2 := Locmap.set (R rres) v rs1).
-  generalize (add_spill_correct rres res (Bgoto s) rs2 m).
-  intros [rs3 [EX3 [RES3 OTHER3]]].
-  exists rs3.
-  split. apply exec_Bgoto. eapply exec_trans. eexact EX1. 
-  eapply exec_trans; eauto. 
-  apply exec_one. unfold rs2. apply exec_Bop. 
-  unfold rargs. rewrite RES1. auto. traceEq.
-  split. rewrite RES3. unfold rs2; apply Locmap.gss. 
-  intros. rewrite OTHER3. unfold rs2. rewrite Locmap.gso.
-  apply OTHER1. assumption. 
-  apply Loc.diff_sym. unfold rres. elim (reg_for_spec res); intro.
-  rewrite H5; auto. 
-  eapply Loc.in_notin_diff; eauto. apply Loc.diff_sym; auto.
-Qed.
-
-Lemma add_load_correct:
-  forall chunk addr args res s rs m a v,
-  (List.length args <= 2)%nat ->
-  Loc.disjoint args temporaries ->
-  eval_addressing ge sp addr (List.map rs args) = Some a ->
-  loadv chunk m a = Some v ->
-  exists rs',
-  exec_block ge sp (add_load chunk addr args res s) rs m E0 (Cont s) rs' m /\
-  rs' res = v /\
-  forall l, Loc.diff l res -> Loc.notin l temporaries -> rs' l = rs l.
-Proof.
-  intros. unfold add_load. 
-  set (rargs := regs_for args). set (rres := reg_for res).
-  assert (LL: (List.length args <= 3)%nat). omega.
-  generalize (add_reloads_correct args
-                (Bload chunk addr rargs rres (add_spill rres res (Bgoto s)))
-                rs m LL H0).
-  intros [rs1 [EX1 [RES1 OTHER1]]].
-  pose (rs2 := Locmap.set (R rres) v rs1).
-  generalize (add_spill_correct rres res (Bgoto s) rs2 m).
-  intros [rs3 [EX3 [RES3 OTHER3]]].
-  exists rs3.
-  split. apply exec_Bgoto. eapply exec_trans; eauto.
-  eapply exec_trans; eauto. 
-  apply exec_one.  unfold rs2. apply exec_Bload with a.
-  unfold rargs; rewrite RES1. assumption. assumption. traceEq.
-  split. rewrite RES3. unfold rs2; apply Locmap.gss.
-  intros. rewrite OTHER3. unfold rs2. rewrite Locmap.gso. 
-  apply OTHER1. assumption. 
-  apply Loc.diff_sym. unfold rres. elim (reg_for_spec res); intro.
-  rewrite H5; auto.
-  eapply Loc.in_notin_diff; eauto. apply Loc.diff_sym; auto.
-Qed.
-
-Lemma add_store_correct:
-  forall chunk addr args src s rs m m' a,
-  (List.length args <= 2)%nat ->
-  Loc.disjoint args temporaries ->
-  Loc.notin src temporaries ->
-  eval_addressing ge sp addr (List.map rs args) = Some a ->
-  storev chunk m a (rs src) = Some m' ->
-  exists rs',
-  exec_block ge sp (add_store chunk addr args src s) rs m E0 (Cont s) rs' m' /\
-  forall l, Loc.notin l temporaries -> rs' l = rs l.
-Proof.
-  intros. 
-  assert (LL: (List.length (src :: args) <= 3)%nat).
-    simpl. omega.
-  assert (DISJ: Loc.disjoint (src :: args) temporaries).
-    red; intros. elim H4; intro. subst x1. 
-    eapply Loc.in_notin_diff; eauto.
-    auto with coqlib.
-  unfold add_store. caseEq (regs_for (src :: args)).
-  unfold regs_for; simpl; intro; discriminate.
-  intros rsrc rargs EQ. 
-  generalize (add_reloads_correct (src :: args)
-               (Bstore chunk addr rargs rsrc (Bgoto s))
-               rs m LL DISJ).
-  intros [rs1 [EX1 [RES1 OTHER1]]].
-  rewrite EQ in RES1. simpl in RES1. injection RES1. 
-  intros RES2 RES3. 
-  exists rs1.
-  split. apply exec_Bgoto. 
-  eapply exec_trans. rewrite <- EQ. eexact EX1. 
-  apply exec_one. apply exec_Bstore with a. 
-  rewrite RES2. assumption. rewrite RES3. assumption. traceEq.
-  exact OTHER1.
-Qed.
-
-Lemma add_alloc_correct:
-  forall arg res s rs m m' sz b,
-  rs arg = Vint sz ->
-  Mem.alloc m 0 (Int.signed sz) = (m', b) ->
-  exists rs',
-  exec_block ge sp (add_alloc arg res s) rs m E0 (Cont s) rs' m' /\
-  rs' res = Vptr b Int.zero /\
-  forall l,
-    Loc.diff l (R Conventions.loc_alloc_argument) ->
-    Loc.diff l (R Conventions.loc_alloc_result) ->
-    Loc.diff l res -> 
-    rs' l = rs l.
-Proof.
-  intros; unfold add_alloc.
-  generalize (add_reload_correct arg loc_alloc_argument
-                (Balloc (add_spill loc_alloc_result res (Bgoto s)))
-                rs m).
-  intros [rs1 [EX1 [RES1 OTHER1]]].
-  pose (rs2 := Locmap.set (R loc_alloc_result) (Vptr b Int.zero) rs1).
-  generalize (add_spill_correct loc_alloc_result res (Bgoto s) rs2 m').
-  intros [rs3 [EX3 [RES3 OTHER3]]].
-  exists rs3.
-  split. apply exec_Bgoto. eapply exec_trans. eexact EX1.
-  eapply exec_trans. apply exec_one. eapply exec_Balloc; eauto. congruence. 
-  fold rs2. eexact EX3. reflexivity. traceEq. 
-  split. rewrite RES3; unfold rs2. apply Locmap.gss.
-  intros. rewrite OTHER3. unfold rs2. rewrite Locmap.gso.
-  apply OTHER1. apply Loc.diff_sym; auto.
-  apply Loc.diff_sym; auto.
-  apply Loc.diff_sym; auto.
-Qed.
-
-Lemma add_cond_correct:
-  forall cond args ifso ifnot rs m b s,
-  (List.length args <= 3)%nat ->
-  Loc.disjoint args temporaries ->
-  eval_condition cond (List.map rs args) = Some b ->
-  s = (if b then ifso else ifnot) ->
-  exists rs',
-  exec_block ge sp (add_cond cond args ifso ifnot) rs m E0 (Cont s) rs' m /\
-  forall l, Loc.notin l temporaries -> rs' l = rs l.
-Proof.
-  intros. unfold add_cond.
-  set (rargs := regs_for args).
-  generalize (add_reloads_correct args
-               (Bcond cond rargs ifso ifnot)
-               rs m H H0).
-  intros [rs1 [EX1 [RES1 OTHER1]]].
-  fold rargs in EX1.
-  exists rs1.
-  split. destruct b; subst s.
-  eapply exec_Bcond_true. eexact EX1. 
-  unfold rargs; rewrite RES1. assumption. 
-  eapply exec_Bcond_false. eexact EX1.
-  unfold rargs; rewrite RES1. assumption. 
-  exact OTHER1.
-Qed.
-
-Definition find_function2 (los: loc + ident) (ls: locset) : option fundef :=
-  match los with
-  | inl l => Genv.find_funct ge (ls l)
-  | inr symb =>
-      match Genv.find_symbol ge symb with
-      | None => None
-      | Some b => Genv.find_funct_ptr ge b
-      end
-  end.
-
-Lemma add_call_correct:
-  forall f vargs m t vres m' sig los args res s ls
-    (EXECF:
-      forall lsi,
-        List.map lsi (loc_arguments (funsig f)) = vargs ->
-        exists lso,
-            exec_function ge f lsi m t lso m'
-         /\ lso (R (loc_result (funsig f))) = vres)
-    (FIND: find_function2 los ls = Some f)
-    (SIG: sig = funsig f)
-    (VARGS: List.map ls args = vargs)
-    (LARGS: List.length args = List.length sig.(sig_args))
-    (AARGS: locs_acceptable args)
-    (RES: loc_acceptable res),
-  exists ls',
-  exec_block ge sp (add_call sig los args res s) ls m t (Cont s) ls' m' /\
-  ls' res = vres /\
-  forall l,
-    Loc.notin l destroyed_at_call -> loc_acceptable l -> Loc.diff l res ->
-    ls' l = ls l.
-Proof.
-  intros until los. 
-  case los; intro fn; intros; simpl in FIND; rewrite <- SIG in EXECF; unfold add_call.
-  (* indirect call *)
-  assert (LEN: List.length args = List.length (loc_arguments sig)).
-    rewrite LARGS. symmetry. apply loc_arguments_length.
-  pose (DISJ := locs_acceptable_disj_temporaries args AARGS).
-  generalize (add_reload_correct fn IT3
-       (parallel_move args (loc_arguments sig)
-          (Bcall sig (inl ident IT3)
-             (add_spill (loc_result sig) res (Bgoto s))))
-       ls m).
-  intros [ls1 [EX1 [RES1 OTHER1]]].
-  generalize
-    (parallel_move_correct args (loc_arguments sig)
-        (Bcall sig (inl ident IT3)
-             (add_spill (loc_result sig) res (Bgoto s)))
-        ls1 m LEN 
-        (no_overlap_arguments args sig AARGS)
-        (loc_arguments_norepet sig)
-        DISJ 
-        (loc_arguments_not_temporaries sig)).
-  intros [ls2 [EX2 [RES2 [TMP2 OTHER2]]]].
-  assert (PARAMS: List.map ls2 (loc_arguments sig) = vargs).
-    rewrite <- VARGS. rewrite RES2. 
-    apply list_map_exten. intros. symmetry. apply OTHER1.
-    apply Loc.diff_sym. apply DISJ. auto. simpl; tauto.
-  generalize (EXECF ls2 PARAMS).
-  intros [ls3 [EX3 RES3]].
-  pose (ls4 := return_regs ls2 ls3).
-  generalize (add_spill_correct (loc_result sig) res
-                (Bgoto s) ls4 m').
-  intros [ls5 [EX5 [RES5 OTHER5]]].
-  exists ls5.
-  (* Execution *)
-  split. apply exec_Bgoto. 
-  eapply exec_trans. eexact EX1.
-  eapply exec_trans. eexact EX2.
-  eapply exec_trans. apply exec_one. apply exec_Bcall with f.
-  unfold find_function. rewrite TMP2. rewrite RES1. 
-  assumption. assumption. eexact EX3.
-  eexact EX5. reflexivity. reflexivity. traceEq.
-  (* Result *)
-  split. rewrite RES5. unfold ls4. rewrite return_regs_result. 
-  assumption.
-  (* Other regs *)
-  intros. rewrite OTHER5; auto.
-  unfold ls4; rewrite return_regs_not_destroyed; auto. 
-  rewrite OTHER2. apply OTHER1. 
-  apply Loc.diff_sym. apply Loc.in_notin_diff with temporaries.  
-  apply temporaries_not_acceptable; auto. simpl; tauto.
-  apply arguments_not_preserved; auto.
-  apply temporaries_not_acceptable; auto.
-  apply Loc.diff_sym; auto.
-  (* direct call *)
-  assert (LEN: List.length args = List.length (loc_arguments sig)).
-    rewrite LARGS. symmetry. apply loc_arguments_length.
-  pose (DISJ := locs_acceptable_disj_temporaries args AARGS).
-  generalize
-    (parallel_move_correct args (loc_arguments sig)
-        (Bcall sig (inr mreg fn)
-             (add_spill (loc_result sig) res (Bgoto s)))
-        ls m LEN 
-        (no_overlap_arguments args sig AARGS)
-        (loc_arguments_norepet sig)
-        DISJ (loc_arguments_not_temporaries sig)).
-  intros [ls2 [EX2 [RES2 [TMP2 OTHER2]]]].
-  assert (PARAMS: List.map ls2 (loc_arguments sig) = vargs).
-    rewrite <- VARGS. rewrite RES2. auto.
-  generalize (EXECF ls2 PARAMS).
-  intros [ls3 [EX3 RES3]].
-  pose (ls4 := return_regs ls2 ls3).
-  generalize (add_spill_correct (loc_result sig) res
-                (Bgoto s) ls4 m').
-  intros [ls5 [EX5 [RES5 OTHER5]]].
-  exists ls5.
-  (* Execution *)
-  split. apply exec_Bgoto. 
-  eapply exec_trans. eexact EX2.
-  eapply exec_trans. apply exec_one. apply exec_Bcall with f.
-  unfold find_function. assumption. assumption. eexact EX3.
-  eexact EX5. reflexivity. traceEq.
-  (* Result *)
-  split. rewrite RES5. 
-  unfold ls4. rewrite return_regs_result. 
-  assumption.
-  (* Other regs *)
-  intros. rewrite OTHER5; auto.
-  unfold ls4; rewrite return_regs_not_destroyed; auto. 
-  apply OTHER2.
-  apply arguments_not_preserved; auto.
-  apply temporaries_not_acceptable; auto.
-  apply Loc.diff_sym; auto.
-Qed.
-
-Lemma add_undefs_correct:
-  forall res b ls m,
-  (forall l, In l res -> loc_acceptable l) ->
-  (forall ofs ty, In (S (Local ofs ty)) res -> ls (S (Local ofs ty)) = Vundef) ->
-  exists ls',
-  exec_instrs ge sp (add_undefs res b) ls m E0 b ls' m /\
-  (forall l, In l res -> ls' l = Vundef) /\
-  (forall l, Loc.notin l res -> ls' l = ls l).
-Proof.
-  induction res; simpl; intros.
-  exists ls. split. apply exec_refl. tauto.
-  assert (ACC: forall l, In l res -> loc_acceptable l).
-    intros. apply H. tauto.
-  destruct a.
-  (* a is a register *)
-  pose (ls1 := Locmap.set (R m0) Vundef ls).
-  assert (UNDEFS: forall ofs ty, In (S (Local ofs ty)) res -> ls1 (S (Local ofs ty)) = Vundef).
-    intros. unfold ls1; rewrite Locmap.gso. auto. red; auto.
-  generalize (IHres b (Locmap.set (R m0) Vundef ls) m ACC UNDEFS).
-  intros [ls2 [EX2 [RES2 OTHER2]]].
-  exists ls2. split.
-  eapply exec_trans. apply exec_one. apply exec_Bop. 
-  simpl; reflexivity. eexact EX2. traceEq.
-  split. intros. case (In_dec Loc.eq l res); intro.
-  apply RES2; auto. 
-  rewrite OTHER2. elim H1; intro.
-  subst l. apply Locmap.gss.
-  contradiction.
-  apply loc_acceptable_notin_notin; auto.  
-  intros. rewrite OTHER2. apply Locmap.gso. 
-  apply Loc.diff_sym; tauto. tauto.
-  (* a is a stack location *)
-  assert (UNDEFS: forall ofs ty, In (S (Local ofs ty)) res -> ls (S (Local ofs ty)) = Vundef).
-    intros. apply H0. tauto.
-  generalize (IHres b ls m ACC UNDEFS).
-  intros [ls2 [EX2 [RES2 OTHER2]]].
-  exists ls2. split. assumption.
-  split. intros. case (In_dec Loc.eq l res); intro.
   auto.
-  rewrite OTHER2. elim H1; intro. 
-  subst l. generalize (H (S s) (in_eq _ _)). 
-  unfold loc_acceptable; destruct s; intuition auto.
-  contradiction.
-  apply loc_acceptable_notin_notin; auto. 
-  intros. apply OTHER2. tauto.
-Qed.
-
-Lemma add_entry_correct:
-  forall sig params undefs s ls m,
-  List.length params = List.length sig.(sig_args) ->
-  Loc.norepet params ->
-  locs_acceptable params ->
-  Loc.disjoint params undefs ->
-  locs_acceptable undefs ->
-  (forall ofs ty, ls (S (Local ofs ty)) = Vundef) ->
-  exists ls',
-  exec_block ge sp (add_entry sig params undefs s) ls m E0 (Cont s) ls' m /\
-  List.map ls' params = List.map ls (loc_parameters sig) /\
-  (forall l, In l undefs -> ls' l = Vundef).
-Proof.
-  intros. 
-  assert (List.length (loc_parameters sig) = List.length params).
-    unfold loc_parameters. rewrite list_length_map. 
-    rewrite loc_arguments_length. auto.
-  assert (DISJ: Loc.disjoint params temporaries).
-    apply locs_acceptable_disj_temporaries; auto.
-  generalize (parallel_move_correct _ _ (add_undefs undefs (Bgoto s))
-                ls m H5
-                (no_overlap_parameters _ _ H1)
-                H0 (loc_parameters_not_temporaries sig) DISJ).
-  intros [ls1 [EX1 [RES1 [TMP1 OTHER1]]]].
-  assert (forall ofs ty, In (S (Local ofs ty)) undefs -> ls1 (S (Local ofs ty)) = Vundef).
-    intros. rewrite OTHER1. auto. apply Loc.disjoint_notin with undefs.
-    apply Loc.disjoint_sym. auto. auto.
-    simpl; tauto.
-  generalize (add_undefs_correct undefs (Bgoto s) ls1 m H3 H6).
-  intros [ls2 [EX2 [RES2 OTHER2]]].
-  exists ls2.
-  split. apply exec_Bgoto. unfold add_entry. 
-  eapply exec_trans. eexact EX1. eexact EX2. traceEq.
-  split. rewrite <- RES1. apply list_map_exten. 
-  intros. symmetry. apply OTHER2. eapply Loc.disjoint_notin; eauto.
-  exact RES2.
-Qed.
-
-Lemma add_return_correct:
-  forall sig optarg ls m,
-  exists ls',
-  exec_block ge sp (add_return sig optarg) ls m E0 Return ls' m /\
-  match optarg with
-  | Some arg => ls' (R (loc_result sig)) = ls arg
-  | None => ls' (R (loc_result sig)) = Vundef
-  end.
-Proof.
-  intros. unfold add_return.
-  destruct optarg.
-  generalize (add_reload_correct l (loc_result sig) Breturn ls m).
-  intros [ls1 [EX1 [RES1 OTH1]]].
-  exists ls1.
-    split. apply exec_Breturn. assumption. assumption.
-  exists (Locmap.set (R (loc_result sig)) Vundef ls).
-    split. apply exec_Breturn. apply exec_one. 
-    apply exec_Bop. reflexivity. apply Locmap.gss. 
-Qed.
-
-End LTL_CONSTRUCTORS.
-
-(** * Exploitation of the typing hypothesis *)
-
-(** Register allocation is applied to RTL code that passed type inference
-  (see file [RTLtyping]), and therefore is well-typed in the type system
-  of [RTLtyping].  We exploit this hypothesis to obtain information on
-  the number of arguments to operations, addressing modes and conditions. *)
-
-Remark length_type_of_condition:
-  forall (c: condition), (List.length (type_of_condition c) <= 3)%nat.
-Proof.
-  destruct c; unfold type_of_condition; simpl; omega.
-Qed.
-
-Remark length_type_of_operation:
-  forall (op: operation), (List.length (fst (type_of_operation op)) <= 3)%nat.
-Proof.
-  destruct op; unfold type_of_operation; simpl; try omega.
-  apply length_type_of_condition.
-Qed.
-
-Remark length_type_of_addressing:
-  forall (addr: addressing), (List.length (type_of_addressing addr) <= 2)%nat.
-Proof.
-  destruct addr; unfold type_of_addressing; simpl; omega.
 Qed.
 
-Lemma length_op_args:
-  forall (env: regenv) (op: operation) (args: list reg) (res: reg),
-  (List.map env args, env res) = type_of_operation op ->
-  (List.length args <= 3)%nat.
-Proof.
-  intros. rewrite <- (list_length_map env). 
-  generalize (length_type_of_operation op).
-  rewrite <- H. simpl. auto.
-Qed.
-
-Lemma length_addr_args:
-  forall (env: regenv) (addr: addressing) (args: list reg),
-  List.map env args = type_of_addressing addr ->
-  (List.length args <= 2)%nat.
-Proof.
-  intros. rewrite <- (list_length_map env). 
-  rewrite H. apply length_type_of_addressing.
-Qed.
-
-Lemma length_cond_args:
-  forall (env: regenv) (cond: condition) (args: list reg),
-  List.map env args = type_of_condition cond ->
-  (List.length args <= 3)%nat.
-Proof.
-  intros. rewrite <- (list_length_map env). 
-  rewrite H. apply length_type_of_condition.
-Qed.
+End AGREE.
 
 (** * Preservation of semantics *)
 
@@ -1176,7 +477,7 @@ Section PRESERVATION.
 
 Variable prog: RTL.program.
 Variable tprog: LTL.program.
-Hypothesis TRANSF: transf_program prog = Some tprog.
+Hypothesis TRANSF: transf_program prog = OK tprog.
 
 Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
@@ -1193,740 +494,460 @@ Lemma functions_translated:
   forall (v: val) (f: RTL.fundef),
   Genv.find_funct ge v = Some f ->
   exists tf,
-  Genv.find_funct tge v = Some tf /\ transf_fundef f = Some tf.
-Proof.  
-  intros. 
-  generalize 
-   (Genv.find_funct_transf_partial transf_fundef TRANSF H).
-  case (transf_fundef f).
-  intros tf [A B]. exists tf. tauto.
-  intros [A B]. elim B. reflexivity.
-Qed.
+  Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
+Proof (Genv.find_funct_transf_partial transf_fundef TRANSF).
 
 Lemma function_ptr_translated:
-  forall (b: Values.block) (f: RTL.fundef),
+  forall (b: block) (f: RTL.fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
-  Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = Some tf.
-Proof.  
-  intros. 
-  generalize 
-   (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF H).
-  case (transf_fundef f).
-  intros tf [A B]. exists tf. tauto.
-  intros [A B]. elim B. reflexivity.
-Qed.
+  Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
+Proof (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF).
 
 Lemma sig_function_translated:
   forall f tf,
-  transf_fundef f = Some tf ->
+  transf_fundef f = OK tf ->
   LTL.funsig tf = RTL.funsig f.
 Proof.
-  intros f tf. destruct f; simpl. 
+  intros f tf. destruct f; simpl.
   unfold transf_function.
   destruct (type_function f).
   destruct (analyze f).
-  destruct (regalloc f t). 
-  intro EQ; injection EQ; intro EQ1; rewrite <- EQ1; simpl; auto.
-  congruence. congruence. congruence.
-  intro EQ; inversion EQ; subst tf. reflexivity.
-Qed.
-
-Lemma entrypoint_function_translated:
-  forall f tf,
-  transf_function f = Some tf ->
-  tf.(LTL.fn_entrypoint) = f.(RTL.fn_nextpc).
-Proof.
-  intros f tf. unfold transf_function.
-  destruct (type_function f).
-  destruct (analyze f).
-  destruct (regalloc f t). 
-  intro EQ; injection EQ; intro EQ1; rewrite <- EQ1; simpl; auto.
-  intros; discriminate.
-  intros; discriminate.
-  intros; discriminate.
+  destruct (regalloc f t).
+  intro. monadInv H. inv EQ. auto.  
+  simpl; congruence. simpl; congruence. simpl; congruence.
+  intro EQ; inv EQ. auto.
 Qed.
 
 (** The proof of semantic preservation is a simulation argument
   based on diagrams of the following form:
 <<
-        pc, rs, m ------------------- pc, ls, m
-            |                             |
-            |                             |
-            v                             v
-        pc', rs', m' ---------------- Cont pc', ls', m'
+           st1 --------------- st2
+            |                   |
+           t|                   |t
+            |                   |
+            v                   v
+           st1'--------------- st2'
 >>
   Hypotheses: the left vertical arrow represents a transition in the
-  original RTL code.  The top horizontal bar expresses agreement between
-  [rs] and [ls] over the pseudo-registers live before the RTL instruction
-  at [pc].  
+  original RTL code.  The top horizontal bar is the [match_states]
+  relation defined below.  It implies agreement between
+  the RTL register map [rs] and the LTL location map [ls]
+  over the pseudo-registers live before the RTL instruction at [pc].  
 
-  Conclusions: the right vertical arrow is an [exec_blocks] transition
+  Conclusions: the right vertical arrow is an [exec_instrs] transition
   in the LTL code generated by translation of the current function.
-  The bottom horizontal bar expresses agreement between [rs'] and [ls']
-  over the pseudo-registers live after the RTL instruction at [pc]
-  (which implies agreement over the pseudo-registers live before
-  the instruction at [pc']).
-
-  We capture these diagrams in the following propositions parameterized
-  by the transition in the original RTL code (the left arrow).
+  The bottom horizontal bar is the [match_states] relation.
 *)
 
-Definition exec_instr_prop
-        (c: RTL.code) (sp: val)
-        (pc: node) (rs: regset) (m: mem) (t: trace)
-        (pc': node) (rs': regset) (m': mem) : Prop :=
-  forall f env live assign ls
-         (CF: c = f.(RTL.fn_code))
-         (WT: wt_function f env)
-         (ASG: regalloc f live (live0 f live) env = Some assign)
-         (AG: agree assign (transfer f pc live!!pc) rs ls),
-  let tc := PTree.map (transf_instr f live assign) c in
-  exists ls',
-    exec_blocks tge tc sp pc ls m t (Cont pc') ls' m' /\
-    agree assign live!!pc rs' ls'.
-
-Definition exec_instrs_prop
-        (c: RTL.code) (sp: val)
-        (pc: node) (rs: regset) (m: mem) (t: trace)
-        (pc': node) (rs': regset) (m': mem) : Prop :=
-  forall f env live assign ls,
-  forall (CF: c = f.(RTL.fn_code))
-         (WT: wt_function f env)
-         (ANL: analyze f = Some live)
-         (ASG: regalloc f live (live0 f live) env = Some assign)
-         (AG: agree assign (transfer f pc live!!pc) rs ls)
-         (VALIDPC': c!pc' <> None),
-  let tc := PTree.map (transf_instr f live assign) c in
-  exists ls',
-    exec_blocks tge tc sp pc ls m t (Cont pc') ls' m' /\
-    agree assign (transfer f pc' live!!pc') rs' ls'.
-
-Definition exec_function_prop
-        (f: RTL.fundef) (args: list val) (m: mem)
-        (t: trace) (res: val) (m': mem) : Prop :=
-  forall ls tf,
-  transf_fundef f = Some tf ->
-  List.map ls (Conventions.loc_arguments (funsig tf)) = args ->
-  exists ls',
-    LTL.exec_function tge tf ls m t ls' m' /\
-    ls' (R (Conventions.loc_result (funsig tf))) = res.
-
-(** The simulation proof is by structural induction over the RTL evaluation
-  derivation.  We prove each case of the proof as a separate lemma.
-  There is one lemma for each RTL evaluation rule.  Each lemma concludes
-  one of the [exec_*_prop] predicates, and takes the induction hypotheses
-  (if any) as hypotheses also expressed with the [exec_*_prop] predicates.
-*)
+Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signature -> Prop :=
+  | match_stackframes_nil: forall ty_args,
+      match_stackframes nil nil (mksignature ty_args (Some Tint))
+  | match_stackframes_cons:
+      forall s ts sig res f sp pc rs ls env live assign,
+      match_stackframes s ts (RTL.fn_sig f) ->
+      wt_function f env ->
+      analyze f = Some live ->
+      regalloc f live (live0 f live) env = Some assign ->
+      (forall rv ls1,
+        (forall l, Loc.notin l destroyed_at_call -> loc_acceptable l -> ls1 l = ls l) ->
+        Val.lessdef rv (ls1 (R (loc_result sig))) ->
+        agree assign (transfer f pc live!!pc)
+              (rs#res <- rv)
+              (Locmap.set (assign res) (ls1 (R (loc_result sig))) ls1)) ->
+      match_stackframes
+        (RTL.Stackframe res (RTL.fn_code f) sp pc rs :: s)
+        (LTL.Stackframe (assign res) (transf_fun f live assign) sp ls pc :: ts)
+        sig.
+
+Inductive match_states: RTL.state -> LTL.state -> Prop :=
+  | match_states_intro:
+      forall s f sp pc rs m ts ls tm live assign env
+      (STACKS: match_stackframes s ts (RTL.fn_sig f))
+      (WT: wt_function f env)
+      (ANL: analyze f = Some live)
+      (ASG: regalloc f live (live0 f live) env = Some assign)
+      (AG: agree assign (transfer f pc live!!pc) rs ls)
+      (MMD: Mem.lessdef m tm),
+      match_states (RTL.State s (RTL.fn_code f) sp pc rs m)
+                   (LTL.State ts (transf_fun f live assign) sp pc ls tm)
+  | match_states_call:
+      forall s f args m ts tf ls tm,
+      match_stackframes s ts (RTL.funsig f) ->
+      transf_fundef f = OK tf ->
+      Val.lessdef_list args (List.map ls (loc_arguments (funsig tf))) ->
+      Mem.lessdef m tm ->
+      (forall l, Loc.notin l destroyed_at_call -> loc_acceptable l -> ls l = parent_locset ts l) ->
+      match_states (RTL.Callstate s f args m)
+                   (LTL.Callstate ts tf ls tm)
+  | match_states_return:
+      forall s v m ts sig ls tm,
+      match_stackframes s ts sig ->
+      Val.lessdef v (ls (R (loc_result sig))) ->
+      Mem.lessdef m tm ->
+      (forall l, Loc.notin l destroyed_at_call -> loc_acceptable l -> ls l = parent_locset ts l) ->
+      match_states (RTL.Returnstate s v m)
+                   (LTL.Returnstate ts sig ls tm).
+
+Remark match_stackframes_change:
+  forall s ts sig,
+  match_stackframes s ts sig ->
+  forall sig',
+  sig_res sig' = sig_res sig ->
+  match_stackframes s ts sig'.
+Proof.
+  induction 1; intros.
+  destruct sig'. simpl in H; inv H. constructor.
+  assert (loc_result sig' = loc_result sig).
+  unfold loc_result. rewrite H4; auto.
+  econstructor; eauto.
+  rewrite H5. auto. 
+Qed.
+
+(** The simulation proof is by case analysis over the RTL transition
+  taken in the source program. *)
 
 Ltac CleanupHyps :=
   match goal with
+  | H: (match_states _ _) |- _ =>
+      inv H; CleanupHyps
   | H1: (PTree.get _ _ = Some _),
-    H2: (_ = RTL.fn_code _),
-    H3: (agree _ (transfer _ _ _) _ _) |- _ =>
-      unfold transfer in H3; rewrite <- H2 in H3; rewrite H1 in H3;
-      simpl in H3;
-      CleanupHyps
+    H2: (agree _ (transfer _ _ _) _ _) |- _ =>
+      unfold transfer in H2; rewrite H1 in H2; simpl in H2; CleanupHyps
+  | _ => idtac
+  end.
+
+Ltac WellTypedHyp :=
+  match goal with
   | H1: (PTree.get _ _ = Some _),
-    H2: (_ = RTL.fn_code _),
-    H3: (wt_function _ _) |- _ =>
-      let H := fresh in
+    H2: (wt_function _ _) |- _ =>
       let R := fresh "WTI" in (
-      generalize (wt_instrs _ _ H3); intro H;
-      rewrite <- H2 in H; generalize (H _ _ H1);
-      intro R; clear H; clear H3);
-      CleanupHyps
+      generalize (wt_instrs _ _ H2 _ _ H1); intro R)
   | _ => idtac
   end.
 
-Ltac CleanupGoal :=
+Ltac TranslInstr :=
   match goal with
-  | H1: (PTree.get _ _ = Some _) |- _ =>
-      eapply exec_blocks_one;
-      [rewrite PTree.gmap; rewrite H1;
-       unfold option_map; unfold transf_instr; reflexivity
-      |idtac]
+  | H: (PTree.get _ _ = Some _) |- _ =>
+      simpl; rewrite PTree.gmap; rewrite H; simpl; auto
   end.
 
-Lemma transl_Inop_correct:
- forall (c : PTree.t instruction) (sp: val) (pc : positive)
-    (rs : regset) (m : mem) (pc' : RTL.node),
-  c ! pc = Some (Inop pc') ->
-  exec_instr_prop c sp pc rs m E0 pc' rs m.
+Ltac MatchStates :=
+  match goal with
+  | |- match_states (RTL.State _ _ _ _ _ _) (LTL.State _ _ _ _ _ _) =>
+      eapply match_states_intro; eauto; MatchStates
+  | H: (PTree.get ?pc _ = Some _) |- agree _ _ _ _ =>
+      eapply agree_succ with (n := pc); eauto; MatchStates
+  | H: (PTree.get _ _ = Some _) |- In _ (RTL.successors _ _) =>
+      unfold RTL.successors; rewrite H; auto with coqlib
+  | _ => idtac
+  end.
+
+
+Lemma transl_find_function:
+  forall ros f args lv rs ls alloc,
+  RTL.find_function ge ros rs = Some f ->
+  agree alloc (reg_list_live args (reg_sum_live ros lv)) rs ls ->
+  exists tf,
+    LTL.find_function tge (sum_left_map alloc ros) ls = Some tf /\
+    transf_fundef f = OK tf.
 Proof.
-  intros; red; intros; CleanupHyps.
-  exists ls. split.
-  CleanupGoal. apply exec_Bgoto. apply exec_refl.
-  assumption.
+  intros; destruct ros; simpl in *.
+  assert (Val.lessdef (rs#r) (ls (alloc r))).
+    eapply agree_eval_reg. eapply agree_reg_list_live; eauto.
+  inv H1. apply functions_translated. auto.
+  exploit Genv.find_funct_inv; eauto. intros [b EQ]. congruence.
+  rewrite symbols_preserved. destruct (Genv.find_symbol ge i).
+  apply function_ptr_translated. auto. discriminate.
 Qed.
 
-Lemma transl_Iop_correct:
-  forall (c : PTree.t instruction) (sp: val) (pc : positive)
-    (rs : Regmap.t val) (m : mem) (op : operation) (args : list reg)
-    (res : reg) (pc' : RTL.node) (v: val),
-  c ! pc = Some (Iop op args res pc') ->
-  eval_operation ge sp op (rs ## args) = Some v ->
-  exec_instr_prop c sp pc rs m E0 pc' (rs # res <- v) m.
+Theorem transl_step_correct:
+  forall s1 t s2, RTL.step ge s1 t s2 ->
+  forall s1', match_states s1 s1' ->
+  exists s2', LTL.step tge s1' t s2' /\ match_states s2 s2'.
 Proof.
-  intros; red; intros; CleanupHyps.
+  induction 1; intros; CleanupHyps; WellTypedHyp.
+
+  (* Inop *)
+  econstructor; split.
+  eapply exec_Lnop. TranslInstr. MatchStates.
+
+  (* Iop *)
+  generalize (PTree.gmap (transf_instr f live assign) pc (RTL.fn_code f)).
+  rewrite H. simpl. 
   caseEq (Regset.mem res live!!pc); intro LV;
   rewrite LV in AG.
   generalize (Regset.mem_2 _ _ LV). intro LV'.
-  assert (LL: (List.length (List.map assign args) <= 3)%nat).
-    rewrite list_length_map. 
-    inversion WTI. simpl; omega. simpl; omega.
-    eapply length_op_args. eauto.
-  assert (DISJ: Loc.disjoint (List.map assign args) temporaries).
-    eapply regalloc_disj_temporaries; eauto.
-  assert (eval_operation tge sp op (map ls (map assign args)) = Some v).
-    replace (map ls (map assign args)) with rs##args. 
-    rewrite (eval_operation_preserved symbols_preserved). assumption.
-    symmetry. eapply agree_eval_regs; eauto.
-  generalize (add_op_correct tge sp op 
-               (List.map assign args) (assign res)
-               pc' ls m v LL DISJ H1).
-  intros [ls' [EX [RES OTHER]]].
-  exists ls'. split. 
-  CleanupGoal. rewrite LV. exact EX. 
-  rewrite CF in H. 
   generalize (regalloc_correct_1 f env live _ _ _ _ ASG H).
-  unfold correct_alloc_instr. 
+  unfold correct_alloc_instr, is_redundant_move.
   caseEq (is_move_operation op args).
   (* Special case for moves *)
   intros arg IMO CORR.
   generalize (is_move_operation_correct _ _ IMO).
   intros [EQ1 EQ2]. subst op; subst args. 
-  injection H0; intro. rewrite <- H2. 
-  apply agree_move_live with f env live ls; auto. 
-  rewrite RES. rewrite <- H2. symmetry. eapply agree_eval_reg.
-  simpl in AG. eexact AG.
+  injection H0; intro.
+  destruct (Loc.eq (assign arg) (assign res)); intro CODE.
+  (* sub-case: redundant move *)
+  econstructor; split. eapply exec_Lnop; eauto.
+  MatchStates. 
+  rewrite <- H1. eapply agree_redundant_move_live; eauto.
+  (* sub-case: non-redundant move *)
+  econstructor; split. eapply exec_Lop; eauto. simpl. eauto.
+  MatchStates.
+  rewrite <- H1. eapply agree_move_live; eauto.
   (* Not a move *)
-  intros INMO CORR.
-  apply agree_assign_live with f env live ls; auto.
+  intros INMO CORR CODE.
+  assert (exists v1,
+          eval_operation tge sp op (map ls (map assign args)) tm = Some v1
+          /\ Val.lessdef v v1).
+    apply eval_operation_lessdef with m (rs##args); auto.
+    eapply agree_eval_regs; eauto.
+    rewrite (eval_operation_preserved symbols_preserved). assumption.
+  destruct H1 as [v1 [EV VMD]].
+  econstructor; split. eapply exec_Lop; eauto. 
+  MatchStates. 
+  apply agree_assign_live with f env live; auto.
   eapply agree_reg_list_live; eauto.
   (* Result is not live, instruction turned into a nop *)
-  exists ls. split.
-  CleanupGoal. rewrite LV. 
-  apply exec_Bgoto; apply exec_refl.
-  apply agree_assign_dead; auto. 
+  intro CODE. econstructor; split. eapply exec_Lnop; eauto.
+  MatchStates. apply agree_assign_dead; auto. 
   red; intro. exploit Regset.mem_1; eauto. congruence.
-Qed.
 
-Lemma transl_Iload_correct:
- forall (c : PTree.t instruction) (sp: val) (pc : positive)
-    (rs : Regmap.t val) (m : mem) (chunk : memory_chunk)
-    (addr : addressing) (args : list reg) (dst : reg) (pc' : RTL.node)
-    (a v : val),
-  c ! pc = Some (Iload chunk addr args dst pc') ->
-  eval_addressing ge sp addr rs ## args = Some a ->
-  loadv chunk m a = Some v ->
-  exec_instr_prop c sp pc rs m E0 pc' rs # dst <- v m.
-Proof.
-  intros; red; intros; CleanupHyps.
+  (* Iload *)
   caseEq (Regset.mem dst live!!pc); intro LV;
   rewrite LV in AG.
   (* dst is live *)
   exploit Regset.mem_2; eauto. intro LV'.
-  assert (LL: (List.length (List.map assign args) <= 2)%nat).
-    rewrite list_length_map. 
-    inversion WTI. 
-    eapply length_addr_args. eauto.
-  assert (DISJ: Loc.disjoint (List.map assign args) temporaries).
-    eapply regalloc_disj_temporaries; eauto.
-  assert (EADDR:
-      eval_addressing tge sp addr (map ls (map assign args)) = Some a).
-    rewrite <- H0. 
-    replace (rs##args) with (map ls (map assign args)).
-    apply eval_addressing_preserved. exact symbols_preserved.
+  assert (exists a',
+      eval_addressing tge sp addr (map ls (map assign args)) = Some a'
+      /\ Val.lessdef a a').
+    apply eval_addressing_lessdef with (rs##args). 
     eapply agree_eval_regs; eauto.
-  generalize (add_load_correct tge sp chunk addr
-               (List.map assign args) (assign dst)
-               pc' ls m _ _ LL DISJ EADDR H1).
-  intros [ls' [EX [RES OTHER]]].
-  exists ls'. split. CleanupGoal. rewrite LV. exact EX. 
-  rewrite CF in H. 
+    rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  destruct H2 as [a' [EVAL VMD]].
+  exploit Mem.loadv_lessdef; eauto. 
+  intros [v' [LOADV VMD2]].
+  econstructor; split.
+  eapply exec_Lload; eauto. TranslInstr. rewrite LV; auto.
   generalize (regalloc_correct_1 f env live _ _ _ _ ASG H).
   unfold correct_alloc_instr. intro CORR.
+  MatchStates. 
   eapply agree_assign_live; eauto.
   eapply agree_reg_list_live; eauto.
   (* dst is dead *)
-  exists ls. split.
-  CleanupGoal. rewrite LV. 
-  apply exec_Bgoto; apply exec_refl.
-  apply agree_assign_dead; auto.
+  econstructor; split.
+  eapply exec_Lnop. TranslInstr. rewrite LV; auto.
+  MatchStates. apply agree_assign_dead; auto.
   red; intro; exploit Regset.mem_1; eauto. congruence.
-Qed.
 
-Lemma transl_Istore_correct:
- forall (c : PTree.t instruction) (sp: val) (pc : positive)
-    (rs : Regmap.t val) (m : mem) (chunk : memory_chunk)
-    (addr : addressing) (args : list reg) (src : reg) (pc' : RTL.node)
-    (a : val) (m' : mem),
-  c ! pc = Some (Istore chunk addr args src pc') ->
-  eval_addressing ge sp addr rs ## args = Some a ->
-  storev chunk m a rs # src = Some m' ->
-  exec_instr_prop c sp pc rs m E0 pc' rs m'.
-Proof.
-  intros; red; intros; CleanupHyps.
-  assert (LL: (List.length (List.map assign args) <= 2)%nat).
-    rewrite list_length_map. 
-    inversion WTI. 
-    eapply length_addr_args. eauto.
-  assert (DISJ: Loc.disjoint (List.map assign args) temporaries).
-    eapply regalloc_disj_temporaries; eauto.
-  assert (SRC: Loc.notin (assign src) temporaries).
-    eapply regalloc_not_temporary; eauto.
-  assert (EADDR:
-      eval_addressing tge sp addr (map ls (map assign args)) = Some a).
-    rewrite <- H0.
-    replace (rs##args) with (map ls (map assign args)).
-    apply eval_addressing_preserved. exact symbols_preserved.
+  (* Istore *)
+  assert (exists a',
+      eval_addressing tge sp addr (map ls (map assign args)) = Some a'
+      /\ Val.lessdef a a').
+    apply eval_addressing_lessdef with (rs##args). 
     eapply agree_eval_regs; eauto.
-  assert (ESRC: ls (assign src) = rs#src).
+    rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  destruct H2 as [a' [EVAL VMD]].
+  assert (ESRC: Val.lessdef rs#src (ls (assign src))).
     eapply agree_eval_reg. eapply agree_reg_list_live. eauto.
-  rewrite <- ESRC in H1.
-  generalize (add_store_correct tge sp chunk addr
-               (List.map assign args) (assign src)
-               pc' ls m m' a LL DISJ SRC EADDR H1).
-  intros [ls' [EX RES]].
-  exists ls'. split. CleanupGoal. exact EX. 
-  rewrite CF in H. 
-  generalize (regalloc_correct_1 f env live _ _ _ _ ASG H).
-  unfold correct_alloc_instr. intro CORR.
-  eapply agree_exten. eauto. 
-  eapply agree_reg_live. eapply agree_reg_list_live. eauto.
-  assumption.
-Qed.  
-
-Lemma transl_Icall_correct:
- forall (c : PTree.t instruction) (sp: val) (pc : positive)
-    (rs : regset) (m : mem) (sig : signature) (ros : reg + ident)
-    (args : list reg) (res : reg) (pc' : RTL.node)
-    (f : RTL.fundef) (vres : val) (m' : mem) (t: trace),
-  c ! pc = Some (Icall sig ros args res pc') ->
-  RTL.find_function ge ros rs = Some f ->
-  RTL.funsig f = sig ->
-  RTL.exec_function ge f (rs##args) m t vres m' ->
-  exec_function_prop f (rs##args) m t vres m' ->
-  exec_instr_prop c sp pc rs m t pc' (rs#res <- vres) m'.
-Proof.
-  intros; red; intros; CleanupHyps.
-  set (los := sum_left_map assign ros).
-  assert (FIND: exists tf,
-            find_function2 tge los ls = Some tf /\
-            transf_fundef f = Some tf).
-    unfold los. destruct ros; simpl; simpl in H0.
-    apply functions_translated. 
-    replace (ls (assign r)) with rs#r. assumption.
-    simpl in AG. symmetry; eapply agree_eval_reg.
-    eapply agree_reg_list_live; eauto.
-    rewrite symbols_preserved. destruct (Genv.find_symbol ge i).
-    apply function_ptr_translated. auto.
-    discriminate.
-  elim FIND; intros tf [AFIND TRF]; clear FIND.
-  assert (ASIG: sig = funsig tf).
-    rewrite (sig_function_translated _ _ TRF). auto.
-  generalize (fun ls => H3 ls tf TRF); intro AEXECF.
-  assert (AVARGS: List.map ls (List.map assign args) = rs##args).
-    eapply agree_eval_regs; eauto.
-  assert (ALARGS: List.length (List.map assign args) = 
-                                   List.length sig.(sig_args)).
-    inversion WTI. rewrite <- H10. 
-    repeat rewrite list_length_map. auto.
-  assert (AACCEPT: locs_acceptable (List.map assign args)).
-    eapply regsalloc_acceptable; eauto.
-  rewrite CF in H. 
-  generalize (regalloc_correct_1 f0 env live _ _ _ _ ASG H).
-  unfold correct_alloc_instr. intros [CORR1 CORR2].
-  assert (ARES: loc_acceptable (assign res)).
-    eapply regalloc_acceptable; eauto.
-  generalize (add_call_correct tge sp tf _ _ _ _ _ _ _ _ _ pc' _
-                AEXECF AFIND ASIG AVARGS ALARGS
-                AACCEPT ARES).
-  intros [ls' [EX [RES OTHER]]].
-  exists ls'.
-  split. rewrite CF. CleanupGoal. exact EX.
-  simpl. eapply agree_call; eauto.
-Qed.
-
-Lemma transl_Ialloc_correct:
-  forall (c : PTree.t instruction) (sp: val) (pc : positive)
-    (rs : Regmap.t val) (m : mem) (pc': RTL.node) (arg res: reg)
-    (sz: int) (m': mem) (b: Values.block),
-  c ! pc = Some (Ialloc arg res pc') ->
-  rs#arg = Vint sz ->
-  Mem.alloc m 0 (Int.signed sz) = (m', b) ->
-  exec_instr_prop c sp pc rs m E0 pc' (rs # res <- (Vptr b Int.zero)) m'.
-Proof.
-  intros; red; intros; CleanupHyps.
-  assert (SZ: ls (assign arg) = Vint sz).
+  assert (exists tm', storev chunk tm a' (ls (assign src)) = Some tm'
+                     /\ Mem.lessdef m' tm').
+    eapply Mem.storev_lessdef; eauto. 
+  destruct H2 as [m1' [STORE MMD']].
+  econstructor; split.
+  eapply exec_Lstore; eauto. TranslInstr.
+  MatchStates. eapply agree_reg_live. eapply agree_reg_list_live. eauto.
+
+  (* Icall *)
+  exploit transl_find_function; eauto.  intros [tf [TFIND TF]].
+  generalize (regalloc_correct_1 f0 env live _ _ _ _ ASG H).
  unfold correct_alloc_instr. intros [CORR1 CORR2].
+  exploit (parmov_spec ls (map assign args) 
+                            (loc_arguments (RTL.funsig f))).
+  apply loc_arguments_norepet.
+  rewrite loc_arguments_length. inv WTI.
+  rewrite <- H7. repeat rewrite list_length_map. auto.
+  intros [PM1 PM2].  
+  econstructor; split. 
+  eapply exec_Lcall; eauto. TranslInstr.
+  rewrite (sig_function_translated _ _ TF). eauto.
+  rewrite (sig_function_translated _ _ TF).
+  econstructor; eauto.
+  econstructor; eauto.
+  intros. eapply agree_succ with (n := pc); eauto.
+  unfold RTL.successors; rewrite H; auto with coqlib.
+  eapply agree_call with (ls := ls); eauto.
+  rewrite Locmap.gss. auto.
+  intros. rewrite Locmap.gso. rewrite H1; auto. apply PM2; auto.
+  eapply arguments_not_preserved; eauto. apply Loc.diff_sym; auto.
+  rewrite (sig_function_translated _ _ TF).
+  change Regset.elt with reg in PM1. 
+  rewrite PM1. eapply agree_eval_regs; eauto. 
+
+  (* Itailcall *)
+  exploit transl_find_function; eauto.  intros [tf [TFIND TF]].
+  exploit (parmov_spec ls (map assign args) 
+                            (loc_arguments (RTL.funsig f))).
+  apply loc_arguments_norepet.
+  rewrite loc_arguments_length. inv WTI.
+  rewrite <- H6. repeat rewrite list_length_map. auto.
+  intros [PM1 PM2].  
+  econstructor; split. 
+  eapply exec_Ltailcall; eauto. TranslInstr.
+  rewrite (sig_function_translated _ _ TF). eauto.
+  rewrite (sig_function_translated _ _ TF).
+  econstructor; eauto.
+  apply match_stackframes_change with (RTL.fn_sig f0); auto.
+  inv WTI. auto.
+  rewrite (sig_function_translated _ _ TF).
+  rewrite return_regs_arguments. 
+  change Regset.elt with reg in PM1. 
+  rewrite PM1. eapply agree_eval_regs; eauto.
+  inv WTI; auto.
+  apply free_lessdef; auto.
+  intros. rewrite return_regs_not_destroyed; auto. 
+
+  (* Ialloc *)
+  assert (Val.lessdef (Vint sz) (ls (assign arg))).
     rewrite <- H0. eapply agree_eval_reg. eauto.
-  generalize (add_alloc_correct tge sp (assign arg) (assign res)
-                                pc' ls m m' sz b SZ H1).
-  intros [ls' [EX [RES OTHER]]].
-  exists ls'. 
-  split. CleanupGoal. exact EX. 
-  rewrite CF in H.
+  inversion H2. subst v. 
+  pose (ls1 := Locmap.set (R loc_alloc_argument) (ls (assign arg)) ls).
+  pose (ls2 := Locmap.set (R loc_alloc_result) (Vptr b Int.zero) ls1).
+  pose (ls3 := Locmap.set (assign res) (ls2 (R loc_alloc_result)) ls2).
+  caseEq (alloc tm 0 (Int.signed sz)). intros tm' b1 ALLOC1.
+  exploit Mem.alloc_lessdef; eauto. intros [EQ MMD1]. subst b1.
+  exists (State ts (transf_fun f live assign) sp pc' ls3 tm'); split.
+  unfold ls3, ls2, ls1. eapply exec_Lalloc; eauto. TranslInstr.
   generalize (regalloc_correct_1 f env live _ _ _ _ ASG H). 
   unfold correct_alloc_instr.  intros [CORR1 CORR2].
-  eapply agree_call with (args := arg :: nil) (ros := inr reg 1%positive) (ls := ls) (ls' := ls'); eauto.
-  intros. apply OTHER. 
-  eapply Loc.in_notin_diff; eauto. 
-  unfold loc_alloc_argument, destroyed_at_call; simpl; tauto.
-  eapply Loc.in_notin_diff; eauto. 
+  MatchStates.
+  eapply agree_call with (args := arg :: nil) (ros := inr reg 1%positive) (ls := ls); eauto.
+  unfold ls3; rewrite Locmap.gss. 
+  unfold ls2; rewrite Locmap.gss. auto.
+  intros. unfold ls3; rewrite Locmap.gso.
+  unfold ls2; rewrite Locmap.gso. 
+  unfold ls1; apply Locmap.gso.
+  apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto. 
   unfold loc_alloc_argument, destroyed_at_call; simpl; tauto.
-  auto.
-Qed.
-
-Lemma transl_Icond_true_correct:
- forall (c : PTree.t instruction) (sp: val) (pc : positive)
-    (rs : Regmap.t val) (m : mem) (cond : condition) (args : list reg)
-    (ifso ifnot : RTL.node),
-  c ! pc = Some (Icond cond args ifso ifnot) ->
-  eval_condition cond rs ## args = Some true ->
-  exec_instr_prop c sp pc rs m E0 ifso rs m.
-Proof.
-  intros; red; intros; CleanupHyps.
-  assert (LL: (List.length (map assign args) <= 3)%nat).
-    rewrite list_length_map. inversion WTI. 
-    eapply length_cond_args. eauto.
-  assert (DISJ: Loc.disjoint (map assign args) temporaries).
-    eapply regalloc_disj_temporaries; eauto.
-  assert (COND: eval_condition cond (map ls (map assign args)) = Some true).
-    replace (map ls (map assign args)) with rs##args. assumption.
-    symmetry. eapply agree_eval_regs; eauto.
-  generalize (add_cond_correct tge sp _ _ _ ifnot _ m _ _
-               LL DISJ COND (refl_equal ifso)).
-  intros [ls' [EX OTHER]].
-  exists ls'. split.
-  CleanupGoal. assumption.
-  eapply agree_exten. eauto. eapply agree_reg_list_live. eauto. 
-  assumption.
-Qed.
-
-Lemma transl_Icond_false_correct:
- forall (c : PTree.t instruction) (sp: val) (pc : positive)
-    (rs : Regmap.t val) (m : mem) (cond : condition) (args : list reg)
-    (ifso ifnot : RTL.node),
-  c ! pc = Some (Icond cond args ifso ifnot) ->
-  eval_condition cond rs ## args = Some false ->
-  exec_instr_prop c sp pc rs m E0 ifnot rs m.
-Proof.
-  intros; red; intros; CleanupHyps.
-  assert (LL: (List.length (map assign args) <= 3)%nat).
-    rewrite list_length_map. inversion WTI. 
-    eapply length_cond_args. eauto.
-  assert (DISJ: Loc.disjoint (map assign args) temporaries).
-    eapply regalloc_disj_temporaries; eauto.
-  assert (COND: eval_condition cond (map ls (map assign args)) = Some false).
-    replace (map ls (map assign args)) with rs##args. assumption.
-    symmetry. eapply agree_eval_regs; eauto.
-  generalize (add_cond_correct tge sp _ _ ifso _ _ m _ _
-               LL DISJ COND (refl_equal ifnot)).
-  intros [ls' [EX OTHER]].
-  exists ls'. split.
-  CleanupGoal. assumption.
-  eapply agree_exten. eauto. eapply agree_reg_list_live. eauto. 
-  assumption.
-Qed.
-
-Lemma transl_refl_correct:
- forall (c : RTL.code) (sp: val) (pc : RTL.node) (rs : regset)
-    (m : mem), exec_instrs_prop c sp pc rs m E0 pc rs m.
-Proof.
-  intros; red; intros. 
-  exists ls. split. apply exec_blocks_refl. assumption.
-Qed.
-
-Lemma transl_one_correct:
- forall (c : RTL.code) (sp: val) (pc : RTL.node) (rs : regset)
-    (m : mem) (t: trace) (pc' : RTL.node) (rs' : regset) (m' : mem),
-  RTL.exec_instr ge c sp pc rs m t pc' rs' m' ->
-  exec_instr_prop c sp pc rs m t pc' rs' m' ->
-  exec_instrs_prop c sp pc rs m t pc' rs' m'.
-Proof.
-  intros; red; intros.
-  generalize (H0 f env live assign ls CF WT ASG AG).
-  intros [ls' [EX AG']].
-  exists ls'. split.
-  exact EX.
-  apply agree_increasing with live!!pc.
-  apply analyze_correct. auto. 
-  rewrite <- CF. eapply exec_instr_present; eauto.
-  rewrite <- CF. auto.
-  eapply RTL.successors_correct.
-  rewrite <- CF. eexact H. exact AG'.
-Qed.
-
-Lemma transl_trans_correct:
- forall (c : RTL.code) (sp: val) (pc1 : RTL.node) (rs1 : regset)
-    (m1 : mem) (t1: trace) (pc2 : RTL.node) (rs2 : regset) (m2 : mem)
-    (t2: trace) (pc3 : RTL.node) (rs3 : regset) (m3 : mem) (t3: trace),
-  RTL.exec_instrs ge c sp pc1 rs1 m1 t1 pc2 rs2 m2 ->
-  exec_instrs_prop c sp pc1 rs1 m1 t1 pc2 rs2 m2 ->
-  RTL.exec_instrs ge c sp pc2 rs2 m2 t2 pc3 rs3 m3 ->
-  exec_instrs_prop c sp pc2 rs2 m2 t2 pc3 rs3 m3 ->
-  t3 = t1 ** t2 ->
-  exec_instrs_prop c sp pc1 rs1 m1 t3 pc3 rs3 m3.
-Proof.
-  intros; red; intros.
-  assert (VALIDPC2: c!pc2 <> None).
-    eapply exec_instrs_present; eauto.
-  generalize (H0 f env live assign ls CF WT ANL ASG AG VALIDPC2).
-  intros [ls1 [EX1 AG1]]. 
-  generalize (H2 f env live assign ls1 CF WT ANL ASG AG1 VALIDPC'). 
-  intros [ls2 [EX2 AG2]].
-  exists ls2. split.
-  eapply exec_blocks_trans. eexact EX1. eexact EX2. auto.
-  exact AG2.
-Qed.
-
-Remark regset_mem_reg_list_dead:
-  forall rl r live,
-  Regset.In r (reg_list_dead rl live) ->
-  ~(In r rl) /\ Regset.In r live.
-Proof.
-  induction rl; simpl; intros.
-  tauto.
-  elim (IHrl r (reg_dead a live) H). intros.
-  assert (a <> r). red; intro; subst r.
-  exploit Regset.remove_1; eauto. 
-  intuition. eapply Regset.remove_3; eauto.
-Qed. 
-
-Lemma transf_entrypoint_correct:
-  forall f env live assign c ls args sp m,
-  wt_function f env ->
-  regalloc f live (live0 f live) env = Some assign ->
-  c!(RTL.fn_nextpc f) = None ->
-  List.map ls (loc_parameters (RTL.fn_sig f)) = args ->
-  (forall ofs ty, ls (S (Local ofs ty)) = Vundef) ->
-  let tc := transf_entrypoint f live assign c in
-  exists ls',
-  exec_blocks tge tc sp (RTL.fn_nextpc f) ls m E0
-                        (Cont (RTL.fn_entrypoint f)) ls' m /\
-  agree assign (transfer f (RTL.fn_entrypoint f) live!!(RTL.fn_entrypoint f))
-        (init_regs args (RTL.fn_params f)) ls'.
-Proof.
-  intros until m.
-  unfold transf_entrypoint. 
-  set (oldentry := RTL.fn_entrypoint f).
-  set (newentry := RTL.fn_nextpc f).
-  set (params := RTL.fn_params f).
-  set (undefs := Regset.elements (reg_list_dead params (transfer f oldentry live!!oldentry))).
-  intros.
-
-  assert (A1: List.length (List.map assign params) =
-              List.length (RTL.fn_sig f).(sig_args)).
-    rewrite <- (wt_params _ _ H).  
-    repeat (rewrite list_length_map). auto.
-  assert (A2: Loc.norepet (List.map assign (RTL.fn_params f))).
-    eapply regalloc_norepet_norepet; eauto.
-    eapply regalloc_correct_2; eauto.
-    eapply wt_norepet; eauto.
-  assert (A3: locs_acceptable (List.map assign (RTL.fn_params f))).
-    eapply regsalloc_acceptable; eauto.
-  assert (A4: Loc.disjoint 
-                (List.map assign (RTL.fn_params f))
-                (List.map assign undefs)).
-    red. intros ap au INAP INAU.
-    generalize (list_in_map_inv _ _ _ INAP).
-    intros [p [AP INP]]. clear INAP; subst ap.
-    generalize (list_in_map_inv _ _ _ INAU).
-    intros [u [AU INU]]. clear INAU; subst au.
-    assert (INU': InA Regset.E.eq u undefs).
-      rewrite InA_alt. exists u; intuition. 
-    generalize (Regset.elements_2 _ _ INU'). intro.
-    generalize (regset_mem_reg_list_dead _ _ _ H4).
-    intros [A B]. 
-    eapply regalloc_noteq_diff; eauto.
-    eapply regalloc_correct_3; eauto.
-    red; intro; subst u. elim (A INP).
-  assert (A5: forall l, In l (List.map assign undefs) -> loc_acceptable l).
-    intros. 
-    generalize (list_in_map_inv _ _ _ H4).
-    intros [r [AR INR]]. clear H4; subst l.
-    eapply regalloc_acceptable; eauto.
-  generalize (add_entry_correct
-    tge sp (RTL.fn_sig f)
-    (List.map assign (RTL.fn_params f))
-    (List.map assign undefs)
-    oldentry ls m A1 A2 A3 A4 A5 H3).
-  intros [ls1 [EX1 [PARAMS1 UNDEFS1]]].
-  exists ls1. 
-  split. eapply exec_blocks_one.
-  rewrite PTree.gss. reflexivity.
-  assumption.
-  change (transfer f oldentry live!!oldentry)
-    with (live0 f live).
-  unfold params; eapply agree_parameters; eauto.
-  change Regset.elt with reg in PARAMS1. 
-  rewrite PARAMS1. assumption.
-  fold oldentry; fold params. intros.
-  apply UNDEFS1. apply in_map. 
-  unfold undefs.
-  change (transfer f oldentry live!!oldentry)
-    with (live0 f live).
-  exploit Regset.elements_1; eauto.
-  rewrite InA_alt. intros [r' [C D]]. hnf in C. subst r'. auto.
-Qed.
-
-Lemma transl_function_correct:
- forall (f : RTL.function) (m m1 : mem) (stk : Values.block)
-    (args : list val) (t: trace) (pc : RTL.node) (rs : regset) (m2 : mem)
-    (or : option reg) (vres : val),
-  alloc m 0 (RTL.fn_stacksize f) = (m1, stk) ->
-  RTL.exec_instrs ge (RTL.fn_code f) (Vptr stk Int.zero)
-    (RTL.fn_entrypoint f) (init_regs args (fn_params f)) m1 t pc rs m2 ->
-  exec_instrs_prop (RTL.fn_code f) (Vptr stk Int.zero)
-    (RTL.fn_entrypoint f) (init_regs args (fn_params f)) m1 t pc rs m2 ->
-  (RTL.fn_code f) ! pc = Some (Ireturn or) ->
-  vres = regmap_optget or Vundef rs ->
-  exec_function_prop (Internal f) args m t vres (free m2 stk).
-Proof.
-  intros; red; intros until tf.
-  unfold transf_fundef, transf_partial_fundef, transf_function.
-  caseEq (type_function f).
-  intros env TRF. 
-  caseEq (analyze f).
-  intros live ANL.
-  change (transfer f (RTL.fn_entrypoint f) live!!(RTL.fn_entrypoint f))
-    with (live0 f live).
-  caseEq (regalloc f live (live0 f live) env).
-  intros alloc ASG.
-  set (tc1 := PTree.map (transf_instr f live alloc) (RTL.fn_code f)).
-  set (tc2 := transf_entrypoint f live alloc tc1).
-  intro EQ; injection EQ; intro TF; clear EQ. intro VARGS. 
-  generalize (type_function_correct _ _ TRF); intro WTF.
-  assert (NEWINSTR: tc1!(RTL.fn_nextpc f) = None).
-    unfold tc1; rewrite PTree.gmap. unfold option_map.
-    elim (RTL.fn_code_wf f (fn_nextpc f)); intro.
-    elim (Plt_ne _ _ H4). auto.
-    rewrite H4. auto.
-  pose (ls1 := call_regs ls).
-  assert (VARGS1: List.map ls1 (loc_parameters (RTL.fn_sig f)) = args).
-    replace (RTL.fn_sig f) with (funsig tf).
-    rewrite <- VARGS. unfold loc_parameters.
-    rewrite list_map_compose. apply list_map_exten.
-    intros. symmetry. unfold ls1. eapply call_regs_param_of_arg; eauto.
-    rewrite <- TF; reflexivity.
-  assert (VUNDEFS: forall (ofs : Z) (ty : typ), ls1 (S (Local ofs ty)) = Vundef).
-    intros. reflexivity.    
-  generalize (transf_entrypoint_correct f env live alloc
-                tc1 ls1 args (Vptr stk Int.zero) m1
-                WTF ASG NEWINSTR VARGS1 VUNDEFS).
-  fold tc2. intros [ls2 [EX2 AGREE2]].
-  assert (VALIDPC: f.(RTL.fn_code)!pc <> None). congruence.
-  generalize (H1 f env live alloc ls2
-               (refl_equal _) WTF ANL ASG AGREE2 VALIDPC).
-  fold tc1. intros [ls3 [EX3 AGREE3]].
-  generalize (add_return_correct tge (Vptr stk Int.zero) (RTL.fn_sig f) 
-                            (option_map alloc or) ls3 m2).
-  intros [ls4 [EX4 RES4]].
-  exists ls4. 
-  (* Execution *)
-  split. rewrite <- TF; apply exec_funct_internal with m1; simpl.
-  assumption.
-  fold ls1. 
-  eapply exec_blocks_trans. eexact EX2. 
-  apply exec_blocks_extends with tc1.
-  intro p. unfold tc2. unfold transf_entrypoint.
-  case (peq p (fn_nextpc f)); intro.
-  subst p. right. unfold tc1; rewrite PTree.gmap. 
-  elim (RTL.fn_code_wf f (fn_nextpc f)); intro.
-  elim (Plt_ne _ _ H4); auto. rewrite H4; reflexivity.
-  left; apply PTree.gso; auto.
-  eapply exec_blocks_trans. eexact EX3.
-  eapply exec_blocks_one. 
-  unfold tc1. rewrite PTree.gmap. rewrite H2. simpl. reflexivity.
-  eexact EX4. reflexivity. traceEq.
-  destruct or.
-  simpl in RES4. simpl in H3.
-  rewrite H3. rewrite <- TF; simpl. rewrite RES4.
-  eapply agree_eval_reg; eauto.
-  unfold transfer in AGREE3; rewrite H2 in AGREE3. 
-  unfold reg_option_live in AGREE3. eexact AGREE3.
-  simpl in RES4. simpl in H3.
-  rewrite <- TF; simpl. congruence.
-  intros; discriminate.
-  intros; discriminate.
-  intros; discriminate.
-Qed.
+  apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto. 
+  unfold loc_alloc_result, destroyed_at_call; simpl; tauto.
+  apply Loc.diff_sym; auto.
 
-Lemma transl_external_function_correct:
-  forall (ef : external_function) (args : list val) (m : mem)
-         (t: trace) (res: val),
-  event_match ef args t res ->
-  exec_function_prop (External ef) args m t res m.
-Proof.
-  intros; red; intros.
-  simpl in H0. 
-  simplify_eq H0; intro.
-  exists (Locmap.set (R (loc_result (funsig tf))) res ls); split.
-  subst tf. eapply exec_funct_external; eauto. 
-  apply Locmap.gss.
+  (* Icond, true *)
+  assert (COND: eval_condition cond (map ls (map assign args)) tm = Some true).
+    eapply eval_condition_lessdef; eauto. 
+    eapply agree_eval_regs; eauto.
+  econstructor; split.
+  eapply exec_Lcond_true; eauto. TranslInstr.
+  MatchStates. eapply agree_reg_list_live. eauto.
+  (* Icond, false *)
+  assert (COND: eval_condition cond (map ls (map assign args)) tm = Some false).
+    eapply eval_condition_lessdef; eauto. 
+    eapply agree_eval_regs; eauto.
+  econstructor; split.
+  eapply exec_Lcond_false; eauto. TranslInstr.
+  MatchStates. eapply agree_reg_list_live. eauto.
+
+  (* Ireturn *)
+  econstructor; split.
+  eapply exec_Lreturn; eauto. TranslInstr; eauto.
+  econstructor; eauto.
+  rewrite return_regs_result.  
+  inv WTI. destruct or; simpl in *. 
+  rewrite Locmap.gss. eapply agree_eval_reg; eauto.
+  constructor. 
+  apply free_lessdef; auto.
+  intros. apply return_regs_not_destroyed; auto.
+
+  (* internal function *)
+  generalize H6. simpl.  unfold transf_function.
+  caseEq (type_function f); simpl; try congruence. intros env TYP.
+  assert (WTF: wt_function f env). apply type_function_correct; auto.
+  caseEq (analyze f); simpl; try congruence. intros live ANL.
+  caseEq (regalloc f live (live0 f live) env); simpl; try congruence.
+  intros alloc ALLOC EQ. inv EQ. simpl in *.
+  caseEq (Mem.alloc tm 0 (RTL.fn_stacksize f)). intros tm' stk' MEMALLOC.
+  exploit alloc_lessdef; eauto. intros [EQ LDM]. subst stk'.
+  econstructor; split.
+  eapply exec_function_internal; simpl; eauto.
+  simpl. econstructor; eauto.
+  apply agree_init_regs. intros; eapply regalloc_correct_3; eauto.
+  inv WTF.
+  exploit (parmov_spec (call_regs ls) 
+                       (loc_parameters (RTL.fn_sig f))
+                       (map alloc (RTL.fn_params f))).
+  eapply regalloc_norepet_norepet; eauto.
+  eapply regalloc_correct_2; eauto.
+  rewrite loc_parameters_length. symmetry. 
+  transitivity (length (map env (RTL.fn_params f))).
+  repeat rewrite list_length_map. auto.
+  rewrite wt_params; auto.
+  intros [PM1 PM2].
+  change Regset.elt with reg in PM1. rewrite PM1.
+  replace (map (call_regs ls) (loc_parameters (RTL.fn_sig f)))
+     with (map ls (loc_arguments (RTL.fn_sig f))).
+  auto.
+  symmetry. unfold loc_parameters. rewrite list_map_compose.
+  apply list_map_exten. intros. symmetry. eapply call_regs_param_of_arg; eauto.
+
+  (* external function *)
+  injection H6; intro EQ; inv EQ.
+  exploit event_match_lessdef; eauto. intros [tres [A B]].
+  econstructor; split.
+  eapply exec_function_external; eauto.
+  eapply match_states_return; eauto.
+  rewrite Locmap.gss. auto.
+  intros. rewrite <- H10; auto. apply Locmap.gso.
+  apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto.
+  apply loc_result_caller_save. 
+
+  (* return *)
+  inv H3. 
+  econstructor; split.
+  eapply exec_return; eauto.
+  econstructor; eauto.
 Qed.
 
-(** The correctness of the code transformation is obtained by
-  structural induction (and case analysis on the last rule used)
-  on the RTL evaluation derivation.
-  This is a 3-way mutual induction, using [exec_instr_prop],
-  [exec_instrs_prop] and [exec_function_prop] as the induction
-  hypotheses, and the lemmas above as cases for the induction. *)
-
-Theorem transl_function_correctness:
-  forall f args m t res m',
-  RTL.exec_function ge f args m t res m' ->
-  exec_function_prop f args m t res m'.
-Proof
-  (exec_function_ind_3 ge 
-          exec_instr_prop 
-          exec_instrs_prop
-          exec_function_prop
-         
-          transl_Inop_correct
-          transl_Iop_correct
-          transl_Iload_correct
-          transl_Istore_correct
-          transl_Icall_correct
-          transl_Ialloc_correct
-          transl_Icond_true_correct
-          transl_Icond_false_correct
-
-          transl_refl_correct
-          transl_one_correct
-          transl_trans_correct
-
-          transl_function_correct
-          transl_external_function_correct).
-
 (** The semantic equivalence between the original and transformed programs
   follows easily. *)
 
-Theorem transl_program_correct:
-  forall (t: trace) (r: val),
-  RTL.exec_program prog t r -> LTL.exec_program tprog t r.
+Lemma transf_initial_states:
+  forall st1, RTL.initial_state prog st1 ->
+  exists st2, LTL.initial_state tprog st2 /\ match_states st1 st2.
 Proof.
-  intros t r [b [f [m [FIND1 [FIND2 [SIG EXEC]]]]]].
-  generalize (function_ptr_translated _ _ FIND2).
-  intros [tf [TFIND TRF]].
+  intros. inversion H.
+  exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
   assert (SIG2: funsig tf = mksignature nil (Some Tint)).
-    rewrite <- SIG. apply sig_function_translated; auto.
-  assert (VPARAMS: map (Locmap.init Vundef) (loc_arguments (funsig tf)) = nil).
-    rewrite SIG2. reflexivity.
-  generalize (transl_function_correctness _ _ _ _ _ _ EXEC
-                (Locmap.init Vundef) tf TRF VPARAMS).
-  intros [ls' [TEXEC RES]].
-  red. exists b; exists tf; exists ls'; exists m.
-  split. rewrite symbols_preserved. 
-  rewrite (transform_partial_program_main _ _ TRANSF).
-  assumption. 
-  split. assumption.
-  split. assumption.
-  split. replace (Genv.init_mem tprog) with (Genv.init_mem prog).
-  assumption. symmetry. 
-  exact (Genv.init_mem_transf_partial _ _ TRANSF).
-  assumption.
+    rewrite <- H2. apply sig_function_translated; auto.
+  assert (VPARAMS: Val.lessdef_list nil (map (Locmap.init Vundef) (loc_arguments (funsig tf)))).
+    rewrite SIG2. simpl. constructor.
+  assert (GENV: (Genv.init_mem tprog) = (Genv.init_mem prog)).
+    exact (Genv.init_mem_transf_partial _ _ TRANSF).
+  assert (MMD: Mem.lessdef (Genv.init_mem prog) (Genv.init_mem tprog)).
+    rewrite GENV. apply Mem.lessdef_refl.
+  exists (LTL.Callstate nil tf (Locmap.init Vundef) (Genv.init_mem tprog)); split.
+  econstructor; eauto.
+  rewrite symbols_preserved. 
+  rewrite (transform_partial_program_main _ _ TRANSF).  auto.
+  constructor; auto. rewrite H2; constructor. 
+Qed.
+
+Lemma transf_final_states:
+  forall st1 st2 r, 
+  match_states st1 st2 -> RTL.final_state st1 r -> LTL.final_state st2 r.
+Proof.
+  intros. inv H0. inv H. inv H3. econstructor.
+  inv H4. auto. 
+Qed.
+
+Theorem transf_program_correct:
+  forall (beh: program_behavior),
+  RTL.exec_program prog beh -> LTL.exec_program tprog beh.
+Proof.
+  unfold RTL.exec_program, LTL.exec_program; intros.
+  eapply simulation_step_preservation; eauto.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  exact transl_step_correct. 
 Qed.
 
 End PRESERVATION.