Ajout construction Sswitch dans Cminor

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

3 files changed, 103 insertions, 9 deletions

diff --git a/backend/Cminor.v b/backend/Cminor.v
index 54d5552..826c529 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 32dd2cf..38b19a0 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 e6ab2c2..d34bae9 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).