new instructions at asm level

5 files changed, 157 insertions, 9 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 1774b102..6a4095da 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -182,7 +182,9 @@ Inductive instruction : Type :=
   | Pfcompl (ft: ftest) (rd rs1 rs2: ireg)          (**r comparison float64 *)

 

   | Paddw               (rd rs1 rs2: ireg)          (**r add word *)

+  | Paddxw (shift : Z)  (rd rs1 rs2: ireg)          (**r add word *)

   | Psubw               (rd rs1 rs2: ireg)          (**r sub word *)

+  | Psubxw (shift : Z)  (rd rs1 rs2: ireg)          (**r add word *)

   | Pmulw               (rd rs1 rs2: ireg)          (**r mul word *)

   | Pandw               (rd rs1 rs2: ireg)          (**r and word *)

   | Pnandw              (rd rs1 rs2: ireg)          (**r nand word *)

@@ -197,9 +199,12 @@ Inductive instruction : Type :=
   | Psrlw               (rd rs1 rs2: ireg)          (**r shift right logical word *)

   | Psllw               (rd rs1 rs2: ireg)          (**r shift left logical word *)

   | Pmaddw              (rd rs1 rs2: ireg)          (**r multiply-add words *)

+  | Pmsubw              (rd rs1 rs2: ireg)          (**r multiply-add words *)

 

   | Paddl               (rd rs1 rs2: ireg)          (**r add long *)

+  | Paddxl (shift : Z)  (rd rs1 rs2: ireg)          (**r add long shift *)

   | Psubl               (rd rs1 rs2: ireg)          (**r sub long *)

+  | Psubxl (shift : Z)  (rd rs1 rs2: ireg)          (**r sub long shift *)

   | Pandl               (rd rs1 rs2: ireg)          (**r and long *)

   | Pnandl              (rd rs1 rs2: ireg)          (**r nand long *)

   | Porl                (rd rs1 rs2: ireg)          (**r or long *)

@@ -214,6 +219,7 @@ Inductive instruction : Type :=
   | Psral               (rd rs1 rs2: ireg)          (**r shift right arithmetic long *)

   | Psrxl               (rd rs1 rs2: ireg)          (**r shift right arithmetic long round to 0*)

   | Pmaddl              (rd rs1 rs2: ireg)          (**r multiply-add long *)

+  | Pmsubl              (rd rs1 rs2: ireg)          (**r multiply-add long *)

 

   | Pfaddd              (rd rs1 rs2: ireg)          (**r Float addition double *)

   | Pfaddw              (rd rs1 rs2: ireg)          (**r Float addition word *)

@@ -226,6 +232,9 @@ Inductive instruction : Type :=
   | Pcompiw (it: itest) (rd rs: ireg) (imm: int)    (**r comparison imm word *)

 

   | Paddiw              (rd rs: ireg) (imm: int)    (**r add imm word *)

+  | Paddxiw (shift : Z) (rd rs: ireg) (imm: int)    (**r add imm word *)

+  | Psubiw              (rd rs: ireg) (imm: int)    (**r subtract imm word *)

+  | Psubxiw (shift : Z) (rd rs: ireg) (imm: int)    (**r subtract imm word *)

   | Pmuliw              (rd rs: ireg) (imm: int)    (**r mul imm word *)

   | Pandiw              (rd rs: ireg) (imm: int)    (**r and imm word *)

   | Pnandiw             (rd rs: ireg) (imm: int)    (**r nand imm word *)

@@ -249,6 +258,9 @@ Inductive instruction : Type :=
   (** Arith RRI64 *)

   | Pcompil (it: itest) (rd rs: ireg) (imm: int64)  (**r comparison imm long *)

   | Paddil              (rd rs: ireg) (imm: int64)  (**r add immediate long *) 

+  | Paddxil (shift : Z) (rd rs: ireg) (imm: int64)  (**r add immediate long *) 

+  | Psubil              (rd rs: ireg) (imm: int64)  (**r subtract imm long *)

+  | Psubxil (shift : Z) (rd rs: ireg) (imm: int64)  (**r subtract imm long *)

   | Pmulil              (rd rs: ireg) (imm: int64)  (**r add immediate long *) 

   | Pandil              (rd rs: ireg) (imm: int64)  (**r and immediate long *) 

   | Pnandil             (rd rs: ireg) (imm: int64)  (**r and immediate long *) 

