diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-07-08 12:04:42 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-07-08 12:04:42 +0000 |
commit | 611e7b09253dbbb98e9cd4ca4e07a60b50e693fd (patch) | |
tree | d784e293ec226fec40c12399816824e24a921899 /backend/Selectionproof.v | |
parent | 0290650b7463088bb228bc96d3143941590b54dd (diff) | |
download | compcert-611e7b09253dbbb98e9cd4ca4e07a60b50e693fd.tar.gz compcert-611e7b09253dbbb98e9cd4ca4e07a60b50e693fd.zip |
Fusion partielle de la branche contsem:
- semantiques a continuation pour Cminor et CminorSel
- goto dans Cminor
Suppression de backend/RTLbigstep.v, devenu inutile.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@692 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Selectionproof.v')
-rw-r--r-- | backend/Selectionproof.v | 265 |
1 files changed, 136 insertions, 129 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 8b4713db..bd4dd233 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -21,6 +21,7 @@ Require Import Values. Require Import Mem. Require Import Events. Require Import Globalenvs. +Require Import Smallstep. Require Import Cminor. Require Import Op. Require Import CminorSel. @@ -1060,17 +1061,18 @@ Proof. Qed. Lemma eval_store: - forall chunk a1 a2 v1 v2 m', + 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' -> - exec_stmt ge sp e m (store chunk a1 a2) E0 e m' Out_normal. + 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 _ _ _ _ _ H (refl_equal _)). destruct (addressing a1). intros [vl [EV EQ]]. - eapply exec_Sstore; eauto. + eapply step_store; eauto. Qed. (** * Correctness of instruction selection for operators *) @@ -1241,144 +1243,149 @@ Hint Resolve sel_exprlist_correct: evalexpr. (** Semantic preservation for terminating function calls and statements. *) -Definition eval_funcall_exec_stmt_ind2 - (P1 : mem -> Cminor.fundef -> list val -> trace -> mem -> val -> Prop) - (P2 : val -> env -> mem -> Cminor.stmt -> trace -> env -> mem -> outcome -> Prop) := - fun a b c d e f g h i j k l m n o p q r => - conj (Cminor.eval_funcall_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r) - (Cminor.exec_stmt_ind2 ge P1 P2 a b c d e f g h i j k l m n o p q r). - -Lemma sel_function_stmt_correct: - (forall m fd vargs t m' vres, - Cminor.eval_funcall ge m fd vargs t m' vres -> - CminorSel.eval_funcall tge m (sel_fundef fd) vargs t m' vres) - /\ (forall sp e m s t e' m' out, - Cminor.exec_stmt ge sp e m s t e' m' out -> - CminorSel.exec_stmt tge sp e m (sel_stmt s) t e' m' out). +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. - apply eval_funcall_exec_stmt_ind2; intros; simpl. - (* Internal function *) - econstructor; eauto. - (* External function *) - econstructor; eauto. - (* Sskip *) - constructor. - (* Sassign *) - econstructor; eauto with evalexpr. - (* Sstore *) - eapply eval_store; eauto with evalexpr. - (* Scall *) - econstructor; eauto with evalexpr. - apply functions_translated; auto. - rewrite <- H2. apply sig_function_translated. - (* Salloc *) - econstructor; eauto with evalexpr. - (* Sifthenelse *) - econstructor; eauto with evalexpr. - eapply eval_condition_of_expr; eauto with evalexpr. - destruct b; auto. - (* Sseq *) - eapply exec_Sseq_continue; eauto. - eapply exec_Sseq_stop; eauto. - (* Sloop *) - eapply exec_Sloop_loop; eauto. - eapply exec_Sloop_stop; eauto. - (* Sblock *) - econstructor; eauto. - (* Sexit *) - constructor. - (* Sswitch *) - econstructor; eauto with evalexpr. - (* Sreturn *) - constructor. - econstructor; eauto with evalexpr. - (* Stailcall *) - econstructor; eauto with evalexpr. - apply functions_translated; auto. - rewrite <- H2. apply sig_function_translated. + induction k; simpl; auto. Qed. -Lemma sel_function_correct: - forall m fd vargs t m' vres, - Cminor.eval_funcall ge m fd vargs t m' vres -> - CminorSel.eval_funcall tge m (sel_fundef fd) vargs t m' vres. -Proof (proj1 sel_function_stmt_correct). - -Lemma sel_stmt_correct: - forall sp e m s t e' m' out, - Cminor.exec_stmt ge sp e m s t e' m' out -> - CminorSel.exec_stmt tge sp e m (sel_stmt s) t e' m' out. -Proof (proj2 sel_function_stmt_correct). - -Hint Resolve sel_stmt_correct: evalexpr. - -(** Semantic preservation for diverging function calls and statements. *) +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 (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_function_divergence_correct: - forall m fd vargs t, - Cminor.evalinf_funcall ge m fd vargs t -> - CminorSel.evalinf_funcall tge m (sel_fundef fd) vargs t. +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. - cofix FUNCALL. - assert (STMT: forall sp e m s t, - Cminor.execinf_stmt ge sp e m s t -> - CminorSel.execinf_stmt tge sp e m (sel_stmt s) t). - cofix STMT; intros. - inversion H; subst; simpl. - (* Call *) + 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; auto. + apply functions_translated; eauto. apply sig_function_translated. - (* Ifthenelse *) - econstructor; eauto with evalexpr. - eapply eval_condition_of_expr; eauto with evalexpr. - destruct b; eapply STMT; eauto. - (* Seq *) - apply execinf_Sseq_1; eauto. - eapply execinf_Sseq_2; eauto with evalexpr. - (* Loop *) - eapply execinf_Sloop_body; eauto. - eapply execinf_Sloop_loop; eauto with evalexpr. - change (Sloop (sel_stmt s0)) with (sel_stmt (Cminor.Sloop s0)). - apply STMT. auto. - (* Block *) - apply execinf_Sblock; eauto. - (* Tailcall *) + constructor; auto. + (* Stailcall *) + econstructor; split. econstructor; eauto with evalexpr. - apply functions_translated; auto. + apply functions_translated; eauto. apply sig_function_translated. - - intros. inv H; simpl. - (* Internal functions *) + constructor; auto. apply call_cont_commut. + (* Salloc *) + exists (State (sel_function f) Sskip (sel_cont k) sp (PTree.set id (Vptr b Int.zero) e) m'); split. econstructor; eauto with evalexpr. - unfold sel_function; simpl. eapply STMT; eauto. -Qed. + constructor; auto. + (* 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. rewrite <- H; reflexivity. + constructor; auto. apply call_cont_commut. + (* Sreturn Some *) + econstructor; split. + econstructor. simpl. auto. 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. -End PRESERVATION. +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. -(** As a corollary, instruction selection preserves the observable - behaviour of programs. *) +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 sel_program_correct: - forall prog beh, - Cminor.exec_program prog beh -> - CminorSel.exec_program (sel_program prog) beh. +Theorem transf_program_correct: + forall (beh: program_behavior), + Cminor.exec_program prog beh -> CminorSel.exec_program tprog beh. Proof. - intros. inv H. - (* Terminating *) - apply program_terminates with b (sel_fundef f) m. - simpl. rewrite <- H0. unfold ge. apply symbols_preserved. - apply function_ptr_translated. auto. - rewrite <- H2. apply sig_function_translated. - replace (Genv.init_mem (sel_program prog)) with (Genv.init_mem prog). - apply sel_function_correct; auto. - symmetry. unfold sel_program. apply Genv.init_mem_transf. - (* Diverging *) - apply program_diverges with b (sel_fundef f). - simpl. rewrite <- H0. unfold ge. apply symbols_preserved. - apply function_ptr_translated. auto. - rewrite <- H2. apply sig_function_translated. - replace (Genv.init_mem (sel_program prog)) with (Genv.init_mem prog). - apply sel_function_divergence_correct; auto. - symmetry. unfold sel_program. apply Genv.init_mem_transf. + 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. |