Forgot to add some files

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

2 files changed, 717 insertions, 0 deletions

diff --git a/backend/Selection.v b/backend/Selection.v
new file mode 100644
index 00000000..4355faf5
--- /dev/null
+++ b/backend/Selection.v
@@ -0,0 +1,212 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Instruction selection *)
+
+(** The instruction selection pass recognizes opportunities for using
+  combined arithmetic and logical operations and addressing modes
+  offered by the target processor.  For instance, the expression [x + 1]
+  can take advantage of the "immediate add" instruction of the processor,
+  and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned
+  into a "rotate and mask" instruction.
+
+  Instruction selection proceeds by bottom-up rewriting over expressions.
+  The source language is Cminor and the target language is CminorSel. *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Mem.
+Require Import Globalenvs.
+Require Cminor.
+Require Import Op.
+Require Import CminorSel.
+Require Import SelectOp.
+
+Open Local Scope cminorsel_scope.
+
+(** Conversion of conditional expressions *)
+
+Fixpoint negate_condexpr (e: condexpr): condexpr :=
+  match e with
+  | CEtrue => CEfalse
+  | CEfalse => CEtrue
+  | CEcond c el => CEcond (negate_condition c) el
+  | CEcondition e1 e2 e3 =>
+      CEcondition e1 (negate_condexpr e2) (negate_condexpr e3)
+  end.
+
+Definition is_compare_neq_zero (c: condition) : bool :=
+  match c with
+  | Ccompimm Cne n => Int.eq n Int.zero
+  | Ccompuimm Cne n => Int.eq n Int.zero
+  | _ => false
+  end.
+
+Definition is_compare_eq_zero (c: condition) : bool :=
+  match c with
+  | Ccompimm Ceq n => Int.eq n Int.zero
+  | Ccompuimm Ceq n => Int.eq n Int.zero
+  | _ => false
+  end.
+
+Fixpoint condexpr_of_expr (e: expr) : condexpr :=
+  match e with
+  | Eop (Ointconst n) Enil =>
+      if Int.eq n Int.zero then CEfalse else CEtrue
+  | Eop (Ocmp c) (e1 ::: Enil) =>
+      if is_compare_neq_zero c then
+        condexpr_of_expr e1
+      else if is_compare_eq_zero c then
+        negate_condexpr (condexpr_of_expr e1)
+      else
+        CEcond c (e1 ::: Enil)
+  | Eop (Ocmp c) el =>
+      CEcond c el
+  | Econdition ce e1 e2 =>
+      CEcondition ce (condexpr_of_expr e1) (condexpr_of_expr e2)
+  | _ =>
+      CEcond (Ccompimm Cne Int.zero) (e:::Enil)
+  end.
+
+(** Conversion of loads and stores *)
+
+Definition load (chunk: memory_chunk) (e1: expr) :=
+  match addressing chunk e1 with
+  | (mode, args) => Eload chunk mode args
+  end.
+
+Definition store (chunk: memory_chunk) (e1 e2: expr) :=
+  match addressing chunk e1 with
+  | (mode, args) => Sstore chunk mode args e2
+  end.
+
+(** Instruction selection for operator applications.  Most of the work
+    is done by the processor-specific smart constructors defined
+    in module [SelectOp]. *)
+
+Definition sel_constant (cst: Cminor.constant) : expr :=
+  match cst with
+  | Cminor.Ointconst n => Eop (Ointconst n) Enil
+  | Cminor.Ofloatconst f => Eop (Ofloatconst f) Enil
+  | Cminor.Oaddrsymbol id ofs => Eop (Oaddrsymbol id ofs) Enil
+  | Cminor.Oaddrstack ofs => Eop (Oaddrstack ofs) Enil
+  end.
+
+Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
+  match op with
+  | Cminor.Ocast8unsigned => cast8unsigned arg 
+  | Cminor.Ocast8signed => cast8signed arg 
+  | Cminor.Ocast16unsigned => cast16unsigned arg 
+  | Cminor.Ocast16signed => cast16signed arg 
+  | Cminor.Onegint => negint arg
+  | Cminor.Onotbool => notbool arg
+  | Cminor.Onotint => notint arg
+  | Cminor.Onegf => negf arg
+  | Cminor.Oabsf => absf arg
+  | Cminor.Osingleoffloat => singleoffloat arg
+  | Cminor.Ointoffloat => intoffloat arg
+  | Cminor.Ointuoffloat => intuoffloat arg
+  | Cminor.Ofloatofint => floatofint arg
+  | Cminor.Ofloatofintu => floatofintu arg
+  end.
+
+Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
+  match op with
+  | Cminor.Oadd => add arg1 arg2
+  | Cminor.Osub => sub arg1 arg2
+  | Cminor.Omul => mul arg1 arg2
+  | Cminor.Odiv => divs arg1 arg2
+  | Cminor.Odivu => divu arg1 arg2
+  | Cminor.Omod => mods arg1 arg2
+  | Cminor.Omodu => modu arg1 arg2
+  | Cminor.Oand => and arg1 arg2
+  | Cminor.Oor => or arg1 arg2
+  | Cminor.Oxor => xor arg1 arg2
+  | Cminor.Oshl => shl arg1 arg2
+  | Cminor.Oshr => shr arg1 arg2
+  | Cminor.Oshru => shru arg1 arg2
+  | Cminor.Oaddf => addf arg1 arg2
+  | Cminor.Osubf => subf arg1 arg2
+  | Cminor.Omulf => mulf arg1 arg2
+  | Cminor.Odivf => divf arg1 arg2
+  | Cminor.Ocmp c => comp c arg1 arg2
+  | Cminor.Ocmpu c => compu c arg1 arg2
+  | Cminor.Ocmpf c => compf c arg1 arg2
+  end.
+
+(** Conversion from Cminor expression to Cminorsel expressions *)
+
+Fixpoint sel_expr (a: Cminor.expr) : expr :=
+  match a with
+  | Cminor.Evar id => Evar id
+  | Cminor.Econst cst => sel_constant cst
+  | Cminor.Eunop op arg => sel_unop op (sel_expr arg)
+  | Cminor.Ebinop op arg1 arg2 => sel_binop op (sel_expr arg1) (sel_expr arg2)
+  | Cminor.Eload chunk addr => load chunk (sel_expr addr)
+  | Cminor.Econdition cond ifso ifnot =>
+      Econdition (condexpr_of_expr (sel_expr cond))
+                 (sel_expr ifso) (sel_expr ifnot)
+  end.
+
+Fixpoint sel_exprlist (al: list Cminor.expr) : exprlist :=
+  match al with
+  | nil => Enil
+  | a :: bl => Econs (sel_expr a) (sel_exprlist bl)
+  end.
+
+(** Conversion from Cminor statements to Cminorsel statements. *)
+
+Fixpoint sel_stmt (s: Cminor.stmt) : stmt :=
+  match s with
+  | Cminor.Sskip => Sskip
+  | Cminor.Sassign id e => Sassign id (sel_expr e)
+  | Cminor.Sstore chunk addr rhs => store chunk (sel_expr addr) (sel_expr rhs)
+  | Cminor.Scall optid sg fn args =>
+      Scall optid sg (sel_expr fn) (sel_exprlist args)
+  | Cminor.Stailcall sg fn args => 
+      Stailcall sg (sel_expr fn) (sel_exprlist args)
+  | Cminor.Sseq s1 s2 => Sseq (sel_stmt s1) (sel_stmt s2)
+  | Cminor.Sifthenelse e ifso ifnot =>
+      Sifthenelse (condexpr_of_expr (sel_expr e))
+                  (sel_stmt ifso) (sel_stmt ifnot)
+  | Cminor.Sloop body => Sloop (sel_stmt body)
+  | Cminor.Sblock body => Sblock (sel_stmt body)
+  | Cminor.Sexit n => Sexit n
+  | Cminor.Sswitch e cases dfl => Sswitch (sel_expr e) cases dfl
+  | Cminor.Sreturn None => Sreturn None
+  | Cminor.Sreturn (Some e) => Sreturn (Some (sel_expr e))
+  | Cminor.Slabel lbl body => Slabel lbl (sel_stmt body)
+  | Cminor.Sgoto lbl => Sgoto lbl
+  end.
+
+(** Conversion of functions and programs. *)
+
+Definition sel_function (f: Cminor.function) : function :=
+  mkfunction
+    f.(Cminor.fn_sig)
+    f.(Cminor.fn_params)
+    f.(Cminor.fn_vars)
+    f.(Cminor.fn_stackspace)
+    (sel_stmt f.(Cminor.fn_body)).
+
+Definition sel_fundef (f: Cminor.fundef) : fundef :=
+  transf_fundef sel_function f.
+
+Definition sel_program (p: Cminor.program) : program :=
+  transform_program sel_fundef p.
+
+
+
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
new file mode 100644
index 00000000..32f90f55
--- /dev/null
+++ b/backend/Selectionproof.v
@@ -0,0 +1,505 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Correctness of instruction selection *)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Mem.
+Require Import Events.
+Require Import Globalenvs.
+Require Import Smallstep.
+Require Import Cminor.
+Require Import Op.
+Require Import CminorSel.
+Require Import SelectOp.
+Require Import Selection.
+Require Import SelectOpproof.
+
+Open Local Scope cminorsel_scope.
+
+(** * Correctness of the instruction selection functions for expressions *)
+
+Section CMCONSTR.
+
+Variable ge: genv.
+Variable sp: val.
+Variable e: env.
+Variable m: mem.
+
+(** Conversion of condition expressions. *)
+
+Lemma negate_condexpr_correct:
+  forall le a b,
+  eval_condexpr ge sp e m le a b ->
+  eval_condexpr ge sp e m le (negate_condexpr a) (negb b).
+Proof.
+  induction 1; simpl.
+  constructor.
+  constructor.
+  econstructor. eauto. apply eval_negate_condition. auto.
+  econstructor. eauto. destruct vb1; auto.
+Qed. 
+
+Scheme expr_ind2 := Induction for expr Sort Prop
+  with exprlist_ind2 := Induction for exprlist Sort Prop.
+
+Fixpoint forall_exprlist (P: expr -> Prop) (el: exprlist) {struct el}: Prop :=
+  match el with
+  | Enil => True
+  | Econs e el' => P e /\ forall_exprlist P el'
+  end.
+
+Lemma expr_induction_principle:
+  forall (P: expr -> Prop),
+  (forall i : ident, P (Evar i)) ->
+  (forall (o : operation) (e : exprlist),
+     forall_exprlist P e -> P (Eop o e)) ->
+  (forall (m : memory_chunk) (a : Op.addressing) (e : exprlist),
+     forall_exprlist P e -> P (Eload m a e)) ->
+  (forall (c : condexpr) (e : expr),
+     P e -> forall e0 : expr, P e0 -> P (Econdition c e e0)) ->
+  (forall e : expr, P e -> forall e0 : expr, P e0 -> P (Elet e e0)) ->
+  (forall n : nat, P (Eletvar n)) ->
+  forall e : expr, P e.
+Proof.
+  intros. apply expr_ind2 with (P := P) (P0 := forall_exprlist P); auto.
+  simpl. auto.
+  intros. simpl. auto.
+Qed.
+
+Lemma eval_base_condition_of_expr:
+  forall le a v b,
+  eval_expr ge sp e m le a v ->
+  Val.bool_of_val v b ->
+  eval_condexpr ge sp e m le 
+                (CEcond (Ccompimm Cne Int.zero) (a ::: Enil))
+                b.
+Proof.
+  intros. 
+  eapply eval_CEcond. eauto with evalexpr. 
+  inversion H0; simpl. rewrite Int.eq_false; auto. auto. auto.
+Qed.
+
+Lemma is_compare_neq_zero_correct:
+  forall c v b,
+  is_compare_neq_zero c = true ->
+  eval_condition c (v :: nil) = Some b ->
+  Val.bool_of_val v b.
+Proof.
+  intros.
+  destruct c; simpl in H; try discriminate;
+  destruct c; simpl in H; try discriminate;
+  generalize (Int.eq_spec i Int.zero); rewrite H; intro; subst i.
+
+  simpl in H0. destruct v; inv H0. 
+  generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl.
+  subst i; constructor. constructor; auto. constructor.
+
+  simpl in H0. destruct v; inv H0. 
+  generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intros; simpl.
+  subst i; constructor. constructor; auto.
+Qed.
+
+Lemma is_compare_eq_zero_correct:
+  forall c v b,
+  is_compare_eq_zero c = true ->
+  eval_condition c (v :: nil) = Some b ->
+  Val.bool_of_val v (negb b).
+Proof.
+  intros. apply is_compare_neq_zero_correct with (negate_condition c).
+  destruct c; simpl in H; simpl; try discriminate;
+  destruct c; simpl; try discriminate; auto.
+  apply eval_negate_condition; auto.
+Qed.
+
+Lemma eval_condition_of_expr:
+  forall a le v b,
+  eval_expr ge sp e m le a v ->
+  Val.bool_of_val v b ->
+  eval_condexpr ge sp e m le (condexpr_of_expr a) b.
+Proof.
+  intro a0; pattern a0.
+  apply expr_induction_principle; simpl; intros;
+    try (eapply eval_base_condition_of_expr; eauto; fail).
+  
+  destruct o; try (eapply eval_base_condition_of_expr; eauto; fail).
+
+  destruct e0. inv H0. inv H5. simpl in H7. inv H7.  
+  inversion H1. 
+  rewrite Int.eq_false; auto. constructor.
+  subst i; rewrite Int.eq_true. constructor.
+  eapply eval_base_condition_of_expr; eauto.
+
+  inv H0. simpl in H7.
+  assert (eval_condition c vl = Some b).
+    destruct (eval_condition c vl); try discriminate.
+    destruct b0; inv H7; inversion H1; congruence.
+  assert (eval_condexpr ge sp e m le (CEcond c e0) b).
+    eapply eval_CEcond; eauto.
+  destruct e0; auto. destruct e1; auto.
+  simpl in H. destruct H.
+  inv H5. inv H11.
+
+  case_eq (is_compare_neq_zero c); intros.
+  eapply H; eauto.
+  apply is_compare_neq_zero_correct with c; auto.
+
+  case_eq (is_compare_eq_zero c); intros.
+  replace b with (negb (negb b)). apply negate_condexpr_correct.
+  eapply H; eauto.
+  apply is_compare_eq_zero_correct with c; auto.
+  apply negb_involutive.
+
+  auto.
+
+  inv H1. destruct v1; eauto with evalexpr.
+Qed.
+
+Lemma eval_load:
+  forall le a v chunk v',
+  eval_expr ge sp e m le a v ->
+  Mem.loadv chunk m v = Some v' ->
+  eval_expr ge sp e m le (load chunk a) v'.
+Proof.
+  intros. generalize H0; destruct v; simpl; intro; try discriminate.
+  unfold load. 
+  generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (refl_equal _)).
+  destruct (addressing chunk a). intros [vl [EV EQ]]. 
+  eapply eval_Eload; eauto. 
+Qed.
+
+Lemma eval_store:
+  forall chunk a1 a2 v1 v2 f k m',
+  eval_expr ge sp e m nil a1 v1 ->
+  eval_expr ge sp e m nil a2 v2 ->
+  Mem.storev chunk m v1 v2 = Some m' ->
+  step ge (State f (store chunk a1 a2) k sp e m)
+       E0 (State f Sskip k sp e m').
+Proof.
+  intros. generalize H1; destruct v1; simpl; intro; try discriminate.
+  unfold store.
+  generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (refl_equal _)).
+  destruct (addressing chunk a1). intros [vl [EV EQ]]. 
+  eapply step_store; eauto. 
+Qed.
+
+(** Correctness of instruction selection for operators *)
+
+Lemma eval_sel_unop:
+  forall le op a1 v1 v,
+  eval_expr ge sp e m le a1 v1 ->
+  eval_unop op v1 = Some v ->
+  eval_expr ge sp e m le (sel_unop op a1) v.
+Proof.
+  destruct op; simpl; intros; FuncInv; try subst v.
+  apply eval_cast8unsigned; auto.
+  apply eval_cast8signed; auto.
+  apply eval_cast16unsigned; auto.
+  apply eval_cast16signed; auto.
+  apply eval_negint; auto.
+  generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intro.
+  change true with (negb false). eapply eval_notbool; eauto. subst i; constructor.
+  change false with (negb true). eapply eval_notbool; eauto. constructor; auto.
+  change Vfalse with (Val.of_bool (negb true)).
+  eapply eval_notbool; eauto. constructor.
+  apply eval_notint; auto.
+  apply eval_negf; auto.
+  apply eval_absf; auto.
+  apply eval_singleoffloat; auto.
+  apply eval_intoffloat; auto.
+  apply eval_intuoffloat; auto.
+  apply eval_floatofint; auto.
+  apply eval_floatofintu; auto.
+Qed.
+
+Lemma eval_sel_binop:
+  forall le op a1 a2 v1 v2 v,
+  eval_expr ge sp e m le a1 v1 ->
+  eval_expr ge sp e m le a2 v2 ->
+  eval_binop op v1 v2 = Some v ->
+  eval_expr ge sp e m le (sel_binop op a1 a2) v.
+Proof.
+  destruct op; simpl; intros; FuncInv; try subst v.
+  apply eval_add; auto.
+  apply eval_add_ptr_2; auto.
+  apply eval_add_ptr; auto.
+  apply eval_sub; auto.
+  apply eval_sub_ptr_int; auto.
+  destruct (eq_block b b0); inv H1. 
+  eapply eval_sub_ptr_ptr; eauto.
+  apply eval_mul; eauto.
+  generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1.
+  apply eval_divs; eauto.
+  generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1.
+  apply eval_divu; eauto.
+  generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1.
+  apply eval_mods; eauto.
+  generalize (Int.eq_spec i0 Int.zero). destruct (Int.eq i0 Int.zero); inv H1.
+  apply eval_modu; eauto.
+  apply eval_and; auto.
+  apply eval_or; auto.
+  apply eval_xor; auto.
+  caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1.
+  apply eval_shl; auto.
+  caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1.
+  apply eval_shr; auto.
+  caseEq (Int.ltu i0 (Int.repr 32)); intro; rewrite H2 in H1; inv H1.
+  apply eval_shru; auto.
+  apply eval_addf; auto.
+  apply eval_subf; auto.
+  apply eval_mulf; auto.
+  apply eval_divf; auto.
+  apply eval_comp_int; auto.
+  eapply eval_comp_int_ptr; eauto.
+  eapply eval_comp_ptr_int; eauto.
+  destruct (eq_block b b0); inv H1.
+  eapply eval_comp_ptr_ptr; eauto.
+  eapply eval_comp_ptr_ptr_2; eauto.
+  eapply eval_compu; eauto.
+  eapply eval_compf; eauto.
+Qed.
+
+End CMCONSTR.
+
+(** * Semantic preservation for instruction selection. *)
+
+Section PRESERVATION.
+
+Variable prog: Cminor.program.
+Let tprog := sel_program prog.
+Let ge := Genv.globalenv prog.
+Let tge := Genv.globalenv tprog.
+
+(** Relationship between the global environments for the original
+  CminorSel program and the generated RTL program. *)
+
+Lemma symbols_preserved:
+  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
+Proof.
+  intros; unfold ge, tge, tprog, sel_program. 
+  apply Genv.find_symbol_transf.
+Qed.
+
+Lemma functions_translated:
+  forall (v: val) (f: Cminor.fundef),
+  Genv.find_funct ge v = Some f ->
+  Genv.find_funct tge v = Some (sel_fundef f).
+Proof.  
+  intros.
+  exact (Genv.find_funct_transf sel_fundef H).
+Qed.
+
+Lemma function_ptr_translated:
+  forall (b: block) (f: Cminor.fundef),
+  Genv.find_funct_ptr ge b = Some f ->
+  Genv.find_funct_ptr tge b = Some (sel_fundef f).
+Proof.  
+  intros. 
+  exact (Genv.find_funct_ptr_transf sel_fundef H).
+Qed.
+
+Lemma sig_function_translated:
+  forall f,
+  funsig (sel_fundef f) = Cminor.funsig f.
+Proof.
+  intros. destruct f; reflexivity.
+Qed.
+
+(** Semantic preservation for expressions. *)
+
+Lemma sel_expr_correct:
+  forall sp e m a v,
+  Cminor.eval_expr ge sp e m a v ->
+  forall le,
+  eval_expr tge sp e m le (sel_expr a) v.
+Proof.
+  induction 1; intros; simpl.
+  (* Evar *)
+  constructor; auto.
+  (* Econst *)
+  destruct cst; simpl; simpl in H; (econstructor; [constructor|simpl;auto]).
+  rewrite symbols_preserved. auto.
+  (* Eunop *)
+  eapply eval_sel_unop; eauto.
+  (* Ebinop *)
+  eapply eval_sel_binop; eauto.
+  (* Eload *)
+  eapply eval_load; eauto.
+  (* Econdition *)
+  econstructor; eauto. eapply eval_condition_of_expr; eauto. 
+  destruct b1; auto.
+Qed.
+
+Hint Resolve sel_expr_correct: evalexpr.
+
+Lemma sel_exprlist_correct:
+  forall sp e m a v,
+  Cminor.eval_exprlist ge sp e m a v ->
+  forall le,
+  eval_exprlist tge sp e m le (sel_exprlist a) v.
+Proof.
+  induction 1; intros; simpl; constructor; auto with evalexpr.
+Qed.
+
+Hint Resolve sel_exprlist_correct: evalexpr.
+
+(** Semantic preservation for terminating function calls and statements. *)
+
+Fixpoint sel_cont (k: Cminor.cont) : CminorSel.cont :=
+  match k with
+  | Cminor.Kstop => Kstop
+  | Cminor.Kseq s1 k1 => Kseq (sel_stmt s1) (sel_cont k1)
+  | Cminor.Kblock k1 => Kblock (sel_cont k1)
+  | Cminor.Kcall id f sp e k1 =>
+      Kcall id (sel_function f) sp e (sel_cont k1)
+  end.
+
+Inductive match_states: Cminor.state -> CminorSel.state -> Prop :=
+  | match_state: forall f s k s' k' sp e m,
+      s' = sel_stmt s ->
+      k' = sel_cont k ->
+      match_states
+        (Cminor.State f s k sp e m)
+        (State (sel_function f) s' k' sp e m)
+  | match_callstate: forall f args k k' m,
+      k' = sel_cont k ->
+      match_states
+        (Cminor.Callstate f args k m)
+        (Callstate (sel_fundef f) args k' m)
+  | match_returnstate: forall v k k' m,
+      k' = sel_cont k ->
+      match_states
+        (Cminor.Returnstate v k m)
+        (Returnstate v k' m).
+
+Remark call_cont_commut:
+  forall k, call_cont (sel_cont k) = sel_cont (Cminor.call_cont k).
+Proof.
+  induction k; simpl; auto.
+Qed.
+
+Remark find_label_commut:
+  forall lbl s k,
+  find_label lbl (sel_stmt s) (sel_cont k) =
+  option_map (fun sk => (sel_stmt (fst sk), sel_cont (snd sk)))
+             (Cminor.find_label lbl s k).
+Proof.
+  induction s; intros; simpl; auto.
+  unfold store. destruct (addressing m (sel_expr e)); auto.
+  change (Kseq (sel_stmt s2) (sel_cont k))
+    with (sel_cont (Cminor.Kseq s2 k)).
+  rewrite IHs1. rewrite IHs2. 
+  destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)); auto.
+  rewrite IHs1. rewrite IHs2. 
+  destruct (Cminor.find_label lbl s1 k); auto.
+  change (Kseq (Sloop (sel_stmt s)) (sel_cont k))
+    with (sel_cont (Cminor.Kseq (Cminor.Sloop s) k)).
+  auto.
+  change (Kblock (sel_cont k))
+    with (sel_cont (Cminor.Kblock k)).
+  auto.
+  destruct o; auto.
+  destruct (ident_eq lbl l); auto.
+Qed.
+
+Lemma sel_step_correct:
+  forall S1 t S2, Cminor.step ge S1 t S2 ->
+  forall T1, match_states S1 T1 ->
+  exists T2, step tge T1 t T2 /\ match_states S2 T2.
+Proof.
+  induction 1; intros T1 ME; inv ME; simpl;
+  try (econstructor; split; [econstructor; eauto with evalexpr | econstructor; eauto]; fail).
+
+  (* skip call *)
+  econstructor; split. 
+  econstructor. destruct k; simpl in H; simpl; auto. 
+  rewrite <- H0; reflexivity.
+  constructor; auto.
+(*
+  (* assign *)
+  exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id v e) m); split.
+  constructor. auto with evalexpr.
+  constructor; auto.
+*)
+  (* store *)
+  econstructor; split.
+  eapply eval_store; eauto with evalexpr.
+  constructor; auto.
+  (* Scall *)
+  econstructor; split.
+  econstructor; eauto with evalexpr.
+  apply functions_translated; eauto. 
+  apply sig_function_translated.
+  constructor; auto.
+  (* Stailcall *)
+  econstructor; split.
+  econstructor; eauto with evalexpr.
+  apply functions_translated; eauto. 
+  apply sig_function_translated.
+  constructor; auto. apply call_cont_commut.
+  (* Sifthenelse *)
+  exists (State (sel_function f) (if b then sel_stmt s1 else sel_stmt s2) (sel_cont k) sp e m); split.
+  constructor. eapply eval_condition_of_expr; eauto with evalexpr.
+  constructor; auto. destruct b; auto.
+  (* Sreturn None *)
+  econstructor; split. 
+  econstructor.
+  constructor; auto. apply call_cont_commut.
+  (* Sreturn Some *)
+  econstructor; split. 
+  econstructor. simpl. eauto with evalexpr. 
+  constructor; auto. apply call_cont_commut.
+  (* Sgoto *)
+  econstructor; split.
+  econstructor. simpl. rewrite call_cont_commut. rewrite find_label_commut.
+  rewrite H. simpl. reflexivity. 
+  constructor; auto.
+Qed.
+
+Lemma sel_initial_states:
+  forall S, Cminor.initial_state prog S ->
+  exists R, initial_state tprog R /\ match_states S R.
+Proof.
+  induction 1.
+  econstructor; split.
+  econstructor.
+  simpl. fold tge. rewrite symbols_preserved. eexact H.
+  apply function_ptr_translated. eauto. 
+  rewrite <- H1. apply sig_function_translated; auto.
+  unfold tprog, sel_program. rewrite Genv.init_mem_transf.
+  constructor; auto.
+Qed.
+
+Lemma sel_final_states:
+  forall S R r,
+  match_states S R -> Cminor.final_state S r -> final_state R r.
+Proof.
+  intros. inv H0. inv H. simpl. constructor.
+Qed.
+
+Theorem transf_program_correct:
+  forall (beh: program_behavior), not_wrong beh ->
+  Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh.
+Proof.
+  unfold CminorSel.exec_program, Cminor.exec_program; intros.
+  eapply simulation_step_preservation; eauto.
+  eexact sel_initial_states.
+  eexact sel_final_states.
+  exact sel_step_correct. 
+Qed.
+
+End PRESERVATION.