@@ -338,7 +350,9 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRR (Asmvliw.Pfcompw ft) rd rs1 rs2 => Pfcompw ft rd rs1 rs2

   | PArithRRR (Asmvliw.Pfcompl ft) rd rs1 rs2 => Pfcompl ft rd rs1 rs2

   | PArithRRR Asmvliw.Paddw rd rs1 rs2       => Paddw rd rs1 rs2

+  | PArithRRR (Asmvliw.Paddxw shift) rd rs1 rs2 => Paddxw shift rd rs1 rs2

   | PArithRRR Asmvliw.Psubw rd rs1 rs2       => Psubw rd rs1 rs2

+  | PArithRRR (Asmvliw.Psubxw shift) rd rs1 rs2 => Psubxw shift rd rs1 rs2

   | PArithRRR Asmvliw.Pmulw rd rs1 rs2       => Pmulw rd rs1 rs2

   | PArithRRR Asmvliw.Pandw rd rs1 rs2       => Pandw rd rs1 rs2

   | PArithRRR Asmvliw.Pnandw rd rs1 rs2      => Pnandw rd rs1 rs2

@@ -354,7 +368,9 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRR Asmvliw.Psllw rd rs1 rs2       => Psllw rd rs1 rs2

 

   | PArithRRR Asmvliw.Paddl rd rs1 rs2       => Paddl rd rs1 rs2

+  | PArithRRR (Asmvliw.Paddxl shift) rd rs1 rs2 => Paddxl shift rd rs1 rs2

   | PArithRRR Asmvliw.Psubl rd rs1 rs2       => Psubl rd rs1 rs2

+  | PArithRRR (Asmvliw.Psubxl shift) rd rs1 rs2 => Psubxl shift rd rs1 rs2

   | PArithRRR Asmvliw.Pandl rd rs1 rs2       => Pandl rd rs1 rs2

   | PArithRRR Asmvliw.Pnandl rd rs1 rs2      => Pnandl rd rs1 rs2

   | PArithRRR Asmvliw.Porl rd rs1 rs2        => Porl rd rs1 rs2

@@ -379,6 +395,9 @@ Definition basic_to_instruction (b: basic) :=
   (* RRI32 *)

   | PArithRRI32 (Asmvliw.Pcompiw it) rd rs imm => Pcompiw it rd rs imm

   | PArithRRI32 Asmvliw.Paddiw rd rs imm       => Paddiw rd rs imm

+  | PArithRRI32 (Asmvliw.Paddxiw shift) rd rs imm => Paddxiw shift rd rs imm

+  | PArithRRI32 Asmvliw.Psubiw rd rs imm       => Psubiw rd rs imm

+  | PArithRRI32 (Asmvliw.Psubxiw shift) rd rs imm => Psubxiw shift rd rs imm

   | PArithRRI32 Asmvliw.Pmuliw rd rs imm       => Pmuliw rd rs imm

   | PArithRRI32 Asmvliw.Pandiw rd rs imm       => Pandiw rd rs imm

   | PArithRRI32 Asmvliw.Pnandiw rd rs imm      => Pnandiw rd rs imm

@@ -401,6 +420,9 @@ Definition basic_to_instruction (b: basic) :=
   (* RRI64 *)

   | PArithRRI64 (Asmvliw.Pcompil it) rd rs imm => Pcompil it rd rs imm

   | PArithRRI64 Asmvliw.Paddil rd rs imm       => Paddil rd rs imm

+  | PArithRRI64 (Asmvliw.Paddxil shift) rd rs imm => Paddxil shift rd rs imm

+  | PArithRRI64 Asmvliw.Psubil rd rs imm       => Psubil rd rs imm

+  | PArithRRI64 (Asmvliw.Psubxil shift) rd rs imm => Psubxil shift rd rs imm

   | PArithRRI64 Asmvliw.Pmulil rd rs imm       => Pmulil rd rs imm

   | PArithRRI64 Asmvliw.Pandil rd rs imm       => Pandil rd rs imm

   | PArithRRI64 Asmvliw.Pnandil rd rs imm      => Pnandil rd rs imm

@@ -414,6 +436,8 @@ Definition basic_to_instruction (b: basic) :=
   (** ARRR *)

   | PArithARRR Asmvliw.Pmaddw rd rs1 rs2       => Pmaddw rd rs1 rs2

   | PArithARRR Asmvliw.Pmaddl rd rs1 rs2       => Pmaddl rd rs1 rs2

+  | PArithARRR Asmvliw.Pmsubw rd rs1 rs2       => Pmsubw rd rs1 rs2

