From 50d4a49522c2090d05032e2acaa91591cae3ec8a Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
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/RTLgen.v | 30 ++++++++++++++++++++++++++----
 1 file changed, 26 insertions(+), 4 deletions(-)

(limited to 'backend/RTLgen.v')

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
-- 
cgit