MPPA - refactored instructions

8 files changed, 556 insertions, 507 deletions

diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index 07e33efa..23fef3f2 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -39,7 +39,7 @@ let new_label () =
         List.fold_left
           (fun next instr ->
             match instr with
-            | Plabel l -> if P.lt l next then next else P.succ l
+            | PExpand (Plabel l) -> if P.lt l next then next else P.succ l
             | _ -> next)
           P.one (!current_function).fn_code
   in
@@ -100,17 +100,17 @@ let expand_debug id sp preg simple l =
   let get_lbl = function
     | None ->
         let lbl = new_label () in
-        emit (Plabel lbl);
+        emit (PExpand (Plabel lbl));
         lbl
     | Some lbl -> lbl in
   let rec  aux lbl scopes = function
     | [] -> ()
-    | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest ->
+    | (PExpand (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i))::rest ->
         let kind = (P.to_int kind) in
         begin
           match kind with
           | 1->
-              emit i;aux lbl scopes rest
+              emit (PExpand i);aux lbl scopes rest
           | 2 ->
               aux  lbl scopes rest
           | 3 ->
@@ -142,11 +142,11 @@ let expand_debug id sp preg simple l =
           | _ ->
               aux None scopes rest
         end
-    | (Plabel lbl)::rest -> simple (Plabel lbl); aux (Some lbl) scopes rest
+    | (PExpand (Plabel lbl))::rest -> simple (PExpand (Plabel lbl)); aux (Some lbl) scopes rest
     | i::rest -> simple i; aux None scopes rest in
   (* We need to move all closing debug annotations before the last real statement *)
   let rec move_debug acc bcc = function
-    | (Pbuiltin(EF_debug (kind,_,_),_,_) as i)::rest ->
+    | (PExpand (Pbuiltin(EF_debug (kind,_,_),_,_)) as i)::rest ->
         let kind = (P.to_int kind) in
         if kind = 1 then
           move_debug acc (i::bcc) rest (* Do not move debug line *)
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index b1b7453a..8dfa8828 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -739,7 +739,7 @@ Lemma tail_nolabel_cons:
 Proof.
   intros. destruct H0. split.
   constructor; auto.
-  intros. simpl. rewrite <- H1. destruct i; reflexivity || contradiction.
+  intros. simpl. rewrite <- H1. destruct i; destruct i; reflexivity || contradiction.
 Qed.
 
 Hint Resolve tail_nolabel_refl: labels.
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 2df185a6..008e6c67 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -152,12 +152,101 @@ Definition label := positive.
   representable range.  Of course, our K1c generator (file
   [Asmgen]) is careful to respect this range. *)
 
-Inductive instruction : Type :=
-(** Get/Set System Registers *)
+(** Instructions to be expanded *)
+Inductive ex_instruction : Type :=
+  (* Pseudo-instructions *)
+  | Pallocframe (sz: Z) (pos: ptrofs)               (**r allocate new stack frame *)
+  | Pfreeframe  (sz: Z) (pos: ptrofs)               (**r deallocate stack frame and restore previous frame *)
+  | Plabel  (lbl: label)                            (**r define a code label *)
+  | Ploadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the address of a symbol *)
+(*| Ploadsymbol_high (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the high part of the address of a symbol *)
+  | Ploadli (rd: ireg) (i: int64)                   (**r load an immediate int64 *)
+  | Ploadfi (rd: freg) (f: float)                   (**r load an immediate float *)
+  | Ploadsi (rd: freg) (f: float32)                 (**r load an immediate single *)
+  | Pbtbl   (r: ireg)  (tbl: list label)            (**r N-way branch through a jump table *) *)
+  | Pbuiltin: external_function -> list (builtin_arg preg)
+              -> builtin_res preg -> ex_instruction   (**r built-in function (pseudo) *)
+.
+
+(** The pseudo-instructions are the following:
+
+- [Plabel]: define a code label at the current program point.
+
+- [Ploadsymbol]: load the address of a symbol in an integer register.
+  Expands to the [la] assembler pseudo-instruction, which does the right
+  thing even if we are in PIC mode.
+
+- [Ploadli rd ival]: load an immediate 64-bit integer into an integer
+  register rd.  Expands to a load from an address in the constant data section,
+  using the integer register x31 as temporary:
+<<
+        lui x31, %hi(lbl)
+        ld rd, %lo(lbl)(x31)
+lbl:
+        .quad ival
+>>
+
+- [Ploadfi rd fval]: similar to [Ploadli] but loads a double FP constant fval
+  into a float register rd.
+
+- [Ploadsi rd fval]: similar to [Ploadli] but loads a singe FP constant fval
+  into a float register rd.
+
+- [Pallocframe sz pos]: in the formal semantics, this
+  pseudo-instruction allocates a memory block with bounds [0] and
+  [sz], stores the value of the stack pointer at offset [pos] in this
+  block, and sets the stack pointer to the address of the bottom of
+  this block.
+  In the printed ASM assembly code, this allocation is:
+<<
+        mv      x30, sp
+        sub     sp,  sp, #sz
+        sw      x30, #pos(sp)
+>>
+  This cannot be expressed in our memory model, which does not reflect
+  the fact that stack frames are adjacent and allocated/freed
+  following a stack discipline.
+
+- [Pfreeframe sz pos]: in the formal semantics, this pseudo-instruction
+  reads the word at [pos] of the block pointed by the stack pointer,
+  frees this block, and sets the stack pointer to the value read.
+  In the printed ASM assembly code, this freeing is just an increment of [sp]:
+<<
+        add     sp,  sp, #sz
+>>
+  Again, our memory model cannot comprehend that this operation
+  frees (logically) the current stack frame.
+
+- [Pbtbl reg table]: this is a N-way branch, implemented via a jump table
+  as follows:
+<<
+        la      x31, table
+        add     x31, x31, reg
+        jr      x31
+table:  .long   table[0], table[1], ...
+>>
+  Note that [reg] contains 4 times the index of the desired table entry.
+
+- [Pseq rd rs1 rs2]: since unsigned comparisons have particular
+  semantics for pointers, we cannot encode equality directly using
+  xor/sub etc, which have only integer semantics.
+<<
+        xor     rd, rs1, rs2
+        sltiu   rd, rd, 1
+>>
+  The [xor] is omitted if one of [rs1] and [rs2] is [x0].
+
+- [Psne rd rs1 rs2]: similarly for unsigned inequality.
+<<
+        xor     rd, rs1, rs2
+        sltu    rd, x0, rd
+>>
+*)
+
+(** Control Flow instructions *)
+Inductive cf_instruction : Type :=
   | Pget    (rd: ireg) (rs: preg)                   (**r get system register *)
   | Pset    (rd: preg) (rs: ireg)                   (**r set system register *)
-
-(** Branch Control Unit instructions *)
   | Pret                                            (**r return *)
   | Pcall   (l: label)                              (**r function call *)
   (* Pgoto is for tailcalls, Pj_l is for jumping to a particular label *)
@@ -166,84 +255,123 @@ Inductive instruction : Type :=
   (* Conditional branches *)
   | Pcb     (bt: btest) (r: ireg) (l: label)        (**r branch based on btest *)
   | Pcbu    (bt: btest) (r: ireg) (l: label)        (**r branch based on btest with unsigned semantics *)
+.
 
