diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-21 17:05:10 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:09 +0200 |
| commit | 3f5f3aedb19165134b45dbf6aeea877e8ab46f6f (patch) | |
| tree | b423ff4a834c50aa4b9e175d12514c95e03d54fc /mppa_k1c/Asm.v | |
| parent | 08b52fc14b054651932469152e15eb929f802416 (diff) | |
| download | compcert-kvx-3f5f3aedb19165134b45dbf6aeea877e8ab46f6f.tar.gz compcert-kvx-3f5f3aedb19165134b45dbf6aeea877e8ab46f6f.zip | |
MPPA - Added Mcall + Pgoto + modified Pcall
Diffstat (limited to 'mppa_k1c/Asm.v')
| -rw-r--r-- | mppa_k1c/Asm.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 521027ae..8657bc44 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -141,6 +141,7 @@ Inductive instruction : Type := | Pset (rd: preg) (rs: ireg) (**r set system register *) | Pret (**r return *) | Pcall (l: label) (**r function call *) + | Pgoto (l: label) (**r goto *) | Pmv (rd: ireg) (rs: ireg) (**r integer move *) (** 32-bit integer register-immediate instructions *) @@ -636,6 +637,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pret => Next (rs#PC <- (rs#RA)) m | Pcall s => + Next (rs#RA <- (Val.offset_ptr (rs#PC) Ptrofs.one)#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m + (* Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m *) + | Pgoto s => Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m | Pmv d s => Next (nextinstr (rs#d <- (rs#s))) m |