Asmblock & cie - ça compile

5 files changed, 102 insertions, 114 deletions

diff --git a/extraction/extraction.v b/extraction/extraction.v
index 9b124a10..6ab2ce3a 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -167,8 +167,7 @@ Set Extraction AccessOpaque.
 Cd "extraction".
 
 Separate Extraction
-(*   Asmgen.addptrofs *)
-   Asm.dummy_function
+   Asm.dummy_function Asmgen.addptrofs Asmgen.storeind_ptr
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
    Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 5229e364..14824b85 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -30,7 +30,7 @@ Require Import Smallstep.
 Require Import Locations.

 Require Stacklayout.

 Require Import Conventions.

-Require Import Asmblock Asmblockgen.

+Require Import Asmblock.

 Require Import Linking.

 Require Import Errors.

 

@@ -256,11 +256,6 @@ Definition basic_to_instruction (b: basic) :=
 

 Section RELSEM.

 

-(** For OCaml code *)

-Definition addptrofs (rd rs: ireg) (n: ptrofs) := basic_to_instruction (addptrofs rd rs n).

-Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) := 

-  basic_to_instruction (storeind_ptr src base ofs).

-

 Definition code := list instruction.

 

 Fixpoint unfold_label (ll: list label) :=

diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index 20abfc38..81c3cf48 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -20,6 +20,7 @@
    of the RISC-V assembly code. *)
 
 open Asm
+open Asmgen
 open Asmexpandaux
 open AST
 open Camlcoq
@@ -47,9 +48,9 @@ let align n a = (n + a - 1) land (-a)
   List.iter emit (Asmgen.loadimm32 dst n [])
 *)
 let expand_addptrofs dst src n =
-  List.iter emit (Asm.addptrofs dst src n [])
+  List.iter emit (addptrofs dst src n :: [])
 let expand_storeind_ptr src base ofs =