-(** Integer Comparisons *)
-  | Pcompw  (it: itest) (rd rs1 rs2: ireg)          (**r comparison word *)
-  | Pcompiw (it: itest) (rd rs1: ireg) (imm: int)   (**r comparison imm word *)
-  | Pcompl  (it: itest) (rd rs1 rs2: ireg)          (**r comparison long *)
-  | Pcompil (it: itest) (rd rs1: ireg) (imm: int64) (**r comparison imm long *)
-
-(** Load immediates *)
-  | Pmake   (rd: ireg)            (imm: int)        (**r load immediate *)
-  | Pmakel  (rd: ireg)            (imm: int64)      (**r load immediate long *)
-
-(** Register move *)
-  | Pmv     (rd: ireg) (rs: ireg)                   (**r register move *)
-
-(** 32-bit integer register-immediate instructions *)
-  | Paddiw  (rd: ireg) (rs: ireg) (imm: int)        (**r add imm word *)
-  | Pandiw  (rd: ireg) (rs: ireg) (imm: int)        (**r and imm word *)
-  | Poriw   (rd: ireg) (rs: ireg) (imm: int)        (**r or imm word *)
-  | Pxoriw  (rd: ireg) (rs: ireg) (imm: int)        (**r xor imm word *)
-  | Psraiw  (rd: ireg) (rs: ireg) (imm: int)        (**r shift right arithmetic imm word *)
-  | Psrliw  (rd: ireg) (rs: ireg) (imm: int)        (**r shift right logical imm word *)
-  | Pslliw  (rd: ireg) (rs: ireg) (imm: int)        (**r shift left logical imm word *)
-
-(** 32-bit integer register-register instructions *)
-  | Paddw   (rd: ireg) (rs1 rs2: ireg)              (**r add word *)
-  | Psubw   (rd: ireg) (rs1 rs2: ireg)              (**r sub word *)
-  | Pmulw   (rd: ireg) (rs1 rs2: ireg)              (**r mul word *)
-  | Pandw   (rd: ireg) (rs1 rs2: ireg)              (**r and word *)
-  | Porw    (rd: ireg) (rs1 rs2: ireg)              (**r or word *)
-  | Pxorw   (rd: ireg) (rs1 rs2: ireg)              (**r xor word *)
-  | Pnegw   (rd: ireg) (rs: ireg)                   (**r negate word *)
-  | Psraw   (rd: ireg) (rs1 rs2: ireg)              (**r shift right arithmetic word *)
-  | Psrlw   (rd: ireg) (rs1 rs2: ireg)              (**r shift right logical word *)
-  | Psllw   (rd: ireg) (rs1 rs2: ireg)              (**r shift left logical word *)
-
-(** 64-bit integer register-immediate instructions *)
-  | Paddil  (rd: ireg) (rs: ireg) (imm: int64)      (**r add immediate long *) 
-  | Pandil  (rd: ireg) (rs: ireg) (imm: int64)      (**r and immediate long *) 
-  | Poril   (rd: ireg) (rs: ireg) (imm: int64)      (**r or immediate long *) 
-  | Pxoril  (rd: ireg) (rs: ireg) (imm: int64)      (**r xor immediate long *) 
-  | Psllil  (rd: ireg) (rs: ireg) (imm: int)        (**r shift left logical immediate long *)
-  | Psrlil  (rd: ireg) (rs: ireg) (imm: int)        (**r shift right logical immediate long *)
-  | Psrail  (rd: ireg) (rs: ireg) (imm: int)        (**r shift right arithmetic immediate long *)
-
-(** 64-bit integer register-register instructions *)
-  | Paddl   (rd: ireg) (rs1 rs2: ireg)              (**r add long *)
-  | Psubl   (rd: ireg) (rs1 rs2: ireg)              (**r sub long *)
-  | Pandl   (rd: ireg) (rs1 rs2: ireg)              (**r and long *)
-  | Porl    (rd: ireg) (rs1 rs2: ireg)              (**r or long *)
-  | Pxorl    (rd: ireg) (rs1 rs2: ireg)             (**r xor long *)
-  | Pnegl   (rd: ireg) (rs: ireg)                   (**r negate long *)
-  | Pmull   (rd: ireg) (rs1 rs2: ireg)              (**r mul long (low part) *)
-  | Pslll   (rd: ireg) (rs1 rs2: ireg)              (**r shift left logical long *)
-  | Psrll   (rd: ireg) (rs1 rs2: ireg)              (**r shift right logical long *)
-  | Psral   (rd: ireg) (rs1 rs2: ireg)              (**r shift right arithmetic long *)
-
-(** Conversions *)
-  | Pcvtl2w (rd: ireg) (rs: ireg)                   (**r Convert Long to Word *)
-  | Pcvtw2l (r : ireg)                              (**r Convert Word to Long *)
-  | Pmvw2l  (rd: ireg) (rs: ireg)                   (**r Move Convert Word to Long *)
-
-(** Loads and Stores *)
+(** Loads **)
+Inductive ld_instruction : Type :=
   | Plb     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load byte *)
   | Plbu    (rd: ireg) (ra: ireg) (ofs: offset)     (**r load byte unsigned *)
-  | Plh    (rd: ireg) (ra: ireg) (ofs: offset)      (**r load half word *)
+  | Plh     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load half word *)
   | Plhu    (rd: ireg) (ra: ireg) (ofs: offset)     (**r load half word unsigned *)
   | Plw     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load int32 *)
   | Plw_a   (rd: ireg) (ra: ireg) (ofs: offset)     (**r load any32 *)
   | Pld     (rd: ireg) (ra: ireg) (ofs: offset)     (**r load int64 *)
   | Pld_a   (rd: ireg) (ra: ireg) (ofs: offset)     (**r load any64 *)
-  | Psb    (rd: ireg) (ra: ireg) (ofs: offset)      (**r store byte *)
-  | Psh    (rd: ireg) (ra: ireg) (ofs: offset)      (**r store half byte *)
+  | Pfls    (rd: freg) (ra: ireg) (ofs: offset)     (**r load float *)
+  | Pfld     (rd: freg) (ra: ireg) (ofs: offset)    (**r load 64-bit float *)
+.
+
+(** Stores **)
+Inductive st_instruction : Type :=
+  | Psb     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store byte *)
+  | Psh     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store half byte *)
   | Psw     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int32 *)
   | Psw_a   (rs: ireg) (ra: ireg) (ofs: offset)     (**r store any32 *)
   | Psd     (rs: ireg) (ra: ireg) (ofs: offset)     (**r store int64 *)
   | Psd_a   (rs: ireg) (ra: ireg) (ofs: offset)     (**r store any64 *)
+  | Pfss    (rs: freg) (ra: ireg) (ofs: offset)     (**r store float *)
+  | Pfsd     (rd: freg) (ra: ireg) (ofs: offset)    (**r store 64-bit float *)
+.
+
+(** Arithmetic instructions **)
+Inductive arith_name_r : Type :=
+  | Pcvtw2l                                         (**r Convert Word to Long *)
+.
+
+Inductive arith_name_rr : Type :=
+  | Pmv                                             (**r register move *)
+  | Pnegw                                           (**r negate word *)
+  | Pnegl                                           (**r negate long *)
+  | Pfnegd                                          (**r float negate double *)
+  | Pcvtl2w                                         (**r Convert Long to Word *)
+  | Pmvw2l                                          (**r Move Convert Word to Long *)
+.
+
+Inductive arith_name_ri32 : Type :=
+  | Pmake                                           (**r load immediate *)
+.
+
+Inductive arith_name_ri64 : Type :=
+  | Pmakel                                          (**r load immediate long *)
+.
+
+Inductive arith_name_rrr : Type :=
+  | Pcompw  (it: itest)                             (**r comparison word *)
+  | Pcompl  (it: itest)                             (**r comparison long *)
+
+  | Paddw                                           (**r add word *)
+  | Psubw                                           (**r sub word *)
+  | Pmulw                                           (**r mul word *)
+  | Pandw                                           (**r and word *)
+  | Porw                                            (**r or word *)
+  | Pxorw                                           (**r xor word *)
+  | Psraw                                           (**r shift right arithmetic word *)
+  | Psrlw                                           (**r shift right logical word *)
+  | Psllw                                           (**r shift left logical word *)
+
+  | Paddl                                           (**r add long *)
+  | Psubl                                           (**r sub long *)
+  | Pandl                                           (**r and long *)
+  | Porl                                            (**r or long *)
+  | Pxorl                                           (**r xor long *)
+  | Pmull                                           (**r mul long (low part) *)
+  | Pslll                                           (**r shift left logical long *)
+  | Psrll                                           (**r shift right logical long *)
+  | Psral                                           (**r shift right arithmetic long *)
+.
+
+Inductive arith_name_rri32 : Type :=
+  | Pcompiw (it: itest)                             (**r comparison imm word *)
+
+  | Paddiw                                          (**r add imm word *)
+  | Pandiw                                          (**r and imm word *)
+  | Poriw                                           (**r or imm word *)
+  | Pxoriw                                          (**r xor imm word *)
+  | Psraiw                                          (**r shift right arithmetic imm word *)
+  | Psrliw                                          (**r shift right logical imm word *)
+  | Pslliw                                          (**r shift left logical imm word *)
+
+  | Psllil                                          (**r shift left logical immediate long *)
+  | Psrlil                                          (**r shift right logical immediate long *)
+  | Psrail                                          (**r shift right arithmetic immediate long *)
+.
+
+Inductive arith_name_rri64 : Type :=
+  | Pcompil (it: itest)                             (**r comparison imm long *)
+  | Paddil                                          (**r add immediate long *) 
+  | Pandil                                          (**r and immediate long *) 
+  | Poril                                           (**r or immediate long *) 
+  | Pxoril                                          (**r xor immediate long *) 
+.
+
+Inductive ar_instruction : Type :=
+  | PArithR     (i: arith_name_r)     (rd: ireg)
+  | PArithRR    (i: arith_name_rr)    (rd rs: ireg)
+  | PArithRI32  (i: arith_name_ri32)  (rd: ireg) (imm: int)
+  | PArithRI64  (i: arith_name_ri64)  (rd: ireg) (imm: int64)
+  | PArithRRR   (i: arith_name_rrr)   (rd rs1 rs2: ireg)
+  | PArithRRI32 (i: arith_name_rri32) (rd rs: ireg) (imm: int)
+  | PArithRRI64 (i: arith_name_rri64) (rd rs: ireg) (imm: int64)
+.
+
+Coercion PArithR:       arith_name_r        >-> Funclass.
+Coercion PArithRR:      arith_name_rr       >-> Funclass.
+Coercion PArithRI32:    arith_name_ri32     >-> Funclass.
+Coercion PArithRI64:    arith_name_ri64     >-> Funclass.
+Coercion PArithRRR:     arith_name_rrr      >-> Funclass.
+Coercion PArithRRI32:   arith_name_rri32    >-> Funclass.
+Coercion PArithRRI64:   arith_name_rri64    >-> Funclass.
 
