diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-10 14:58:33 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-11-10 14:58:33 +0000 |
| commit | 8ccc7f2f597aff2c8590c4e62552fb53406ad0f8 (patch) | |
| tree | a553844ce1b6960ae5240f65593c085be733e3b2 /powerpc/Asm.v | |
| parent | 74487f079dd56663f97f9731cea328931857495c (diff) | |
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
Diffstat (limited to 'powerpc/Asm.v')
| -rw-r--r-- | powerpc/Asm.v | 15 |
1 files changed, 9 insertions, 6 deletions
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 => |