From 74487f079dd56663f97f9731cea328931857495c Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 10 Nov 2009 12:50:57 +0000 Subject: Added support for jump tables in back end. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1171 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgen.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'backend/RTLgen.v') diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 39add986..942dc50b 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -474,6 +474,15 @@ Definition transl_exit (nexits: list node) (n: nat) : mon node := | Some ne => ret ne end. +Fixpoint transl_jumptable (nexits: list node) (tbl: list nat) : mon (list node) := + match tbl with + | nil => ret nil + | t1 :: tl => + do n1 <- transl_exit nexits t1; + do nl <- transl_jumptable nexits tl; + ret (n1 :: nl) + end. + Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree) {struct t} : mon node := match t with @@ -487,6 +496,14 @@ Fixpoint transl_switch (r: reg) (nexits: list node) (t: comptree) do n2 <- transl_switch r nexits t2; do n1 <- transl_switch r nexits t1; add_instr (Icond (Ccompuimm Clt key) (r :: nil) n1 n2) + | CTjumptable ofs sz tbl t' => + do rt <- new_reg; + do ttbl <- transl_jumptable nexits tbl; + do n1 <- add_instr (Ijumptable rt ttbl); + do n2 <- transl_switch r nexits t'; + do n3 <- add_instr (Icond (Ccompuimm Clt sz) (rt :: nil) n1 n2); + let op := if Int.eq ofs Int.zero then Omove else Oaddimm (Int.neg ofs) in + add_instr (Iop op (r :: nil) rt n3) end. (** Translation of statements. [transl_stmt map s nd nexits nret rret] -- cgit