diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-21 15:07:37 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:09 +0200 |
| commit | 08b52fc14b054651932469152e15eb929f802416 (patch) | |
| tree | dd3ef97310ae8793a7c6c4e4bf1e6336aeab88f3 /mppa_k1c/Asmgen.v | |
| parent | 482c4d6f63113ab8486ba1773694bc7756cd0f00 (diff) | |
| download | compcert-kvx-08b52fc14b054651932469152e15eb929f802416.tar.gz compcert-kvx-08b52fc14b054651932469152e15eb929f802416.zip | |
MPPA - Added Mgetstack, loadind, a bunch of loads
Diffstat (limited to 'mppa_k1c/Asmgen.v')
| -rw-r--r-- | mppa_k1c/Asmgen.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 300f21a2..33442dd0 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -696,7 +696,7 @@ Definition indexed_memory_access | Imm64_large imm => Pmake GPR31 imm :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm Ptrofs.zero) :: k *)end. -(* + Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) := match ty, preg_of dst with | Tint, IR rd => OK (indexed_memory_access (Plw rd) base ofs k) @@ -707,7 +707,7 @@ Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) := | Tany64, IR rd => OK (indexed_memory_access (Pld_a rd) base ofs k) | _, _ => Error (msg "Asmgen.loadind") end. - +(* Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) := match ty, preg_of src with | Tint, IR rd => OK (indexed_memory_access (Psw rd) base ofs k) @@ -810,9 +810,9 @@ Definition make_epilogue (f: Mach.function) (k: code) := Definition transl_instr (f: Mach.function) (i: Mach.instruction) (ep: bool) (k: code) := match i with -(*| Mgetstack ofs ty dst => + | Mgetstack ofs ty dst => loadind SP ofs ty dst k - | Msetstack src ofs ty => +(*| Msetstack src ofs ty => storeind src SP ofs ty k | Mgetparam ofs ty dst => (* load via the frame pointer if it is valid *) |