diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-03-21 17:46:45 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-04-04 16:30:09 +0200 |
| commit | 447ceed8642e2ed000a20036298adb8448ac594b (patch) | |
| tree | 8d5935601d9c48818e3ea7e1b44e73f0eec74302 /mppa_k1c/Asmgen.v | |
| parent | 0a7a6ed916a95b53b63a9d4bdf1e545aacf3f82b (diff) | |
| download | compcert-kvx-447ceed8642e2ed000a20036298adb8448ac594b.tar.gz compcert-kvx-447ceed8642e2ed000a20036298adb8448ac594b.zip | |
MPPA - Added Msetstack + bunch of store --> on a des call !
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 3445c898..8dd23041 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -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) @@ -719,7 +719,7 @@ Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) : | _, _ => Error (msg "Asmgen.storeind") end. -*) + Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) (k: code) := indexed_memory_access (Pld dst) base ofs k. @@ -812,9 +812,9 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) match i with | 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 => +(*| Mgetparam ofs ty dst => (* load via the frame pointer if it is valid *) do c <- loadind GPR30 ofs ty dst k; OK (if ep then c |