MPPA - The project compiles.

Supports very simple programs that load integer immediates. It starts
the main, loads integer in registers, and return correctly.

Addition in Mach not yet supported, but should not be hard to add them.

Function calls are not yet supported.

The ABI for now is the same as the RiscV, with a small twist: $ra is
first loaded in a user register, then this user register is pushed
(instead of pushing $ra straight away).

2 files changed, 144 insertions, 147 deletions

diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index 945974e0..fea71f61 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -42,9 +42,10 @@ let wordsize = if Archi.ptr64 then 8 else 4
 let align n a = (n + a - 1) land (-a)
 
 (* Emit instruction sequences that set or offset a register by a constant. *)
-
-let expand_loadimm32 dst n =
+(*
+  let expand_loadimm32 dst n =
   List.iter emit (Asmgen.loadimm32 dst n [])
+*)
 let expand_addptrofs dst src n =
   List.iter emit (Asmgen.addptrofs dst src n [])
 let expand_storeind_ptr src base ofs =
@@ -60,11 +61,12 @@ let expand_storeind_ptr src base ofs =
 (* Fix-up code around calls to variadic functions.  Floating-point arguments
    residing in FP registers need to be moved to integer registers. *)
 
-let int_param_regs   = [| X10; X11; X12; X13; X14; X15; X16; X17 |]
-let float_param_regs = [| F10; F11; F12; F13; F14; F15; F16; F17 |]
+let int_param_regs   = [| GPR0; GPR1; GPR2; GPR3; GPR4; GPR5; GPR6; GPR7 |]
+(* let float_param_regs = [| F10; F11; F12; F13; F14; F15; F16; F17 |] *)
+let float_param_regs = [| |]
 
-let rec fixup_variadic_call pos tyl =
-  if pos < 8 then
+let fixup_variadic_call pos tyl = assert false
+(*if pos < 8 then
     match tyl with
     | [] ->
         ()
@@ -98,14 +100,15 @@ let rec fixup_variadic_call pos tyl =
             fixup_variadic_call (pos + 2) tyl
           end
         end
+*)
         
 let fixup_call sg =
   if sg.sig_cc.cc_vararg then fixup_variadic_call 0 sg.sig_args
 
 (* Handling of annotations *)
 
-let expand_annot_val kind txt targ args res =
-  emit (Pbuiltin (EF_annot(kind,txt,[targ]), args, BR_none));
+let expand_annot_val kind txt targ args res = assert false
+(*emit (Pbuiltin (EF_annot(kind,txt,[targ]), args, BR_none));
   match args, res with
   | [BA(IR src)], BR(IR dst) ->
      if dst <> src then emit (Pmv (dst, src))
@@ -113,6 +116,7 @@ let expand_annot_val kind txt targ args res =
      if dst <> src then emit (Pfmv (dst, src))
   | _, _ ->
      raise (Error "ill-formed __builtin_annot_val")
+*)
 
 (* Handling of memcpy *)
 
@@ -121,20 +125,21 @@ let expand_annot_val kind txt targ args res =
 let offset_in_range ofs =
   let ofs = Z.to_int64 ofs in -2048L <= ofs && ofs < 2048L
   
-let memcpy_small_arg sz arg tmp =
-  match arg with
+let memcpy_small_arg sz arg tmp = assert false
+(*match arg with
   | BA (IR r) ->
       (r, _0)
   | BA_addrstack ofs ->
       if offset_in_range ofs
       && offset_in_range (Ptrofs.add ofs (Ptrofs.repr (Z.of_uint sz)))
-      then (X2, ofs)
-      else begin expand_addptrofs tmp X2 ofs; (tmp, _0) end
+      then (GPR12, ofs)
+      else begin expand_addptrofs tmp GPR12 ofs; (tmp, _0) end
   | _ ->
       assert false
+*)
 
-let expand_builtin_memcpy_small sz al src dst =
-  let (tsrc, tdst) =
+let expand_builtin_memcpy_small sz al src dst = assert false
+(*let (tsrc, tdst) =
     if dst <> BA (IR X5) then (X5, X6) else (X6, X5) in
   let (rsrc, osrc) = memcpy_small_arg sz src tsrc in
   let (rdst, odst) = memcpy_small_arg sz dst tdst in
@@ -164,17 +169,19 @@ let expand_builtin_memcpy_small sz al src dst =
         copy (Ptrofs.add osrc _1) (Ptrofs.add odst _1) (sz - 1)
       end
   in copy osrc odst sz
+*)
 