+  | PArithARRR Asmvliw.Pmsubl rd rs1 rs2       => Pmsubl rd rs1 rs2

   | PArithARRR (Asmvliw.Pcmove cond) rd rs1 rs2=> Pcmove cond rd rs1 rs2

   | PArithARRR (Asmvliw.Pcmoveu cond) rd rs1 rs2=> Pcmoveu cond rd rs1 rs2

 

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index eb3900d5..82062fab 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1405,12 +1405,14 @@ Definition string_of_name_rf64 (n: arith_name_rf64): pstring :=
 
 Definition string_of_name_rrr (n: arith_name_rrr): pstring :=
   match n with
-    Pcompw _ => "Pcompw"
+  | Pcompw _ => "Pcompw"
   | Pcompl _ => "Pcompl"
   | Pfcompw _ => "Pfcompw"
   | Pfcompl _ => "Pfcompl"
   | Paddw => "Paddw"
+  | Paddxw _ => "Paddxw"
   | Psubw => "Psubw"
+  | Psubxw _ => "Psubxw"
   | Pmulw => "Pmulw"
   | Pandw => "Pandw"
   | Pnandw => "Pnandw"
@@ -1425,7 +1427,9 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring :=
   | Psrxw => "Psrxw"
   | Psllw => "Psllw"
   | Paddl => "Paddl"
+  | Paddxl _ => "Paddxl"
   | Psubl => "Psubl"
+  | Psubxl _ => "Psubxl"
   | Pandl => "Pandl"
   | Pnandl => "Pnandl"
   | Porl => "Porl"
@@ -1451,6 +1455,9 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring :=
   match n with
     Pcompiw _ => "Pcompiw"
   | Paddiw => "Paddiw"
+  | Psubiw => "Psubiw"
+  | Paddxiw _ => "Paddxiw"
+  | Psubxiw _ => "Psubxiw"
   | Pmuliw => "Pmuliw"
   | Pandiw => "Pandiw"
   | Pnandiw => "Pnandiw"
@@ -1475,6 +1482,9 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring :=
   match n with
     Pcompil _ => "Pcompil"
   | Paddil => "Paddil"
+  | Psubil => "Psubil"
+  | Paddxil _ => "Paddxil"
+  | Psubxil _ => "Psubxil"
   | Pmulil => "Pmulil"
   | Pandil => "Pandil"
   | Pnandil => "Pnandil"
@@ -1490,6 +1500,8 @@ Definition string_of_name_arrr (n: arith_name_arrr): pstring :=
   match n with
   | Pmaddw  => "Pmaddw"
   | Pmaddl  => "Pmaddl"
+  | Pmsubw  => "Pmsubw"
+  | Pmsubl  => "Pmsubl"
   | Pcmove _ => "Pcmove"
   | Pcmoveu _ => "Pcmoveu"
   end.
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 3bef1a5c..e8ea4318 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -429,7 +429,9 @@ Inductive arith_name_rrr : Type :=
   | Pfcompl (ft: ftest)                             (**r comparison float64 *)
 
   | Paddw                                           (**r add word *)
-  | Psubw                                           (**r sub word *)
+  | Paddxw (shift : Z)                              (**r add shift *)
+  | Psubw                                           (**r sub word word *)
+  | Psubxw (shift : Z)                              (**r sub shift word *)
   | Pmulw                                           (**r mul word *)
   | Pandw                                           (**r and word *)
   | Pnandw                                          (**r nand word *)
@@ -445,7 +447,9 @@ Inductive arith_name_rrr : Type :=
   | Psllw                                           (**r shift left logical word *)
 
   | Paddl                                           (**r add long *)
+  | Paddxl (shift : Z)                              (**r add shift long *)
   | Psubl                                           (**r sub long *)
+  | Psubxl (shift : Z)                              (**r sub shift long *)
   | Pandl                                           (**r and long *)
   | Pnandl                                          (**r nand long *)
   | Porl                                            (**r or long *)
@@ -472,6 +476,9 @@ Inductive arith_name_rri32 : Type :=
   | Pcompiw (it: itest)                             (**r comparison imm word *)
 
   | Paddiw                                          (**r add imm word *)
+  | Paddxiw (shift : Z)
+  | Psubiw                                          (**r add imm word *)
+  | Psubxiw (shift : Z)
   | Pmuliw                                          (**r add imm word *)
   | Pandiw                                          (**r and imm word *)
   | Pnandiw                                         (**r nand imm word *)