-  (* Synchronization *)
 (*| Pfence                                          (**r fence *)
 
   (* floating point register move *)
@@ -251,9 +379,7 @@ Inductive instruction : Type :=
   | Pfmvxs   (rd: ireg) (rs: freg)                  (**r move FP single to integer register *)
   | Pfmvxd   (rd: ireg) (rs: freg)                  (**r move FP double to integer register *)
 
-  (* 32-bit (single-precision) floating point *)
-*)| Pfls     (rd: freg) (ra: ireg) (ofs: offset)    (**r load float *)
-  | Pfss     (rs: freg) (ra: ireg) (ofs: offset)    (**r store float *)
+*)(* 32-bit (single-precision) floating point *)
 
 (*| Pfnegs   (rd: freg) (rs: freg)                  (**r negation *)
   | Pfabss   (rd: freg) (rs: freg)                  (**r absolute value *)
@@ -286,14 +412,11 @@ Inductive instruction : Type :=
   | Pfcvtsl  (rd: freg) (rs: ireg)                 (**r int64 -> float32 conversion *)
   | Pfcvtslu (rd: freg) (rs: ireg)                 (**r unsigned int 64-> float32 conversion *)
 
-  (* 64-bit (double-precision) floating point *)
-*)| Pfld     (rd: freg) (ra: ireg) (ofs: offset)    (**r load 64-bit float *)
+*)(* 64-bit (double-precision) floating point *)
 (*| Pfld_a   (rd: freg) (ra: ireg) (ofs: offset)    (**r load any64 *)
-*)| Pfsd     (rd: freg) (ra: ireg) (ofs: offset)    (**r store 64-bit float *)
-(*| Pfsd_a   (rd: freg) (ra: ireg) (ofs: offset)    (**r store any64 *)
+  | Pfsd_a   (rd: freg) (ra: ireg) (ofs: offset)    (**r store any64 *)
 
-*)| Pfnegd   (rd: freg) (rs: freg)                  (**r negation *)
-(*| Pfabsd   (rd: freg) (rs: freg)                  (**r absolute value *)
+  | Pfabsd   (rd: freg) (rs: freg)                  (**r absolute value *)
 
   | Pfaddd   (rd: freg) (rs1 rs2: freg)             (**r addition *)
   | Pfsubd   (rd: freg) (rs1 rs2: freg)             (**r subtraction *)
@@ -326,93 +449,20 @@ Inductive instruction : Type :=
   | Pfcvtds  (rd: freg) (rs: freg)                  (**r float32 -> float   *)
   | Pfcvtsd  (rd: freg) (rs: freg)                  (**r float   -> float32 *)
 *)
-  (* Pseudo-instructions *)
-  | Pallocframe (sz: Z) (pos: ptrofs)               (**r allocate new stack frame *)
-  | Pfreeframe  (sz: Z) (pos: ptrofs)               (**r deallocate stack frame and restore previous frame *)
-  | Plabel  (lbl: label)                            (**r define a code label *)
-  | Ploadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the address of a symbol *)
-(*| Ploadsymbol_high (rd: ireg) (id: ident) (ofs: ptrofs) (**r load the high part of the address of a symbol *)
-  | Ploadli (rd: ireg) (i: int64)                   (**r load an immediate int64 *)
-  | Ploadfi (rd: freg) (f: float)                   (**r load an immediate float *)
-  | Ploadsi (rd: freg) (f: float32)                 (**r load an immediate single *)
-  | Pbtbl   (r: ireg)  (tbl: list label)            (**r N-way branch through a jump table *) *)
-  | Pbuiltin: external_function -> list (builtin_arg preg)
-              -> builtin_res preg -> instruction.   (**r built-in function (pseudo) *)
-
-(** The pseudo-instructions are the following:
-
-- [Plabel]: define a code label at the current program point.
-
-- [Ploadsymbol]: load the address of a symbol in an integer register.
-  Expands to the [la] assembler pseudo-instruction, which does the right
-  thing even if we are in PIC mode.
-
-- [Ploadli rd ival]: load an immediate 64-bit integer into an integer
-  register rd.  Expands to a load from an address in the constant data section,
-  using the integer register x31 as temporary:
-<<
-        lui x31, %hi(lbl)
-        ld rd, %lo(lbl)(x31)
-lbl:
-        .quad ival
->>
-
-- [Ploadfi rd fval]: similar to [Ploadli] but loads a double FP constant fval
-  into a float register rd.
-
-- [Ploadsi rd fval]: similar to [Ploadli] but loads a singe FP constant fval
-  into a float register rd.
-
-- [Pallocframe sz pos]: in the formal semantics, this
-  pseudo-instruction allocates a memory block with bounds [0] and
-  [sz], stores the value of the stack pointer at offset [pos] in this
-  block, and sets the stack pointer to the address of the bottom of
-  this block.
-  In the printed ASM assembly code, this allocation is:
-<<
-        mv      x30, sp
-        sub     sp,  sp, #sz
-        sw      x30, #pos(sp)
->>
-  This cannot be expressed in our memory model, which does not reflect
-  the fact that stack frames are adjacent and allocated/freed
-  following a stack discipline.
-
-- [Pfreeframe sz pos]: in the formal semantics, this pseudo-instruction
-  reads the word at [pos] of the block pointed by the stack pointer,
-  frees this block, and sets the stack pointer to the value read.
-  In the printed ASM assembly code, this freeing is just an increment of [sp]:
-<<
-        add     sp,  sp, #sz
->>
-  Again, our memory model cannot comprehend that this operation
-  frees (logically) the current stack frame.
-
-- [Pbtbl reg table]: this is a N-way branch, implemented via a jump table
-  as follows:
-<<
-        la      x31, table
-        add     x31, x31, reg
-        jr      x31
-table:  .long   table[0], table[1], ...
->>
-  Note that [reg] contains 4 times the index of the desired table entry.
 
-- [Pseq rd rs1 rs2]: since unsigned comparisons have particular
-  semantics for pointers, we cannot encode equality directly using
-  xor/sub etc, which have only integer semantics.
-<<
-        xor     rd, rs1, rs2
-        sltiu   rd, rd, 1
->>
-  The [xor] is omitted if one of [rs1] and [rs2] is [x0].
-
-- [Psne rd rs1 rs2]: similarly for unsigned inequality.
-<<
-        xor     rd, rs1, rs2
-        sltu    rd, x0, rd
->>
-*)
+Inductive instruction : Type :=
+  | PExpand         (i: ex_instruction)
+  | PControlFlow    (i: cf_instruction)
+  | PLoad           (i: ld_instruction)
+  | PStore          (i: st_instruction)
+  | PArith          (i: ar_instruction)
+.
+
+Coercion PExpand:       ex_instruction >-> instruction.
+Coercion PControlFlow:  cf_instruction >-> instruction.
+Coercion PLoad:         ld_instruction >-> instruction.
+Coercion PStore:        st_instruction >-> instruction.
+Coercion PArith:        ar_instruction >-> instruction.
 
 Definition code := list instruction.
 Record function : Type := mkfunction { fn_sig: signature; fn_code: code }.
@@ -503,6 +553,7 @@ Lemma is_label_correct:
   if is_label lbl instr then instr = Plabel lbl else instr <> Plabel lbl.
 Proof.
   intros.  destruct instr; simpl; try discriminate.
+  destruct i; simpl; try discriminate.
   case (peq lbl lbl0); intro; congruence.
 Qed.
 
@@ -750,109 +801,81 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       | (None, _) => Stuck
       end
 
