diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-11-23 16:26:11 +0100 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-11-23 16:26:11 +0100 |
commit | be51963b3a2fca4e50059bcf1776c7b5b6bc5b63 (patch) | |
tree | dedeb95b5b107761b99aa8220847572ce1701ce1 /mppa_k1c/Asmblockgen.v | |
parent | bdaa3eb0ad6486186519ba1ba574e8ac92505cf0 (diff) | |
download | compcert-kvx-be51963b3a2fca4e50059bcf1776c7b5b6bc5b63.tar.gz compcert-kvx-be51963b3a2fca4e50059bcf1776c7b5b6bc5b63.zip |
Changed ABI to match GCC - interoperability not tested yet
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 24 |
1 files changed, 13 insertions, 11 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index d024a74f..8bcbc712 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -25,6 +25,8 @@ Require Import Op Locations Machblock Asmblock. Local Open Scope string_scope. Local Open Scope error_monad_scope. +Notation "'MFP'" := R14 (only parsing). + (** The code generation functions take advantage of several characteristics of the [Mach] code generated by earlier passes of the compiler, mostly that argument and result registers are of the correct @@ -447,10 +449,10 @@ Definition transl_op | Oshrximm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (if Int.eq n Int.zero then Pmv rd rs ::i k else - Psraiw GPR31 rs (Int.repr 31) ::i - Psrliw GPR31 GPR31 (Int.sub Int.iwordsize n) ::i - Paddw GPR31 rs GPR31 ::i - Psraiw rd GPR31 n ::i k) + Psraiw RTMP rs (Int.repr 31) ::i + Psrliw RTMP RTMP (Int.sub Int.iwordsize n) ::i + Paddw RTMP rs RTMP ::i + Psraiw rd RTMP n ::i k) (* [Omakelong], [Ohighlong] should not occur *) | Olowlong, a1 :: nil => @@ -695,7 +697,7 @@ Definition transl_memory_access do rs <- ireg_of a1; OK (indexed_memory_access mk_instr rs ofs ::i k) | Aglobal id ofs, nil => - OK (Ploadsymbol id ofs GPR31 ::i (mk_instr GPR31 (Ofsimm Ptrofs.zero) ::i k)) + OK (Ploadsymbol id ofs RTMP ::i (mk_instr RTMP (Ofsimm Ptrofs.zero) ::i k)) | Ainstack ofs, nil => OK (indexed_memory_access mk_instr SP ofs ::i k) | _, _ => @@ -761,8 +763,8 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing) (** Function epilogue *) Definition make_epilogue (f: Machblock.function) (k: code) := - (loadind_ptr SP f.(fn_retaddr_ofs) GPR8) - ::g Pset RA GPR8 ::g Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::g k. + (loadind_ptr SP f.(fn_retaddr_ofs) GPRA) + ::g Pset RA GPRA ::g Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::g k. (** Translation of a Mach instruction. *) @@ -830,8 +832,8 @@ Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.co Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool := match i with | MBsetstack src ofs ty => before - | MBgetparam ofs ty dst => negb (mreg_eq dst R10) - | MBop op args res => before && negb (mreg_eq res R10) + | MBgetparam ofs ty dst => negb (mreg_eq dst MFP) + | MBop op args res => before && negb (mreg_eq res MFP) | _ => false end. @@ -919,8 +921,8 @@ Definition transl_function (f: Machblock.function) := do lb <- transl_blocks f f.(Machblock.fn_code) true; OK (mkfunction f.(Machblock.fn_sig) (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b - Pget GPR8 RA ::b - storeind_ptr GPR8 SP f.(fn_retaddr_ofs) ::b lb)). + Pget GPRA RA ::b + storeind_ptr GPRA SP f.(fn_retaddr_ofs) ::b lb)). Fixpoint size_blocks (l: bblocks): Z := match l with |