@@ -495,6 +502,9 @@ Inductive arith_name_rri32 : Type :=
 Inductive arith_name_rri64 : Type :=
   | Pcompil (it: itest)                             (**r comparison imm long *)
   | Paddil                                          (**r add immediate long *) 
+  | Paddxil (shift : Z)
+  | Psubil
+  | Psubxil (shift : Z)
   | Pmulil                                          (**r mul immediate long *) 
   | Pandil                                          (**r and immediate long *) 
   | Pnandil                                         (**r nand immediate long *) 
@@ -509,6 +519,8 @@ Inductive arith_name_rri64 : Type :=
 Inductive arith_name_arrr : Type :=
   | Pmaddw                                           (**r multiply add word *)
   | Pmaddl                                           (**r multiply add long *)
+  | Pmsubw                                           (**r multiply subtract word *)
+  | Pmsubl                                           (**r multiply subtract long *)
   | Pcmove (bt: btest)                               (**r conditional move *)
   | Pcmoveu (bt: btest)                              (**r conditional move, test on unsigned semantics *)
 .
@@ -1055,12 +1067,33 @@ Definition arith_eval_rrr n v1 v2 :=
   | Pfsbfw => Val.subfs v1 v2
   | Pfmuld => Val.mulf v1 v2
   | Pfmulw => Val.mulfs v1 v2
+
+  | Paddxw shift =>
+    if Z.leb shift 4 && Z.leb 1 shift
+    then Val.add v1 (Val.shl v2 (Vint (Int.repr shift)))
+    else Vundef
+
+  | Paddxl shift =>
+    if Z.leb shift 4 && Z.leb 1 shift
+    then Val.addl v1 (Val.shll v2 (Vint (Int.repr shift)))
+    else Vundef
+
+  | Psubxw shift =>
+    if Z.leb shift 4 && Z.leb 1 shift
+    then Val.sub v1 (Val.shl v2 (Vint (Int.repr shift)))
+    else Vundef
+
+  | Psubxl shift =>
+    if Z.leb shift 4 && Z.leb 1 shift
+    then Val.subl v1 (Val.shll v2 (Vint (Int.repr shift)))
+    else Vundef
   end.
 
 Definition arith_eval_rri32 n v i :=
   match n with
   | Pcompiw c => compare_int c v (Vint i)
   | Paddiw  => Val.add   v (Vint i)
+  | Psubiw  => Val.sub   v (Vint i)
   | Pmuliw  => Val.mul   v (Vint i)
   | Pandiw  => Val.and   v (Vint i)
   | Pnandiw => Val.notint (Val.and  v (Vint i))
@@ -1079,12 +1112,21 @@ Definition arith_eval_rri32 n v i :=
   | Psrxil  => ExtValues.val_shrxl v (Vint i)
   | Psrlil  => Val.shrlu v (Vint i)
   | Psrail  => Val.shrl  v (Vint i)
+  | Paddxiw shift =>
+        if Z.leb shift 4 && Z.leb 1 shift
+        then Val.add (Vint i) (Val.shl v (Vint (Int.repr shift)))
+        else Vundef
+  | Psubxiw shift =>
+        if Z.leb shift 4 && Z.leb 1 shift
+        then Val.sub (Vint i) (Val.shl v (Vint (Int.repr shift)))
+        else Vundef
   end.
 
 Definition arith_eval_rri64 n v i :=
   match n with
   | Pcompil c => compare_long c v (Vlong i)
   | Paddil  => Val.addl v (Vlong i)
+  | Psubil  => Val.subl v (Vlong i)
   | Pmulil  => Val.mull v (Vlong i)
   | Pandil  => Val.andl v (Vlong i)
   | Pnandil  => Val.notl (Val.andl v (Vlong i))
@@ -1094,12 +1136,22 @@ Definition arith_eval_rri64 n v i :=
   | Pnxoril  => Val.notl (Val.xorl  v (Vlong i))
   | Pandnil => Val.andl (Val.notl v) (Vlong i)
   | Pornil  => Val.orl (Val.notl v) (Vlong i)
+  | Paddxil shift =>
+    if Z.leb shift 4 && Z.leb 1 shift
+    then Val.addl (Vlong i) (Val.shll v (Vint (Int.repr shift)))
+    else Vundef
+  | Psubxil shift =>
+    if Z.leb shift 4 && Z.leb 1 shift
+    then Val.subl (Vlong i) (Val.shll v (Vint (Int.repr shift)))
+    else Vundef
   end.
 
 Definition arith_eval_arrr n v1 v2 v3 :=
   match n with
   | Pmaddw => Val.add v1 (Val.mul v2 v3)
   | Pmaddl => Val.addl v1 (Val.mull v2 v3)