-let memcpy_big_arg sz arg tmp =
-  match arg with
+let memcpy_big_arg sz arg tmp = assert false
+(*match arg with
   | BA (IR r) -> if r <> tmp then emit (Pmv(tmp, r))
   | BA_addrstack ofs ->
       expand_addptrofs tmp X2 ofs
   | _ ->
       assert false
+*)
 
-let expand_builtin_memcpy_big sz al src dst =
-  assert (sz >= al);
+let expand_builtin_memcpy_big sz al src dst = assert false
+(*assert (sz >= al);
   assert (sz mod al = 0);
   let (s, d) =
     if dst <> BA (IR X5) then (X5, X6) else (X6, X5) in
@@ -200,6 +207,7 @@ let expand_builtin_memcpy_big sz al src dst =
   emit store;
   expand_addptrofs d d delta;
   emit (Pbnew (X X7, X0, lbl))
+*)
 
 let expand_builtin_memcpy  sz al args =
   let (dst, src) =
@@ -210,8 +218,8 @@ let expand_builtin_memcpy  sz al args =
 
 (* Handling of volatile reads and writes *)
 
-let expand_builtin_vload_common chunk base ofs res =
-  match chunk, res with
+let expand_builtin_vload_common chunk base ofs res = assert false
+(*match chunk, res with
   | Mint8unsigned, BR(IR res) ->
      emit (Plbu (res, base, Ofsimm ofs))
   | Mint8signed, BR(IR res) ->
@@ -239,30 +247,32 @@ let expand_builtin_vload_common chunk base ofs res =
      emit (Pfld (res, base, Ofsimm ofs))
   | _ ->
      assert false
+*)
 
-let expand_builtin_vload chunk args res =
-  match args with
+let expand_builtin_vload chunk args res = assert false
+(*match args with
   | [BA(IR addr)] ->
       expand_builtin_vload_common chunk addr _0 res
   | [BA_addrstack ofs] ->
       if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then
-        expand_builtin_vload_common chunk X2 ofs res
+        expand_builtin_vload_common chunk GPR12 ofs res
       else begin
-        expand_addptrofs X31 X2 ofs; (* X31 <- sp + ofs *)
-        expand_builtin_vload_common chunk X31 _0 res
+        expand_addptrofs GPR32 GPR12 ofs; (* X31 <- sp + ofs *)
+        expand_builtin_vload_common chunk GPR32 _0 res
       end
   | [BA_addptr(BA(IR addr), (BA_int ofs | BA_long ofs))] ->
       if offset_in_range (Z.add ofs (Memdata.size_chunk chunk)) then
         expand_builtin_vload_common chunk addr ofs res
       else begin
-        expand_addptrofs X31 addr ofs; (* X31 <- addr + ofs *)
-        expand_builtin_vload_common chunk X31 _0 res
+        expand_addptrofs GPR32 addr ofs; (* X31 <- addr + ofs *)
+        expand_builtin_vload_common chunk GPR32 _0 res
       end
   | _ ->
       assert false
+*)
 
-let expand_builtin_vstore_common chunk base ofs src =
-  match chunk, src with
+let expand_builtin_vstore_common chunk base ofs src = assert false
+(*match chunk, src with
   | (Mint8signed | Mint8unsigned), BA(IR src) ->
      emit (Psb (src, base, Ofsimm ofs))
   | (Mint16signed | Mint16unsigned), BA(IR src) ->
@@ -281,9 +291,10 @@ let expand_builtin_vstore_common chunk base ofs src =
      emit (Pfsd (src, base, Ofsimm ofs))
   | _ ->
      assert false
+*)
 
-let expand_builtin_vstore chunk args =
-  match args with
+let expand_builtin_vstore chunk args = assert false
+(*match args with
   | [BA(IR addr); src] ->
       expand_builtin_vstore_common chunk addr _0 src
   | [BA_addrstack ofs; src] ->
@@ -302,6 +313,7 @@ let expand_builtin_vstore chunk args =
       end
   | _ ->
       assert false
+*)
 
 (* Handling of varargs *)
 
@@ -322,19 +334,20 @@ let save_arguments first_reg base_ofs =
   for i = first_reg to 7 do
     expand_storeind_ptr
       int_param_regs.(i)