-(** Comparisons *)
-  | Pcompw c d s1 s2 => 
-      Next (nextinstr (rs#d <- (compare_int c rs##s1 rs##s2 m))) m
-  | Pcompiw c d s i => 
-      Next (nextinstr (rs#d <- (compare_int c rs##s (Vint i) m))) m
-  | Pcompl c d s1 s2 => 
-      Next (nextinstr (rs#d <- (compare_long c rs###s1 rs###s2 m))) m
-  | Pcompil c d s i => 
-      Next (nextinstr (rs#d <- (compare_long c rs###s (Vlong i) m))) m
-
-(** Load immediates *)
-  | Pmakel d i =>
-      Next (nextinstr (rs#d <- (Vlong i))) m
-  | Pmake d i =>
-      Next (nextinstr (rs#d <- (Vint i))) m
-
-(** Register move *)
-  | Pmv d s =>
-      Next (nextinstr (rs#d <- (rs#s))) m
+(** Arithmetic Instructions *)
+  | PArithR n d =>
+      match n with
+      | Pcvtw2l => Next (nextinstr (rs#d <- (Val.longofint rs#d))) m
+      end
+  
+  | PArithRR n d s =>
+      match n with
+      | Pmv => Next (nextinstr (rs#d <- (rs#s))) m
+      | Pnegw => Next (nextinstr (rs#d <- (Val.neg rs###s))) m
+      | Pnegl => Next (nextinstr (rs#d <- (Val.negl rs###s))) m
+      | Pfnegd => Next (nextinstr (rs#d <- (Val.negf rs#s))) m
+      | Pcvtl2w => Next (nextinstr (rs#d <- (Val.loword rs###s))) m
+      | Pmvw2l => Next (nextinstr (rs#d <- (Val.longofint rs#s))) m
+      end
+
+  | PArithRI32 n d i =>
+      match n with
+      | Pmake => Next (nextinstr (rs#d <- (Vint i))) m
+      end
+
+  | PArithRI64 n d i =>
+      match n with
+      | Pmakel => Next (nextinstr (rs#d <- (Vlong i))) m
+      end
 
-(** 32-bit integer register-immediate instructions *)
-  | Paddiw d s i =>
-      Next (nextinstr (rs#d <- (Val.add rs##s (Vint i)))) m
-  | Pandiw d s i =>
-      Next (nextinstr (rs#d <- (Val.and rs##s (Vint i)))) m
-  | Poriw  d s i =>
-      Next (nextinstr (rs#d <- (Val.or  rs##s (Vint i)))) m
-  | Pxoriw  d s i =>
-      Next (nextinstr (rs#d <- (Val.xor  rs##s (Vint i)))) m
-  | Psraiw d s i =>
-      Next (nextinstr (rs#d <- (Val.shr rs##s (Vint i)))) m
-  | Psrliw d s i =>
-      Next (nextinstr (rs#d <- (Val.shru rs##s (Vint i)))) m
-  | Pslliw d s i =>
-      Next (nextinstr (rs#d <- (Val.shl rs##s (Vint i)))) m
-
-(** 32-bit integer register-register instructions *)
-  | Paddw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.add rs##s1 rs##s2))) m
-  | Psubw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.sub rs##s1 rs##s2))) m
-  | Pmulw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.mul rs##s1 rs##s2))) m
-  | Pandw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.and rs##s1 rs##s2))) m
-  | Porw  d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.or  rs##s1 rs##s2))) m
-  | Pxorw  d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.xor rs##s1 rs##s2))) m
-  | Pnegw d s =>
-      Next (nextinstr (rs#d <- (Val.neg rs###s))) m
-  | Psrlw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.shru rs##s1 rs##s2))) m
-  | Psraw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.shr rs##s1 rs##s2))) m
-  | Psllw d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.shl rs##s1 rs##s2))) m
-
-(** 64-bit integer register-immediate instructions *)
-  | Paddil d s i =>
-      Next (nextinstr (rs#d <- (Val.addl rs###s (Vlong i)))) m
-  | Pandil d s i =>
-      Next (nextinstr (rs#d <- (Val.andl rs###s (Vlong i)))) m
-  | Poril  d s i =>
-      Next (nextinstr (rs#d <- (Val.orl  rs###s (Vlong i)))) m
-  | Pxoril  d s i =>
-      Next (nextinstr (rs#d <- (Val.xorl  rs###s (Vlong i)))) m
-  | Psllil  d s i =>
-      Next (nextinstr (rs#d <- (Val.shll  rs###s (Vint i)))) m
-  | Psrlil  d s i =>
-      Next (nextinstr (rs#d <- (Val.shrlu  rs###s (Vint i)))) m
-  | Psrail d s i =>
-      Next (nextinstr (rs#d <- (Val.shrl rs###s (Vint i)))) m
-
-(** 64-bit integer register-register instructions *)
-  | Paddl d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.addl rs###s1 rs###s2))) m
-  | Psubl d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.subl rs###s1 rs###s2))) m
-  | Pandl d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.andl rs###s1 rs###s2))) m
-  | Porl  d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.orl  rs###s1 rs###s2))) m
-  | Pxorl  d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.xorl  rs###s1 rs###s2))) m
-  | Pnegl d s =>
-      Next (nextinstr (rs#d <- (Val.negl rs###s))) m
-  | Pmull d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.mull rs###s1 rs###s2))) m
-  | Pslll d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.shll rs###s1 rs###s2))) m
-  | Psrll d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.shrlu rs###s1 rs###s2))) m
-  | Psral d s1 s2 =>
-      Next (nextinstr (rs#d <- (Val.shrl rs###s1 rs###s2))) m
-
-(** Conversions *)
-  | Pcvtl2w d s =>
-      Next (nextinstr (rs#d <- (Val.loword rs###s))) m
-  | Pcvtw2l r   =>
-      Next (nextinstr (rs#r <- (Val.longofint rs#r))) m
-  | Pmvw2l d s =>
-      Next (nextinstr (rs#d <- (Val.longofint rs#s))) m
+  | PArithRRR n d s1 s2 =>
+      match n with
+      | Pcompw c => Next (nextinstr (rs#d <- (compare_int c rs##s1 rs##s2 m))) m
+      | Pcompl c => Next (nextinstr (rs#d <- (compare_long c rs###s1 rs###s2 m))) m
+      | Paddw  => Next (nextinstr (rs#d <- (Val.add  rs##s1 rs##s2))) m
+      | Psubw  => Next (nextinstr (rs#d <- (Val.sub  rs##s1 rs##s2))) m
+      | Pmulw  => Next (nextinstr (rs#d <- (Val.mul  rs##s1 rs##s2))) m
+      | Pandw  => Next (nextinstr (rs#d <- (Val.and  rs##s1 rs##s2))) m
+      | Porw   => Next (nextinstr (rs#d <- (Val.or   rs##s1 rs##s2))) m
+      | Pxorw  => Next (nextinstr (rs#d <- (Val.xor  rs##s1 rs##s2))) m
+      | Psrlw  => Next (nextinstr (rs#d <- (Val.shru rs##s1 rs##s2))) m
+      | Psraw  => Next (nextinstr (rs#d <- (Val.shr  rs##s1 rs##s2))) m
+      | Psllw  => Next (nextinstr (rs#d <- (Val.shl  rs##s1 rs##s2))) m
+
+      | Paddl => Next (nextinstr (rs#d <- (Val.addl rs###s1 rs###s2))) m
+      | Psubl => Next (nextinstr (rs#d <- (Val.subl rs###s1 rs###s2))) m
+      | Pandl => Next (nextinstr (rs#d <- (Val.andl rs###s1 rs###s2))) m
+      | Porl  => Next (nextinstr (rs#d <- (Val.orl  rs###s1 rs###s2))) m
+      | Pxorl  => Next (nextinstr (rs#d <- (Val.xorl  rs###s1 rs###s2))) m
+      | Pmull => Next (nextinstr (rs#d <- (Val.mull rs###s1 rs###s2))) m
+      | Pslll => Next (nextinstr (rs#d <- (Val.shll rs###s1 rs###s2))) m
+      | Psrll => Next (nextinstr (rs#d <- (Val.shrlu rs###s1 rs###s2))) m
+      | Psral => Next (nextinstr (rs#d <- (Val.shrl rs###s1 rs###s2))) m
+      end
+
+  | PArithRRI32 n d s i =>
+      match n with
+      | Pcompiw c => Next (nextinstr (rs#d <- (compare_int c rs##s (Vint i) m))) m
+      | Paddiw  => Next (nextinstr (rs#d <- (Val.add   rs##s (Vint i)))) m
+      | Pandiw  => Next (nextinstr (rs#d <- (Val.and   rs##s (Vint i)))) m
+      | Poriw   => Next (nextinstr (rs#d <- (Val.or    rs##s (Vint i)))) m
+      | Pxoriw  => Next (nextinstr (rs#d <- (Val.xor   rs##s (Vint i)))) m
+      | Psraiw  => Next (nextinstr (rs#d <- (Val.shr   rs##s (Vint i)))) m
+      | Psrliw  => Next (nextinstr (rs#d <- (Val.shru  rs##s (Vint i)))) m
+      | Pslliw  => Next (nextinstr (rs#d <- (Val.shl   rs##s (Vint i)))) m
+
+      | Psllil  => Next (nextinstr (rs#d <- (Val.shll  rs###s (Vint i)))) m
+      | Psrlil  => Next (nextinstr (rs#d <- (Val.shrlu rs###s (Vint i)))) m
+      | Psrail  => Next (nextinstr (rs#d <- (Val.shrl  rs###s (Vint i)))) m
+      end
+
+  | PArithRRI64 n d s i =>
+      match n with
+      | Pcompil c => Next (nextinstr (rs#d <- (compare_long c rs###s (Vlong i) m))) m
+      | Paddil  => Next (nextinstr (rs#d <- (Val.addl rs###s (Vlong i)))) m
+      | Pandil  => Next (nextinstr (rs#d <- (Val.andl rs###s (Vlong i)))) m
+      | Poril   => Next (nextinstr (rs#d <- (Val.orl  rs###s (Vlong i)))) m
+      | Pxoril  => Next (nextinstr (rs#d <- (Val.xorl  rs###s (Vlong i)))) m
+      end
 
 (** Loads and stores *)
   | Plb d a ofs =>
@@ -942,9 +965,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
 (*| Pfsd_a s a ofs =>
       exec_store Many64 rs m s a ofs
 
-*)| Pfnegd d s =>
-      Next (nextinstr (rs#d <- (Val.negf rs#s))) m
-(*| Pfabsd d s =>
+  | Pfabsd d s =>
       Next (nextinstr (rs#d <- (Val.absf rs#s))) m
 
   | Pfaddd d s1 s2 =>
@@ -1124,7 +1145,7 @@ Inductive step: state -> trace -> state -> Prop :=
       forall b ofs f ef args res rs m vargs t vres rs' m',
       rs PC = Vptr b ofs ->
       Genv.find_funct_ptr ge b = Some (Internal f) ->
-      find_instr (Ptrofs.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) ->
+      find_instr (Ptrofs.unsigned ofs) f.(fn_code) = Some (A:=instruction) (Pbuiltin ef args res) ->
       eval_builtin_args ge rs (rs SP) m args vargs ->
       external_call ef ge vargs m t vres m' ->
       rs' = nextinstr
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml
index 301e1624..f0a9404c 100644
--- a/mppa_k1c/Asmexpand.ml
+++ b/mppa_k1c/Asmexpand.ml
@@ -493,9 +493,9 @@ let expand_builtin_inline name args res =
 
 let expand_instruction instr =
   match instr with
-  | Pallocframe (sz, ofs) ->
+  | PExpand Pallocframe (sz, ofs) ->
       let sg = get_current_function_sig() in
-      emit (Pmv (GPR10, GPR12));
+      emit (PArith (PArithRR (Pmv, GPR10, 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
@@ -511,7 +511,7 @@ let expand_instruction instr =
         expand_storeind_ptr GPR10 GPR12 ofs;
         vararg_start_ofs := None
       end
-  | Pfreeframe (sz, ofs) ->
+  | PExpand Pfreeframe (sz, ofs) ->
      let sg = get_current_function_sig() in
      let extra_sz =
       if sg.sig_cc.cc_vararg then begin
@@ -548,10 +548,10 @@ let expand_instruction instr =
       end else begin
         emit (Pxorl(rd, rs1, rs2)); emit (Psltul(rd, X0, X rd))
       end
-*)| Pcvtl2w(rd, rs) ->
+*)| PArith PArithRR (Pcvtl2w,rd, rs) ->
       assert Archi.ptr64;
-      emit (Paddiw(rd, rs, Int.zero))  (* 32-bit sign extension *)
-  | Pcvtw2l(r) ->
+      emit (PArith (PArithRRI32 (Paddiw,rd, rs, Int.zero)))  (* 32-bit sign extension *)
+  | PArith PArithR 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 ? *)
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 05dc948e..dbd7b4f5 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -58,6 +58,8 @@ Inductive immed64 : Type :=
 (* For now, let's suppose all instructions of K1c can handle 64-bits immediate *)
 Definition make_immed64 (val: int64) := Imm64_single val.
 
+Notation "a ::i b" := (cons (A:=instruction) a b) (at level 49, right associativity).
+
 (** Smart constructors for arithmetic operations involving
   a 32-bit or 64-bit integer constant.  Depending on whether the
   constant fits in 12 bits or not, one or several instructions
@@ -66,14 +68,14 @@ Definition make_immed64 (val: int64) := Imm64_single val.
 
 Definition loadimm32 (r: ireg) (n: int) (k: code) :=
   match make_immed32 n with
-  | Imm32_single imm => Pmake r imm :: k
+  | Imm32_single imm => Pmake r imm ::i k
   end.
 
-Definition opimm32 (op: ireg -> ireg -> ireg -> instruction)
-                   (opimm: ireg -> ireg -> int -> instruction)
+Definition opimm32 (op: arith_name_rrr)
+                   (opimm: arith_name_rri32)
                    (rd rs: ireg) (n: int) (k: code) :=
   match make_immed32 n with
-  | Imm32_single imm => opimm rd rs imm :: k
+  | Imm32_single imm => opimm rd rs imm ::i k
   end.
 
 Definition addimm32 := opimm32 Paddw Paddiw.
@@ -87,14 +89,14 @@ Definition sltuimm32 := opimm32 Psltuw Psltiuw.
 
 Definition loadimm64 (r: ireg) (n: int64) (k: code) :=
   match make_immed64 n with
-  | Imm64_single imm => Pmakel r imm :: k
+  | Imm64_single imm => Pmakel r imm ::i k
   end.
 
-Definition opimm64 (op: ireg -> ireg -> ireg -> instruction)
-                   (opimm: ireg -> ireg -> int64 -> instruction)
+Definition opimm64 (op: arith_name_rrr)
+                   (opimm: arith_name_rri64)
                    (rd rs: ireg) (n: int64) (k: code) :=
   match make_immed64 n with
-  | Imm64_single imm => opimm rd rs imm :: k
+  | Imm64_single imm => opimm rd rs imm ::i k
 end.
 
 Definition addimm64 := opimm64 Paddl Paddil.
@@ -109,13 +111,13 @@ Definition sltuimm64 := opimm64 Psltul Psltiul.
 
 Definition cast32signed (rd rs: ireg) (k: code) := 
   if (ireg_eq rd rs)
-    then Pcvtw2l rd :: k
-    else Pmvw2l rd rs :: k
+    then Pcvtw2l rd ::i k
+    else Pmvw2l rd rs ::i k
   .
 
 Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   if Ptrofs.eq_dec n Ptrofs.zero then
-    Pmv rd rs :: k
+    Pmv rd rs ::i k
   else
     addimm64 rd rs (Ptrofs.to_int64 n) k.
 
@@ -123,11 +125,11 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
 
 Definition transl_comp
     (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction :=
-  Pcompw (itest_for_cmp c s) RTMP r1 r2 :: Pcb BTwnez RTMP lbl :: k.
+  Pcompw (itest_for_cmp c s) RTMP r1 r2 ::i Pcb BTwnez RTMP lbl ::i k.
 
 Definition transl_compl
     (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction :=
-  Pcompl (itest_for_cmp c s) RTMP r1 r2 :: Pcb BTwnez RTMP lbl :: k.
+  Pcompl (itest_for_cmp c s) RTMP r1 r2 ::i Pcb BTwnez RTMP lbl ::i k.
 
 Definition select_comp (n: int) (c: comparison) : option comparison :=
   if Int.eq n Int.zero then
@@ -143,8 +145,8 @@ Definition select_comp (n: int) (c: comparison) : option comparison :=
 Definition transl_opt_compuimm
     (n: int) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction :=
   match select_comp n c with
-  | Some Ceq => Pcbu BTweqz r1 lbl :: k
-  | Some Cne => Pcbu BTwnez r1 lbl :: k
+  | Some Ceq => Pcbu BTweqz r1 lbl ::i k
+  | Some Cne => Pcbu BTwnez r1 lbl ::i k
   | Some _   => nil (* Never happens *)
   | None     => loadimm32 RTMP n (transl_comp c Unsigned r1 RTMP lbl k)
   end
@@ -164,8 +166,8 @@ Definition select_compl (n: int64) (c: comparison) : option comparison :=
 Definition transl_opt_compluimm
     (n: int64) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction :=
   match select_compl n c with
-  | Some Ceq => Pcbu BTdeqz r1 lbl :: k
-  | Some Cne => Pcbu BTdnez r1 lbl :: k
+  | Some Ceq => Pcbu BTdeqz r1 lbl ::i k
+  | Some Cne => Pcbu BTdnez r1 lbl ::i k
   | Some _   => nil (* Never happens *)
   | None     => loadimm64 RTMP n (transl_compl c Unsigned r1 RTMP lbl k)
   end
@@ -186,7 +188,7 @@ Definition transl_cbranch
   | Ccompimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
       OK (if Int.eq n Int.zero then
-            Pcb (btest_for_cmpswz c) r1 lbl :: k
+            Pcb (btest_for_cmpswz c) r1 lbl ::i k
           else
             loadimm32 RTMP n (transl_comp c Signed r1 RTMP lbl k)
          )
@@ -202,7 +204,7 @@ Definition transl_cbranch
   | Ccomplimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
       OK (if Int64.eq n Int64.zero then
-            Pcb (btest_for_cmpsdz c) r1 lbl :: k
+            Pcb (btest_for_cmpsdz c) r1 lbl ::i k
           else
             loadimm64 RTMP n (transl_compl c Signed r1 RTMP lbl k)
          )
@@ -231,28 +233,28 @@ Definition transl_cbranch
   condition. *)
 
 Definition transl_cond_int32s (cmp: comparison) (rd r1 r2: ireg) (k: code) :=
-  Pcompw (itest_for_cmp cmp Signed) rd r1 r2 :: k.
+  Pcompw (itest_for_cmp cmp Signed) rd r1 r2 ::i k.
 
 Definition transl_cond_int32u (cmp: comparison) (rd r1 r2: ireg) (k: code) :=
-  Pcompw (itest_for_cmp cmp Unsigned) rd r1 r2 :: k.
+  Pcompw (itest_for_cmp cmp Unsigned) rd r1 r2 ::i k.
 
 Definition transl_cond_int64s (cmp: comparison) (rd r1 r2: ireg) (k: code) :=
-  Pcompl (itest_for_cmp cmp Signed) rd r1 r2 :: k.
+  Pcompl (itest_for_cmp cmp Signed) rd r1 r2 ::i k.
 
 Definition transl_cond_int64u (cmp: comparison) (rd r1 r2: ireg) (k: code) :=
-  Pcompl (itest_for_cmp cmp Unsigned) rd r1 r2 :: k.
+  Pcompl (itest_for_cmp cmp Unsigned) rd r1 r2 ::i k.
 
 Definition transl_condimm_int32s (cmp: comparison) (rd r1: ireg) (n: int) (k: code) :=
-  Pcompiw (itest_for_cmp cmp Signed) rd r1 n :: k.
+  Pcompiw (itest_for_cmp cmp Signed) rd r1 n ::i k.
 
 Definition transl_condimm_int32u (cmp: comparison) (rd r1: ireg) (n: int) (k: code) :=
-  Pcompiw (itest_for_cmp cmp Unsigned) rd r1 n :: k.
+  Pcompiw (itest_for_cmp cmp Unsigned) rd r1 n ::i k.
 
 Definition transl_condimm_int64s (cmp: comparison) (rd r1: ireg) (n: int64) (k: code) :=
-  Pcompil (itest_for_cmp cmp Signed) rd r1 n :: k.
+  Pcompil (itest_for_cmp cmp Signed) rd r1 n ::i k.
 
 Definition transl_condimm_int64u (cmp: comparison) (rd r1: ireg) (n: int64) (k: code) :=
-  Pcompil (itest_for_cmp cmp Unsigned) rd r1 n :: k.
+  Pcompil (itest_for_cmp cmp Unsigned) rd r1 n ::i k.
 
 Definition transl_cond_op
            (cond: condition) (rd: ireg) (args: list mreg) (k: code) :=
@@ -309,7 +311,7 @@ Definition transl_op
   match op, args with
   | Omove, a1 :: nil =>
       match preg_of res, preg_of a1 with
-      | IR r, IR a => OK (Pmv r a :: k)
+      | IR r, IR a => OK (Pmv r a ::i k)
       |  _  ,  _   => Error(msg "Asmgen.Omove")
       end
   | Ointconst n, nil =>
@@ -331,33 +333,33 @@ Definition transl_op
 *)| Oaddrsymbol s ofs, nil =>
       do rd <- ireg_of res;
       OK (if Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)
-          then Ploadsymbol rd s Ptrofs.zero :: addptrofs rd rd ofs k
-          else Ploadsymbol rd s ofs :: k)
+          then Ploadsymbol rd s Ptrofs.zero ::i addptrofs rd rd ofs k
+          else Ploadsymbol rd s ofs ::i k)
   | Oaddrstack n, nil =>
       do rd <- ireg_of res;
       OK (addptrofs rd SP n k)
 
   | Ocast8signed, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Pslliw rd rs (Int.repr 24) :: Psraiw rd rd (Int.repr 24) :: k)
+      OK (Pslliw rd rs (Int.repr 24) ::i Psraiw rd rd (Int.repr 24) ::i k)
   | Ocast16signed, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Pslliw rd rs (Int.repr 16) :: Psraiw rd rd (Int.repr 16) :: k)
+      OK (Pslliw rd rs (Int.repr 16) ::i Psraiw rd rd (Int.repr 16) ::i k)
   | Oadd, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Paddw rd rs1 rs2 :: k)
+      OK (Paddw rd rs1 rs2 ::i k)
   | Oaddimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (addimm32 rd rs n k)
   | Oneg, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (Pnegw rd rs :: k)
+      OK (Pnegw rd rs ::i k)
   | Osub, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Psubw rd rs1 rs2 :: k)
+      OK (Psubw rd rs1 rs2 ::i k)
   | Omul, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pmulw rd rs1 rs2 :: k)
+      OK (Pmulw rd rs1 rs2 ::i k)
 (*| Omulhs, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pmulhw rd rs1 rs2 :: k)
@@ -378,52 +380,52 @@ Definition transl_op
       OK (Premuw rd rs1 rs2 :: k)
 *)| Oand, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pandw rd rs1 rs2 :: k)
+      OK (Pandw rd rs1 rs2 ::i k)
   | Oandimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (andimm32 rd rs n k)
   | Oor, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Porw rd rs1 rs2 :: k)
+      OK (Porw rd rs1 rs2 ::i k)
   | Oorimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (orimm32 rd rs n k)
   | Oxor, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pxorw rd rs1 rs2 :: k)
+      OK (Pxorw rd rs1 rs2 ::i k)
   | Oxorimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (xorimm32 rd rs n k)
   | Oshl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Psllw rd rs1 rs2 :: k)
+      OK (Psllw rd rs1 rs2 ::i k)
   | Oshlimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Pslliw rd rs n :: k)
+      OK (Pslliw rd rs n ::i k)
   | Oshr, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Psraw rd rs1 rs2 :: k)
+      OK (Psraw rd rs1 rs2 ::i k)
   | Oshrimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Psraiw rd rs n :: k)
+      OK (Psraiw rd rs n ::i k)
   | Oshru, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Psrlw rd rs1 rs2 :: k)
+      OK (Psrlw rd rs1 rs2 ::i k)
   | Oshruimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Psrliw rd rs n :: k)
+      OK (Psrliw rd rs n ::i k)
   | 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 :: k else
-          Psraiw GPR31 rs (Int.repr 31) ::
-          Psrliw GPR31 GPR31 (Int.sub Int.iwordsize n) ::
-          Paddw GPR31 rs GPR31 ::
-          Psraiw rd GPR31 n :: k)
+      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)
 
   (* [Omakelong], [Ohighlong]  should not occur *)
   | Olowlong, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Pcvtl2w rd rs :: k)  
+      OK (Pcvtl2w rd rs ::i k)  
   | Ocast32signed, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (cast32signed rd rs k)
@@ -433,19 +435,19 @@ Definition transl_op
       OK (Pcvtw2l rd :: Psllil rd rd (Int.repr 32) :: Psrlil rd rd (Int.repr 32) :: k)
 *)| Oaddl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Paddl rd rs1 rs2 :: k)
+      OK (Paddl rd rs1 rs2 ::i k)
   | Oaddlimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (addimm64 rd rs n k)
   | Onegl, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (Pnegl rd rs :: k)
+      OK (Pnegl rd rs ::i k)
   | Osubl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Psubl rd rs1 rs2 :: k)
+      OK (Psubl rd rs1 rs2 ::i k)
   | Omull, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pmull rd rs1 rs2 :: k)
+      OK (Pmull rd rs1 rs2 ::i k)
 (*| Omullhs, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pmulhl rd rs1 rs2 :: k)
@@ -466,40 +468,40 @@ Definition transl_op
       OK (Premul rd rs1 rs2 :: k)
 *)| Oandl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pandl rd rs1 rs2 :: k)
+      OK (Pandl rd rs1 rs2 ::i k)
   | Oandlimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (andimm64 rd rs n k)
   | Oorl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Porl rd rs1 rs2 :: k)
+      OK (Porl rd rs1 rs2 ::i k)
   | Oorlimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (orimm64 rd rs n k)
   | Oxorl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pxorl rd rs1 rs2 :: k)
+      OK (Pxorl rd rs1 rs2 ::i k)
   | Oxorlimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (xorimm64 rd rs n k)
   | Oshll, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pslll rd rs1 rs2 :: k)
+      OK (Pslll rd rs1 rs2 ::i k)
   | Oshllimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Psllil rd rs n :: k)
+      OK (Psllil rd rs n ::i k)
   | Oshrl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Psral rd rs1 rs2 :: k)
+      OK (Psral rd rs1 rs2 ::i k)
   | Oshrlimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Psrail rd rs n :: k)
+      OK (Psrail rd rs n ::i k)
   | Oshrlu, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Psrll rd rs1 rs2 :: k)
+      OK (Psrll rd rs1 rs2 ::i k)
   | Oshrluimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
-      OK (Psrlil rd rs n :: k)
+      OK (Psrlil rd rs n ::i k)
 (*| Oshrxlimm n, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
       OK (if Int.eq n Int.zero then Pmv rd rs :: k else
@@ -510,7 +512,7 @@ Definition transl_op
 
 *)| Onegf, a1 :: nil =>
       do rd <- freg_of res; do rs <- freg_of a1;
-      OK (Pfnegd rd rs :: k)
+      OK (Pfnegd rd rs ::i k)
 (*| Oabsf, a1 :: nil =>
       do rd <- freg_of res; do rs <- freg_of a1;
       OK (Pfabsd rd rs :: k)
@@ -618,7 +620,7 @@ Definition indexed_memory_access
         (base: ireg) (ofs: ptrofs) (k: code) :=
   match make_immed64 (Ptrofs.to_int64 ofs) with
   | Imm64_single imm =>
-      mk_instr base (Ofsimm (Ptrofs.of_int64 imm)) :: k
+      mk_instr base (Ofsimm (Ptrofs.of_int64 imm)) ::i k
 (*| Imm64_pair hi lo =>
       Pluil GPR31 hi :: Paddl GPR31 base GPR31 :: mk_instr GPR31 (Ofsimm (Ptrofs.of_int64 lo)) :: k
   | Imm64_large imm =>
@@ -663,7 +665,7 @@ Definition transl_memory_access
       do rs <- ireg_of a1;
       OK (indexed_memory_access mk_instr rs ofs k)
   | Aglobal id ofs, nil =>
-      OK (Ploadsymbol GPR31 id ofs :: mk_instr GPR31 (Ofsimm Ptrofs.zero) :: k)
+      OK (Ploadsymbol GPR31 id ofs ::i (mk_instr GPR31 (Ofsimm Ptrofs.zero) ::i k))
   | Ainstack ofs, nil =>
       OK (indexed_memory_access mk_instr SP ofs k)
   | _, _ =>
@@ -730,7 +732,7 @@ Definition transl_store (chunk: memory_chunk) (addr: addressing)
 
 Definition make_epilogue (f: Mach.function) (k: code) :=
   loadind_ptr SP f.(fn_retaddr_ofs) GPR8 
-  (Pset RA GPR8 :: Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: k).
+  (Pset RA GPR8 ::i Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::i k).
 
 (** Translation of a Mach instruction. *)
 
@@ -755,23 +757,23 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
 (*| Mcall sig (inl r) =>
       do r1 <- ireg_of r; OK (Pjal_r r1 sig :: k)
 *)| Mcall sig (inr symb) =>
-      OK ((Pcall symb) :: k)
+      OK ((Pcall symb) ::i k)
 (*| Mtailcall sig (inl r) =>
       do r1 <- ireg_of r;
       OK (make_epilogue f (Pcall :: k))
 *)| Mtailcall sig (inr symb) =>
-      OK (make_epilogue f ((Pgoto symb) :: k))
+      OK (make_epilogue f ((Pgoto symb) ::i k))
   | Mbuiltin ef args res =>
-      OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) :: k)
+      OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) ::i k)
   | Mlabel lbl =>
-      OK (Plabel lbl :: k)
+      OK (Plabel lbl ::i k)
   | Mgoto lbl =>
-      OK (Pj_l lbl :: k)
+      OK (Pj_l lbl ::i k)
   | Mcond cond args lbl =>
       transl_cbranch cond args lbl k
 (*| Mjumptable arg tbl => do r <- ireg_of arg; OK (Pbtbl r tbl :: k)
 *)| Mreturn =>
-      OK (make_epilogue f (Pret :: k))
+      OK (make_epilogue f (Pret ::i k))
       (*OK (make_epilogue f (Pj_r RA f.(Mach.fn_sig) :: k))*)
   | _ =>
       Error (msg "Asmgen.transl_instr")
@@ -821,8 +823,8 @@ Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bo
 Definition transl_function (f: Mach.function) :=
   do c <- transl_code' f f.(Mach.fn_code) true;
   OK (mkfunction f.(Mach.fn_sig)
-        (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
-         Pget GPR8 RA ::
+        (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::i
+         Pget GPR8 RA ::i
          storeind_ptr GPR8 SP f.(fn_retaddr_ofs) c)).
 
 Definition transf_function (f: Mach.function) : res Asm.function :=
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 39f832b4..896e9ce9 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -124,7 +124,7 @@ Qed.
 Hint Resolve loadimm32_label: labels.
 
 Remark opimm32_label:
-  forall op opimm r1 r2 n k,
+  forall (op: arith_name_rrr) (opimm: arith_name_rri32) r1 r2 n k,
   (forall r1 r2 r3, nolabel (op r1 r2 r3)) ->
   (forall r1 r2 n, nolabel (opimm r1 r2 n)) ->
   tail_nolabel k (opimm32 op opimm r1 r2 n k).
@@ -150,7 +150,7 @@ Qed.
 Hint Resolve cast32signed_label: labels.
 
 Remark opimm64_label:
-  forall op opimm r1 r2 n k,
+  forall (op: arith_name_rrr) (opimm: arith_name_rri64) r1 r2 n k,
   (forall r1 r2 r3, nolabel (op r1 r2 r3)) ->
   (forall r1 r2 n, nolabel (opimm r1 r2 n)) ->
   tail_nolabel k (opimm64 op opimm r1 r2 n k).
@@ -376,7 +376,7 @@ Qed.
 Lemma transl_instr_label:
   forall f i ep k c,
   transl_instr f i ep k = OK c ->
-  match i with Mlabel lbl => c = Plabel lbl :: k | _ => tail_nolabel k c end.
+  match i with Mlabel lbl => c = Plabel lbl ::i k | _ => tail_nolabel k c end.
 Proof.
   unfold transl_instr; intros; destruct i; TailNoLabel.
 (* loadind *)
@@ -985,8 +985,8 @@ Local Transparent destroyed_by_op.
   intros [m3' [P Q]].
   (* Execution of function prologue *)
   monadInv EQ0. rewrite transl_code'_transl_code in EQ1.
-  set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) ::
-                 Pget GPR8 RA ::
+  set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) ::i
+                 Pget GPR8 RA ::i
                  storeind_ptr GPR8 SP (fn_retaddr_ofs f) x0) in *.
   set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *.
   set (rs2 := nextinstr (rs0#FP <- (parent_sp s) #SP <- sp #GPR31 <- Vundef)).
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index 2234404c..ecb06802 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -213,8 +213,8 @@ Qed.
 *)
 
 Lemma opimm64_correct:
-  forall (op: ireg -> ireg -> ireg -> instruction)
-         (opi: ireg -> ireg -> int64 -> instruction)
+  forall (op: arith_name_rrr)
+         (opi: arith_name_rri64)
          (sem: val -> val -> val) m,
   (forall d s1 s2 rs,
    exec_instr ge fn (op d s1 s2) rs m = Next (nextinstr (rs#d <- (sem rs###s1 rs###s2))) m) ->
@@ -328,7 +328,7 @@ Qed.
 Lemma transl_comp_correct:
   forall cmp r1 r2 lbl k rs m b,
   exists rs',
-     exec_straight ge fn (transl_comp cmp Signed r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl :: k) rs' m
+     exec_straight ge fn (transl_comp cmp Signed r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl ::i k) rs' m
   /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
   /\ ( Val.cmp_bool cmp rs##r1 rs##r2 = Some b ->
        exec_instr ge fn (Pcb BTwnez GPR31 lbl) rs' m = eval_branch fn lbl rs' m (Some b))
@@ -356,7 +356,7 @@ Qed.
 Lemma transl_compu_correct:
   forall cmp r1 r2 lbl k rs m b,
   exists rs',
-     exec_straight ge fn (transl_comp cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl :: k) rs' m
+     exec_straight ge fn (transl_comp cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl ::i k) rs' m
   /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
   /\ ( Val.cmpu_bool (Mem.valid_pointer m) cmp rs##r1 rs##r2 = Some b ->
        exec_instr ge fn (Pcb BTwnez GPR31 lbl) rs' m = eval_branch fn lbl rs' m (Some b))
@@ -383,7 +383,7 @@ Qed.
 Lemma transl_compl_correct:
   forall cmp r1 r2 lbl k rs m b,
   exists rs',
-     exec_straight ge fn (transl_compl cmp Signed r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl :: k) rs' m
+     exec_straight ge fn (transl_compl cmp Signed r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl ::i k) rs' m
   /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
   /\ ( Val.cmpl_bool cmp rs###r1 rs###r2 = Some b ->
        exec_instr ge fn (Pcb BTwnez GPR31 lbl) rs' m = eval_branch fn lbl rs' m (Some b))
@@ -412,7 +412,7 @@ Qed.
 Lemma transl_complu_correct:
   forall cmp r1 r2 lbl k rs m b,
   exists rs',
-     exec_straight ge fn (transl_compl cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl :: k) rs' m
+     exec_straight ge fn (transl_compl cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez GPR31 lbl ::i k) rs' m
   /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
   /\ ( Val.cmplu_bool (Mem.valid_pointer m) cmp rs###r1 rs###r2 = Some b ->
        exec_instr ge fn (Pcb BTwnez GPR31 lbl) rs' m = eval_branch fn lbl rs' m (Some b))
@@ -1347,7 +1347,7 @@ Lemma Pget_correct:
   forall (dst: gpreg) (src: preg) k (rs: regset) m,
   src = RA ->
   exists rs',
-     exec_straight ge fn (Pget dst src :: k) rs m k rs' m
+     exec_straight ge fn (Pget dst src ::i k) rs m k rs' m
   /\ rs'#dst = rs#src
   /\ forall r, r <> PC -> r <> dst -> rs'#r = rs#r.
 Proof.
@@ -1362,7 +1362,7 @@ Lemma Pset_correct:
   forall (dst: preg) (src: gpreg) k (rs: regset) m,
   dst = RA ->
   exists rs',
-     exec_straight ge fn (Pset dst src :: k) rs m k rs' m
+     exec_straight ge fn (Pset dst src ::i k) rs m k rs' m
   /\ rs'#dst = rs#src
   /\ forall r, r <> PC -> r <> dst -> rs'#r = rs#r.
 Proof.
@@ -1546,7 +1546,7 @@ Proof.
   rewrite chunk_of_Tptr in *.
 
   exploit (loadind_ptr_correct SP (fn_retaddr_ofs f) GPR8 (Pset RA GPR8
-           :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: k) rs tm).
+           ::i Pfreeframe (fn_stacksize f) (fn_link_ofs f) ::i k) rs tm).
   - rewrite <- (sp_val _ _ rs AG). simpl. eexact LRA'.
   - congruence.
   - intros (rs1 & A1 & B1 & C1).
@@ -1555,7 +1555,7 @@ Proof.
       apply mkagree; auto.
       rewrite C1; discriminate || auto.
       intro. rewrite C1; auto; destruct r; simpl; try discriminate.
-    + exploit (Pset_correct RA GPR8 (Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: k) rs1 tm). auto.
+    + exploit (Pset_correct RA GPR8 (Pfreeframe (fn_stacksize f) (fn_link_ofs f) ::i k) rs1 tm). auto.
       intros (rs2 & A2 & B2 & C2).
       econstructor; econstructor; split.
       * eapply exec_straight_trans.
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 04dfe9e7..8e3cce5a 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -188,144 +188,12 @@ module Target : TARGET =
     let bcond oc c = fprintf oc "%s" (bcond_name c)
 
 (* Printing of instructions *)
-    let print_instruction oc = function
-      | Pcall(s) ->
-         fprintf oc "	call	%a\n;;\n" symbol s
-      | Pgoto(s) ->
-         fprintf oc "	goto	%a\n;;\n" symbol s
-      | Pj_l(s) ->
-         fprintf oc "	goto	%a\n;;\n" print_label s
-      | 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) | Pmvw2l(rd, rs) ->
-         fprintf oc "	addd	%a = %a, 0\n;;\n"     ireg rd ireg rs
-
-      | Paddiw (rd, rs, imm) ->
-         fprintf oc "	addw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Paddw(rd, rs1, rs2) ->
-         fprintf oc "	addw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Paddil (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Paddl(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-
-      | Psubw(rd, rs1, rs2) ->
-         fprintf oc "	sbfw	%a = %a, %a\n;;\n" ireg rd ireg rs2 ireg rs1
-      | Psubl(rd, rs1, rs2) ->
-         fprintf oc "	sbfd	%a = %a, %a\n;;\n" ireg rd ireg rs2 ireg rs1
-
-      | Pmulw(rd, rs1, rs2) ->
-         fprintf oc "	mulw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Pmull(rd, rs1, rs2) ->
-         fprintf oc "	muld	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-
-      | Psrliw (rd, rs, imm) ->
-         fprintf oc "	srlw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Psrlil (rd, rs, imm) ->
-         fprintf oc "	srld	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Psrll (rd, rs1, rs2) ->
-         fprintf oc "	srld	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Psrlw (rd, rs1, rs2) ->
-         fprintf oc "	srlw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Pslliw (rd, rs, imm) ->
-         fprintf oc "	sllw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Psllw (rd, rs1, rs2) ->
-         fprintf oc "	sllw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Psllil (rd, rs, imm) ->
-         fprintf oc "	slld	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Pslll (rd, rs1, rs2) ->
-         fprintf oc "	slld	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Psraw  (rd, rs1, rs2) ->
-         fprintf oc "	sraw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Psraiw  (rd, rs1, imm) ->
-         fprintf oc "	sraw	%a = %a, %a\n;;\n" ireg rd ireg rs1 coqint64 imm
-      | Psral  (rd, rs1, rs2) ->
-         fprintf oc "	srad	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Psrail  (rd, rs1, imm) ->
-         fprintf oc "	srad	%a = %a, %a\n;;\n" ireg rd ireg rs1 coqint64 imm
-
-      | Poril (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	ord	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Porl(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	ord	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Poriw (rd, rs, imm) -> 
-         fprintf oc "	orw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Porw(rd, rs1, rs2) -> 
-         fprintf oc "	orw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-
-      | Pxoriw (rd, rs, imm) -> 
-         fprintf oc "	xorw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Pxorw(rd, rs1, rs2) -> 
-         fprintf oc "	xorw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Pxoril (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	xord	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Pxorl(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	xord	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-
-      | Pandiw (rd, rs, imm) ->
-         fprintf oc "	andw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Pandw(rd, rs1, rs2) ->
-         fprintf oc "	andw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-      | Pandil (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	andd	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
-      | Pandl(rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	andd	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
-
-      | 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
-
-      | Pnegl(rd, rs) -> assert Archi.ptr64;
-         fprintf oc "	negd	%a = %a\n;;\n" ireg rd ireg rs
-      | Pnegw(rd, rs) ->
-         fprintf oc "	negw	%a = %a\n;;\n" ireg rd ireg rs
-
-      | Pcompw (it, rd, rs1, rs2) ->
-         fprintf oc "	compw.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs1 ireg rs2
-      | Pcompiw (it, rd, rs1, imm) ->
-         fprintf oc "	compw.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs1 coqint64 imm
-      | Pcompl (it, rd, rs1, rs2) ->
-         fprintf oc "	compd.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs1 ireg rs2
-      | Pcompil (it, rd, rs1, imm) ->
-         fprintf oc "	compd.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs1 coqint64 imm
-      | Pcb (bt, r, lbl) | Pcbu (bt, r, lbl) ->
-         fprintf oc "	cb.%a	%a?%a\n;;\n" bcond bt ireg r print_label lbl
-
-      | Plb(rd, ra, ofs) ->
-         fprintf oc "	lbs	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
-      | Plbu(rd, ra, ofs) ->
-         fprintf oc "	lbz	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
-      | Plh(rd, ra, ofs) ->
-         fprintf oc "	lhs	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
-      | Plhu(rd, ra, ofs) ->
-         fprintf oc "	lhz	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
-      | Plw(rd, ra, ofs) | Plw_a(rd, ra, ofs) | Pfls(rd, ra, ofs) ->
-         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
-      | Psb(rd, ra, ofs) ->
-         fprintf oc "	sb	%a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
-      | Psh(rd, ra, ofs) ->
-         fprintf oc "	sh	%a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
-      | Psw(rd, ra, ofs) | Psw_a(rd, ra, ofs) | Pfss(rd, ra, ofs) ->
-         fprintf oc "	sw	%a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
-      | 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
-
-      | Pfnegd(rd, ra) ->
-         fprintf oc "	fnegd	%a = %a\n;;\n" ireg ra ireg rd
-
+    let print_ex_instruction oc = function
       (* Pseudo-instructions expanded in Asmexpand *)
       | Pallocframe(sz, ofs) ->
          assert false
       | Pfreeframe(sz, ofs) ->
          assert false
-      | Pcvtl2w _ | Pcvtw2l _ -> assert false
 
       (* Pseudo-instructions that remain *)
       | Plabel lbl ->
@@ -354,6 +222,164 @@ module Target : TARGET =
               assert false
          end
 
+      let print_cf_instruction oc = function
+      | 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
+      | Pret ->
+         fprintf oc "	ret	\n;;\n"
+      | Pcall(s) ->
+         fprintf oc "	call	%a\n;;\n" symbol s
+      | Pgoto(s) ->
+         fprintf oc "	goto	%a\n;;\n" symbol s
+      | Pj_l(s) ->
+         fprintf oc "	goto	%a\n;;\n" print_label s
+      | 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
+      | Plb(rd, ra, ofs) ->
+         fprintf oc "	lbs	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
+      | Plbu(rd, ra, ofs) ->
+         fprintf oc "	lbz	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
+      | Plh(rd, ra, ofs) ->
+         fprintf oc "	lhs	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
+      | Plhu(rd, ra, ofs) ->
+         fprintf oc "	lhz	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
+      | Plw(rd, ra, ofs) | Plw_a(rd, ra, ofs) | Pfls(rd, ra, ofs) ->
+         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) ->
+         fprintf oc "	sh	%a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
+      | Psw(rd, ra, ofs) | Psw_a(rd, ra, ofs) | Pfss(rd, ra, ofs) ->
+         fprintf oc "	sw	%a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
+      | 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
+
+      let print_ar_rr_instruction oc rd rs = function
+      | Pmv | Pmvw2l ->
+         fprintf oc "	addd	%a = %a, 0\n;;\n"     ireg rd ireg rs
+      | Pcvtl2w -> assert false
+      | Pnegl -> assert Archi.ptr64;
+         fprintf oc "	negd	%a = %a\n;;\n" ireg rd ireg rs
+      | Pnegw ->
+         fprintf oc "	negw	%a = %a\n;;\n" ireg rd ireg rs
+      | Pfnegd ->
+         fprintf oc "	fnegd	%a = %a\n;;\n" ireg rs ireg rd
+
+      let print_ar_ri32_instruction oc rd imm = (* function  
+         | 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) -> *)
+         fprintf oc "	make	%a, %a\n;;\n" ireg rd coqint64 imm
+
+      let print_ar_rrr_instruction oc rd rs1 rs2 = function
+      | Pcompw (it) ->
+         fprintf oc "	compw.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs1 ireg rs2
+      | Pcompl (it) ->
+         fprintf oc "	compd.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs1 ireg rs2
+
+      | Paddw ->
+         fprintf oc "	addw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Psubw ->
+         fprintf oc "	sbfw	%a = %a, %a\n;;\n" ireg rd ireg rs2 ireg rs1
+      | Pmulw ->
+         fprintf oc "	mulw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Pandw ->
+         fprintf oc "	andw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Porw -> 
+         fprintf oc "	orw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Pxorw -> 
+         fprintf oc "	xorw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Psraw ->
+         fprintf oc "	sraw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Psrlw ->
+         fprintf oc "	srlw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Psllw ->
+         fprintf oc "	sllw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+
+      | Paddl -> assert Archi.ptr64;
+         fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Psubl ->
+         fprintf oc "	sbfd	%a = %a, %a\n;;\n" ireg rd ireg rs2 ireg rs1
+      | Pandl -> assert Archi.ptr64;
+         fprintf oc "	andd	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Porl -> assert Archi.ptr64;
+         fprintf oc "	ord	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Pxorl -> assert Archi.ptr64;
+         fprintf oc "	xord	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Pmull ->
+         fprintf oc "	muld	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Pslll  ->
+         fprintf oc "	slld	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Psrll  ->
+         fprintf oc "	srld	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Psral   ->
+         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) ->
+         fprintf oc "	compw.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs coqint64 imm
+      | Paddiw ->
+         fprintf oc "	addw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Pandiw ->
+         fprintf oc "	andw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Poriw -> 
+         fprintf oc "	orw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Pxoriw -> 
+         fprintf oc "	xorw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Psraiw ->
+         fprintf oc "	sraw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Psrliw ->
+         fprintf oc "	srlw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Pslliw ->
+         fprintf oc "	sllw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Psllil ->
+         fprintf oc "	slld	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Psrlil ->
+         fprintf oc "	srld	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Psrail ->
+         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) ->
+         fprintf oc "	compd.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs coqint64 imm
+      | Paddil -> assert Archi.ptr64;
+         fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Pandil -> assert Archi.ptr64;
+         fprintf oc "	andd	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Poril -> assert Archi.ptr64;
+         fprintf oc "	ord	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
+      | Pxoril -> 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