From cdf83055d96e2af784a97c783c94b83ba2032ae1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 19 Nov 2009 13:31:08 +0000 Subject: Added support for jump tables. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1181 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asm.v | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) (limited to 'arm/Asm.v') diff --git a/arm/Asm.v b/arm/Asm.v index a8151a85..e8503bbd 100644 --- a/arm/Asm.v +++ b/arm/Asm.v @@ -148,7 +148,8 @@ Inductive instruction : Type := | Pallocframe: Z -> Z -> int -> instruction (**r allocate new stack frame *) | Pfreeframe: int -> instruction (**r deallocate stack frame and restore previous frame *) | Plabel: label -> instruction (**r define a code label *) - | Ploadsymbol: ireg -> ident -> int -> instruction. (**r load the address of a symbol *) + | Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *) + | Pbtbl: ireg -> list label -> instruction. (**r N-way branch through a jump table *) (** The pseudo-instructions are the following: @@ -187,6 +188,14 @@ lbl: .word symbol >> Again, our memory model cannot comprehend that this operation frees (logically) the current stack frame. +- [Pbtbl reg table]: this is a N-way branch, implemented via a jump table + as follows: +<< + ldr pc, [pc, reg] + mov r0, r0 (* no-op *) + .word table[0], table[1], ... +>> + Note that [reg] contains 4 times the index of the desired table entry. *) Definition code := list instruction. @@ -507,6 +516,18 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome OK (nextinstr rs) m | Ploadsymbol r1 lbl ofs => OK (nextinstr (rs#r1 <- (symbol_offset lbl ofs))) m + | Pbtbl r tbl => + match rs#r with + | Vint n => + let pos := Int.signed n in + if zeq (Zmod pos 4) 0 then + match list_nth_z tbl (pos / 4) with + | None => Error + | Some lbl => goto_label c lbl rs m + end + else Error + | _ => Error + end end. (** Translation of the LTL/Linear/Mach view of machine registers -- cgit