-  List.iter emit (Asm.storeind_ptr src base ofs [])
+  List.iter emit (storeind_ptr src base ofs :: [])
 
 (* Built-ins.  They come in two flavors:
    - annotation statements: take their arguments in registers or stack
@@ -61,7 +62,7 @@ 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   = [| GPR0; GPR1; GPR2; GPR3; GPR4; GPR5; GPR6; GPR7 |]
+let int_param_regs   = let open Asmblock in [| GPR0; GPR1; GPR2; GPR3; GPR4; GPR5; GPR6; GPR7 |]
 (* let float_param_regs = [| F10; F11; F12; F13; F14; F15; F16; F17 |] *)
 let float_param_regs = [| |]
 
@@ -330,7 +331,7 @@ let rec args_size sz = function
 let arguments_size sg =
   args_size 0 sg.sig_args
 
-let save_arguments first_reg base_ofs =
+let save_arguments first_reg base_ofs = let open Asmblock in
   for i = first_reg to 7 do
     expand_storeind_ptr
       int_param_regs.(i)
@@ -412,7 +413,7 @@ let expand_bswap64 d s = assert false
 
 (* Handling of compiler-inlined builtins *)
 
-let expand_builtin_inline name args res =
+let expand_builtin_inline name args res = let open Asmblock in
   match name, args, res with
   (* Synchronization *)
   | "__builtin_membar", [], _ ->
@@ -438,32 +439,32 @@ let expand_builtin_inline name args res =
 
 let expand_instruction instr =
   match instr with
-  | PExpand Pallocframe (sz, ofs) ->
+  | Pallocframe (sz, ofs) ->
       let sg = get_current_function_sig() in
-      emit (PArith (PArithRR (Pmv, GPR10, GPR12)));
+      emit (Pmv (Asmblock.GPR10, Asmblock.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 GPR12 GPR12 (Ptrofs.repr (Z.neg full_sz));
-        expand_storeind_ptr GPR10 GPR12 ofs;
+        expand_addptrofs Asmblock.GPR12 Asmblock.GPR12 (Ptrofs.repr (Z.neg full_sz));
+        expand_storeind_ptr Asmblock.GPR10 Asmblock.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 GPR12 GPR12 (Ptrofs.repr (Z.neg sz));
-        expand_storeind_ptr GPR10 GPR12 ofs;
+        expand_addptrofs Asmblock.GPR12 Asmblock.GPR12 (Ptrofs.repr (Z.neg sz));
+        expand_storeind_ptr Asmblock.GPR10 Asmblock.GPR12 ofs;
         vararg_start_ofs := None
       end
-  | PExpand Pfreeframe (sz, ofs) ->
+  | Pfreeframe (sz, ofs) ->
      let sg = get_current_function_sig() in
      let extra_sz =
       if sg.sig_cc.cc_vararg then begin
         let n = arguments_size sg in
         if n >= 8 then 0 else align 16 ((8 - n) * wordsize)
       end else 0 in
-     expand_addptrofs GPR12 GPR12 (Ptrofs.repr (Z.add sz (Z.of_uint extra_sz)))
+     expand_addptrofs Asmblock.GPR12 Asmblock.GPR12 (Ptrofs.repr (Z.add sz (Z.of_uint extra_sz)))
 
 (*| Pseqw(rd, rs1, rs2) ->
       (* emulate based on the fact that x == 0 iff x <u 1 (unsigned cmp) *)
@@ -493,10 +494,10 @@ let expand_instruction instr =
       end else begin
         emit (Pxorl(rd, rs1, rs2)); emit (Psltul(rd, X0, X rd))
       end
-*)| PArith PArithRR (Pcvtl2w,rd, rs) ->
+*)| Pcvtl2w (rd, rs) ->
       assert Archi.ptr64;
-      emit (PArith (PArithRRI32 (Paddiw,rd, rs, Int.zero)))  (* 32-bit sign extension *)
-  | PArith PArithR r -> (* Pcvtw2l *)
+      emit (Paddiw (rd, rs, Int.zero))  (* 32-bit sign extension *)
+  | Pcvtw2l (r) -> (* Pcvtw2l *)
       assert Archi.ptr64
       (* no-operation because the 32-bit integer was kept sign extended already *)
       (* FIXME - is it really the case on the MPPA ? *)
@@ -532,7 +533,7 @@ let expand_instruction instr =
 
 (* NOTE: Dwarf register maps for RV32G are not yet specified
    officially.  This is just a placeholder.  *)
-let int_reg_to_dwarf = function
+let int_reg_to_dwarf = let open Asmblock in function
    | 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
@@ -547,10 +548,13 @@ let int_reg_to_dwarf = function
    | GPR55 -> 56  | GPR56 -> 57  | GPR57 -> 58  | GPR58 -> 59  | GPR59 -> 60
    | GPR60 -> 61  | GPR61 -> 62  | GPR62 -> 63  | GPR63 -> 64
 
-let preg_to_dwarf = function
+let breg_to_dwarf = let open Asmblock in function
    | IR r -> int_reg_to_dwarf r
    | FR r -> int_reg_to_dwarf r
    | RA   -> 65 (* FIXME - No idea what is $ra DWARF number in k1-gdb *)
+
+let preg_to_dwarf = let open Asmblock in function
+   | BaR r -> breg_to_dwarf r
    | _ -> assert false
 
 let expand_function id fn =
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 15892818..8c3d1e8c 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -15,22 +15,28 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-Require Import Mach Asm Asmblockgen Machblockgen.
+Require Import Integers.
+Require Import Mach Asm Asmblock Asmblockgen Machblockgen.
 Require Import Errors.
 
 Local Open Scope error_monad_scope.
 
+(** For OCaml code *)
+Definition addptrofs (rd rs: ireg) (n: ptrofs) := basic_to_instruction (addptrofs rd rs n).
+Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) := 
+  basic_to_instruction (storeind_ptr src base ofs).
+
 Definition transf_program (p: Mach.program) : res Asm.program :=
   let mbp := Machblockgen.transf_program p in
   do abp <- Asmblockgen.transf_program mbp;
   OK (Asm.transf_program abp).
 
-Definition transf_function (f: Mach.function) : res function :=
+Definition transf_function (f: Mach.function) : res Asm.function :=
   let mbf := Machblockgen.transf_function f in
   do abf <- Asmblockgen.transf_function mbf;
   OK (Asm.transf_function abf).
 
-Definition transl_code (f: Mach.function) (l: Mach.code) : res (list instruction) :=
+Definition transl_code (f: Mach.function) (l: Mach.code) : res (list Asm.instruction) :=
   let mbf := Machblockgen.transf_function f in
   let mbc := Machblockgen.trans_code l in
   do abc <- transl_blocks mbf mbc;
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 41ea06e4..819e11ae 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -40,7 +40,7 @@ module Target : TARGET =
 
     let print_label oc lbl = label oc (transl_label lbl)
 
-    let int_reg_name = function
+    let int_reg_name = let open Asmblock in 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"
@@ -62,16 +62,22 @@ module Target : TARGET =
 
     let ireg = ireg
 
-    let preg oc = function
+    let breg oc = let open Asmblock in function
       | IR r -> ireg oc r
       | FR r -> ireg oc r
       | RA   -> output_string oc "$ra"
-      | _    -> assert false
 
-    let preg_annot = function
+    let breg_annot = let open Asmblock in function
       | IR r -> int_reg_name r
       | FR r -> int_reg_name r
       | RA   -> "$ra"
+
+    let preg oc = let open Asmblock in function
+      | BaR r -> breg oc r
+      | _ -> assert false
+
+    let preg_annot = let open Asmblock in function
+      | BaR r -> breg_annot r
       | _ -> assert false
 
 (* Names of sections *)
@@ -149,11 +155,11 @@ module Target : TARGET =
   *)
 (* Offset part of a load or store *)
 
