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, 408 insertions, 457 deletions

diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 5937fc3..c729908 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -8,10 +8,12 @@ Require Import Values.
 Require Import Mem.
 Require Import Events.
 Require Import Globalenvs.
+Require Import Smallstep.
 Require Import Op.
 Require Import Locations.
 Require Import LTL.
-Require Import Linear.
+Require Import LTLtyping.
+Require Import LTLin.
 Require Import Linearize.
 Require Import Lattice.
 
@@ -46,6 +48,18 @@ Proof.
   destruct f; reflexivity.
 Qed.
 
+Lemma find_function_translated:
+  forall ros ls f,
+  LTL.find_function ge ros ls = Some f ->
+  find_function tge ros ls = Some (transf_fundef f).
+Proof.
+  intros until f. destruct ros; simpl.
+  intro. apply functions_translated; auto.
+  rewrite symbols_preserved. destruct (Genv.find_symbol ge i).
+  apply function_ptr_translated; auto.
+  congruence.
+Qed.
+
 (** * Correctness of reachability analysis *)
 
 (** The entry point of the function is reachable. *)
@@ -62,11 +76,10 @@ Proof.
   intros. apply PMap.gi.
 Qed.
 
-(** The successors of a reachable basic block are reachable. *)
+(** The successors of a reachable instruction are reachable. *)
 
 Lemma reachable_successors:
   forall f pc pc',
-  f.(LTL.fn_code)!pc <> None ->
   In pc' (successors f pc) ->
   (reachable f)!!pc = true ->
   (reachable f)!!pc' = true.
@@ -74,51 +87,19 @@ Proof.
   intro f. unfold reachable.
   caseEq (reachable_aux f).
   unfold reachable_aux. intro reach; intros.
