diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-21 20:29:57 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-21 20:29:57 +0100 |
| commit | 47a4ccade6f73e95be34cd2d55be3655302fff97 (patch) | |
| tree | c2369513d83bf3a5a7872dce60e20926de8e76f0 /mppa_k1c/Asmblock.v | |
| parent | ab5528fb4caf637a0c7014d943302198079e7c20 (diff) | |
| download | compcert-kvx-47a4ccade6f73e95be34cd2d55be3655302fff97.tar.gz compcert-kvx-47a4ccade6f73e95be34cd2d55be3655302fff97.zip | |
begin jumptables (does not work)
Diffstat (limited to 'mppa_k1c/Asmblock.v')
| -rw-r--r-- | mppa_k1c/Asmblock.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index d335801e..dfe46e04 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -233,6 +233,7 @@ Inductive cf_instruction : Type := | Pret (**r return *) | Pcall (l: label) (**r function call *) | Picall (r: ireg) (**r function call on register value *) + | Pjumptable (r: ireg) (labels: list label) (**r N-way branch through a jump table (pseudo) *) (* Pgoto is for tailcalls, Pj_l is for jumping to a particular label *) | Pgoto (l: label) (**r goto *) @@ -1470,6 +1471,16 @@ Definition exec_control (f: function) (oc: option control) (rs: regset) (m: mem) Next (rs#PC <- (rs#r)) m | Pj_l l => goto_label f l rs m + | Pjumptable r tbl => + match rs#r with + | Vint n => + match list_nth_z tbl (Int.unsigned n) with + | None => Stuck + | Some lbl => goto_label f lbl (rs #GPR62 <- Vundef #GPR63 <- Vundef) m + end + | _ => Stuck + end + | Pcb bt r l => match cmp_for_btest bt with | (Some c, Int) => eval_branch f l rs m (Val.cmp_bool c rs#r (Vint (Int.repr 0))) |