-    let offset oc = function
+    let offset oc = let open Asmblock in function
     | Ofsimm n -> ptrofs oc n
     | Ofslow(id, ofs) -> fprintf oc "%%lo(%a)" symbol_offset (id, ofs)
 
-    let icond_name = function
+    let icond_name = let open Asmblock in function
       | ITne | ITneu -> "ne"
       | ITeq | ITequ -> "eq"
       | ITlt   -> "lt"
@@ -171,7 +177,7 @@ module Target : TARGET =
 
     let icond oc c = fprintf oc "%s" (icond_name c)
   
-    let bcond_name = function
+    let bcond_name = let open Asmblock in function
       | BTwnez -> "wnez"
       | BTweqz -> "weqz"
       | BTwltz -> "wltz"
@@ -188,7 +194,7 @@ module Target : TARGET =
     let bcond oc c = fprintf oc "%s" (bcond_name c)
 
 (* Printing of instructions *)
-    let print_ex_instruction oc = function
+    let print_instruction oc = function
       (* Pseudo-instructions expanded in Asmexpand *)
       | Pallocframe(sz, ofs) ->
          assert false
@@ -221,14 +227,9 @@ module Target : TARGET =
           | _ ->
               assert false
          end
+      | Pnop -> fprintf oc "	nop\n;;\n"
 
-      (* Pseudo-instructions not generated by Asmgen *)
-      | Pclzll(rd, rs) ->
-         fprintf oc "	clzd	%a = %a\n;;\n" ireg rd ireg rs
-      | Pstsud(rd, rs1, rs2) ->
-         fprintf oc "	stsud	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-
-      let print_cf_instruction oc = function
+      (* Control flow instructions *)
       | Pget (rd, rs) ->
          fprintf oc "	get	%a = %a\n;;\n" ireg rd preg rs
       | Pset (rd, rs) ->
@@ -244,7 +245,7 @@ module Target : TARGET =
       | Pcb (bt, r, lbl) | Pcbu (bt, r, lbl) ->
          fprintf oc "	cb.%a	%a?%a\n;;\n" bcond bt ireg r print_label lbl
 
-      let print_ld_instruction oc = function
+      (* Load/Store instructions *)
       | Plb(rd, ra, ofs) ->
          fprintf oc "	lbs	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
       | Plbu(rd, ra, ofs) ->