+  elim (LTL.fn_code_wf f pc); intro.
   assert (LBoolean.ge reach!!pc' reach!!pc).
   change (reach!!pc) with ((fun pc r => r) pc (reach!!pc)).
-  eapply DS.fixpoint_solution. eexact H.
-  elim (fn_code_wf f pc); intro. auto. contradiction.
-  auto. 
+  eapply DS.fixpoint_solution. eexact H. auto. auto.
   elim H3; intro. congruence. auto.
+  unfold successors in H0. rewrite H2 in H0. contradiction.
   intros. apply PMap.gi.
 Qed.
 
-(* If we have a valid LTL transition from [pc] to [pc'], and
-  [pc] is reachable, then [pc'] is reachable. *)
-
-Lemma reachable_correct_1:
-  forall f sp pc rs m t pc' rs' m' b,
-  f.(LTL.fn_code)!pc = Some b ->
-  exec_block ge sp b rs m t (Cont pc') rs' m' ->
-  (reachable f)!!pc = true ->
-  (reachable f)!!pc' = true.
-Proof.
-  intros. apply reachable_successors with pc; auto.
-  congruence.
-  eapply successors_correct; eauto.
-Qed.
-
-Lemma reachable_correct_2:
-  forall c sp pc rs m t out rs' m',
-  exec_blocks ge c sp pc rs m t out rs' m' ->  
-  forall f pc',
-  c = f.(LTL.fn_code) ->
-  out = Cont pc' ->
-  (reachable f)!!pc = true ->
-  (reachable f)!!pc' = true.
-Proof.
-  induction 1; intros.
-  congruence.
-  eapply reachable_correct_1. rewrite <- H1; eauto. 
-  subst out; eauto. auto.
-  auto.
-Qed.
-
 (** * Properties of node enumeration *)
 
 (** An enumeration of CFG nodes is correct if the following conditions hold:
 - All nodes for reachable basic blocks must be in the list.
-- The function entry point is the first element in the list.
 - The list is without repetition (so that no code duplication occurs).
 
 We prove that our [enumerate] function satisfies all three. *)
@@ -131,10 +112,10 @@ Lemma enumerate_complete:
 Proof.
   intros. 
   assert (forall p, 
-    Plt p (Psucc f.(fn_entrypoint)) ->
+    Plt p f.(fn_nextpc) ->
     (reachable f)!!p = true ->
     In p (enumerate f)).
-  unfold enumerate. pattern (Psucc (fn_entrypoint f)).
+  unfold enumerate. pattern (fn_nextpc f).
   apply positive_Peano_ind. 
   intros. compute in H1. destruct p; discriminate. 
   intros. rewrite positive_rec_succ. elim (Plt_succ_inv _ _ H2); intro.
@@ -143,27 +124,15 @@ Proof.
   elim (LTL.fn_code_wf f pc); intro. auto. congruence.
 Qed. 
 
-Lemma enumerate_head:
-  forall f, exists l, enumerate f = f.(LTL.fn_entrypoint) :: l.
-Proof.
-  intro. unfold enumerate. rewrite positive_rec_succ. 
-  rewrite reachable_entrypoint.
-  exists (positive_rec (list node) nil
-    (fun (pc : positive) (nodes : list node) =>
-      if (reachable f) !! pc then pc :: nodes else nodes) 
-    (fn_entrypoint f) ).
-  auto.
-Qed.
-
 Lemma enumerate_norepet:
   forall f, list_norepet (enumerate f).
 Proof.
   intro. 
-  unfold enumerate. pattern (Psucc (fn_entrypoint f)).
+  unfold enumerate. pattern (fn_nextpc f).
   apply positive_Peano_ind.  
   rewrite positive_rec_base. constructor.
   intros. rewrite positive_rec_succ.
-  case (reachable f)!!x. auto.
+  case (reachable f)!!x.
   constructor. 
   assert (forall y,
     In y (positive_rec
@@ -183,9 +152,9 @@ Proof.
   auto.
 Qed.
 
-(** * Correctness of the cleanup pass *)
+(** * Properties related to labels *)
 
-(** If labels are globally unique and the Linear code [c] contains
+(** If labels are globally unique and the LTLin code [c] contains
   a subsequence [Llabel lbl :: c1], [find_label lbl c] returns [c1].
 *)
 
@@ -196,27 +165,6 @@ Fixpoint unique_labels (c: code) : Prop :=
   | i :: c => unique_labels c
   end.
 
-Inductive is_tail: code -> code -> Prop :=
-  | is_tail_refl:
-      forall c, is_tail c c
-  | is_tail_cons:
-      forall i c1 c2, is_tail c1 c2 -> is_tail c1 (i :: c2).
-
-Lemma is_tail_in:
-  forall i c1 c2, is_tail (i :: c1) c2 -> In i c2.
-Proof.
-  induction c2; simpl; intros.
-  inversion H.
-  inversion H. tauto. right; auto.
-Qed.
-
-Lemma is_tail_cons_left:
-  forall i c1 c2, is_tail (i :: c1) c2 -> is_tail c1 c2.
-Proof.
-  induction c2; intros; inversion H.
-  constructor. constructor. constructor. auto. 
-Qed.
-
 Lemma find_label_unique:
   forall lbl c1 c2 c3,
   is_tail (Llabel lbl :: c1) c2 ->
@@ -237,163 +185,51 @@ Qed.
 (** Correctness of the [starts_with] test. *)
 
 Lemma starts_with_correct:
-  forall lbl c1 c2 c3 f sp ls m,
+  forall lbl c1 c2 c3 s f sp ls m,
   is_tail c1 c2 ->
   unique_labels c2 ->
   starts_with lbl c1 = true ->
   find_label lbl c2 = Some c3 ->
-  exec_instrs tge f sp (cleanup_code c1) ls m 
-                    E0 (cleanup_code c3) ls m.
+  plus step tge (State s f sp c1 ls m)
+             E0 (State s f sp c3 ls m).
 Proof.
   induction c1.
   simpl; intros; discriminate.
   simpl starts_with. destruct a; try (intros; discriminate).
-  intros. apply exec_trans with E0 (cleanup_code c1) ls m E0.
-  simpl. 
-  constructor. constructor. 
+  intros. 
+  apply plus_left with E0 (State s f sp c1 ls m) E0.
+  simpl. constructor. 
   destruct (peq lbl l).
   subst l. replace c3 with c1. constructor.
   apply find_label_unique with lbl c2; auto.
+  apply plus_star. 
   apply IHc1 with c2; auto. eapply is_tail_cons_left; eauto.
   traceEq.
 Qed.
 
-(** Code cleanup preserves the labeling of the code. *)
-
-Lemma find_label_cleanup_code:
-  forall lbl c c',
-  find_label lbl c = Some c' ->
-  find_label lbl (cleanup_code c) = Some (cleanup_code c').
-Proof.
-  induction c.  
-  simpl. intros; discriminate.
-  generalize (is_label_correct lbl a). 
-  simpl find_label. case (is_label lbl a); intro.
-  subst a. intros. injection H; intros. subst c'. 
-  simpl. rewrite peq_true. auto.
-  intros. destruct a; auto. 
-  simpl. rewrite peq_false. auto.
-  congruence. 
-  case (starts_with l c). auto. simpl. auto.
-Qed.
-
-(** One transition in the original Linear code corresponds to zero
-  or one transitions in the cleaned-up code. *)
-
-Lemma cleanup_code_correct_1:
-  forall f sp c1 ls1 m1 t c2 ls2 m2,
-  exec_instr tge f sp c1 ls1 m1 t c2 ls2 m2 ->
-  is_tail c1 f.(fn_code) ->
-  unique_labels f.(fn_code) ->
-  exec_instrs tge (cleanup_function f) sp 
-                       (cleanup_code c1) ls1 m1
-                     t (cleanup_code c2) ls2 m2.
-Proof.
-  induction 1; simpl; intros;
-  try (apply exec_one; econstructor; eauto; fail).
-  (* goto *)
-  caseEq (starts_with lbl b); intro SW.
-  eapply starts_with_correct; eauto.
-  eapply is_tail_cons_left; eauto.
-  constructor. constructor. 
-  unfold cleanup_function; simpl. 
-  apply find_label_cleanup_code. auto.
-  (* cond, taken *)
-  constructor. apply exec_Lcond_true. auto.
-  unfold cleanup_function; simpl. 
-  apply find_label_cleanup_code. auto.
-  (* cond, not taken *)
-  constructor. apply exec_Lcond_false. auto.
-Qed. 
-
-Lemma is_tail_find_label:
-  forall lbl c2 c1,
-  find_label lbl c1 = Some c2 -> is_tail c2 c1.
-Proof.
-  induction c1; simpl.
-  intros; discriminate.
-  case (is_label lbl a). intro. injection H; intro. subst c2.
-  constructor. constructor.
-  intro. constructor. auto. 
-Qed.
-
-Lemma is_tail_exec_instr:
-  forall f sp c1 ls1 m1 t c2 ls2 m2,
-  exec_instr tge f sp c1 ls1 m1 t c2 ls2 m2 ->
-  is_tail c1 f.(fn_code) -> is_tail c2 f.(fn_code).
-Proof.
-  induction 1; intros;
-  try (eapply is_tail_cons_left; eauto; fail).
-  eapply is_tail_find_label; eauto.
-  eapply is_tail_find_label; eauto.
-Qed.
-
-Lemma is_tail_exec_instrs:
-  forall f sp c1 ls1 m1 t c2 ls2 m2,
-  exec_instrs tge f sp c1 ls1 m1 t c2 ls2 m2 ->
-  is_tail c1 f.(fn_code) -> is_tail c2 f.(fn_code).
-Proof.
-  induction 1; intros.
-  auto.
-  eapply is_tail_exec_instr; eauto.
-  auto.
-Qed.
-
-(** Zero, one or several transitions in the original Linear code correspond
-  to zero, one or several transitions in the cleaned-up code. *)
-
-Lemma cleanup_code_correct_2:
-  forall f sp c1 ls1 m1 t c2 ls2 m2,
-  exec_instrs tge f sp c1 ls1 m1 t c2 ls2 m2 ->
-  is_tail c1 f.(fn_code) ->
-  unique_labels f.(fn_code) ->
-  exec_instrs tge (cleanup_function f) sp 
-                       (cleanup_code c1) ls1 m1
-                     t (cleanup_code c2) ls2 m2.
-Proof.
-  induction 1; simpl; intros.
-  apply exec_refl.
-  eapply cleanup_code_correct_1; eauto.
-  apply exec_trans with t1 (cleanup_code b2) rs2 m2 t2.
-  auto. 
-  apply IHexec_instrs2; auto.
-  eapply is_tail_exec_instrs; eauto.
-  auto.
-Qed.
+(** Connection between [find_label] and linearization. *)
 
-Lemma cleanup_function_correct:
-  forall f ls1 m1 t ls2 m2,
-  exec_function tge (Internal f) ls1 m1 t ls2 m2 ->
-  unique_labels f.(fn_code) ->
-  exec_function tge (Internal (cleanup_function f)) ls1 m1 t ls2 m2. 
+Lemma find_label_add_branch:
+  forall lbl k s,
+  find_label lbl (add_branch s k) = find_label lbl k.
 Proof.
-  intros. inversion H; subst.
-  generalize (cleanup_code_correct_2 _ _ _ _ _ _ _ _ _ H3 (is_tail_refl _) H0).
-  simpl. intro.
-  econstructor; eauto.
+  intros. unfold add_branch. destruct (starts_with s k); auto.
 Qed.
 
-(** * Properties of linearized code *)
-
-(** We now state useful properties of the Linear code generated by
-  the naive LTL-to-Linear translation. *)
-
-(** Connection between [find_label] and linearization. *)
-
-Lemma find_label_lin_block:
+Lemma find_label_lin_instr:
   forall lbl k b,
-  find_label lbl (linearize_block b k) = find_label lbl k.
+  find_label lbl (linearize_instr b k) = find_label lbl k.
 Proof.
+  intros lbl k. generalize (find_label_add_branch lbl k); intro.
   induction b; simpl; auto.
-  case (starts_with n k); reflexivity.
+  case (starts_with n k); simpl; auto.
 Qed.
 
 Lemma find_label_lin_rec:
   forall f enum pc b,
   In pc enum ->
   f.(LTL.fn_code)!pc = Some b ->
-  exists k,
-  find_label pc (linearize_body f enum) = Some (linearize_block b k).
+  exists k, find_label pc (linearize_body f enum) = Some (linearize_instr b k).
 Proof.
   induction enum; intros.
   elim H.
@@ -403,7 +239,7 @@ Proof.
   assert (In pc enum). simpl in H. tauto.
   elim (IHenum pc b H1 H0). intros k FIND.
   exists k. simpl. destruct (LTL.fn_code f)!a. 
-  simpl. rewrite peq_false. rewrite find_label_lin_block. auto. auto.
+  simpl. rewrite peq_false. rewrite find_label_lin_instr. auto. auto.
   auto.
 Qed.
 
@@ -412,20 +248,56 @@ Lemma find_label_lin:
   f.(LTL.fn_code)!pc = Some b ->
   (reachable f)!!pc = true ->
   exists k,
-  find_label pc (fn_code (linearize_function f)) = Some (linearize_block b k).
+  find_label pc (fn_code (transf_function f)) = Some (linearize_instr b k).
 Proof.
-  intros. unfold linearize_function; simpl. apply find_label_lin_rec.
+  intros. unfold transf_function; simpl.
+  rewrite find_label_add_branch. apply find_label_lin_rec.
   eapply enumerate_complete; eauto. auto.
 Qed.
 
+Lemma find_label_lin_inv:
+  forall f pc b k ,
+  f.(LTL.fn_code)!pc = Some b ->
+  (reachable f)!!pc = true ->
+  find_label pc (fn_code (transf_function f)) = Some k ->
+  exists k', k = linearize_instr b k'.
+Proof.
+  intros. exploit find_label_lin; eauto. intros [k' FIND].
+  exists k'. congruence.
+Qed.
+
+Lemma find_label_lin_succ:
+  forall f s,
+  valid_successor f s ->
+  (reachable f)!!s = true ->
+  exists k,
+  find_label s (fn_code (transf_function f)) = Some k.
+Proof.
+  intros. destruct H as [i AT]. 
+  exploit find_label_lin; eauto. intros [k FIND].
+  exists (linearize_instr i k); auto.
+Qed.
+
 (** Unique label property for linearized code. *)
 
-Lemma label_in_lin_block:
+Lemma label_in_add_branch:
+  forall lbl s k,
+  In (Llabel lbl) (add_branch s k) -> In (Llabel lbl) k.
+Proof.
+  intros until k; unfold add_branch.
+  destruct (starts_with s k); simpl; intuition congruence.
+Qed.
+
+Lemma label_in_lin_instr:
   forall lbl k b,
-  In (Llabel lbl) (linearize_block b k) -> In (Llabel lbl) k.
+  In (Llabel lbl) (linearize_instr b k) -> In (Llabel lbl) k.
 Proof.
-  induction b; simpl; try (intuition congruence).
-  case (starts_with n k); simpl; intuition congruence.
+  induction b; simpl; intros;
+  try (apply label_in_add_branch with n; intuition congruence);
+  try (intuition congruence).
+  destruct (starts_with n k); simpl in H.
+  apply label_in_add_branch with n; intuition congruence.
+  apply label_in_add_branch with n0; intuition congruence.
 Qed.
 
 Lemma label_in_lin_rec:
@@ -436,16 +308,24 @@ Proof.
   simpl; auto.
   simpl. destruct (LTL.fn_code f)!a. 
   simpl. intros [A|B]. left; congruence. 
-  right. apply IHenum. eapply label_in_lin_block; eauto.
+  right. apply IHenum. eapply label_in_lin_instr; eauto.
   intro; right; auto.
 Qed.
 
-Lemma unique_labels_lin_block:
+Lemma unique_labels_add_branch:
+  forall lbl k,
+  unique_labels k -> unique_labels (add_branch lbl k).
+Proof.
+  intros; unfold add_branch. 
+  destruct (starts_with lbl k); simpl; intuition.
+Qed.
+
+Lemma unique_labels_lin_instr:
   forall k b,
-  unique_labels k -> unique_labels (linearize_block b k).
+  unique_labels k -> unique_labels (linearize_instr b k).
 Proof.
-  induction b; simpl; auto.
-  case (starts_with n k); simpl; auto.
+  induction b; intro; simpl; auto; try (apply unique_labels_add_branch; auto).
+  case (starts_with n k); simpl; apply unique_labels_add_branch; auto.
 Qed.
 
 Lemma unique_labels_lin_rec:
@@ -458,268 +338,339 @@ Proof.
   intro. simpl. destruct (LTL.fn_code f)!a. 
   simpl. split. red. intro. inversion H. elim H3.
   apply label_in_lin_rec with f. 
-  apply label_in_lin_block with b. auto.
-  apply unique_labels_lin_block. apply IHenum. inversion H; auto.
+  apply label_in_lin_instr with i. auto.
+  apply unique_labels_lin_instr. apply IHenum. inversion H; auto.
   apply IHenum. inversion H; auto.
 Qed.
 
-Lemma unique_labels_lin_function:
+Lemma unique_labels_transf_function:
   forall f,
-  unique_labels (fn_code (linearize_function f)).
+  unique_labels (fn_code (transf_function f)).
 Proof.
-  intros. unfold linearize_function; simpl.
+  intros. unfold transf_function; simpl.
+  apply unique_labels_add_branch. 
   apply unique_labels_lin_rec. apply enumerate_norepet. 
 Qed.
 
-(** * Correctness of linearization *)
+(** Correctness of [add_branch]. *)
+
+Lemma is_tail_find_label:
+  forall lbl c2 c1,
+  find_label lbl c1 = Some c2 -> is_tail c2 c1.
+Proof.
+  induction c1; simpl.
+  intros; discriminate.
+  case (is_label lbl a). intro. injection H; intro. subst c2.
+  constructor. constructor.
+  intro. constructor. auto. 
+Qed.
 
-(** The outcome of an LTL [exec_block] or [exec_blocks] execution
-  is valid if it corresponds to a reachable, existing basic block.
-  All outcomes occurring in an LTL program execution are actually
-  valid, but we will prove that along with the main simulation proof. *)
+Lemma is_tail_add_branch:
+  forall lbl c1 c2, is_tail (add_branch lbl c1) c2 -> is_tail c1 c2.
+Proof.
+  intros until c2. unfold add_branch. destruct (starts_with lbl c1).
+  auto. eauto with coqlib.
+Qed.
 
-Definition valid_outcome (f: LTL.function) (out: outcome) :=
-  match out with
-  | Cont s =>
-      (reachable f)!!s = true /\ exists b, f.(LTL.fn_code)!s = Some b
-  | Return => True
-  end.
+Lemma add_branch_correct:
+  forall lbl c k s f sp ls m,
+  is_tail k (transf_function f).(fn_code) ->
+  find_label lbl (transf_function f).(fn_code) = Some c ->
+  plus step tge (State s (transf_function f) sp (add_branch lbl k) ls m)
+             E0 (State s (transf_function f) sp c ls m).
+Proof.
+  intros. unfold add_branch.
+  caseEq (starts_with lbl k); intro SW.
+  eapply starts_with_correct; eauto.
+  apply unique_labels_transf_function.
+  apply plus_one. apply exec_Lgoto. auto.
+Qed.
 
-(** Auxiliary lemma used to establish the [valid_outcome] property. *)
+(** * Correctness of linearization *)
 
-Lemma exec_blocks_valid_outcome:
-  forall c sp pc ls1 m1 t out ls2 m2,
-  exec_blocks ge c sp pc ls1 m1 t out ls2 m2 ->
-  forall f,
-  c = f.(LTL.fn_code) ->
-  (reachable f)!!pc = true ->
-  valid_outcome f out ->
-  valid_outcome f (Cont pc).
+(** The proof of semantic preservation is a simulation argument
+  based on diagrams of the following form:
+<<
+           st1 --------------- st2
+            |                   |
+           t|                  +|t
+            |                   |
+            v                   v
+           st1'--------------- st2'
+>>
+  The invariant (horizontal lines above) is the [match_states]
+  predicate defined below.  It captures the fact that the flow
+  of data is the same in the source and linearized codes.
+  Moreover, whenever the source state is at node [pc] in its
+  control-flow graph, the transformed state is at a code
+  sequence [c] that starts with the label [pc]. *)
+
+Inductive match_stackframes: LTL.stackframe -> LTLin.stackframe -> Prop :=
+  | match_stackframe_intro:
+      forall res f sp pc ls c,
+      (reachable f)!!pc = true ->
+      valid_successor f pc ->
+      is_tail c (fn_code (transf_function f)) ->
+      wt_function f ->
+      match_stackframes
+        (LTL.Stackframe res f sp ls pc)
+        (LTLin.Stackframe res (transf_function f) sp ls (add_branch pc c)).
+
+Inductive match_states: LTL.state -> LTLin.state -> Prop :=
+  | match_states_intro:
+      forall s f sp pc ls m ts c
+        (STACKS: list_forall2 match_stackframes s ts)
+        (REACH: (reachable f)!!pc = true)
+        (AT: find_label pc (fn_code (transf_function f)) = Some c)
+        (WTF: wt_function f),
+      match_states (LTL.State s f sp pc ls m)
+                   (LTLin.State ts (transf_function f) sp c ls m)
+  | match_states_call:
+      forall s f ls m ts,
+      list_forall2 match_stackframes s ts ->
+      wt_fundef f ->
+      match_states (LTL.Callstate s f ls m)
+                   (LTLin.Callstate ts (transf_fundef f) ls m)
+  | match_states_return:
+      forall s sig ls m ts,
+      list_forall2 match_stackframes s ts ->
+      match_states (LTL.Returnstate s sig ls m)
+                   (LTLin.Returnstate ts sig ls m).
+
+Remark parent_locset_match:
+  forall s ts,
+  list_forall2 match_stackframes s ts ->
+  parent_locset ts = LTL.parent_locset s.
 Proof.
-  induction 1.
-  auto.
-  intros. simpl. split. auto. exists b. congruence. 
-  intros. apply IHexec_blocks1. auto. auto.
-  apply IHexec_blocks2. auto. 
-  eapply reachable_correct_2. eexact H. auto. auto. auto.
-  auto.
+  induction 1; simpl; auto. inv H; auto. 
 Qed.
 
-(** Correspondence between an LTL outcome and a fragment of generated
-  Linear code. *)
-
-Inductive cont_for_outcome: LTL.function -> outcome -> code -> Prop :=
-  | co_return:
-      forall f k,
-      cont_for_outcome f Return (Lreturn :: k)
-  | co_goto:
-      forall f s k,
-      find_label s (linearize_function f).(fn_code) = Some k ->
-      cont_for_outcome f (Cont s) k.
-
-(** The simulation properties used in the inductive proof.
-  They are parameterized by an LTL execution, and state
-  that a matching execution is possible in the generated Linear code. *)
-
-Definition exec_instr_prop 
-  (sp: val) (b1: block) (ls1: locset) (m1: mem)
-  (t: trace) (b2: block) (ls2: locset) (m2: mem) : Prop :=
-  forall f k,
-  exec_instr tge (linearize_function f) sp
-                 (linearize_block b1 k) ls1 m1
-               t (linearize_block b2 k) ls2 m2.
-
-Definition exec_instrs_prop
-  (sp: val) (b1: block) (ls1: locset) (m1: mem)
-  (t: trace) (b2: block) (ls2: locset) (m2: mem) : Prop :=
-  forall f k,
-  exec_instrs tge (linearize_function f) sp
-                  (linearize_block b1 k) ls1 m1
-                t (linearize_block b2 k) ls2 m2.
-
-Definition exec_block_prop
-  (sp: val) (b: block) (ls1: locset) (m1: mem) 
-  (t: trace) (out: outcome) (ls2: locset) (m2: mem): Prop :=
-  forall f k,
-  valid_outcome f out ->
-  exists k',
-  exec_instrs tge (linearize_function f) sp
-                  (linearize_block b k) ls1 m1
-                t k' ls2 m2
-  /\ cont_for_outcome f out k'.
-
-Definition exec_blocks_prop
-  (c: LTL.code) (sp: val) (pc: node) (ls1: locset) (m1: mem) 
-         (t: trace) (out: outcome) (ls2: locset) (m2: mem): Prop :=
-  forall f k,
-  c = f.(LTL.fn_code) ->
-  (reachable f)!!pc = true ->
-  find_label pc (fn_code (linearize_function f)) = Some k ->
-  valid_outcome f out ->
-  exists k',
-  exec_instrs tge (linearize_function f) sp
-                  k ls1 m1
-                t k' ls2 m2
-  /\ cont_for_outcome f out k'.
-
-Definition exec_function_prop
-  (f: LTL.fundef) (ls1: locset) (m1: mem) (t: trace)
-  (ls2: locset) (m2: mem): Prop :=
-  exec_function tge (transf_fundef f) ls1 m1 t ls2 m2.
-
-Scheme exec_instr_ind5 := Minimality for LTL.exec_instr Sort Prop
-  with exec_instrs_ind5 := Minimality for LTL.exec_instrs Sort Prop
-  with exec_block_ind5 := Minimality for LTL.exec_block Sort Prop
-  with exec_blocks_ind5 := Minimality for LTL.exec_blocks Sort Prop
-  with exec_function_ind5 := Minimality for LTL.exec_function Sort Prop.
-
-(** The obligatory proof by structural induction on the LTL evaluation
-  derivation. *)
-
-Lemma transf_function_correct:
-  forall f ls1 m1 t ls2 m2,
-  LTL.exec_function ge f ls1 m1 t ls2 m2 ->
-  exec_function_prop f ls1 m1 t ls2 m2.
+Hypothesis wt_prog: wt_program prog.
+
+Theorem transf_step_correct:
+  forall s1 t s2, LTL.step ge s1 t s2 ->
+  forall s1' (MS: match_states s1 s1'),
+  exists s2', plus LTLin.step tge s1' t s2' /\ match_states s2 s2'.
 Proof.
-  apply (exec_function_ind5 ge
-           exec_instr_prop
-           exec_instrs_prop
-           exec_block_prop
-           exec_blocks_prop
-           exec_function_prop);
-  intros; red; intros; simpl.
-  (* getstack *)
-  constructor.
-  (* setstack *)
-  constructor.
-  (* op *)
-  constructor. rewrite <- H. apply eval_operation_preserved.
-  exact symbols_preserved.
-  (* load *)
-  apply exec_Lload with a. 
-  rewrite <- H. apply eval_addressing_preserved.
-  exact symbols_preserved.
-  auto.
-  (* store *)
-  apply exec_Lstore with a.
-  rewrite <- H. apply eval_addressing_preserved.
-  exact symbols_preserved.
-  auto.
-  (* call *)
-  apply exec_Lcall with (transf_fundef f).
-  generalize H. destruct ros; simpl.
-  intro; apply functions_translated; auto.
-  rewrite symbols_preserved. destruct (Genv.find_symbol ge i).
-  intro; apply function_ptr_translated; auto. congruence.
-  generalize (sig_preserved f). congruence.
-  apply H2. 
-  (* alloc *)
-  eapply exec_Lalloc; eauto. 
-  (* instr_refl *)
-  apply exec_refl.
-  (* instr_one *)
-  apply exec_one. apply H0. 
-  (* instr_trans *)
-  apply exec_trans with t1 (linearize_block b2 k) rs2 m2 t2.
-  apply H0. apply H2. auto.
-  (* goto *)
-  elim H1. intros REACH [b2 AT2]. 
-  generalize (H0 f k). simpl. intro.
-  elim (find_label_lin f s b2 AT2 REACH). intros k2 FIND.
-  exists (linearize_block b2 k2).
-  split. 
-  eapply exec_trans. eexact H2. constructor. constructor. auto. traceEq.
-  constructor. auto. 
-  (* cond, true *)
-  elim H2. intros REACH [b2 AT2]. 
-  elim (find_label_lin f ifso b2 AT2 REACH). intros k2 FIND.
-  exists (linearize_block b2 k2).
-  split.
-  generalize (H0 f k). simpl. 
-  case (starts_with ifso k); intro.
-  eapply exec_trans. eexact H3. 
-  eapply exec_trans. apply exec_one. apply exec_Lcond_false.
-  change false with (negb true). apply eval_negate_condition. auto.
-  apply exec_one. apply exec_Lgoto. auto. reflexivity. traceEq.
-  eapply exec_trans. eexact H3. 
-  apply exec_one. apply exec_Lcond_true.
-  auto. auto. traceEq.
-  constructor; auto.
-  (* cond, false *)
-  elim H2. intros REACH [b2 AT2]. 
-  elim (find_label_lin f ifnot b2 AT2 REACH). intros k2 FIND.
-  exists (linearize_block b2 k2).
-  split.
-  generalize (H0 f k). simpl. 
-  case (starts_with ifso k); intro.
-  eapply exec_trans. eexact H3. 
-  apply exec_one. apply exec_Lcond_true. 
-  change true with (negb false). apply eval_negate_condition. auto.
-  auto. traceEq.
-  eapply exec_trans. eexact H3.
-  eapply exec_trans. apply exec_one. apply exec_Lcond_false. auto.
-  apply exec_one. apply exec_Lgoto. auto. reflexivity. traceEq.
-  constructor; auto.
-  (* return *)
-  exists (Lreturn :: k). split. 
-  exact (H0 f k). constructor.
-  (* refl blocks *)
-  exists k. split. apply exec_refl. constructor. auto.
-  (* one blocks *)
-  subst c. elim (find_label_lin f pc b H H3). intros k' FIND.
-  assert (k = linearize_block b k'). congruence. subst k.
-  elim (H1 f k' H5). intros k'' [EXEC CFO].
-  exists k''. tauto.
-  (* trans blocks *)
-  assert ((reachable f)!!pc2 = true).
-    eapply reachable_correct_2. eexact H. auto. auto. auto.
-  assert (valid_outcome f (Cont pc2)).
-    eapply exec_blocks_valid_outcome; eauto.
-  generalize (H0 f k H4 H5 H6 H9). intros [k1 [EX1 CFO2]].
-  inversion CFO2. 
-  generalize (H2 f k1 H4 H8 H12 H7). intros [k2 [EX2 CFO3]].
-  exists k2. split. eapply exec_trans; eauto. auto.
-  (* internal function -- TA-DA! *)
-  assert (REACH0: (reachable f)!!(fn_entrypoint f) = true).
+  induction 1; intros; try (inv MS);
+  try (generalize (wt_instrs _ WTF _ _ H); intro WTI).
+  (* Lnop *)
+  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  simpl in EQ. subst c.
+  assert (REACH': (reachable f)!!pc' = true).
+  eapply reachable_successors; eauto.
+  unfold successors; rewrite H; auto with coqlib.
+  exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
+  econstructor; split.
+  eapply add_branch_correct; eauto.
+  eapply is_tail_add_branch. eapply is_tail_find_label. eauto.
+  econstructor; eauto. 
+  (* Lop *)
+  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  simpl in EQ. subst c.
+  assert (REACH': (reachable f)!!pc' = true).
+  eapply reachable_successors; eauto.
+  unfold successors; rewrite H; auto with coqlib.
+  exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
+  econstructor; split.
+  eapply plus_left'.
+  eapply exec_Lop with (v := v); eauto.
+  rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
+  eapply add_branch_correct; eauto.
+  eapply is_tail_add_branch. eapply is_tail_cons_left. 
+  eapply is_tail_find_label. eauto.
+  traceEq.
+  econstructor; eauto.
+  (* Lload *)
+  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  simpl in EQ. subst c.
+  assert (REACH': (reachable f)!!pc' = true).
+  eapply reachable_successors; eauto.
+  unfold successors; rewrite H; auto with coqlib.
+  exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
+  econstructor; split.
+  eapply plus_left'.
+  eapply exec_Lload; eauto.
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply add_branch_correct; eauto.
+  eapply is_tail_add_branch. eapply is_tail_cons_left. 
+  eapply is_tail_find_label. eauto.
+  traceEq.
+  econstructor; eauto.
+  (* Lstore *)
+  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  simpl in EQ. subst c.
+  assert (REACH': (reachable f)!!pc' = true).
+  eapply reachable_successors; eauto.
+  unfold successors; rewrite H; auto with coqlib.
+  exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
+  econstructor; split.
+  eapply plus_left'.
+  eapply exec_Lstore; eauto.
+  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply add_branch_correct; eauto.
+  eapply is_tail_add_branch. eapply is_tail_cons_left. 
+  eapply is_tail_find_label. eauto.
+  traceEq.
+  econstructor; eauto.
+  (* Lcall *)
+  unfold rs1 in *. inv MS. fold rs1.
+  generalize (wt_instrs _ WTF _ _ H); intro WTI.
+  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  simpl in EQ. subst c.
+  assert (REACH': (reachable f)!!pc' = true).
+  eapply reachable_successors; eauto.
+  unfold successors; rewrite H; auto with coqlib.
+  assert (VALID: valid_successor f pc'). inv WTI; auto.
+  econstructor; split.
+  apply plus_one. eapply exec_Lcall with (f' := transf_fundef f'); eauto.
+  apply find_function_translated; auto.
+  symmetry; apply sig_preserved.
+  econstructor; eauto.
+  constructor; auto. econstructor; eauto.
+  eapply is_tail_add_branch. eapply is_tail_cons_left. 
+  eapply is_tail_find_label. eauto.
+  destruct ros; simpl in H0.
+  eapply Genv.find_funct_prop; eauto.
+  destruct (Genv.find_symbol ge i); try discriminate.  
+  eapply Genv.find_funct_ptr_prop; eauto.
+
+  (* Ltailcall *)
+  unfold rs2, rs1 in *. inv MS. fold rs1; fold rs2.
+  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  simpl in EQ. subst c.
+  econstructor; split.
+  apply plus_one. eapply exec_Ltailcall with (f' := transf_fundef f'); eauto.
+  apply find_function_translated; auto.
+  symmetry; apply sig_preserved.
+  rewrite (parent_locset_match _ _ STACKS).
+  econstructor; eauto.
+  destruct ros; simpl in H0.
+  eapply Genv.find_funct_prop; eauto.
+  destruct (Genv.find_symbol ge i); try discriminate.  
+  eapply Genv.find_funct_ptr_prop; eauto.
+
+  (* Lalloc *)
+  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  simpl in EQ. subst c.
+  assert (REACH': (reachable f)!!pc' = true).
+  eapply reachable_successors; eauto.
+  unfold successors; rewrite H; auto with coqlib.
+  exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
+  econstructor; split.
+  eapply plus_left'. 
+  eapply exec_Lalloc; eauto.
+  eapply add_branch_correct; eauto.
+  eapply is_tail_add_branch. eapply is_tail_cons_left. 
+  eapply is_tail_find_label. eauto.
+  traceEq.
+  econstructor; eauto.
+  (* Lcond true *)
+  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  simpl in EQ. subst c.
+  assert (REACH': (reachable f)!!ifso = true).
+  eapply reachable_successors; eauto.
+  unfold successors; rewrite H; auto with coqlib.
+  exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
+  destruct (starts_with ifso c').
+  econstructor; split.
+  eapply plus_left'.  
+  eapply exec_Lcond_false; eauto.
+  change false with (negb true). apply eval_negate_condition; auto.
+  eapply add_branch_correct; eauto.
+  eapply is_tail_add_branch. eapply is_tail_cons_left. 
+  eapply is_tail_find_label. eauto.
+  traceEq.
+  econstructor; eauto.
+  econstructor; split.
+  apply plus_one. eapply exec_Lcond_true; eauto.
+  econstructor; eauto.
+  (* Lcond false *)
+  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  simpl in EQ. subst c.
+  assert (REACH': (reachable f)!!ifnot = true).
+  eapply reachable_successors; eauto.
+  unfold successors; rewrite H; auto with coqlib.
+  exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT'].
+  destruct (starts_with ifso c').
+  econstructor; split.
+  apply plus_one. eapply exec_Lcond_true; eauto.
+  change true with (negb false). apply eval_negate_condition; auto.
+  econstructor; eauto.
+  econstructor; split.
+  eapply plus_left'. 
+  eapply exec_Lcond_false; eauto.
+  eapply add_branch_correct; eauto.
+  eapply is_tail_add_branch. eapply is_tail_cons_left. 
+  eapply is_tail_find_label. eauto.
+  traceEq.
+  econstructor; eauto.
+  (* Lreturn *)
+  destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ].
+  simpl in EQ. subst c.
+  econstructor; split.
+  apply plus_one. eapply exec_Lreturn; eauto.
+  rewrite (parent_locset_match _ _ STACKS).
+  econstructor; eauto. 
+  (* internal function *)
+  assert (REACH: (reachable f)!!(LTL.fn_entrypoint f) = true).
     apply reachable_entrypoint.
-  assert (VO2: valid_outcome f Return). simpl; auto.
-  assert (VO1: valid_outcome f (Cont (fn_entrypoint f))).
-    eapply exec_blocks_valid_outcome; eauto.
-  assert (exists k, fn_code (linearize_function f) = Llabel f.(fn_entrypoint) :: k).
-    unfold linearize_function; simpl. 
-    elim (enumerate_head f). intros tl EN. rewrite EN. 
-    simpl. elim VO1. intros REACH [b EQ]. rewrite EQ. 
-    exists (linearize_block b (linearize_body f tl)). auto.
-  elim H2; intros k EQ.
-  assert (find_label (fn_entrypoint f) (fn_code (linearize_function f)) =
-            Some k).
-    rewrite EQ. simpl. rewrite peq_true. auto.
-  generalize (H1 f k (refl_equal _) REACH0 H3 VO2). 
-  intros [k' [EX CO]].
-  inversion CO. subst k'. 
-  unfold transf_function. apply cleanup_function_correct.
-  econstructor. eauto. rewrite EQ. eapply exec_trans.
-  apply exec_one. constructor. eauto. traceEq.
-  apply unique_labels_lin_function.
+  inv H6. 
+  exploit find_label_lin_succ; eauto. inv H1; auto. intros [c'' AT'].
+  simpl. econstructor; split.
+  eapply plus_left'.  
+  eapply exec_function_internal; eauto.
+  simpl. eapply add_branch_correct. 
+  simpl. eapply is_tail_add_branch. constructor. eauto.
+  traceEq.
+  econstructor; eauto.
   (* external function *)
+  simpl. econstructor; split.
+  apply plus_one. eapply exec_function_external; eauto.
+  econstructor; eauto.
+  (* return *)
+  inv H4. inv H1.
+  exploit find_label_lin_succ; eauto. intros [c' AT].
+  econstructor; split.
+  eapply plus_left'.
+  eapply exec_return; eauto.
+  eapply add_branch_correct; eauto. traceEq.
   econstructor; eauto.
 Qed.
 
-End LINEARIZATION.
+Lemma transf_initial_states:
+  forall st1, LTL.initial_state prog st1 ->
+  exists st2, LTLin.initial_state tprog st2 /\ match_states st1 st2.
+Proof.
+  intros. inversion H. 
+  exists (Callstate nil (transf_fundef f) (Locmap.init Vundef) (Genv.init_mem tprog)); split.
+  econstructor; eauto.
+  change (prog_main tprog) with (prog_main prog).
+  rewrite symbols_preserved. eauto.
+  apply function_ptr_translated; auto.
+  rewrite <- H2. apply sig_preserved.
+  replace (Genv.init_mem tprog) with (Genv.init_mem prog).
+  constructor. constructor.
+  eapply Genv.find_funct_ptr_prop; eauto.
+  symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf.
+Qed.
+
+Lemma transf_final_states:
+  forall st1 st2 r, 
+  match_states st1 st2 -> LTL.final_state st1 r -> LTLin.final_state st2 r.
+Proof.
+  intros. inv H0. inv H. inv H6. constructor. auto. 
+Qed.
 
 Theorem transf_program_correct:
-  forall (p: LTL.program) (t: trace) (r: val),
-  LTL.exec_program p t r ->
-  Linear.exec_program (transf_program p) t r.
+  forall (beh: program_behavior),
+  LTL.exec_program prog beh -> LTLin.exec_program tprog beh.
 Proof.
-  intros p t r [b [f [ls [m [FIND1 [FIND2 [SIG [EX RES]]]]]]]].
-  red. exists b; exists (transf_fundef f); exists ls; exists m.
-  split. change (prog_main (transf_program p)) with (prog_main p).
-  rewrite symbols_preserved; auto.
-  split. apply function_ptr_translated. auto.
-  split. generalize (sig_preserved f); congruence.
-  split. apply transf_function_correct. 
-  unfold transf_program. rewrite Genv.init_mem_transf. auto.
-  rewrite sig_preserved. exact RES.
+  unfold LTL.exec_program, exec_program; intros.
+  eapply simulation_plus_preservation; eauto.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  eexact transf_step_correct.
 Qed.
 
+End LINEARIZATION.