diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-20 17:57:46 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:09 +0200 |
| commit | 482c4d6f63113ab8486ba1773694bc7756cd0f00 (patch) | |
| tree | 2931c0b45db8362058214992cc246fd386c91998 /mppa_k1c/Asm.v | |
| parent | 6bf497f210737fa30b54a69454f6f96d92d2a67a (diff) | |
| download | compcert-kvx-482c4d6f63113ab8486ba1773694bc7756cd0f00.tar.gz compcert-kvx-482c4d6f63113ab8486ba1773694bc7756cd0f00.zip | |
MPPA - Activated Mtailcall + Pcall
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 42b5f85f..59b1a139 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -140,7 +140,7 @@ Inductive instruction : Type := | Pget (rd: ireg) (rs: preg) (**r get system register *) | Pset (rd: preg) (rs: ireg) (**r set system register *) | Pret (**r return *) - + | Pcall (l: label) (**r function call *) | Pmv (rd: ireg) (rs: ireg) (**r integer move *) (** 32-bit integer register-immediate instructions *) @@ -567,7 +567,17 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) := | _ => Stuck end end. - +(* +Definition do_call (f: function) (lbl: label) (rs: regset) (m: mem) := + match label_pos lbl 0 (fn_code f) with + | None => Stuck + | Some pos => + match rs#PC with + | Vptr b ofs => Next (rs#PC <- (Vptr b (Ptrofs.repr pos))#RA <- (rs#PC)) m + | _ => Stuck + end + end. +*) (** Auxiliaries for memory accesses *) Definition eval_offset (ofs: offset) : ptrofs := @@ -625,6 +635,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out end | Pret => Next (rs#PC <- (rs#RA)) m + | Pcall s => + Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m | Pmv d s => Next (nextinstr (rs#d <- (rs#s))) m |