Ajout Sswitch dans Csharpminor. Renommage type variable_info -> var_kind

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

3 files changed, 61 insertions, 27 deletions

diff --git a/backend/Cminorgen.v b/backend/Cminorgen.v
index eeb7b7c..e4c9a42 100644
--- a/backend/Cminorgen.v
+++ b/backend/Cminorgen.v
@@ -264,11 +264,12 @@ Fixpoint transl_stmt (cenv: compilenv) (s: Csharpminor.stmt)
       Some (Sblock ts)
   | Csharpminor.Sexit n =>
       Some (Sexit n)
+  | Csharpminor.Sswitch e cases default =>
+      do te <- transl_expr cenv e; Some(Sswitch te cases default)
   | Csharpminor.Sreturn None =>
       Some (Sreturn None)
   | Csharpminor.Sreturn (Some e) =>
-      do te <- transl_expr cenv e;
-      Some (Sreturn (Some te))
+      do te <- transl_expr cenv e; Some (Sreturn (Some te))
   end.
 
 (** Computation of the set of variables whose address is taken in
@@ -314,6 +315,7 @@ Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t :=
   | Csharpminor.Sloop s => addr_taken_stmt s
   | Csharpminor.Sblock s => addr_taken_stmt s
   | Csharpminor.Sexit n => Identset.empty
+  | Csharpminor.Sswitch e cases default => addr_taken_expr e
   | Csharpminor.Sreturn None => Identset.empty
   | Csharpminor.Sreturn (Some e) => addr_taken_expr e
   end.
@@ -326,7 +328,7 @@ Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t :=
 
 Definition assign_variable
     (atk: Identset.t)
-    (id_lv: ident * variable_info)
+    (id_lv: ident * var_kind)
     (cenv_stacksize: compilenv * Z) : compilenv * Z :=
   let (cenv, stacksize) := cenv_stacksize in
   match id_lv with
@@ -344,7 +346,7 @@ Definition assign_variable
 
 Fixpoint assign_variables
     (atk: Identset.t)
-    (id_lv_list: list (ident * variable_info))
+    (id_lv_list: list (ident * var_kind))
     (cenv_stacksize: compilenv * Z)
     {struct id_lv_list}: compilenv * Z :=
   match id_lv_list with
@@ -361,7 +363,7 @@ Definition build_compilenv
     (globenv, 0).
 
 Definition assign_global_variable
-     (ce: compilenv) (id_vi: ident * variable_info) : compilenv :=
+     (ce: compilenv) (id_vi: ident * var_kind) : compilenv :=
   match id_vi with
   | (id, Vscalar chunk) => PTree.set id (Var_global_scalar chunk) ce
   | (id, Varray sz) => PTree.set id Var_global_array ce
diff --git a/backend/Cminorgenproof.v b/backend/Cminorgenproof.v
index 9158876..e6218a8 100644
--- a/backend/Cminorgenproof.v
+++ b/backend/Cminorgenproof.v
@@ -61,7 +61,7 @@ Proof.
   intros [A B]. elim B. reflexivity.
 Qed.
 
-Definition var_info_global (id: ident) (vi: var_info) (lv: variable_info) :=
+Definition var_info_global (id: ident) (vi: var_info) (lv: var_kind) :=
   match vi with
   | Var_global_scalar chunk => lv = Vscalar chunk
   | Var_global_array => exists sz, lv = Varray sz
@@ -74,7 +74,7 @@ Lemma global_compilenv_charact:
 Proof.
   set (mkgve := fun gv vars =>
          List.fold_left
-          (fun gv (id_vi: ident * variable_info) => PTree.set (fst id_vi) (snd id_vi) gv)
+          (fun gv (id_vi: ident * var_kind) => PTree.set (fst id_vi) (snd id_vi) gv)
           vars gv).
   assert (forall vars gv ce,
             (forall id vi, ce!id = Some vi ->
@@ -94,7 +94,7 @@ Proof.
   inversion H1. exists (Varray z). split. auto. red. exists z; auto.
   eauto.
 
-  intros. change (global_var_env prog) with (mkgve (PTree.empty variable_info) prog.(Csharpminor.prog_vars)).
+  intros. change (global_var_env prog) with (mkgve (PTree.empty var_kind) prog.(Csharpminor.prog_vars)).
   apply H with (PTree.empty var_info). 
   intros until vi0. rewrite PTree.gempty. congruence.
   exact H0.
@@ -332,7 +332,7 @@ Proof.
   case (peq id id0); intro.
     (* the stored variable *)
     subst id0. 
-    change Csharpminor.variable_info with variable_info in H6. 
+    change Csharpminor.var_kind with var_kind in H6. 
     rewrite H in H6. injection H6; clear H6; intros; subst b0 chunk0.
     econstructor. eauto. 
     eapply load_store_same; eauto. auto. 
@@ -1361,7 +1361,7 @@ Lemma match_callstack_alloc_variables:
   match_callstack f cs m.(nextblock) tm.(nextblock) m ->
   mem_inject f m tm ->
   let tparams := List.map (@fst ident memory_chunk) fn.(Csharpminor.fn_params) in
-  let tvars := List.map (@fst ident variable_info) fn.(Csharpminor.fn_vars) in
+  let tvars := List.map (@fst ident var_kind) fn.(Csharpminor.fn_vars) in
   let te := set_locals tvars (set_params targs tparams) in
   exists f',
      inject_incr f f'
@@ -1598,10 +1598,10 @@ Lemma vars_vals_match_holds:
   List.length params = List.length args ->
   val_list_inject f args targs ->
   forall vars,
-  list_norepet (List.map (@fst ident variable_info) vars
+  list_norepet (List.map (@fst ident var_kind) vars
              ++ List.map (@fst ident memory_chunk) params) ->
   vars_vals_match f params args
-    (set_locals (List.map (@fst ident variable_info) vars)
+    (set_locals (List.map (@fst ident var_kind) vars)
       (set_params targs (List.map (@fst ident memory_chunk) params))).
 Proof.
   induction vars; simpl; intros.
@@ -1904,7 +1904,7 @@ Qed.
 Lemma transl_expr_Eaddrof_correct:
    forall (le : Csharpminor.letenv)
      (e : Csharpminor.env) (m : mem) (id : positive)
-     (b : block) (lv : variable_info),
+     (b : block) (lv : var_kind),
    eval_var prog e id b lv ->
    eval_expr_prop le e m (Eaddrof id) m (Vptr b Int.zero).
 Proof.
@@ -2394,6 +2394,24 @@ Proof.
   intuition. subst ts; constructor. constructor.
 Qed.
 
+Lemma transl_stmt_Sswitch_correct:
+  forall (e : Csharpminor.env) (m : mem)
+         (a : Csharpminor.expr) (cases : list (int * nat)) (default : nat)
+         (m1 : mem) (n : int),
+  Csharpminor.eval_expr prog nil e m a m1 (Vint n) ->
+  eval_expr_prop nil e m a m1 (Vint n) ->
+  exec_stmt_prop e m (Csharpminor.Sswitch a cases default) m1
+       (Csharpminor.Out_exit (Csharpminor.switch_target n default cases)).
+Proof.
+  intros; red; intros. monadInv TR.
+  destruct (H0 _ _ _ _ _ _ _ _ _ _ EQ (val_nil_inject f1) MINJ MATCH)
+  as [f2 [te2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]].
+  exists f2; exists te2; exists tm2; 
+  exists (Out_exit (switch_target n default cases)). intuition. 
+  subst ts. constructor. inversion VINJ1. subst tv1. assumption.
+  constructor. 
+Qed.
+
 Lemma transl_stmt_Sreturn_none_correct:
    forall (e : Csharpminor.env) (m : mem),
    exec_stmt_prop e m (Csharpminor.Sreturn None) m
@@ -2457,6 +2475,7 @@ Proof
      transl_stmt_Sloop_exit_correct
      transl_stmt_Sblock_correct
      transl_stmt_Sexit_correct
+     transl_stmt_Sswitch_correct
      transl_stmt_Sreturn_none_correct
      transl_stmt_Sreturn_some_correct).
 
diff --git a/backend/Csharpminor.v b/backend/Csharpminor.v
index 8006042..c0d4cae 100644
--- a/backend/Csharpminor.v
+++ b/backend/Csharpminor.v
@@ -93,6 +93,7 @@ Inductive stmt : Set :=
   | Sloop: stmt -> stmt
   | Sblock: stmt -> stmt
   | Sexit: nat -> stmt
+  | Sswitch: expr -> list (int * nat) -> nat -> stmt
   | Sreturn: option expr -> stmt.
 
 (** The variables can be either scalar variables
@@ -100,26 +101,26 @@ Inductive stmt : Set :=
   or array variables (of the indicated sizes).  The only operation
   permitted on an array variable is taking its address. *)
 
-Inductive variable_info : Set :=
-  | Vscalar: memory_chunk -> variable_info
-  | Varray: Z -> variable_info.
+Inductive var_kind : Set :=
+  | Vscalar: memory_chunk -> var_kind
+  | Varray: Z -> var_kind.
 
 (** Functions are composed of a signature, a list of parameter names
   with associated memory chunks (parameters must be scalar), a list of
-  local variables with associated [variable_info] description, and a
+  local variables with associated [var_kind] description, and a
   statement representing the function body.  *)
 
 Record function : Set := mkfunction {
   fn_sig: signature;
   fn_params: list (ident * memory_chunk);
-  fn_vars: list (ident * variable_info);
+  fn_vars: list (ident * var_kind);
   fn_body: stmt
 }.
 
 Record program : Set := mkprogram {
   prog_funct: list (ident * function);
   prog_main: ident;
-  prog_vars: list (ident * variable_info)
+  prog_vars: list (ident * var_kind)
 }.
 
 (** * Operational semantics *)
@@ -150,6 +151,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.
+
 (** Four kinds of evaluation environments are involved:
 - [genv]: global environments, define symbols and functions;
 - [gvarenv]: map global variables to var info;
@@ -157,12 +165,12 @@ Definition outcome_block (out: outcome) : outcome :=
 - [lenv]: let environments, map de Bruijn indices to values.
 *)
 Definition genv := Genv.t function.
-Definition gvarenv := PTree.t variable_info.
-Definition env := PTree.t (block * variable_info).
-Definition empty_env : env := PTree.empty (block * variable_info).
+Definition gvarenv := PTree.t var_kind.
+Definition env := PTree.t (block * var_kind).
+Definition empty_env : env := PTree.empty (block * var_kind).
 Definition letenv := list val.
 
-Definition sizeof (lv: variable_info) : Z :=
+Definition sizeof (lv: var_kind) : Z :=
   match lv with
   | Vscalar chunk => size_chunk chunk
   | Varray sz => Zmax 0 sz
@@ -183,12 +191,12 @@ Definition fn_params_names (f: function) :=
   List.map (@fst ident memory_chunk) f.(fn_params).
 
 Definition fn_vars_names (f: function) :=
-  List.map (@fst ident variable_info) f.(fn_vars).
+  List.map (@fst ident var_kind) f.(fn_vars).
 
 Definition global_var_env (p: program): gvarenv :=
   List.fold_left
     (fun gve id_vi => PTree.set (fst id_vi) (snd id_vi) gve)
-    p.(prog_vars) (PTree.empty variable_info).
+    p.(prog_vars) (PTree.empty var_kind).
 
 (** Evaluation of operator applications. *)
 
@@ -282,7 +290,7 @@ Definition cast (chunk: memory_chunk) (v: val) : option val :=
   bound to the reference to a fresh block of the appropriate size. *)
 
 Inductive alloc_variables: env -> mem ->
-                           list (ident * variable_info) ->
+                           list (ident * var_kind) ->
                            env -> mem -> list block -> Prop :=
   | alloc_variables_nil:
       forall e m,
@@ -320,7 +328,7 @@ Let ge := Genv.globalenv (program_of_program prg).
    that variable [id] in environment [e] evaluates to block [b]
    and is associated with the variable info [vi]. *)
 
-Inductive eval_var: env -> ident -> block -> variable_info -> Prop :=
+Inductive eval_var: env -> ident -> block -> var_kind -> Prop :=
   | eval_var_local:
       forall e id b vi,
       PTree.get id e = Some (b, vi) ->
@@ -494,6 +502,11 @@ with exec_stmt:
   | exec_Sexit:
       forall e m n,
       exec_stmt e m (Sexit n) m (Out_exit n)
+  | exec_Sswitch:
+      forall e m a cases default m1 n,
+      eval_expr nil e m a m1 (Vint n) ->
+      exec_stmt e m (Sswitch a cases default)
+                  m1 (Out_exit (switch_target n default cases))
   | exec_Sreturn_none:
       forall e m,
       exec_stmt e m (Sreturn None) m (Out_return None)