-      X2
+      GPR12
       (Ptrofs.repr (Z.add base_ofs (Z.of_uint ((i - first_reg) * wordsize))))
   done
 
 let vararg_start_ofs : Z.t option ref = ref None
 
-let expand_builtin_va_start r =
-  match !vararg_start_ofs with
+let expand_builtin_va_start r = assert false
+(*match !vararg_start_ofs with
   | None ->
       invalid_arg "Fatal error: va_start used in non-vararg function"
   | Some ofs ->
       expand_addptrofs X31 X2 (Ptrofs.repr ofs);
       expand_storeind_ptr X31 r Ptrofs.zero
+*)
 
 (* Auxiliary for 64-bit integer arithmetic built-ins.  They expand to
    two instructions, one computing the low 32 bits of the result,
@@ -343,26 +356,27 @@ let expand_builtin_va_start r =
    instruction, we must go through X31 to hold the low 32 bits of the result.
 *)
 
-let expand_int64_arith conflict rl fn =
-  if conflict then (fn X31; emit (Pmv(rl, X31))) else fn rl
+let expand_int64_arith conflict rl fn = assert false
+(*if conflict then (fn X31; emit (Pmv(rl, X31))) else fn rl *)
 
 (* Byte swaps.  There are no specific instructions, so we use standard,
    not-very-efficient formulas. *)
 
-let expand_bswap16 d s =
+let expand_bswap16 d s = assert false
   (* d = (s & 0xFF) << 8 | (s >> 8) & 0xFF *)
-  emit (Pandiw(X31, X s, coqint_of_camlint 0xFFl));
+(*emit (Pandiw(X31, X s, coqint_of_camlint 0xFFl));
   emit (Pslliw(X31, X X31, _8));
   emit (Psrliw(d, X s, _8));
   emit (Pandiw(d, X d, coqint_of_camlint 0xFFl));
   emit (Porw(d, X X31, X d))
+*)
 
-let expand_bswap32 d s =
+let expand_bswap32 d s = assert false
   (* d = (s << 24)
        | (((s >> 8) & 0xFF) << 16)
        | (((s >> 16) & 0xFF) << 8)
        | (s >> 24)  *)
-  emit (Pslliw(X1, X s, coqint_of_camlint 24l));
+(*emit (Pslliw(X1, X s, coqint_of_camlint 24l));
   emit (Psrliw(X31, X s, _8));
   emit (Pandiw(X31, X X31, coqint_of_camlint 0xFFl));
   emit (Pslliw(X31, X X31, _16));
@@ -373,8 +387,9 @@ let expand_bswap32 d s =
   emit (Porw(X1, X X1, X X31));
   emit (Psrliw(X31, X s, coqint_of_camlint 24l));
   emit (Porw(d, X X1, X X31))
+*)
 
-let expand_bswap64 d s =
+let expand_bswap64 d s = assert false
   (* d = s << 56
          | (((s >> 8) & 0xFF) << 48)
          | (((s >> 16) & 0xFF) << 40)
@@ -383,7 +398,7 @@ let expand_bswap64 d s =
          | (((s >> 40) & 0xFF) << 16)
          | (((s >> 48) & 0xFF) << 8)
          | s >> 56 *)