+  | Pmsubw => Val.sub v1 (Val.mul v2 v3)
+  | Pmsubl => Val.subl v1 (Val.mull v2 v3)
   | Pcmove bt =>
     match cmp_for_btest bt with
     | (Some c, Int)  =>
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 39a14727..9b22cd01 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -61,7 +61,9 @@ let arith_rrr_str = function
   | Pfcompw ft -> "Pfcompw"
   | Pfcompl ft -> "Pfcompl"
   | Paddw -> "Paddw"
+  | Paddxw _ -> "Paddxw"
   | Psubw -> "Psubw"
+  | Psubxw _ -> "Psubxw"
   | Pmulw -> "Pmulw"
   | Pandw -> "Pandw"
   | Pnandw -> "Pnandw"
@@ -76,7 +78,9 @@ let arith_rrr_str = function
   | Psrxw -> "Psrxw"
   | Psllw -> "Psllw"
   | Paddl -> "Paddl"
+  | Paddxl _ -> "Paddxl"
   | Psubl -> "Psubl"
+  | Psubxl _ -> "Psubxl"
   | Pandl -> "Pandl"
   | Pnandl -> "Pnandl"
   | Porl -> "Porl"
@@ -100,6 +104,9 @@ let arith_rrr_str = function
 let arith_rri32_str = function
   | Pcompiw it -> "Pcompiw"
   | Paddiw -> "Paddiw"
+  | Paddxiw _ -> "Paddxiw"
+  | Psubiw -> "Psubiw"
+  | Psubxiw _ -> "Psubxiw"
   | Pmuliw -> "Pmuliw"
   | Pandiw -> "Pandiw"
   | Pnandiw -> "Pnandiw"
@@ -122,6 +129,9 @@ let arith_rri32_str = function
 let arith_rri64_str = function
   | Pcompil it -> "Pcompil"
   | Paddil -> "Paddil"
+  | Psubil -> "Psubil"
+  | Paddxil _ -> "Paddxil"
+  | Psubxil _ -> "Psubxil"
   | Pmulil -> "Pmulil"
   | Pandil -> "Pandil"
   | Pnandil -> "Pnandil"
@@ -140,6 +150,8 @@ let arith_arr_str = function
 let arith_arrr_str = function
   | Pmaddw -> "Pmaddw"
   | Pmaddl -> "Pmaddl"
+  | Pmsubw -> "Pmsubw"
+  | Pmsubl -> "Pmsubl"
   | Pcmove _ -> "Pcmove"
   | Pcmoveu _ -> "Pcmoveu"
             
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 114297c9..83d12da7 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -513,8 +513,18 @@ module Target (*: TARGET*) =
 
       | Paddw (rd, rs1, rs2) ->
          fprintf oc "	addw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+      | Paddxw (zshift, rd, rs1, rs2) ->
+         let shift = camlint_of_coqint zshift in
+         assert(shift >= 1l && shift <= 4l);
+         fprintf oc "	addx%dw	%a = %a, %a\n" (1 lsl (Int32.to_int shift))
+           ireg rd ireg rs1 ireg rs2
       | Psubw (rd, rs1, rs2) ->
          fprintf oc "	sbfw	%a = %a, %a\n" ireg rd ireg rs2 ireg rs1
+      | Psubxw (zshift, rd, rs1, rs2) ->
+         let shift = camlint_of_coqint zshift in
+         assert(shift >= 1l && shift <= 4l);
+         fprintf oc "	subx%dw	%a = %a, %a\n" (1 lsl (Int32.to_int shift))
+           ireg rd ireg rs1 ireg rs2
       | Pmulw (rd, rs1, rs2) ->
          fprintf oc "	mulw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Pandw (rd, rs1, rs2) ->
@@ -543,22 +553,34 @@ module Target (*: TARGET*) =
          fprintf oc "	sllw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Pmaddw (rd, rs1, rs2) ->
          fprintf oc "	maddw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+      | Pmsubw (rd, rs1, rs2) ->
+         fprintf oc "	msbfw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
 
-      | Paddl (rd, rs1, rs2) -> assert Archi.ptr64;
+      | Paddl (rd, rs1, rs2) ->
          fprintf oc "	addd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+      | Paddxl (zshift, rd, rs1, rs2) ->
