Changed ABI to match GCC - interoperability not tested yet

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