-  emit (Psllil(X1, X s, coqint_of_camlint 56l));
+(*emit (Psllil(X1, X s, coqint_of_camlint 56l));
   List.iter
     (fun (n1, n2) ->
       emit (Psrlil(X31, X s, coqint_of_camlint n1));
@@ -393,6 +408,7 @@ let expand_bswap64 d s =
     [(8l,48l); (16l,40l); (24l,32l); (32l,24l); (40l,16l); (48l,8l)];
   emit (Psrlil(X31, X s, coqint_of_camlint 56l));
   emit (Porl(d, X X1, X X31))
+*)
 
 (* Handling of compiler-inlined builtins *)
 
@@ -401,13 +417,13 @@ let expand_builtin_inline name args res =
   (* Synchronization *)
   | "__builtin_membar", [], _ ->
      ()
-  | "__builtin_fence", [], _ ->
+(*| "__builtin_fence", [], _ ->
      emit Pfence
-  (* Vararg stuff *)
+*)(* Vararg stuff *)
   | "__builtin_va_start", [BA(IR a)], _ ->
      expand_builtin_va_start a
   (* Byte swaps *)
-  | "__builtin_bswap16", [BA(IR a1)], BR(IR res) ->
+(*| "__builtin_bswap16", [BA(IR a1)], BR(IR res) ->
      expand_bswap16 res a1
   | ("__builtin_bswap"| "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
      expand_bswap32 res a1
@@ -468,7 +484,7 @@ let expand_builtin_inline name args res =
                         (fun rl ->
                           emit (Pmulw (rl, X a, X b));
                           emit (Pmulhuw (rh, X a, X b)))
-
+*)
   (* Catch-all *)
   | _ ->
      raise (Error ("unrecognized builtin " ^ name))
@@ -479,20 +495,20 @@ let expand_instruction instr =
   match instr with
   | Pallocframe (sz, ofs) ->
       let sg = get_current_function_sig() in
-      emit (Pmv (X30, X2));
+      emit (Pmv (GPR32, GPR12));
       if sg.sig_cc.cc_vararg then begin
         let n = arguments_size sg in
         let extra_sz = if n >= 8 then 0 else align 16 ((8 - n) * wordsize) in
         let full_sz = Z.add sz (Z.of_uint extra_sz) in
-        expand_addptrofs X2 X2 (Ptrofs.repr (Z.neg full_sz));
-        expand_storeind_ptr X30 X2 ofs;
+        expand_addptrofs GPR12 GPR12 (Ptrofs.repr (Z.neg full_sz));
+        expand_storeind_ptr GPR32 GPR12 ofs;
         let va_ofs =
           Z.add full_sz (Z.of_sint ((n - 8) * wordsize)) in
         vararg_start_ofs := Some va_ofs;
         save_arguments n va_ofs
       end else begin
-        expand_addptrofs X2 X2 (Ptrofs.repr (Z.neg sz));
-        expand_storeind_ptr X30 X2 ofs;
+        expand_addptrofs GPR12 GPR12 (Ptrofs.repr (Z.neg sz));
+        expand_storeind_ptr GPR32 GPR12 ofs;
         vararg_start_ofs := None
       end
   | Pfreeframe (sz, ofs) ->
@@ -502,9 +518,9 @@ let expand_instruction instr =
         let n = arguments_size sg in
         if n >= 8 then 0 else align 16 ((8 - n) * wordsize)
       end else 0 in
-     expand_addptrofs X2 X2 (Ptrofs.repr (Z.add sz (Z.of_uint extra_sz)))
+     expand_addptrofs GPR12 GPR12 (Ptrofs.repr (Z.add sz (Z.of_uint extra_sz)))
 
-  | Pseqw(rd, rs1, rs2) ->
+(*| Pseqw(rd, rs1, rs2) ->
       (* emulate based on the fact that x == 0 iff x <u 1 (unsigned cmp) *)
       if rs2 = X0 then begin
         emit (Psltiuw(rd, rs1, Int.one))
@@ -565,34 +581,30 @@ let expand_instruction instr =
      | _ ->
         assert false
      end
-  | _ ->
+*)| _ ->
      emit instr
 
 (* NOTE: Dwarf register maps for RV32G are not yet specified
    officially.  This is just a placeholder.  *)
 let int_reg_to_dwarf = function
-               | X1  -> 1  | X2  -> 2  | X3  -> 3
-   | X4  -> 4  | X5  -> 5  | X6  -> 6  | X7  -> 7
-   | X8  -> 8  | X9  -> 9  | X10 -> 10 | X11 -> 11
-   | X12 -> 12 | X13 -> 13 | X14 -> 14 | X15 -> 15
-   | X16 -> 16 | X17 -> 17 | X18 -> 18 | X19 -> 19
-   | X20 -> 20 | X21 -> 21 | X22 -> 22 | X23 -> 23
-   | X24 -> 24 | X25 -> 25 | X26 -> 26 | X27 -> 27
-   | X28 -> 28 | X29 -> 29 | X30 -> 30 | X31 -> 31
-
-let float_reg_to_dwarf = function
-   | F0  -> 32 | F1  -> 33 | F2  -> 34 | F3  -> 35
-   | F4  -> 36 | F5  -> 37 | F6  -> 38 | F7  -> 39
-   | F8  -> 40 | F9  -> 41 | F10 -> 42 | F11 -> 43
-   | F12 -> 44 | F13 -> 45 | F14 -> 46 | F15 -> 47
-   | F16 -> 48 | F17 -> 49 | F18 -> 50 | F19 -> 51
-   | F20 -> 52 | F21 -> 53 | F22 -> 54 | F23 -> 55
-   | F24 -> 56 | F25 -> 57 | F26 -> 58 | F27 -> 59
-   | F28 -> 60 | F29 -> 61 | F30 -> 62 | F31 -> 63
+   | GPR0  -> 1   | GPR1  -> 2   | GPR2  -> 3   | GPR3  -> 4   | GPR4  -> 5
+   | GPR5  -> 6   | GPR6  -> 7   | GPR7  -> 8   | GPR8  -> 9   | GPR9  -> 10
+   | GPR10 -> 11  | GPR11 -> 12  | GPR12 -> 13  | GPR13 -> 14  | GPR14 -> 15
+   | GPR15 -> 16  | GPR16 -> 17  | GPR17 -> 18  | GPR18 -> 19  | GPR19 -> 20
+   | GPR20 -> 21  | GPR21 -> 22  | GPR22 -> 23  | GPR23 -> 24  | GPR24 -> 25
+   | GPR25 -> 26  | GPR26 -> 27  | GPR27 -> 28  | GPR28 -> 29  | GPR29 -> 30
+   | GPR30 -> 31  | GPR31 -> 32  | GPR32 -> 33  | GPR33 -> 34  | GPR34 -> 35
+   | GPR35 -> 36  | GPR36 -> 37  | GPR37 -> 38  | GPR38 -> 39  | GPR39 -> 40
+   | GPR40 -> 41  | GPR41 -> 42  | GPR42 -> 43  | GPR43 -> 44  | GPR44 -> 45
+   | GPR45 -> 46  | GPR46 -> 47  | GPR47 -> 48  | GPR48 -> 49  | GPR49 -> 50
+   | GPR50 -> 51  | GPR51 -> 52  | GPR52 -> 53  | GPR53 -> 54  | GPR54 -> 55
+   | GPR55 -> 56  | GPR56 -> 57  | GPR57 -> 58  | GPR58 -> 59  | GPR59 -> 60
+   | GPR60 -> 61  | GPR61 -> 62  | GPR62 -> 63  | GPR63 -> 64
 
 let preg_to_dwarf = function
    | IR r -> int_reg_to_dwarf r
-   | FR r -> float_reg_to_dwarf r
+   | FR r -> int_reg_to_dwarf r
+   | RA   -> 65 (* FIXME - No idea *)
    | _ -> assert false
 
 let expand_function id fn =
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 696bc87f..3d348655 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -40,66 +40,41 @@ module Target : TARGET =
 
     let print_label oc lbl = label oc (transl_label lbl)
 
-    let use_abi_name = false
-
-    let int_reg_num_name = function
-                     | X1  -> "x1"  | X2  -> "x2"  | X3  -> "x3"
-      | X4  -> "x4"  | X5  -> "x5"  | X6  -> "x6"  | X7  -> "x7"
-      | X8  -> "x8"  | X9  -> "x9"  | X10 -> "x10" | X11 -> "x11"
-      | X12 -> "x12" | X13 -> "x13" | X14 -> "x14" | X15 -> "x15"
-      | X16 -> "x16" | X17 -> "x17" | X18 -> "x18" | X19 -> "x19"
-      | X20 -> "x20" | X21 -> "x21" | X22 -> "x22" | X23 -> "x23"
-      | X24 -> "x24" | X25 -> "x25" | X26 -> "x26" | X27 -> "x27"
-      | X28 -> "x28" | X29 -> "x29" | X30 -> "x30" | X31 -> "x31"
-
-    let int_reg_abi_name = function
-                     | X1  -> "ra"  | X2  -> "sp"  | X3  -> "gp"
-      | X4  -> "tp"  | X5  -> "t0"  | X6  -> "t1"  | X7  -> "t2"
-      | X8  -> "s0"  | X9  -> "s1"  | X10 -> "a0"  | X11 -> "a1"
-      | X12 -> "a2"  | X13 -> "a3"  | X14 -> "a4"  | X15 -> "a5"
-      | X16 -> "a6"  | X17 -> "a7"  | X18 -> "s2"  | X19 -> "s3"
-      | X20 -> "s4"  | X21 -> "s5"  | X22 -> "s6"  | X23 -> "s7"
-      | X24 -> "s8"  | X25 -> "s9"  | X26 -> "s10" | X27 -> "s11"
-      | X28 -> "t3"  | X29 -> "t4"  | X30 -> "t5"  | X31 -> "t6"
-
-    let float_reg_num_name = function
-      | F0  -> "f0"  | F1  -> "f1"  | F2  -> "f2"  | F3  -> "f3"
-      | F4  -> "f4"  | F5  -> "f5"  | F6  -> "f6"  | F7  -> "f7"
-      | F8  -> "f8"  | F9  -> "f9"  | F10 -> "f10" | F11 -> "f11"
-      | F12 -> "f12" | F13 -> "f13" | F14 -> "f14" | F15 -> "f15"
-      | F16 -> "f16" | F17 -> "f17" | F18 -> "f18" | F19 -> "f19"
-      | F20 -> "f20" | F21 -> "f21" | F22 -> "f22" | F23 -> "f23"
-      | F24 -> "f24" | F25 -> "f25" | F26 -> "f26" | F27 -> "f27"
-      | F28 -> "f28" | F29 -> "f29" | F30 -> "f30" | F31 -> "f31"
-
-    let float_reg_abi_name = function
-      | F0  -> "ft0" | F1  -> "ft1" | F2  -> "ft2" | F3  -> "ft3"
-      | F4  -> "ft4" | F5  -> "ft5" | F6  -> "ft6" | F7  -> "ft7"
-      | F8  -> "fs0" | F9  -> "fs1" | F10 -> "fa0" | F11 -> "fa1"
-      | F12 -> "fa2" | F13 -> "fa3" | F14 -> "fa4" | F15 -> "fa5"
-      | F16 -> "fa6" | F17 -> "fa7" | F18 -> "fs2" | F19 -> "fs3"
-      | F20 -> "fs4" | F21 -> "fs5" | F22 -> "fs6" | F23 -> "fs7"
-      | F24 -> "fs8" | F25 -> "fs9" | F26 ->"fs10" | F27 -> "fs11"
-      | F28 -> "ft3" | F29 -> "ft4" | F30 -> "ft5" | F31 -> "ft6"
-
-    let int_reg_name   = if use_abi_name then int_reg_abi_name   else int_reg_num_name
-    let float_reg_name = if use_abi_name then float_reg_abi_name else float_reg_num_name
+    let int_reg_name = function
+      | GPR0  -> "$r0"  | GPR1  -> "$r1"  | GPR2  -> "$r2"  | GPR3  -> "$r3"
+      | GPR4  -> "$r4"  | GPR5  -> "$r5"  | GPR6  -> "$r6"  | GPR7  -> "$r7"
+      | GPR8  -> "$r8"  | GPR9  -> "$r9"  | GPR10 -> "$r10" | GPR11 -> "$r11"
+      | GPR12 -> "$r12" | GPR13 -> "$r13" | GPR14 -> "$r14" | GPR15 -> "$r15"
+      | GPR16 -> "$r16" | GPR17 -> "$r17" | GPR18 -> "$r18" | GPR19 -> "$r19"
+      | GPR20 -> "$r20" | GPR21 -> "$r21" | GPR22 -> "$r22" | GPR23 -> "$r23"
+      | GPR24 -> "$r24" | GPR25 -> "$r25" | GPR26 -> "$r26" | GPR27 -> "$r27"
+      | GPR28 -> "$r28" | GPR29 -> "$r29" | GPR30 -> "$r30" | GPR31 -> "$r31"
+      | GPR32 -> "$r32" | GPR33 -> "$r33" | GPR34 -> "$r34" | GPR35 -> "$r35"
+      | GPR36 -> "$r36" | GPR37 -> "$r37" | GPR38 -> "$r38" | GPR39 -> "$r39"
+      | GPR40 -> "$r40" | GPR41 -> "$r41" | GPR42 -> "$r42" | GPR43 -> "$r43"
+      | GPR44 -> "$r44" | GPR45 -> "$r45" | GPR46 -> "$r46" | GPR47 -> "$r47"
+      | GPR48 -> "$r48" | GPR49 -> "$r49" | GPR50 -> "$r50" | GPR51 -> "$r51"
+      | GPR52 -> "$r52" | GPR53 -> "$r53" | GPR54 -> "$r54" | GPR55 -> "$r55"
+      | GPR56 -> "$r56" | GPR57 -> "$r57" | GPR58 -> "$r58" | GPR59 -> "$r59"
+      | GPR60 -> "$r60" | GPR61 -> "$r61" | GPR62 -> "$r62" | GPR63 -> "$r63"
 
     let ireg oc r = output_string oc (int_reg_name r)
-    let freg oc r = output_string oc (float_reg_name r)
 
+    let ireg0 = ireg
+(*
     let ireg0 oc = function
-      | X0 -> output_string oc "x0"
-      | X r -> ireg oc r
-
+      | GPR r -> ireg oc r
+*)
     let preg oc = function
       | IR r -> ireg oc r
-      | FR r -> freg oc r
+      | FR r -> ireg oc r
+      | RA   -> output_string oc "$ra"
       | _    -> assert false
 
     let preg_annot = function
       | IR r -> int_reg_name r
-      | FR r -> float_reg_name r
+      | FR r -> int_reg_name r
+      | RA   -> "$ra"
       | _ -> assert false
 
 (* Names of sections *)
@@ -152,7 +127,7 @@ module Target : TARGET =
 
 (* Generate code to load the address of id + ofs in register r *)
 
-    let loadsymbol oc r id ofs =
+  (*let loadsymbol oc r id ofs =
       if Archi.pic_code () then begin
         assert (ofs = Integers.Ptrofs.zero);
         fprintf oc "	la	%a, %s\n" ireg r (extern_atom id)
@@ -162,7 +137,7 @@ module Target : TARGET =
         fprintf oc "	addi	%a, %a, %%lo(%a)\n"
                                 ireg r ireg r symbol_offset (id, ofs)
       end
-
+  *)
 (* Emit .file / .loc debugging directives *)
 
     let print_file_line oc file line =
@@ -175,9 +150,9 @@ module Target : TARGET =
 
 (* Add "w" suffix to 32-bit instructions if we are in 64-bit mode *)
   
-    let w oc =
+  (*let w oc =
       if Archi.ptr64 then output_string oc "w"
-
+  *)
 (* Offset part of a load or store *)
 
     let offset oc = function
@@ -186,11 +161,17 @@ module Target : TARGET =
 
 (* Printing of instructions *)
     let print_instruction oc = function
+      | Pret ->
+         fprintf oc "	ret\n;;\n"
+      | Pget (rd, rs) ->
+         fprintf oc "	get	%a = %a\n;;\n" ireg rd preg rs
+      | Pset (rd, rs) ->
+         fprintf oc "	set	%a = %a\n;;\n" preg rd ireg rs
       | Pmv(rd, rs) ->
-         fprintf oc "	mv	%a, %a\n"     ireg rd ireg rs
+         fprintf oc "	addd	%a = %a, 0\n;;\n"     ireg rd ireg rs
 
       (* 32-bit integer register-immediate instructions *)
-      | Paddiw (rd, rs, imm) ->
+    (*| Paddiw (rd, rs, imm) ->
          fprintf oc "	addi%t	%a, %a, %a\n" w ireg rd ireg0 rs coqint imm
       | Psltiw (rd, rs, imm) ->
          fprintf oc "	slti	%a, %a, %a\n" ireg rd ireg0 rs coqint imm
@@ -251,10 +232,10 @@ module Target : TARGET =
       | Psraw(rd, rs1, rs2) ->
          fprintf oc "	sra%t	%a, %a, %a\n" w ireg rd ireg0 rs1 ireg0 rs2
 
-      (* 64-bit integer register-immediate instructions *)
+    *)(* 64-bit integer register-immediate instructions *)
       | Paddil (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	addi	%a, %a, %a\n" ireg rd ireg0 rs coqint64 imm
-      | Psltil (rd, rs, imm) -> assert Archi.ptr64;
+         fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg0 rs coqint64 imm
+    (*| Psltil (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	slti	%a, %a, %a\n" ireg rd ireg0 rs coqint64 imm
       | Psltiul (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	sltiu	%a, %a, %a\n" ireg rd ireg0 rs coqint64 imm
@@ -272,11 +253,15 @@ module Target : TARGET =
          fprintf oc "	srai	%a, %a, %a\n" ireg rd ireg0 rs coqint64 imm
       | Pluil (rd, imm) -> assert Archi.ptr64;
          fprintf oc "	lui	%a, %a\n"     ireg rd coqint64 imm
-
+    *)
+      | Pmake (rd, imm) ->
+         fprintf oc "	make	%a, %a\n;;\n" ireg rd coqint imm
+      | Pmakel (rd, imm) ->
+         fprintf oc "	make	%a, %a\n;;\n" ireg rd coqint64 imm
       (* 64-bit integer register-register instructions *)
       | Paddl(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	add	%a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2
-      | Psubl(rd, rs1, rs2) -> assert Archi.ptr64;
+         fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg0 rs1 ireg0 rs2
+    (*| Psubl(rd, rs1, rs2) -> assert Archi.ptr64;
          fprintf oc "	sub	%a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2
 
       | Pmull(rd, rs1, rs2) -> assert Archi.ptr64;
@@ -366,21 +351,21 @@ module Target : TARGET =
          fprintf oc "	lhu	%a, %a(%a)\n" ireg rd offset ofs ireg ra
       | Plw(rd, ra, ofs) | Plw_a(rd, ra, ofs) ->
          fprintf oc "	lw	%a, %a(%a)\n" ireg rd offset ofs ireg ra
-      | Pld(rd, ra, ofs) | Pld_a(rd, ra, ofs) -> assert Archi.ptr64;
-         fprintf oc "	ld	%a, %a(%a)\n" ireg rd offset ofs ireg ra
+    *)| Pld(rd, ra, ofs) (*| Pld_a(rd, ra, ofs)*) -> assert Archi.ptr64;
+         fprintf oc "	ld	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
 
-      | Psb(rd, ra, ofs) ->
+    (*| Psb(rd, ra, ofs) ->
          fprintf oc "	sb	%a, %a(%a)\n" ireg rd offset ofs ireg ra
       | Psh(rd, ra, ofs) ->
          fprintf oc "	sh	%a, %a(%a)\n" ireg rd offset ofs ireg ra
       | Psw(rd, ra, ofs) | Psw_a(rd, ra, ofs) ->
          fprintf oc "	sw	%a, %a(%a)\n" ireg rd offset ofs ireg ra
-      | Psd(rd, ra, ofs) | Psd_a(rd, ra, ofs) -> assert Archi.ptr64;
-         fprintf oc "	sd	%a, %a(%a)\n" ireg rd offset ofs ireg ra
+    *)| Psd(rd, ra, ofs) (*| Psd_a(rd, ra, ofs)*) -> assert Archi.ptr64;
+         fprintf oc "	sd	%a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
 
 
       (* Synchronization *)
-      | Pfence ->
+    (*| Pfence ->
          fprintf oc "	fence\n"
 
       (* floating point register move.
@@ -522,17 +507,17 @@ module Target : TARGET =
          fprintf oc "	fcvt.s.d	%a, %a\n" freg fd freg fs
 
       (* Pseudo-instructions expanded in Asmexpand *)
-      | Pallocframe(sz, ofs) ->
+    *)| Pallocframe(sz, ofs) ->
          assert false
       | Pfreeframe(sz, ofs) ->
          assert false
-      | Pseqw _ | Psnew _ | Pseql _ | Psnel _ | Pcvtl2w _ | Pcvtw2l _ ->
+    (*| Pseqw _ | Psnew _ | Pseql _ | Psnel _ | Pcvtl2w _ | Pcvtw2l _ ->
          assert false
 
       (* Pseudo-instructions that remain *)
-      | Plabel lbl ->
+    *)| Plabel lbl ->
          fprintf oc "%a:\n" print_label lbl
-      | Ploadsymbol(rd, id, ofs) ->
+    (*| Ploadsymbol(rd, id, ofs) ->
          loadsymbol oc rd id ofs
       | Ploadsymbol_high(rd, id, ofs) ->
          fprintf oc "	lui	%a, %%hi(%a)\n" ireg rd symbol_offset (id, ofs)
@@ -563,7 +548,7 @@ module Target : TARGET =
          fprintf oc "	jr	x5\n";
          jumptables := (lbl, tbl) :: !jumptables;
          fprintf oc "%s end pseudoinstr btbl\n" comment
-      | Pbuiltin(ef, args, res) ->
+    *)| Pbuiltin(ef, args, res) ->
          begin match ef with
            | EF_annot(kind,txt, targs) ->
              let annot =
@@ -635,7 +620,7 @@ module Target : TARGET =
     let address = if Archi.ptr64 then ".quad" else ".long"
 
     let print_prologue oc =
-      fprintf oc "	.option %s\n" (if Archi.pic_code() then "pic" else "nopic");
+      (* fprintf oc "	.option %s\n" (if Archi.pic_code() then "pic" else "nopic"); *)
       if !Clflags.option_g then begin
         section oc Section_text;
       end