+         let shift = camlint_of_coqint zshift in
+         assert(shift >= 1l && shift <= 4l);
+         fprintf oc "	addx%dd	%a = %a, %a\n" (1 lsl (Int32.to_int shift))
+           ireg rd ireg rs1 ireg rs2
       | Psubl (rd, rs1, rs2) ->
          fprintf oc "	sbfd	%a = %a, %a\n" ireg rd ireg rs2 ireg rs1
-      | Pandl (rd, rs1, rs2) -> assert Archi.ptr64;
+      | Psubxl (zshift, rd, rs1, rs2) ->
+         let shift = camlint_of_coqint zshift in
+         assert(shift >= 1l && shift <= 4l);
+         fprintf oc "	sbfx%dd	%a = %a, %a\n" (1 lsl (Int32.to_int shift))
+           ireg rd ireg rs1 ireg rs2
+      | Pandl (rd, rs1, rs2) ->
          fprintf oc "	andd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Pnandl (rd, rs1, rs2) -> assert Archi.ptr64;
+      | Pnandl (rd, rs1, rs2) ->
          fprintf oc "	nandd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Porl (rd, rs1, rs2) -> assert Archi.ptr64;
+      | Porl (rd, rs1, rs2) ->
          fprintf oc "	ord	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Pnorl (rd, rs1, rs2) -> assert Archi.ptr64;
+      | Pnorl (rd, rs1, rs2) ->
          fprintf oc "	nord	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Pxorl (rd, rs1, rs2) -> assert Archi.ptr64;
+      | Pxorl (rd, rs1, rs2) ->
          fprintf oc "	xord	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
-      | Pnxorl (rd, rs1, rs2) -> assert Archi.ptr64;
+      | Pnxorl (rd, rs1, rs2) -> 
          fprintf oc "	nxord	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Pandnl (rd, rs1, rs2) -> 
          fprintf oc "	andnd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
@@ -576,6 +598,8 @@ module Target (*: TARGET*) =
          fprintf oc "	srad	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Pmaddl (rd, rs1, rs2) ->
          fprintf oc "	maddd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+      | Pmsubl (rd, rs1, rs2) ->
+         fprintf oc "	msbfd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
 
       | Pfaddd (rd, rs1, rs2) ->
          fprintf oc "	faddd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
@@ -595,6 +619,18 @@ module Target (*: TARGET*) =
          fprintf oc "	compw.%a	%a = %a, %a\n" icond it ireg rd ireg rs coqint imm
       | Paddiw (rd, rs, imm) ->
          fprintf oc "	addw	%a = %a, %a\n" ireg rd ireg rs coqint imm
+      | Paddxiw (zshift, rd, rs, imm) ->
+         let shift = camlint_of_coqint zshift in
+         assert(shift >= 1l && shift <= 4l);
+         fprintf oc "	addx%dw	%a = %a, %a\n"  (1 lsl (Int32.to_int shift))
+           ireg rd ireg rs coqint imm
+      | Psubiw (rd, rs, imm) ->
+         fprintf oc "	sbfw	%a = %a, %a\n" ireg rd ireg rs coqint imm
+      | Psubxiw (zshift, rd, rs, imm) ->
+         let shift = camlint_of_coqint zshift in
+         assert(shift >= 1l && shift <= 4l);
+         fprintf oc "	sbfx%dw	%a = %a, %a\n"  (1 lsl (Int32.to_int shift))
+           ireg rd ireg rs coqint imm
       | Pmuliw (rd, rs, imm) ->
          fprintf oc "	mulw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Pandiw (rd, rs, imm) ->
@@ -640,6 +676,18 @@ module Target (*: TARGET*) =
          fprintf oc "	compd.%a	%a = %a, %a\n" icond it ireg rd ireg rs coqint64 imm
       | Paddil (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	addd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+      | Paddxil (zshift, rd, rs, imm) ->
+         let shift = camlint_of_coqint zshift in
+         assert(shift >= 1l && shift <= 4l);
+         fprintf oc "	addx%dd	%a = %a, %a\n"  (1 lsl (Int32.to_int shift))
+           ireg rd ireg rs coqint imm
+      | Psubil (rd, rs, imm) ->
+         fprintf oc "	sbfd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+      | Psubxil (zshift, rd, rs, imm) ->
+         let shift = camlint_of_coqint zshift in
+         assert(shift >= 1l && shift <= 4l);
+         fprintf oc "	sbfx%dd	%a = %a, %a\n"  (1 lsl (Int32.to_int shift))
+           ireg rd ireg rs coqint64 imm
       | Pmulil (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	muld	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
       | Pandil (rd, rs, imm) -> assert Archi.ptr64;