@@ -257,8 +258,7 @@ module Target : TARGET =
          fprintf oc "	lws	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
       | Pld(rd, ra, ofs) | Pfld(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
-
-      let print_st_instruction oc = function
+    
       | Psb(rd, ra, ofs) ->
          fprintf oc "	sb	%a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
       | Psh(rd, ra, ofs) ->
@@ -268,124 +268,108 @@ module Target : TARGET =
       | Psd(rd, ra, ofs) | Psd_a(rd, ra, ofs) | Pfsd(rd, ra, ofs) -> assert Archi.ptr64;
          fprintf oc "	sd	%a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
 
-      let print_ar_r_instruction oc rd = (* function
-      | Pcvtw2l ->*) assert false
+      (* Arith R instructions *)
+      | Pcvtw2l(rd) -> assert false
 
-      let print_ar_rr_instruction oc rd rs = function
-      | Pmv | Pmvw2l ->
+      (* Arith RR instructions *)
+      | Pmv(rd, rs) | Pmvw2l(rd, rs) ->
          fprintf oc "	addd	%a = %a, 0\n;;\n"     ireg rd ireg rs
-      | Pcvtl2w -> assert false
-      | Pnegl -> assert Archi.ptr64;
+      | Pcvtl2w(rd, rs) -> assert false
+      | Pnegl(rd, rs) -> assert Archi.ptr64;
          fprintf oc "	negd	%a = %a\n;;\n" ireg rd ireg rs
-      | Pnegw ->
+      | Pnegw(rd, rs) ->
          fprintf oc "	negw	%a = %a\n;;\n" ireg rd ireg rs
-      | Pfnegd ->
+      | Pfnegd(rd, rs) ->
          fprintf oc "	fnegd	%a = %a\n;;\n" ireg rs ireg rd
 
-      let print_ar_ri32_instruction oc rd imm = (* function  
-         | Pmake (rd, imm) -> *)
+      (* Arith RI32 instructions *)
+      | Pmake (rd, imm) ->
          fprintf oc "	make	%a, %a\n;;\n" ireg rd coqint imm
 
-      let print_ar_ri64_instruction oc rd imm = (* function
-         | Pmakel (rd, imm) -> *)
+      (* Arith RI64 instructions *)
+      | Pmakel (rd, imm) ->
          fprintf oc "	make	%a, %a\n;;\n" ireg rd coqint64 imm
 
-      let print_ar_rrr_instruction oc rd rs1 rs2 = function
-      | Pcompw (it) ->
+      (* Arith RRR instructions *)
+      | Pcompw (it, rd, rs1, rs2) ->
          fprintf oc "	compw.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs1 ireg rs2
-      | Pcompl (it) ->
+      | Pcompl (it, rd, rs1, rs2) ->
          fprintf oc "	compd.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs1 ireg rs2
 
-      | Paddw ->
+      | Paddw (rd, rs1, rs2) ->
          fprintf oc "	addw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Psubw ->
+      | Psubw (rd, rs1, rs2) ->
          fprintf oc "	sbfw	%a = %a, %a\n;;\n" ireg rd ireg rs2 ireg rs1
-      | Pmulw ->
+      | Pmulw (rd, rs1, rs2) ->
          fprintf oc "	mulw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Pandw ->
+      | Pandw (rd, rs1, rs2) ->
          fprintf oc "	andw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Porw -> 
+      | Porw (rd, rs1, rs2) -> 
          fprintf oc "	orw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Pxorw -> 
+      | Pxorw (rd, rs1, rs2) -> 
          fprintf oc "	xorw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Psraw ->
+      | Psraw (rd, rs1, rs2) ->
          fprintf oc "	sraw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Psrlw ->
+      | Psrlw (rd, rs1, rs2) ->
          fprintf oc "	srlw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Psllw ->
+      | Psllw (rd, rs1, rs2) ->
          fprintf oc "	sllw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
 
-      | Paddl -> assert Archi.ptr64;
+      | Paddl (rd, rs1, rs2) -> assert Archi.ptr64;
          fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Psubl ->
+      | Psubl (rd, rs1, rs2) ->
          fprintf oc "	sbfd	%a = %a, %a\n;;\n" ireg rd ireg rs2 ireg rs1
-      | Pandl -> assert Archi.ptr64;
+      | Pandl (rd, rs1, rs2) -> assert Archi.ptr64;
          fprintf oc "	andd	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Porl -> assert Archi.ptr64;
+      | Porl (rd, rs1, rs2) -> assert Archi.ptr64;
          fprintf oc "	ord	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Pxorl -> assert Archi.ptr64;
+      | Pxorl (rd, rs1, rs2) -> assert Archi.ptr64;
          fprintf oc "	xord	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Pmull ->
+      | Pmull (rd, rs1, rs2) ->
          fprintf oc "	muld	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Pslll  ->
+      | Pslll  (rd, rs1, rs2) ->
          fprintf oc "	slld	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Psrll  ->
+      | Psrll  (rd, rs1, rs2) ->
          fprintf oc "	srld	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Psral   ->
+      | Psral   (rd, rs1, rs2) ->
          fprintf oc "	srad	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
 
-    let print_ar_rri32_instruction oc rd rs imm = function
-      | Pcompiw (it) ->
+      (* Arith RRI32 instructions *)
+      | Pcompiw (it, rd, rs, imm) ->
          fprintf oc "	compw.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs coqint64 imm
-      | Paddiw ->
+      | Paddiw (rd, rs, imm) ->
          fprintf oc "	addw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Pandiw ->
+      | Pandiw (rd, rs, imm) ->
          fprintf oc "	andw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Poriw -> 
+      | Poriw (rd, rs, imm) -> 
          fprintf oc "	orw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Pxoriw -> 
+      | Pxoriw (rd, rs, imm) -> 
          fprintf oc "	xorw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Psraiw ->
+      | Psraiw (rd, rs, imm) ->
          fprintf oc "	sraw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Psrliw ->
+      | Psrliw (rd, rs, imm) ->
          fprintf oc "	srlw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Pslliw ->
+      | Pslliw (rd, rs, imm) ->
          fprintf oc "	sllw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Psllil ->
+      | Psllil (rd, rs, imm) ->
          fprintf oc "	slld	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Psrlil ->
+      | Psrlil (rd, rs, imm) ->
          fprintf oc "	srld	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Psrail ->
+      | Psrail (rd, rs, imm) ->
          fprintf oc "	srad	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
 
-    let print_ar_rri64_instruction oc rd rs imm = function
-      | Pcompil (it) ->
+    (* Arith RRI64 instructions *)
+      | Pcompil (it, rd, rs, imm) ->
          fprintf oc "	compd.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs coqint64 imm
-      | Paddil -> assert Archi.ptr64;
+      | Paddil (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Pandil -> assert Archi.ptr64;
+      | Pandil (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	andd	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Poril -> assert Archi.ptr64;
+      | Poril (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	ord	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Pxoril -> assert Archi.ptr64;
+      | Pxoril (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	xord	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
 
-    let print_ar_instruction oc = function
-      | PArithR(d) -> print_ar_r_instruction oc d
-      | PArithRR(ins, d, s) -> print_ar_rr_instruction oc d s ins
-      | PArithRI32(d, i) -> print_ar_ri32_instruction oc d i
-      | PArithRI64(d, i) -> print_ar_ri64_instruction oc d i
-      | PArithRRR(ins, d, s1, s2) -> print_ar_rrr_instruction oc d s1 s2 ins
-      | PArithRRI32(ins, d, s, i) -> print_ar_rri32_instruction oc d s i ins
-      | PArithRRI64(ins, d, s, i) -> print_ar_rri64_instruction oc d s i ins
-
-    let print_instruction oc = function
-      | PExpand(i) -> print_ex_instruction oc i
-      | PControlFlow(i) -> print_cf_instruction oc i
-      | PLoad(i) -> print_ld_instruction oc i
-      | PStore(i) -> print_st_instruction oc i
-      | PArith(i) -> print_ar_instruction oc i
-
     let get_section_names name =
       let (text, lit) =
         match C2C.atom_sections name with