From 50d4a49522c2090d05032e2acaa91591cae3ec8a Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 5 Jun 2006 09:02:16 +0000 Subject: Ajout construction Sswitch dans Cminor git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@31 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Cminor.v | 13 ++++++++++ backend/RTLgen.v | 30 +++++++++++++++++++--- backend/RTLgenproof.v | 69 +++++++++++++++++++++++++++++++++++++++++++++++---- 3 files changed, 103 insertions(+), 9 deletions(-) (limited to 'backend') diff --git a/backend/Cminor.v b/backend/Cminor.v index 54d55529..826c5298 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -59,6 +59,7 @@ Inductive stmt : Set := | Sloop: stmt -> stmt | Sblock: stmt -> stmt | Sexit: nat -> stmt + | Sswitch: expr -> list (int * nat) -> nat -> stmt | Sreturn: option expr -> stmt. (** Functions are composed of a signature, a list of parameter names, @@ -106,6 +107,13 @@ Definition outcome_block (out: outcome) : outcome := | Out_return optv => Out_return optv end. +Fixpoint switch_target (n: int) (dfl: nat) (cases: list (int * nat)) + {struct cases} : nat := + match cases with + | nil => dfl + | (n1, lbl1) :: rem => if Int.eq n n1 then lbl1 else switch_target n dfl rem + end. + (** Three kinds of evaluation environments are involved: - [genv]: global environments, define symbols and functions; - [env]: local environments, map local variables to values; @@ -310,6 +318,11 @@ with exec_stmt: | exec_Sexit: forall sp e m n, exec_stmt sp e m (Sexit n) e m (Out_exit n) + | exec_Sswitch: + forall sp e m a cases default e1 m1 n, + eval_expr sp nil e m a e1 m1 (Vint n) -> + exec_stmt sp e m (Sswitch a cases default) + e1 m1 (Out_exit (switch_target n default cases)) | exec_Sreturn_none: forall sp e m, exec_stmt sp e m (Sreturn None) e m (Out_return None) diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 32dd2cfa..38b19a01 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -378,6 +378,26 @@ with transl_exprlist (map: mapping) (mut: list ident) Parameter more_likely: condexpr -> stmt -> stmt -> bool. +(** Auxiliary for translating [Sswitch] statements. *) + +Definition transl_exit (nexits: list node) (n: nat) : mon node := + match nth_error nexits n with + | None => error node + | Some ne => ret ne + end. + +Fixpoint transl_switch (r: reg) (nexits: list node) + (cases: list (int * nat)) (default: nat) + {struct cases} : mon node := + match cases with + | nil => + transl_exit nexits default + | (key1, exit1) :: cases' => + do ncont <- transl_switch r nexits cases' default; + do nfound <- transl_exit nexits exit1; + add_instr (Icond (Ccompimm Ceq key1) (r :: nil) nfound ncont) + end. + (** Translation of statements. [transl_stmt map s nd nexits nret rret] enriches the current CFG with the RTL instructions necessary to execute the Cminor statement [s], and returns the node of the first @@ -417,10 +437,12 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) | Sblock sbody => transl_stmt map sbody nd (nd :: nexits) nret rret | Sexit n => - match nth_error nexits n with - | None => error node - | Some ne => ret ne - end + transl_exit nexits n + | Sswitch a cases default => + let mut := mutated_expr a in + do r <- alloc_reg map mut a; + do ns <- transl_switch r nexits cases default; + transl_expr map mut a r ns | Sreturn opt_a => match opt_a, rret with | None, None => ret nret diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index e6ab2c27..d34bae96 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -1169,16 +1169,74 @@ Proof. destruct n; simpl; auto. Qed. +Lemma transl_exit_correct: + forall nexits ex s nd s', + transl_exit nexits ex s = OK nd s' -> + nth_error nexits ex = Some nd. +Proof. + intros until s'. unfold transl_exit. + case (nth_error nexits ex); intros; simplify_eq H; congruence. +Qed. + Lemma transl_stmt_Sexit_correct: forall (sp: val) (e : env) (m : mem) (n : nat), transl_stmt_correct sp e m (Sexit n) e m (Out_exit n). Proof. intros; red; intros. - generalize TE. simpl. caseEq (nth_error nexits n). - intros n' NE. monadSimpl. subst n'. - simpl in OUT. assert (ns = nd). congruence. subst ns. - exists rs. intuition. apply exec_refl. - intro. monadSimpl. + simpl in TE. simpl in OUT. + generalize (transl_exit_correct _ _ _ _ _ TE); intro. + assert (ns = nd). congruence. subst ns. + exists rs. simpl. intuition. apply exec_refl. +Qed. + +Lemma transl_switch_correct: + forall sp rs m r i nexits nd default cases s ns s', + transl_switch r nexits cases default s = OK ns s' -> + nth_error nexits (switch_target i default cases) = Some nd -> + rs#r = Vint i -> + exec_instrs tge s'.(st_code) sp ns rs m nd rs m. +Proof. + induction cases; simpl; intros. + generalize (transl_exit_correct _ _ _ _ _ H). intros. + assert (ns = nd). congruence. subst ns. apply exec_refl. + destruct a as [key1 exit1]. monadInv H. clear H. intro EQ1. + caseEq (Int.eq i key1); intro IEQ; rewrite IEQ in H0. + (* i = key1 *) + apply exec_trans with n0 rs m. apply exec_one. + eapply exec_Icond_true. eauto with rtlg. simpl. rewrite H1. congruence. + generalize (transl_exit_correct _ _ _ _ _ EQ0); intro. + assert (n0 = nd). congruence. subst n0. apply exec_refl. + (* i <> key1 *) + apply exec_trans with n rs m. apply exec_one. + eapply exec_Icond_false. eauto with rtlg. simpl. rewrite H1. congruence. + apply exec_instrs_incr with s0; eauto with rtlg. +Qed. + +Lemma transl_stmt_Sswitch_correct: + forall (sp : val) (e : env) (m : mem) (a : expr) + (cases : list (int * nat)) (default : nat) (e1 : env) (m1 : mem) + (n : int), + eval_expr ge sp nil e m a e1 m1 (Vint n) -> + transl_expr_correct sp nil e m a e1 m1 (Vint n) -> + transl_stmt_correct sp e m (Sswitch a cases default) e1 m1 + (Out_exit (switch_target n default cases)). +Proof. + intros; red; intros. monadInv TE. clear TE; intros EQ1. + simpl in OUT. + assert (state_incr s s1). eauto with rtlg. + + red in H0. + assert (MWF1: map_wf map s1). eauto with rtlg. + assert (TRG1: target_reg_ok s1 map (mutated_expr a) a r). eauto with rtlg. + destruct (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME (incl_refl _) TRG1) + as [rs' [EXEC1 [ME1 [RES1 OTHER1]]]]. + simpl. exists rs'. + (* execution *) + split. eapply exec_trans. eexact EXEC1. + apply exec_instrs_incr with s1. eauto with rtlg. + eapply transl_switch_correct; eauto. + (* match_env & match_reg *) + tauto. Qed. Lemma transl_stmt_Sreturn_none_correct: @@ -1256,6 +1314,7 @@ Proof transl_stmt_Sloop_stop_correct transl_stmt_Sblock_correct transl_stmt_Sexit_correct + transl_stmt_Sswitch_correct transl_stmt_Sreturn_none_correct transl_stmt_Sreturn_some_correct). -- cgit