From 8ccc7f2f597aff2c8590c4e62552fb53406ad0f8 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 10 Nov 2009 14:58:33 +0000 Subject: More realistic treatment of jump tables: show the absence of overflow when accessing the table git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1172 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asm.v | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'powerpc/Asm.v') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 18dc93a..1582b41 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -298,8 +298,7 @@ lbl: .long 0x43300000, 0x00000000 - [Pbtbl reg table]: this is a N-way branch, implemented via a jump table as follows: << - rlwinm r12, reg, 2, 0, 29 - addis r12, r12, ha16(lbl) + addis r12, reg, ha16(lbl) lwz r12, lo16(lbl)(r12) mtctr r12 bctr r12 @@ -307,6 +306,7 @@ lbl: .long 0x43300000, 0x00000000 lbl: .long table[0], table[1], ... .text >> + Note that [reg] contains 4 times the index of the desired table entry. *) Definition code := list instruction. @@ -624,10 +624,13 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Pbtbl r tbl => match rs#r with | Vint n => - match list_nth_z tbl (Int.signed n) with - | None => Error - | Some lbl => goto_label c lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m - end + 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 #GPR12 <- Vundef #CTR <- Vundef) m + end + else Error | _ => Error end | Pcmplw r1 r2 => -- cgit v1.2.3