diff options
-rw-r--r-- | backend/Selection.v | 212 | ||||
-rw-r--r-- | backend/Selectionproof.v | 505 |
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. |