Merge remote-tracking branch 'origin/mppa-work' into mppa-cos

21 files changed, 891 insertions, 53 deletions

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index b1afab6f..651d644e 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -70,4 +70,5 @@ let use_standard_headers =  ref Configuration.has_standard_headers
 let option_fglobaladdrtmp = ref false
 let option_fglobaladdroffset = ref false
 let option_fxsaddr = ref true  
-let option_coalesce_mem = ref true  
+let option_faddx = ref false  
+let option_fcoalesce_mem = ref true  
diff --git a/driver/Compopts.v b/driver/Compopts.v
index f7de596c..9c6448b7 100644
--- a/driver/Compopts.v
+++ b/driver/Compopts.v
@@ -43,17 +43,20 @@ Parameter optim_redundancy: unit -> bool.
 Parameter optim_postpass: unit -> bool.
 
 (** FIXME TEMPORARY Flag -fglobaladdrtmp. Use a temporary register for loading the address of global variables (default false) *)
-Parameter optim_fglobaladdrtmp: unit -> bool.
+Parameter optim_globaladdrtmp: unit -> bool.
 
 (** FIXME TEMPORARY Flag -fglobaladdroffset. Fold offsets into global addresses  (default false) *)
-Parameter optim_fglobaladdroffset: unit -> bool.
+Parameter optim_globaladdroffset: unit -> bool.
 
 (** FIXME TEMPORARY Flag -fxsaddr. Use .xs addressing mode (default true) *)
-Parameter optim_fxsaddr: unit -> bool.
+Parameter optim_xsaddr: unit -> bool.
 
 (** FIXME TEMPORARY Flag -fcoaelesce-mem. Fuse (default true) *)
 Parameter optim_coalesce_mem: unit -> bool.
 
+(** FIXME TEMPORARY Flag -faddx. Fuse (default false) *)
+Parameter optim_addx: unit -> bool.
+
 (** Flag -fthumb.  For the ARM back-end. *)
 Parameter thumb: unit -> bool.
 
diff --git a/driver/Driver.ml b/driver/Driver.ml
index cfafcaa3..74e7ae77 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -375,7 +375,8 @@ let cmdline_actions =
   @ f_opt "globaladdrtmp" option_fglobaladdrtmp
   @ f_opt "globaladdroffset" option_fglobaladdroffset
   @ f_opt "xsaddr" option_fxsaddr
-  @ f_opt "coalesce-mem" option_coalesce_mem
+  @ f_opt "addx" option_faddx
+  @ f_opt "coalesce-mem" option_fcoalesce_mem
 (* Code generation options *)
   @ f_opt "fpu" option_ffpu
   @ f_opt "sse" option_ffpu (* backward compatibility *)
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 979e1d49..e2ffd65d 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -117,14 +117,16 @@ Extract Constant Compopts.thumb =>
   "fun _ -> !Clflags.option_mthumb".
 Extract Constant Compopts.debug =>
   "fun _ -> !Clflags.option_g".
-Extract Constant Compopts.optim_fglobaladdrtmp =>
+Extract Constant Compopts.optim_globaladdrtmp =>
   "fun _ -> !Clflags.option_fglobaladdrtmp".
-Extract Constant Compopts.optim_fglobaladdroffset =>
+Extract Constant Compopts.optim_globaladdroffset =>
   "fun _ -> !Clflags.option_fglobaladdroffset".
-Extract Constant Compopts.optim_fxsaddr =>
+Extract Constant Compopts.optim_xsaddr =>
   "fun _ -> !Clflags.option_fxsaddr".
+Extract Constant Compopts.optim_addx =>
+  "fun _ -> !Clflags.option_faddx".
 Extract Constant Compopts.optim_coalesce_mem =>
-  "fun _ -> !Clflags.option_coalesce_mem".
+  "fun _ -> !Clflags.option_fcoalesce_mem".
 
 (* Compiler *)
 Extract Constant Compiler.print_Clight => "PrintClight.print_if".
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 1774b102..e5f81fbb 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 : shift1_4)  (rd rs1 rs2: ireg)          (**r add word *)

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

+  | Prevsubxw (shift : shift1_4)  (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 : shift1_4)  (rd rs1 rs2: ireg)          (**r add long shift *)

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

+  | Prevsubxl (shift : shift1_4)  (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 : shift1_4) (rd rs: ireg) (imm: int)    (**r add imm word *)

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

+  | Prevsubxiw (shift : shift1_4) (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 : shift1_4) (rd rs: ireg) (imm: int64)  (**r add immediate long *) 

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

+  | Prevsubxil (shift : shift1_4) (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.Prevsubxw shift) rd rs1 rs2 => Prevsubxw 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.Prevsubxl shift) rd rs1 rs2 => Prevsubxl 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.Prevsubiw rd rs imm       => Prevsubiw rd rs imm

+  | PArithRRI32 (Asmvliw.Prevsubxiw shift) rd rs imm => Prevsubxiw 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.Prevsubil rd rs imm       => Prevsubil rd rs imm

+  | PArithRRI64 (Asmvliw.Prevsubxil shift) rd rs imm => Prevsubxil 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..616ec6db 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"
+  | Prevsubxw _ => "Prevsubxw"
   | 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"
+  | Prevsubxl _ => "Prevsubxl"
   | 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"
+  | Paddxiw _ => "Paddxiw"
+  | Prevsubiw => "Prevsubiw"
+  | Prevsubxiw _ => "Prevsubxiw"
   | 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"
+  | Prevsubil => "Prevsubil"
+  | Paddxil _ => "Paddxil"
+  | Prevsubxil _ => "Prevsubxil"
   | 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/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index a4364051..941796cd 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -443,12 +443,33 @@ Definition transl_op
   | Oaddimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (addimm32 rd rs n ::i k)
+  | Oaddx shift, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Paddxw shift rd rs1 rs2 ::i k)
+  | Oaddximm shift n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (Paddxiw shift rd rs n ::i k)
+  | Oaddxl shift, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Paddxl shift rd rs1 rs2 ::i k)
+  | Oaddxlimm shift n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (Paddxil shift rd rs n ::i k)
   | Oneg, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       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 ::i k)
+  | Orevsubimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (Prevsubiw rd rs n ::i k)
+  | Orevsubx shift, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Prevsubxw shift rd rs1 rs2 ::i k)
+  | Orevsubximm shift n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (Prevsubxiw shift rd rs n ::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 ::i k)
@@ -543,6 +564,12 @@ Definition transl_op
       do r1 <- ireg_of a1;
       do r2 <- ireg_of a2;
         OK (Pmaddiw r1 r2 n ::i k)
+  | Omsub, a1 :: a2 :: a3 :: nil =>
+    assertion (mreg_eq a1 res);
+      do r1 <- ireg_of a1;
+      do r2 <- ireg_of a2;
+      do r3 <- ireg_of a3;
+        OK (Pmsubw r1 r2 r3 ::i k)
   (* [Omakelong], [Ohighlong]  should not occur *)
   | Olowlong, a1 :: nil =>
       do rd <- ireg_of res; do rs <- ireg_of a1;
@@ -567,6 +594,15 @@ Definition transl_op
   | Osubl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Psubl rd rs1 rs2 ::i k)
+  | Orevsubxl shift, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Prevsubxl shift rd rs1 rs2 ::i k)
+  | Orevsublimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (Prevsubil rd rs n ::i k)
+  | Orevsubxlimm shift n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (Prevsubxil shift rd rs n ::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 ::i k)
@@ -662,6 +698,12 @@ Definition transl_op
       do r1 <- ireg_of a1;
       do r2 <- ireg_of a2;
         OK (Pmaddil r1 r2 n ::i k)
+  | Omsubl, a1 :: a2 :: a3 :: nil =>
+    assertion (mreg_eq a1 res);
+      do r1 <- ireg_of a1;
+      do r2 <- ireg_of a2;
+      do r3 <- ireg_of a3;
+        OK (Pmsubl r1 r2 r3 ::i k)
   | Oabsf, a1 :: nil =>
       do rd <- freg_of res; do rs <- freg_of a1;
       OK (Pfabsd rd rs ::i k)
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 3bef1a5c..886228ad 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 : shift1_4)                              (**r add shift *)
+  | Psubw                                           (**r sub word word *)
+  | Prevsubxw (shift : shift1_4)                              (**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 : shift1_4)                              (**r add shift long *)
   | Psubl                                           (**r sub long *)
+  | Prevsubxl (shift : shift1_4)                              (**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 : shift1_4)
+  | Prevsubiw                                          (**r add imm word *)
+  | Prevsubxiw (shift : shift1_4)
   | 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 : shift1_4)
+  | Prevsubil
+  | Prevsubxil (shift : shift1_4)
   | 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,19 @@ Definition arith_eval_rrr n v1 v2 :=
   | Pfsbfw => Val.subfs v1 v2
   | Pfmuld => Val.mulf v1 v2
   | Pfmulw => Val.mulfs v1 v2
+
+  | Paddxw shift => ExtValues.addx (int_of_shift1_4 shift) v1 v2
+  | Paddxl shift => ExtValues.addxl (int_of_shift1_4 shift) v1 v2
+
+  | Prevsubxw shift => ExtValues.revsubx (int_of_shift1_4 shift) v1 v2
+  | Prevsubxl shift => ExtValues.revsubxl (int_of_shift1_4 shift) v1 v2
   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)
+  | Prevsubiw  => Val.sub (Vint i) v
   | Pmuliw  => Val.mul   v (Vint i)
   | Pandiw  => Val.and   v (Vint i)
   | Pnandiw => Val.notint (Val.and  v (Vint i))
@@ -1079,12 +1098,15 @@ 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 => ExtValues.addx (int_of_shift1_4 shift) v (Vint i)
+  | Prevsubxiw shift => ExtValues.revsubx (int_of_shift1_4 shift) v (Vint i)
   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)
+  | Prevsubil  => Val.subl (Vlong i) v
   | Pmulil  => Val.mull v (Vlong i)
   | Pandil  => Val.andl v (Vlong i)
   | Pnandil  => Val.notl (Val.andl v (Vlong i))
@@ -1094,12 +1116,16 @@ 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 => ExtValues.addxl (int_of_shift1_4 shift) v (Vlong i)
+  | Prevsubxil shift => ExtValues.revsubxl (int_of_shift1_4 shift) v (Vlong i)
   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/ConstpropOp.vp b/mppa_k1c/ConstpropOp.vp
index b5128357..7ee3dfe8 100644
--- a/mppa_k1c/ConstpropOp.vp
+++ b/mppa_k1c/ConstpropOp.vp
@@ -298,7 +298,7 @@ Nondetfunction addr_strength_reduction
                 (addr: addressing) (args: list reg) (vl: list aval) :=
   match addr, args, vl with
   | Aindexed n, r1 :: nil, Ptr(Gl symb n1) :: nil =>
-      if (orb (Archi.pic_code tt) (negb (Compopts.optim_fglobaladdrtmp tt)))
+      if (orb (Archi.pic_code tt) (negb (Compopts.optim_globaladdrtmp tt)))
       then (addr, args)
       else (Aglobal symb (Ptrofs.add n1 n), nil)
   | Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil =>
diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
index 980e18f8..155afa83 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -2,6 +2,42 @@ Require Import Coqlib.
 Require Import Integers.
 Require Import Values.
 
+Inductive shift1_4 : Type :=
+| SHIFT1 | SHIFT2 | SHIFT3 | SHIFT4.
+
+Definition z_of_shift1_4 (x : shift1_4) :=
+  match x with
+  | SHIFT1 => 1
+  | SHIFT2 => 2
+  | SHIFT3 => 3
+  | SHIFT4 => 4
+  end.
+
+Definition shift1_4_of_z (x : Z) :=
+  if Z.eq_dec x 1 then Some SHIFT1
+  else if Z.eq_dec x 2 then Some SHIFT2
+  else if Z.eq_dec x 3 then Some SHIFT3
+  else if Z.eq_dec x 4 then Some SHIFT4
+  else None.
+
+Lemma shift1_4_of_z_correct :
+  forall z,
+    match shift1_4_of_z z with
+    | Some x => z_of_shift1_4 x = z
+    | None => True
+    end.
+Proof.
+  intro. unfold shift1_4_of_z.
+  destruct (Z.eq_dec _ _); simpl; try congruence.
+  destruct (Z.eq_dec _ _); simpl; try congruence.
+  destruct (Z.eq_dec _ _); simpl; try congruence.
+  destruct (Z.eq_dec _ _); simpl; try congruence.
+  trivial.
+Qed.
+
+Definition int_of_shift1_4 (x : shift1_4) :=
+  Int.repr (z_of_shift1_4 x).
+
 Definition is_bitfield stop start :=
   (Z.leb start stop)
     && (Z.geb start Z.zero)
@@ -577,3 +613,61 @@ Proof.
     }
   }
 Qed.
+
+Lemma sub_add_neg :
+  forall x y, Val.sub x y = Val.add x (Val.neg y).
+Proof.
+  destruct x; destruct y; simpl; trivial.
+  f_equal.
+  apply Int.sub_add_opp.
+Qed.
+
+Lemma neg_mul_distr_r :
+  forall x y, Val.neg (Val.mul x y) = Val.mul x (Val.neg y).
+Proof.
+  destruct x; destruct y; simpl; trivial.
+  f_equal.
+  apply Int.neg_mul_distr_r.
+Qed.
+
+(* pointer diff
+Lemma sub_addl_negl :
+  forall x y, Val.subl x y = Val.addl x (Val.negl y).
+Proof.
+  destruct x; destruct y; simpl; trivial.
+  + f_equal. apply Int64.sub_add_opp.
+  + destruct (Archi.ptr64) eqn:ARCHI64; trivial.
+    f_equal. rewrite Ptrofs.sub_add_opp.
+    pose (Ptrofs.agree64_neg ARCHI64 (Ptrofs.of_int64 i0) i0) as Hagree.
+    unfold Ptrofs.agree64 in Hagree.
+    unfold Ptrofs.add.
+    f_equal. f_equal.
+    rewrite Hagree.
+    pose (Ptrofs.agree64_of_int ARCHI64 (Int64.neg i0)) as Hagree2.
+    rewrite Hagree2.
+    reflexivity.
+    exact (Ptrofs.agree64_of_int ARCHI64 i0).
+  +  destruct (Archi.ptr64) eqn:ARCHI64; simpl; trivial.
+     destruct (eq_block _ _); simpl; trivial.
+Qed.
+ *)
+
+Lemma negl_mull_distr_r :
+  forall x y, Val.negl (Val.mull x y) = Val.mull x (Val.negl y).
+Proof.
+  destruct x; destruct y; simpl; trivial.
+  f_equal.
+  apply Int64.neg_mul_distr_r.
+Qed.
+
+Definition addx sh v1 v2 :=
+  Val.add v2 (Val.shl v1 (Vint sh)).
+
+Definition addxl sh v1 v2 :=
+  Val.addl v2 (Val.shll v1 (Vint sh)).
+
+Definition revsubx sh v1 v2 :=
+  Val.sub v2 (Val.shl v1 (Vint sh)).
+
+Definition revsubxl sh v1 v2 :=
+  Val.subl v2 (Val.shll v1 (Vint sh)).
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v
index cd8c6606..db3dfe64 100644
--- a/mppa_k1c/Machregs.v
+++ b/mppa_k1c/Machregs.v
@@ -213,7 +213,9 @@ Global Opaque
 
 Definition two_address_op (op: operation) : bool :=
   match op with
-  | Omadd | Omaddimm _ | Omaddl | Omaddlimm _
+  | Omadd | Omaddimm _
+  | Omaddl | Omaddlimm _
+  | Omsub | Omsubl
   | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _
   | Oinsf _ _ | Oinsfl _ _ => true
   | _ => false
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index c10f5c56..5ba9851f 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -42,8 +42,13 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Ocast16signed => op1 (sign_ext 16 nv)
   | Oadd => op2 (modarith nv)
   | Oaddimm n => op1 (modarith nv)
+  | Oaddx _ => op2 (default nv)
+  | Oaddximm _ _ => op1 (default nv)
   | Oneg => op1 (modarith nv)
   | Osub => op2 (default nv)
+  | Orevsubimm _ => op1 (default nv)
+  | Orevsubx _ => op2 (default nv)
+  | Orevsubximm _ _ => op1 (default nv)
   | Omul => op2 (modarith nv)
   | Omulimm _ => op1 (modarith nv)
   | Omulhs | Omulhu | Odiv | Odivu | Omod | Omodu => op2 (default nv)
@@ -72,12 +77,18 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Oshrximm n => op1 (default nv)
   | Omadd => op3 (modarith nv)
   | Omaddimm n => op2 (modarith nv)
+  | Omsub => op3 (modarith nv)
   | Omakelong => op2 (default nv)
   | Olowlong | Ohighlong => op1 (default nv)
   | Ocast32signed => op1 (default nv)
   | Ocast32unsigned => op1 (default nv)
   | Oaddl => op2 (default nv)
   | Oaddlimm n => op1 (default nv)
+  | Oaddxl _ => op2 (default nv)
+  | Oaddxlimm _ _ => op1 (default nv)
+  | Orevsublimm _ => op1 (default nv)
+  | Orevsubxl _ => op2 (default nv)
+  | Orevsubxlimm _ _ => op1 (default nv)
   | Onegl => op1 (default nv)
   | Osubl => op2 (default nv)
   | Omull => op2 (default nv)
@@ -107,6 +118,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Oshrxlimm n => op1 (default nv)
   | Omaddl => op3 (default nv)
   | Omaddlimm n => op2 (default nv)
+  | Omsubl => op3 (default nv)
   | Onegf | Oabsf => op1 (default nv)
   | Oaddf | Osubf | Omulf | Odivf => op2 (default nv)
   | Onegfs | Oabsfs => op1 (default nv)
@@ -229,6 +241,26 @@ Proof.
   - apply Val.addl_lessdef; trivial.
 Qed.
 
+Lemma subl_lessdef:
+  forall v1 v1' v2 v2',
+  Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Val.lessdef (Val.subl v1 v2) (Val.subl v1' v2').
+Proof.
+  intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto.
+Qed.
+
+Lemma subl_sound:
+  forall v1 w1 v2 w2 x,
+  vagree v1 w1 (default x) -> vagree v2 w2 (default x) ->
+  vagree (Val.subl v1 v2) (Val.subl w1 w2) x.
+Proof.
+  unfold default; intros.
+  destruct x; simpl in *; trivial.
+  - unfold Val.subl.
+    destruct v1; destruct v2; trivial; destruct Archi.ptr64; simpl; trivial.
+    destruct (eq_block _ _) ; simpl; trivial.
+  - apply subl_lessdef; trivial.
+Qed.
+
 
 Lemma mull_sound:
   forall v1 w1 v2 w2 x,
@@ -423,7 +455,7 @@ Remark default_idem: forall nv, default (default nv) = default nv.
 Proof.
   destruct nv; simpl; trivial.
 Qed.
-
+  
 Lemma needs_of_operation_sound:
   forall op args v nv args',
   eval_operation ge (Vptr sp Ptrofs.zero) op args m1 = Some v ->
@@ -466,11 +498,22 @@ Proof.
   (* madd *)
 - apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption.
 - apply add_sound; try apply mul_sound; auto with na; rewrite modarith_idem; assumption.
+- repeat rewrite ExtValues.sub_add_neg.
+  apply add_sound; trivial.
+  apply neg_sound; trivial.
+  rewrite modarith_idem.
+  apply mul_sound;
+  rewrite modarith_idem; trivial.
   (* maddl *)
 - apply addl_sound; trivial.
   apply mull_sound; trivial.
   rewrite default_idem; trivial.
   rewrite default_idem; trivial.
+  (* msubl *)
+- apply subl_sound; trivial.
+  apply mull_sound; trivial.
+  rewrite default_idem; trivial.
+  rewrite default_idem; trivial.
   (* select *)
 - apply select_sound; trivial.
   (* selectl *)
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 5e80589b..4df157b0 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -79,8 +79,13 @@ Inductive operation : Type :=
   | Ocast16signed            (**r [rd] is 16-bit sign extension of [r1] *)
   | Oadd                     (**r [rd = r1 + r2] *)
   | Oaddimm (n: int)         (**r [rd = r1 + n] *)
+  | Oaddx (shift: shift1_4)         (**r [rd = r1 << shift + r2] *)
+  | Oaddximm (shift: shift1_4) (n: int) (**r [rd = r1 << shift + n] *)
   | Oneg                     (**r [rd = - r1]   *)                     
   | Osub                     (**r [rd = r1 - r2] *)
+  | Orevsubimm (n: int)      (**r [rd = n - r1] *)
+  | Orevsubx (shift: shift1_4)         (**r [rd = r2 -r1 << shift] *)
+  | Orevsubximm (shift: shift1_4) (n: int) (**r [rd = n -r1 << shift] *)
   | Omul                     (**r [rd = r1 * r2] *)
   | Omulimm (n: int)         (**r [rd = r1 * n] *)
   | Omulhs                   (**r [rd = high part of r1 * r2, signed] *)
@@ -116,6 +121,7 @@ Inductive operation : Type :=
   | Ororimm (n: int)         (**r rotate right immediate *)
   | Omadd                    (**r [rd = rd + r1 * r2] *)
   | Omaddimm (n: int)        (**r [rd = rd + r1 * imm] *)
+  | Omsub                    (**r [rd = rd - r1 * r2] *)
 (*c 64-bit integer arithmetic: *)
   | Omakelong                (**r [rd = r1 << 32 | r2] *)
   | Olowlong                 (**r [rd = low-word(r1)] *)
@@ -124,6 +130,11 @@ Inductive operation : Type :=
   | Ocast32unsigned          (**r [rd] is 32-bit zero extension of [r1] *)
   | Oaddl                    (**r [rd = r1 + r2] *)
   | Oaddlimm (n: int64)      (**r [rd = r1 + n] *)
+  | Oaddxl (shift: shift1_4)         (**r [rd = r1 << shift + r2] *)
+  | Oaddxlimm (shift: shift1_4) (n: int64) (**r [rd = r1 << shift + n] *)
+  | Orevsublimm (n: int64)      (**r [rd = n - r1] *)
+  | Orevsubxl (shift: shift1_4)         (**r [rd = r2 -r1 << shift] *)
+  | Orevsubxlimm (shift: shift1_4) (n: int64) (**r [rd = n -r1 << shift] *)
   | Onegl                    (**r [rd = - r1] *)
   | Osubl                    (**r [rd = r1 - r2] *)
   | Omull                    (**r [rd = r1 * r2] *)
@@ -160,6 +171,7 @@ Inductive operation : Type :=
   | Oshrxlimm (n: int)       (**r [rd = r1 / 2^n] (signed) *)
   | Omaddl                   (**r [rd = rd + r1 * r2] *)
   | Omaddlimm (n: int64)     (**r [rd = rd + r1 * imm] *)
+  | Omsubl                   (**r [rd = rd - r1 * r2] *)
 (*c Floating-point arithmetic: *)
   | Onegf                    (**r [rd = - r1] *)
   | Oabsf                    (**r [rd = abs(r1)] *)
@@ -235,9 +247,14 @@ Proof.
   decide equality.
 Defined.
 
+Definition eq_shift1_4 (x y : shift1_4): {x=y} + {x<>y}.
+Proof.
+  decide equality.
+Defined.
+
 Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}.
 Proof.
-  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition eq_condition0 Z.eq_dec; intros.
+  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition eq_condition0 Z.eq_dec eq_shift1_4; intros.
   decide equality.
 Defined.
 
@@ -386,8 +403,13 @@ Definition eval_operation
   | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1)
   | Oadd, v1 :: v2 :: nil => Some (Val.add v1 v2)
   | Oaddimm n, v1 :: nil => Some (Val.add v1 (Vint n))
+  | Oaddx s14, v1 :: v2 :: nil => Some (addx (int_of_shift1_4 s14) v1 v2)
+  | Oaddximm s14 n, v1 :: nil => Some (addx (int_of_shift1_4 s14) v1 (Vint n))
   | Oneg, v1 :: nil => Some (Val.neg v1)
   | Osub, v1 :: v2 :: nil => Some (Val.sub v1 v2)
+  | Orevsubimm n, v1 :: nil => Some (Val.sub (Vint n) v1)
+  | Orevsubx shift, v1 :: v2 :: nil => Some (ExtValues.revsubx (int_of_shift1_4 shift) v1 v2)
+  | Orevsubximm shift n, v1 :: nil => Some (ExtValues.revsubx (int_of_shift1_4 shift) v1 (Vint n))
   | Omul, v1 :: v2 :: nil => Some (Val.mul v1 v2)
   | Omulimm n, v1 :: nil => Some (Val.mul v1 (Vint n))
   | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2)
@@ -423,6 +445,7 @@ Definition eval_operation
   | Oshrximm n, v1::nil => Val.shrx v1 (Vint n)
   | Omadd, v1::v2::v3::nil => Some (Val.add v1 (Val.mul v2 v3))
   | (Omaddimm n), v1::v2::nil => Some (Val.add v1 (Val.mul v2 (Vint n)))
+  | Omsub, v1::v2::v3::nil => Some (Val.sub v1 (Val.mul v2 v3))
                                      
   | Omakelong, v1::v2::nil => Some (Val.longofwords v1 v2)
   | Olowlong, v1::nil => Some (Val.loword v1)
@@ -431,8 +454,13 @@ Definition eval_operation
   | Ocast32unsigned, v1 :: nil => Some (Val.longofintu v1)
   | Oaddl, v1 :: v2 :: nil => Some (Val.addl v1 v2)
   | Oaddlimm n, v1::nil => Some (Val.addl v1 (Vlong n))
+  | Oaddxl s14, v1 :: v2 :: nil => Some (addxl (int_of_shift1_4 s14) v1 v2)
+  | Oaddxlimm s14 n, v1 :: nil => Some (addxl (int_of_shift1_4 s14) v1 (Vlong n))
   | Onegl, v1::nil => Some (Val.negl v1)
   | Osubl, v1::v2::nil => Some (Val.subl v1 v2)
+  | Orevsublimm n, v1 :: nil => Some (Val.subl (Vlong n) v1)
+  | Orevsubxl shift, v1 :: v2 :: nil => Some (ExtValues.revsubxl (int_of_shift1_4 shift) v1 v2)
+  | Orevsubxlimm shift n, v1 :: nil => Some (ExtValues.revsubxl (int_of_shift1_4 shift) v1 (Vlong n))
   | Omull, v1::v2::nil => Some (Val.mull v1 v2)
   | Omullimm n, v1::nil => Some (Val.mull v1 (Vlong n))
   | Omullhs, v1::v2::nil => Some (Val.mullhs v1 v2)
@@ -467,6 +495,7 @@ Definition eval_operation
   | Oshrxlimm n, v1::nil => Val.shrxl v1 (Vint n)
   | Omaddl, v1::v2::v3::nil => Some (Val.addl v1 (Val.mull v2 v3))
   | (Omaddlimm n), v1::v2::nil => Some (Val.addl v1 (Val.mull v2 (Vlong n)))
+  | Omsubl, v1::v2::v3::nil => Some (Val.subl v1 (Val.mull v2 v3))
                                       
   | Onegf, v1::nil => Some (Val.negf v1)
   | Oabsf, v1::nil => Some (Val.absf v1)
@@ -583,8 +612,13 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Ocast16signed => (Tint :: nil, Tint)
   | Oadd => (Tint :: Tint :: nil, Tint)
   | Oaddimm _ => (Tint :: nil, Tint)
+  | Oaddx _ => (Tint :: Tint :: nil, Tint)
+  | Oaddximm _ _ => (Tint :: nil, Tint)
   | Oneg => (Tint :: nil, Tint)
   | Osub => (Tint :: Tint :: nil, Tint)
+  | Orevsubimm _ => (Tint :: nil, Tint)
+  | Orevsubx _ => (Tint :: Tint :: nil, Tint)
+  | Orevsubximm _ _ => (Tint :: nil, Tint)
   | Omul => (Tint :: Tint :: nil, Tint)
   | Omulimm _ => (Tint :: nil, Tint)
   | Omulhs => (Tint :: Tint :: nil, Tint)
@@ -620,6 +654,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Ororimm _ => (Tint :: nil, Tint)
   | Omadd => (Tint :: Tint :: Tint :: nil, Tint)
   | Omaddimm _ => (Tint :: Tint :: nil, Tint)
+  | Omsub => (Tint :: Tint :: Tint :: nil, Tint)
                    
   | Omakelong => (Tint :: Tint :: nil, Tlong)
   | Olowlong => (Tlong :: nil, Tint)
@@ -628,6 +663,11 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Ocast32unsigned => (Tint :: nil, Tlong)
   | Oaddl => (Tlong :: Tlong :: nil, Tlong)
   | Oaddlimm _ => (Tlong :: nil, Tlong)
+  | Oaddxl _ => (Tlong :: Tlong :: nil, Tlong)
+  | Oaddxlimm _ _ => (Tlong :: nil, Tlong)
+  | Orevsublimm _ => (Tlong :: nil, Tlong)
+  | Orevsubxl _ => (Tlong :: Tlong :: nil, Tlong)
+  | Orevsubxlimm _ _ => (Tlong :: nil, Tlong)
   | Onegl => (Tlong :: nil, Tlong)
   | Osubl => (Tlong :: Tlong :: nil, Tlong)
   | Omull => (Tlong :: Tlong :: nil, Tlong)
@@ -664,6 +704,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Oshrxlimm _ => (Tlong :: nil, Tlong)
   | Omaddl => (Tlong :: Tlong :: Tlong :: nil, Tlong)
   | Omaddlimm _ => (Tlong :: Tlong :: nil, Tlong)
+  | Omsubl => (Tlong :: Tlong :: Tlong :: nil, Tlong)
 
   | Onegf => (Tfloat :: nil, Tfloat)
   | Oabsf => (Tfloat :: nil, Tfloat)
@@ -736,6 +777,32 @@ Proof.
   intros. unfold Val.has_type, Val.addl. destruct Archi.ptr64, v1, v2; auto.
 Qed.
 
+Remark type_sub:
+  forall v1 v2, Val.has_type (Val.sub v1 v2) Tint.
+Proof.
+  intros. unfold Val.has_type, Val.sub. destruct Archi.ptr64, v1, v2; simpl; auto.
+  destruct (eq_block _ _); auto.
+Qed.
+
+Remark type_subl:
+  forall v1 v2, Val.has_type (Val.subl v1 v2) Tlong.
+Proof.
+  intros. unfold Val.has_type, Val.subl. destruct Archi.ptr64, v1, v2; simpl; auto.
+  destruct (eq_block _ _); auto.
+Qed.
+
+Remark type_shl:
+  forall v1 v2, Val.has_type (Val.shl v1 v2) Tint.
+Proof.
+  destruct v1, v2; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial.
+Qed.
+
+Remark type_shll:
+  forall v1 v2, Val.has_type (Val.shll v1 v2) Tlong.
+Proof.
+  destruct v1, v2; simpl; trivial; destruct (Int.ltu _ _); simpl; trivial.
+Qed.
+
 Lemma type_of_operation_sound:
   forall op vl sp v m,
   op <> Omove ->
@@ -761,9 +828,18 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* add, addimm *)
   - apply type_add.
   - apply type_add.
+  (* addx, addximm *)
+  - apply type_add.
+  - destruct v0; simpl; trivial.
+    destruct (Int.ltu _ _); simpl; trivial.
   (* neg, sub *)
   - destruct v0...
-  - unfold Val.sub. destruct v0; destruct v1... 
+  - apply type_sub.
+  (* revsubimm, revsubx, revsubximm *)
+  - destruct v0...
+  - apply type_sub.
+  - destruct v0; simpl; trivial.
+    destruct (Int.ltu _ _); simpl; trivial.
   (* mul, mulimm, mulhs, mulhu *)
   - destruct v0; destruct v1...
   - destruct v0...
@@ -819,8 +895,10 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* shrimm *)
   - destruct v0; simpl...   
   (* madd *)
-  - destruct v0; destruct v1; destruct v2...   
-  - destruct v0; destruct v1...
+  - apply type_add.
+  - apply type_add.
+  (* msub *)
+  - apply type_sub.
   (* makelong, lowlong, highlong *)
   - destruct v0; destruct v1...
   - destruct v0...
@@ -831,11 +909,17 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* addl, addlimm *)
   - apply type_addl.
   - apply type_addl.
+  (* addxl addxlimm *)
+  - apply type_addl.
+  - destruct v0; simpl; trivial.
+    destruct (Int.ltu _ _); simpl; trivial.
   (* negl, subl *)
   - destruct v0...
-  - unfold Val.subl. destruct v0; destruct v1... 
-    unfold Val.has_type; destruct Archi.ptr64...
-    destruct (eq_block b b0)...
+  - apply type_subl.
+  - destruct v0; simpl; trivial.
+    destruct (Int.ltu _ _); simpl; trivial.
+  - destruct v0...
+  - apply type_subl.
   (* mull, mullhs, mullhu *)
   - destruct v0; destruct v1...
   - destruct v0...
@@ -889,10 +973,10 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* shrxl *)
   - destruct v0; simpl in H0; try discriminate. destruct (Int.ltu n (Int.repr 63)); inv H0...
   (* maddl, maddlim *)
-  - destruct v0; destruct v1; destruct v2; simpl; trivial.
-    destruct Archi.ptr64; simpl; trivial.
-  - destruct v0; destruct v1; simpl; trivial.
-    destruct Archi.ptr64; simpl; trivial.
+  - apply type_addl.
+  - apply type_addl.
+  (* msubl *)
+  - apply type_subl.
   (* negf, absf *)
   - destruct v0...
   - destruct v0...
@@ -1359,9 +1443,19 @@ Proof.
   (* add, addimm *)
   - apply Val.add_inject; auto.
   - apply Val.add_inject; auto.
+  (* addx, addximm *)
+  - apply Val.add_inject; trivial.
+    inv H4; inv H2; simpl; try destruct (Int.ltu _ _); simpl; auto.
+  - inv H4; simpl; trivial.
+    destruct (Int.ltu _ _); simpl; trivial.
   (* neg, sub *)
   - inv H4; simpl; auto.
   - apply Val.sub_inject; auto.
+  (* revsubimm, revsubx, revsubximm *)
+  - inv H4; simpl; trivial.
+  - apply Val.sub_inject; trivial.
+    inv H4; inv H2; simpl; try destruct (Int.ltu _ _); simpl; auto.
+  - inv H4; simpl; try destruct (Int.ltu _ _); simpl; auto.
   (* mul, mulimm, mulhs, mulhu *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
@@ -1424,6 +1518,9 @@ Proof.
   (* madd, maddim *)
   - inv H2; inv H3; inv H4; simpl; auto.
   - inv H2; inv H4; simpl; auto.
+  (* msub *)
+  - apply Val.sub_inject; auto.
+    inv H3; inv H2; simpl; auto.
   (* makelong, highlong, lowlong *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
@@ -1434,9 +1531,21 @@ Proof.
   (* addl, addlimm *)
   - apply Val.addl_inject; auto.
   - apply Val.addl_inject; auto.
+  (* addxl, addxlimm *)
+  - apply Val.addl_inject; auto.
+    inv H4; simpl; trivial.
+    destruct (Int.ltu _ _); simpl; trivial.
+  - inv H4; simpl; trivial.
+    destruct (Int.ltu _ _); simpl; trivial.
   (* negl, subl *)
   - inv H4; simpl; auto.
   - apply Val.subl_inject; auto.
+    inv H4; inv H2; simpl; trivial;
+    destruct (Int.ltu _ _); simpl; trivial.
+  - inv H4; simpl; trivial;
+      destruct (Int.ltu _ _); simpl; trivial.
+  - inv H4; simpl; auto.
+  - apply Val.subl_inject; auto.
   (* mull, mullhs, mullhu *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
@@ -1500,6 +1609,9 @@ Proof.
     inv H2; inv H3; inv H4; simpl; auto.
   - apply Val.addl_inject; auto.
     inv H4; inv H2; simpl; auto.
+  (* msubl, msublimm *)
+  - apply Val.subl_inject; auto.
+    inv H2; inv H3; inv H4; simpl; auto.
     
   (* negf, absf *)
   - inv H4; simpl; auto.
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 7015fd5f..af1e8f85 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"
+  | Prevsubxw _ -> "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"
+  | Prevsubxl _ -> "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"
+  | Prevsubiw -> "Psubiw"
+  | Prevsubxiw _ -> "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"
+  | Prevsubil -> "Psubil"
+  | Paddxil _ -> "Paddxil"
+  | Prevsubxil _ -> "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"
             
@@ -393,6 +405,10 @@ let alu_lite_x : int array = let resmap = fun r -> match r with
   | "ISSUE" -> 2 | "TINY" -> 1 | "LITE" -> 1 |  _ -> 0 
   in Array.of_list (List.map resmap resource_names)
 
+let alu_lite_y : int array = let resmap = fun r -> match r with 
+  | "ISSUE" -> 3 | "TINY" -> 1 | "LITE" -> 1 |  _ -> 0 
+  in Array.of_list (List.map resmap resource_names)
+
 let alu_full : int array = let resmap = fun r -> match r with
   | "ISSUE" -> 1 | "TINY" -> 1 | "LITE" -> 1 | "ALU" -> 1 | _ -> 0
   in Array.of_list (List.map resmap resource_names)
@@ -452,8 +468,9 @@ type real_instruction =
   | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Srsw | Rorw | Xorw
   | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Srsd | Xord
   | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd
-  | Maddw | Maddd | Cmoved
+  | Maddw | Maddd | Msbfw | Msbfd | Cmoved
   | Make | Nop | Extfz | Extfs | Insf
+  | Addxw | Addxd
   (* LSU *)
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo
   | Sb | Sh | Sw | Sd | Sq | So
@@ -467,6 +484,8 @@ type real_instruction =
 
 let ab_inst_to_real = function
   | "Paddw" | "Paddiw" | "Pcvtl2w" -> Addw
+  | "Paddxw" | "Paddxiw" -> Addxw
+  | "Paddxl" | "Paddxil" -> Addxd
   | "Paddl" | "Paddil" | "Pmv" | "Pmvw2l" -> Addd
   | "Pandw" | "Pandiw" -> Andw
   | "Pnandw" | "Pnandiw" -> Nandw
@@ -493,6 +512,7 @@ let ab_inst_to_real = function
   | "Psllw" | "Pslliw" -> Sllw
   | "Proriw" -> Rorw
   | "Pmaddw" | "Pmaddiw" -> Maddw
+  | "Pmsubw" | "Pmsubiw" -> Msbfw
   | "Pslll" | "Psllil" -> Slld
   | "Pxorw" | "Pxoriw" -> Xorw
   | "Pnxorw" | "Pnxoriw" -> Nxorw
@@ -502,7 +522,8 @@ let ab_inst_to_real = function
   | "Pnxorl" | "Pnxoril" -> Nxord
   | "Pandnl" | "Pandnil" -> Andnd
   | "Pornl" | "Pornil" -> Ornd
-  | "Pmaddl" -> Maddd
+  | "Pmaddl" | "Pmaddil" -> Maddd
+  | "Pmsubl" | "Pmsubil" -> Msbfd
   | "Pmake" | "Pmakel" | "Pmakefs" | "Pmakef" | "Ploadsymbol" -> Make
   | "Pnop" | "Pcvtw2l" -> Nop
   | "Pextfz" | "Pextfzl" | "Pzxwd" -> Extfz
@@ -571,7 +592,7 @@ let rec_to_usage r =
   and real_inst = ab_inst_to_real r.inst
   in match real_inst with
   | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw
-  | Nxorw | Andnw | Ornw  -> 
+  | Nxorw | Andnw | Ornw -> 
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | _ -> raise InvalidEncoding)
@@ -580,6 +601,14 @@ let rec_to_usage r =
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | Some E27U27L10 -> alu_tiny_y)
+  | Addxw -> 
+      (match encoding with None | Some U6 | Some S10 -> alu_lite 
+                          | Some U27L5 | Some U27L10 -> alu_lite_x
+                          | _ -> raise InvalidEncoding)
+  | Addxd -> 
+      (match encoding with None | Some U6 | Some S10 -> alu_lite 
+                          | Some U27L5 | Some U27L10 -> alu_lite_x
+                          | Some E27U27L10 -> alu_lite_y)
   | Compw -> (match encoding with None -> alu_tiny
                                 | Some U6 | Some S10 | Some U27L5 -> alu_tiny_x
                                 | _ -> raise InvalidEncoding)
@@ -596,10 +625,10 @@ let rec_to_usage r =
                           | Some U27L5 | Some U27L10 -> alu_tiny_x 
                           | Some E27U27L10 -> alu_tiny_y 
                           | _ -> raise InvalidEncoding)
-  | Mulw| Maddw -> (match encoding with None -> mau
+  | Mulw| Maddw | Msbfw -> (match encoding with None -> mau
                                 | Some U6 | Some S10 | Some U27L5 -> mau_x
                                 | _ -> raise InvalidEncoding)
-  | Muld | Maddd -> (match encoding with None | Some U6 | Some S10 -> mau
+  | Muld | Maddd | Msbfd -> (match encoding with None | Some U6 | Some S10 -> mau
                                 | Some U27L5 | Some U27L10 -> mau_x
                                 | Some E27U27L10 -> mau_y)
   | Nop -> alu_nop
@@ -629,10 +658,10 @@ let real_inst_to_latency = function
   | Rorw | Nandw | Norw | Nxorw | Ornw | Andnw
   | Nandd | Nord | Nxord | Ornd | Andnd
   | Addd | Andd | Compd | Ord | Sbfd | Srad | Srsd | Srld | Slld | Xord | Make
-  | Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved
+  | Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved | Addxw | Addxd
         -> 1
   | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4
-  | Mulw | Muld | Maddw | Maddd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *)
+  | Mulw | Muld | Maddw | Maddd | Msbfw | Msbfd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *)
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq | Lo -> 3
   | Sb | Sh | Sw | Sd | Sq | So -> 1 (* See k1c-Optimization.pdf page 19 *)
   | Get -> 1
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp
index 717b0120..4e369e11 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -66,19 +66,39 @@ Definition longofintu (e: expr) :=
 
 (** ** Integer addition and pointer addition *)
 
+Definition addlimm_shllimm sh k2 e1 :=
+  if Compopts.optim_addx tt
+  then
+    match shift1_4_of_z (Int.unsigned sh) with
+    | Some s14 => Eop (Oaddxlimm s14 k2) (e1:::Enil)
+    | None => Eop (Oaddlimm k2) ((Eop (Oshllimm sh) (e1:::Enil)):::Enil)
+    end
+  else Eop (Oaddlimm k2) ((Eop (Oshllimm sh) (e1:::Enil)):::Enil).
+
 Nondetfunction addlimm (n: int64) (e: expr) :=
   if Int64.eq n Int64.zero then e else
   match e with
   | Eop (Olongconst m) Enil => longconst (Int64.add n m)
   | Eop (Oaddrsymbol s m) Enil   =>
-    (if Compopts.optim_fglobaladdroffset tt
+    (if Compopts.optim_globaladdroffset tt
      then Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int64 n) m)) Enil
      else Eop (Oaddlimm n) (e ::: Enil))
   | Eop (Oaddrstack m) Enil      => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int64 n) m)) Enil
   | Eop (Oaddlimm m) (t ::: Enil) => Eop (Oaddlimm(Int64.add n m)) (t ::: Enil)
+  | Eop (Oaddxlimm sh m) (t ::: Enil) => Eop (Oaddxlimm sh (Int64.add n m)) (t ::: Enil)
+  | Eop (Oshllimm sh) (t1:::Enil) => addlimm_shllimm sh n t1
   | _ => Eop (Oaddlimm n) (e ::: Enil)
   end.
 
+Definition addl_shllimm n e1 e2 :=
+  if Compopts.optim_addx tt
+  then
+    match shift1_4_of_z (Int.unsigned n) with
+    | Some s14 => Eop (Oaddxl s14) (e1:::e2:::Enil)
+    | None => Eop Oaddl (e2:::(Eop (Oshllimm n) (e1:::Enil)):::Enil)
+    end
+  else Eop Oaddl (e2:::(Eop (Oshllimm n) (e1:::Enil)):::Enil).
+
 Nondetfunction addl (e1: expr) (e2: expr) :=
   if Archi.splitlong then SplitLong.addl e1 e2 else
   match e1, e2 with
@@ -102,6 +122,10 @@ Nondetfunction addl (e1: expr) (e2: expr) :=
       Eop (Omaddlimm n) (t1:::t2:::Enil)
   | (Eop (Omullimm n) (t2:::Enil)), t1 =>
       Eop (Omaddlimm n) (t1:::t2:::Enil)
+  | (Eop (Oshllimm n) (t1:::Enil)), t2 =>
+    addl_shllimm n t1 t2
+  | t2, (Eop (Oshllimm n) (t1:::Enil)) =>
+    addl_shllimm n t1 t2
   | _, _ => Eop Oaddl (e1:::e2:::Enil)
   end.
 
@@ -118,6 +142,10 @@ Nondetfunction subl (e1: expr) (e2: expr) :=
       addlimm n1 (Eop Osubl (t1:::t2:::Enil))
   | t1, Eop (Oaddlimm n2) (t2:::Enil) =>
       addlimm (Int64.neg n2) (Eop Osubl (t1:::t2:::Enil))
+  | t1, (Eop Omull (t2:::t3:::Enil)) =>
+      Eop Omsubl (t1:::t2:::t3:::Enil)
+  | t1, (Eop (Omullimm n) (t2:::Enil)) =>
+      Eop (Omaddlimm (Int64.neg n)) (t1:::t2:::Enil)
   | _, _ => Eop Osubl (e1:::e2:::Enil)
   end.
 
@@ -225,7 +253,7 @@ Definition mullimm_base (n1: int64) (e2: expr) :=
   | i :: j :: nil =>
       Elet e2 (addl (shllimm (Eletvar 0) i) (shllimm (Eletvar 0) j))
   | _ =>
-      Eop Omull (e2 ::: longconst n1 ::: Enil)
+      Eop (Omullimm n1) (e2 ::: Enil)
   end.
 
 Nondetfunction mullimm (n1: int64) (e2: expr) :=
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 3b724c01..78a2bb31 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -119,6 +119,76 @@ Proof.
 - TrivialExists.
 Qed.
 
+
+Theorem eval_addlimm_shllimm:
+  forall sh k2, unary_constructor_sound (addlimm_shllimm sh k2) (fun x => ExtValues.addxl sh x (Vlong k2)).
+Proof.
+  red; unfold addlimm_shllimm; intros.
+  destruct (Compopts.optim_addx tt).
+  {
+  destruct (shift1_4_of_z (Int.unsigned sh)) as [s14 |] eqn:SHIFT.
+  - TrivialExists. simpl.
+    f_equal.
+    unfold shift1_4_of_z, int_of_shift1_4, z_of_shift1_4 in *.
+    destruct (Z.eq_dec _ _) as [e1|].
+    { replace s14 with SHIFT1 by congruence.
+      destruct x; simpl; trivial.
+      replace (Int.ltu _ _) with true by reflexivity.
+      unfold Int.ltu.
+      rewrite e1.
+      replace (if zlt _ _ then true else false) with true by reflexivity.
+      rewrite <- e1.
+      rewrite Int.repr_unsigned.
+      reflexivity.
+    }
+    destruct (Z.eq_dec _ _) as [e2|].
+    { replace s14 with SHIFT2 by congruence.
+      destruct x; simpl; trivial.
+      replace (Int.ltu _ _) with true by reflexivity.
+      unfold Int.ltu.
+      rewrite e2.
+      replace (if zlt _ _ then true else false) with true by reflexivity.
+      rewrite <- e2.
+      rewrite Int.repr_unsigned.
+      reflexivity.
+    }
+    destruct (Z.eq_dec _ _) as [e3|].
+    { replace s14 with SHIFT3 by congruence.
+      destruct x; simpl; trivial.
+      replace (Int.ltu _ _) with true by reflexivity.
+      unfold Int.ltu.
+      rewrite e3.
+      replace (if zlt _ _ then true else false) with true by reflexivity.
+      rewrite <- e3.
+      rewrite Int.repr_unsigned.
+      reflexivity.
+    }
+    destruct (Z.eq_dec _ _) as [e4|].
+    { replace s14 with SHIFT4 by congruence.
+      destruct x; simpl; trivial.
+      replace (Int.ltu _ _) with true by reflexivity.
+      unfold Int.ltu.
+      rewrite e4.
+      replace (if zlt _ _ then true else false) with true by reflexivity.
+      rewrite <- e4.
+      rewrite Int.repr_unsigned.
+      reflexivity.
+    }
+    discriminate.
+  - unfold addxl. rewrite Val.addl_commut.
+    TrivialExists.
+    repeat (try eassumption; try econstructor).
+    simpl.
+    reflexivity.
+  }
+  { unfold addxl. rewrite Val.addl_commut.
+    TrivialExists.
+    repeat (try eassumption; try econstructor).
+    simpl.
+    reflexivity.
+  }
+Qed.
+
 Theorem eval_addlimm: forall n, unary_constructor_sound (addlimm n) (fun v => Val.addl v (Vlong n)).
 Proof.
   unfold addlimm; intros; red; intros.
@@ -127,7 +197,7 @@ Proof.
   destruct x; simpl; rewrite ?Int64.add_zero, ?Ptrofs.add_zero; auto.
   destruct (addlimm_match a); InvEval.
 - econstructor; split. apply eval_longconst. rewrite Int64.add_commut; auto.
-- destruct (Compopts.optim_fglobaladdroffset _).
+- destruct (Compopts.optim_globaladdroffset _).
   + econstructor; split. EvalOp. simpl; eauto. 
     unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. 
     destruct Archi.ptr64; auto. rewrite Ptrofs.add_commut; auto.
@@ -136,9 +206,58 @@ Proof.
   destruct sp; simpl; auto. destruct Archi.ptr64; auto. 
   rewrite Ptrofs.add_assoc, (Ptrofs.add_commut m0). auto. 
 - subst x. rewrite Val.addl_assoc. rewrite Int64.add_commut. TrivialExists.
+- TrivialExists; simpl. subst x.
+      destruct v1; simpl; trivial.
+      destruct (Int.ltu _ _); simpl; trivial.
+      rewrite Int64.add_assoc. rewrite Int64.add_commut.
+      reflexivity.
+-  pose proof eval_addlimm_shllimm as ADDXL.
+      unfold unary_constructor_sound in ADDXL.
+      unfold addxl in ADDXL.
+      rewrite Val.addl_commut.
+      subst x.
+      apply ADDXL; assumption.
 - TrivialExists.
 Qed.
 
+Lemma eval_addxl: forall n, binary_constructor_sound (addl_shllimm n) (ExtValues.addxl n).
+Proof.
+  red.
+  intros.
+  unfold addl_shllimm.
+  destruct (Compopts.optim_addx tt).
+  {
+  destruct (shift1_4_of_z (Int.unsigned n)) as [s14 |] eqn:SHIFT.
+  - TrivialExists.
+    simpl.
+    f_equal. f_equal.
+    unfold shift1_4_of_z, int_of_shift1_4, z_of_shift1_4 in *.
+    destruct (Z.eq_dec _ _) as [e1|].
+    { replace s14 with SHIFT1 by congruence.
+      rewrite <- e1.
+      apply Int.repr_unsigned. }
+    destruct (Z.eq_dec _ _) as [e2|].
+    { replace s14 with SHIFT2 by congruence.
+      rewrite <- e2.
+      apply Int.repr_unsigned. }
+    destruct (Z.eq_dec _ _) as [e3|].
+    { replace s14 with SHIFT3 by congruence.
+      rewrite <- e3.
+      apply Int.repr_unsigned. }
+    destruct (Z.eq_dec _ _) as [e4|].
+    { replace s14 with SHIFT4 by congruence.
+      rewrite <- e4.
+      apply Int.repr_unsigned. }
+    discriminate.
+    (* Oaddxl *)
+  - TrivialExists;
+      repeat econstructor; eassumption.
+  }
+  { TrivialExists;
+      repeat econstructor; eassumption.
+  }
+Qed.
+
 Theorem eval_addl: binary_constructor_sound addl Val.addl.
 Proof.
   unfold addl. destruct Archi.splitlong eqn:SL. 
@@ -193,6 +312,14 @@ Proof.
   - subst. rewrite Val.addl_commut. TrivialExists.
   - subst. TrivialExists.
   - subst. rewrite Val.addl_commut. TrivialExists.
+  - subst. pose proof eval_addxl as ADDXL.
+    unfold binary_constructor_sound in ADDXL.
+    rewrite Val.addl_commut.
+    apply ADDXL; assumption.
+    (* Oaddxl *)
+  - subst. pose proof eval_addxl as ADDXL.
+    unfold binary_constructor_sound in ADDXL.
+    apply ADDXL; assumption.
   - TrivialExists.
 Qed.
 
@@ -208,6 +335,23 @@ Proof.
 - subst. rewrite Val.subl_addl_l. apply eval_addlimm; EvalOp.
 - subst. rewrite Val.subl_addl_r.
   apply eval_addlimm; EvalOp.
+- TrivialExists. simpl. subst. reflexivity.
+- TrivialExists. simpl. subst.
+  destruct v1; destruct x; simpl; trivial.
+  + f_equal. f_equal.
+    rewrite <- Int64.neg_mul_distr_r.
+    rewrite Int64.sub_add_opp.
+    reflexivity.
+  + destruct (Archi.ptr64) eqn:ARCHI64; simpl; trivial.
+    f_equal. f_equal.
+    rewrite <- Int64.neg_mul_distr_r.
+    rewrite Ptrofs.sub_add_opp.
+    unfold Ptrofs.add.
+    f_equal. f_equal.
+    rewrite (Ptrofs.agree64_neg ARCHI64 (Ptrofs.of_int64 (Int64.mul i n)) (Int64.mul i n)).
+    rewrite (Ptrofs.agree64_of_int ARCHI64  (Int64.neg (Int64.mul i n))).
+    reflexivity.
+    apply (Ptrofs.agree64_of_int ARCHI64).
 - TrivialExists.
 Qed.
 
@@ -371,7 +515,7 @@ Proof.
     auto. }
   generalize (Int64.one_bits'_decomp n); intros D.
   destruct (Int64.one_bits' n) as [ | i [ | j [ | ? ? ]]] eqn:B.
-- apply DEFAULT.
+- TrivialExists.
 - replace (Val.mull x (Vlong n)) with (Val.shll x (Vint i)).
   apply eval_shllimm; auto.
   simpl in D. rewrite D, Int64.add_zero. destruct x; simpl; auto.
@@ -389,7 +533,7 @@ Proof.
   rewrite (Int64.one_bits'_range n) in B2 by (rewrite B; auto with coqlib).
   inv B1; inv B2. simpl in B3; inv B3.
   rewrite Int64.mul_add_distr_r. rewrite <- ! Int64.shl'_mul. auto.
-- apply DEFAULT.
+- TrivialExists.
 Qed.
 
 Theorem eval_mullimm: forall n, unary_constructor_sound (mullimm n) (fun v => Val.mull v (Vlong n)).
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index aac3010e..23d234aa 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -104,6 +104,15 @@ Definition addrstack (ofs: ptrofs) :=
 
 (** ** Integer addition and pointer addition *)
 
+Definition addimm_shlimm sh k2 e1 :=
+  if Compopts.optim_addx tt
+  then
+    match shift1_4_of_z (Int.unsigned sh) with
+    | Some s14 => Eop (Oaddximm s14 k2) (e1:::Enil)
+    | None => Eop (Oaddimm k2) ((Eop (Oshlimm sh) (e1:::Enil)):::Enil)
+    end
+  else Eop (Oaddimm k2) ((Eop (Oshlimm sh) (e1:::Enil)):::Enil).
+
 Nondetfunction addimm (n: int) (e: expr) :=
   if Int.eq n Int.zero then e else
   match e with
@@ -111,9 +120,20 @@ Nondetfunction addimm (n: int) (e: expr) :=
   | Eop (Oaddrsymbol s m) Enil   => Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) Enil
   | Eop (Oaddrstack m) Enil      => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil
   | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil)
+  | Eop (Oaddximm sh m) (t ::: Enil) => Eop (Oaddximm sh (Int.add n m)) (t ::: Enil)
+  | Eop (Oshlimm sh) (t1:::Enil) => addimm_shlimm sh n t1
   | _ => Eop (Oaddimm n) (e ::: Enil)
   end.
 
+Definition add_shlimm n e1 e2 :=
+  if Compopts.optim_addx tt
+  then
+    match shift1_4_of_z (Int.unsigned n) with
+    | Some s14 => Eop (Oaddx s14) (e1:::e2:::Enil)
+    | None => Eop Oadd (e2:::(Eop (Oshlimm n) (e1:::Enil)):::Enil)
+    end
+  else Eop Oadd (e2:::(Eop (Oshlimm n) (e1:::Enil)):::Enil).
+
 Nondetfunction add (e1: expr) (e2: expr) :=
   match e1, e2 with
   | Eop (Ointconst n1) Enil, t2 => addimm n1 t2
@@ -135,7 +155,11 @@ Nondetfunction add (e1: expr) (e2: expr) :=
   | t1, (Eop (Omulimm n) (t2:::Enil)) =>
       Eop (Omaddimm n) (t1:::t2:::Enil)
   | (Eop (Omulimm n) (t2:::Enil)), t1 =>
-      Eop (Omaddimm n) (t1:::t2:::Enil)
+    Eop (Omaddimm n) (t1:::t2:::Enil)
+  | (Eop (Oshlimm n) (t1:::Enil)), t2 =>
+    add_shlimm n t1 t2
+  | t2, (Eop (Oshlimm n) (t1:::Enil)) =>
+    add_shlimm n t1 t2
   | _, _ => Eop Oadd (e1:::e2:::Enil)
   end.
 
@@ -151,6 +175,10 @@ Nondetfunction sub (e1: expr) (e2: expr) :=
       addimm n1 (Eop Osub (t1:::t2:::Enil))
   | t1, Eop (Oaddimm n2) (t2:::Enil) =>
       addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil))
+  | t1, (Eop Omul (t2:::t3:::Enil)) =>
+      Eop Omsub (t1:::t2:::t3:::Enil)
+  | t1, (Eop (Omulimm n) (t2:::Enil)) =>
+      Eop (Omaddimm (Int.neg n)) (t1:::t2:::Enil)
   | _, _ => Eop Osub (e1:::e2:::Enil)
   end.
 
@@ -592,18 +620,26 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   match e with
   | Eop (Oaddrstack n) Enil => (Ainstack n, Enil)
   | Eop (Oaddrsymbol id ofs) Enil =>
-    (if (orb (Archi.pic_code tt) (negb (Compopts.optim_fglobaladdrtmp tt)))
+    (if (orb (Archi.pic_code tt) (negb (Compopts.optim_globaladdrtmp tt)))
      then (Aindexed Ptrofs.zero, e:::Enil)
      else (Aglobal id ofs, Enil))
   | Eop (Oaddimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int n), e1:::Enil)
   | Eop (Oaddlimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int64 n), e1:::Enil)
   | Eop Oaddl (e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil) =>
-    (if Compopts.optim_fxsaddr tt
+    (if Compopts.optim_xsaddr tt
      then let zscale := Int.unsigned scale in
           if Z.eq_dec zscale (zscale_of_chunk chunk)
           then (Aindexed2XS zscale, e1:::e2:::Enil) 
           else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil)
      else (Aindexed2, e1:::(Eop (Oshllimm scale) (e2:::Enil)):::Enil))
+  | Eop (Oaddxl sh) (e1:::e2:::Enil) =>
+    let zscale := ExtValues.z_of_shift1_4 sh in
+    let scale := Int.repr zscale in
+    (if Compopts.optim_xsaddr tt
+     then if Z.eq_dec zscale (zscale_of_chunk chunk)
+          then (Aindexed2XS zscale, e2:::e1:::Enil) 
+          else (Aindexed2, e2:::(Eop (Oshllimm scale) (e1:::Enil)):::Enil)
+     else (Aindexed2, e2:::(Eop (Oshllimm scale) (e1:::Enil)):::Enil))
   | Eop Oaddl (e1:::e2:::Enil) => (Aindexed2, e1:::e2:::Enil) 
   | _ => (Aindexed Ptrofs.zero, e:::Enil)
   end.
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index d22725d5..a5154611 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -183,6 +183,75 @@ Proof.
   auto.
 Qed.
 
+Theorem eval_addimm_shlimm:
+  forall sh k2, unary_constructor_sound (addimm_shlimm sh k2) (fun x => ExtValues.addx sh x (Vint k2)).
+Proof.
+  red; unfold addimm_shlimm; intros.
+  destruct (Compopts.optim_addx tt).
+  {
+  destruct (shift1_4_of_z (Int.unsigned sh)) as [s14 |] eqn:SHIFT.
+  - TrivialExists. simpl.
+    f_equal.
+    unfold shift1_4_of_z, int_of_shift1_4, z_of_shift1_4 in *.
+    destruct (Z.eq_dec _ _) as [e1|].
+    { replace s14 with SHIFT1 by congruence.
+      destruct x; simpl; trivial.
+      replace (Int.ltu _ _) with true by reflexivity.
+      unfold Int.ltu.
+      rewrite e1.
+      replace (if zlt _ _ then true else false) with true by reflexivity.
+      rewrite <- e1.
+      rewrite Int.repr_unsigned.
+      reflexivity.
+    }
+    destruct (Z.eq_dec _ _) as [e2|].
+    { replace s14 with SHIFT2 by congruence.
+      destruct x; simpl; trivial.
+      replace (Int.ltu _ _) with true by reflexivity.
+      unfold Int.ltu.
+      rewrite e2.
+      replace (if zlt _ _ then true else false) with true by reflexivity.
+      rewrite <- e2.
+      rewrite Int.repr_unsigned.
+      reflexivity.
+    }
+    destruct (Z.eq_dec _ _) as [e3|].
+    { replace s14 with SHIFT3 by congruence.
+      destruct x; simpl; trivial.
+      replace (Int.ltu _ _) with true by reflexivity.
+      unfold Int.ltu.
+      rewrite e3.
+      replace (if zlt _ _ then true else false) with true by reflexivity.
+      rewrite <- e3.
+      rewrite Int.repr_unsigned.
+      reflexivity.
+    }
+    destruct (Z.eq_dec _ _) as [e4|].
+    { replace s14 with SHIFT4 by congruence.
+      destruct x; simpl; trivial.
+      replace (Int.ltu _ _) with true by reflexivity.
+      unfold Int.ltu.
+      rewrite e4.
+      replace (if zlt _ _ then true else false) with true by reflexivity.
+      rewrite <- e4.
+      rewrite Int.repr_unsigned.
+      reflexivity.
+    }
+    discriminate.
+  - unfold addx. rewrite Val.add_commut.
+    TrivialExists.
+    repeat (try eassumption; try econstructor).
+    simpl.
+    reflexivity.
+  }
+  { unfold addx. rewrite Val.add_commut.
+    TrivialExists.
+    repeat (try eassumption; try econstructor).
+    simpl.
+    reflexivity.
+    }
+Qed.
+
 Theorem eval_addimm:
   forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)).
 Proof.
@@ -198,9 +267,57 @@ Proof.
     + econstructor; split. EvalOp. simpl; eauto. 
       destruct sp; simpl; auto.
     + TrivialExists; simpl. subst x. rewrite Val.add_assoc. rewrite Int.add_commut. auto.
+    + TrivialExists; simpl. subst x.
+      destruct v1; simpl; trivial.
+      destruct (Int.ltu _ _); simpl; trivial.
+      rewrite Int.add_assoc. rewrite Int.add_commut.
+      reflexivity.
+    + pose proof eval_addimm_shlimm as ADDX.
+      unfold unary_constructor_sound in ADDX.
+      unfold addx in ADDX.
+      rewrite Val.add_commut.
+      subst x.
+      apply ADDX; assumption.
     + TrivialExists.
 Qed.
 
+Lemma eval_addx: forall n, binary_constructor_sound (add_shlimm n) (ExtValues.addx n).
+Proof.
+  red.
+  intros.
+  unfold add_shlimm.
+  destruct (Compopts.optim_addx tt).
+  {
+  destruct (shift1_4_of_z (Int.unsigned n)) as [s14 |] eqn:SHIFT.
+  - TrivialExists.
+    simpl.
+    f_equal. f_equal.
+    unfold shift1_4_of_z, int_of_shift1_4, z_of_shift1_4 in *.
+    destruct (Z.eq_dec _ _) as [e1|].
+    { replace s14 with SHIFT1 by congruence.
+      rewrite <- e1.
+      apply Int.repr_unsigned. }
+    destruct (Z.eq_dec _ _) as [e2|].
+    { replace s14 with SHIFT2 by congruence.
+      rewrite <- e2.
+      apply Int.repr_unsigned. }
+    destruct (Z.eq_dec _ _) as [e3|].
+    { replace s14 with SHIFT3 by congruence.
+      rewrite <- e3.
+      apply Int.repr_unsigned. }
+    destruct (Z.eq_dec _ _) as [e4|].
+    { replace s14 with SHIFT4 by congruence.
+      rewrite <- e4.
+      apply Int.repr_unsigned. }
+    discriminate.
+  - TrivialExists;
+      repeat econstructor; eassumption.
+  }
+  { TrivialExists;
+      repeat econstructor; eassumption.
+  }
+Qed.
+  
 Theorem eval_add: binary_constructor_sound add Val.add.
 Proof.
   red; intros until y.
@@ -238,6 +355,15 @@ Proof.
     subst. TrivialExists.
   - (* Omaddimm rev *)
     subst. rewrite Val.add_commut. TrivialExists.
+    (* Oaddx *)
+  - subst. pose proof eval_addx as ADDX.
+    unfold binary_constructor_sound in ADDX.
+    rewrite Val.add_commut.
+    apply ADDX; assumption.
+    (* Oaddx *)
+  - subst. pose proof eval_addx as ADDX.
+    unfold binary_constructor_sound in ADDX.
+    apply ADDX; assumption.
   - TrivialExists.
 Qed.
 
@@ -251,6 +377,12 @@ Proof.
     apply eval_addimm; EvalOp.
   - subst. rewrite Val.sub_add_l. apply eval_addimm; EvalOp.
   - subst. rewrite Val.sub_add_r. apply eval_addimm; EvalOp.
+  - TrivialExists. simpl. subst. reflexivity.
+  - TrivialExists. simpl. subst.
+    rewrite sub_add_neg.
+    rewrite neg_mul_distr_r.
+    unfold Val.neg.
+    reflexivity.
   - TrivialExists.
 Qed.
 
@@ -1297,7 +1429,7 @@ Proof.
   - exists (v1 :: nil); split. eauto with evalexpr. simpl.
     destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. 
     simpl. auto.
-  - destruct (Compopts.optim_fxsaddr tt).
+  - destruct (Compopts.optim_xsaddr tt).
     + destruct (Z.eq_dec _ _).
       * exists (v1 :: v2 :: nil); split.
         repeat (constructor; auto). simpl. rewrite Int.repr_unsigned. destruct v2; simpl in *; congruence.
@@ -1309,6 +1441,25 @@ Proof.
         repeat (constructor; auto). econstructor.
         repeat (constructor; auto). eassumption. simpl. congruence.
         simpl. congruence.
+  - unfold addxl in *.
+    destruct (Compopts.optim_xsaddr tt).
+    + unfold int_of_shift1_4 in *.
+      destruct (Z.eq_dec _ _).
+      * exists (v0 :: v1 :: nil); split.
+        repeat (constructor; auto). simpl.
+        congruence.
+      * eexists; split.
+        repeat (constructor; auto). eassumption.
+        econstructor.
+        repeat (constructor; auto). eassumption. simpl.
+        reflexivity.
+        simpl. congruence.
+    + eexists; split.
+        repeat (constructor; auto). eassumption.
+        econstructor.
+        repeat (constructor; auto). eassumption. simpl.
+        reflexivity.
+        simpl. unfold int_of_shift1_4 in *. congruence.
   - exists (v1 :: v0 :: nil); split. repeat (constructor; auto). simpl. congruence.
   - exists (v :: nil);  split. eauto with evalexpr. subst. simpl. rewrite Ptrofs.add_zero; auto.
 Qed.
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 96779517..34765726 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -145,6 +145,12 @@ module Target (*: TARGET*) =
       | RA   -> "$ra"
       | _ -> assert false
 
+    let scale_of_shift1_4 = let open ExtValues in function
+      | SHIFT1 -> 2
+      | SHIFT2 -> 4
+      | SHIFT3 -> 8
+      | SHIFT4 -> 16;;
+    
 (* Names of sections *)
 
     let name_of_section = function
@@ -528,8 +534,14 @@ module Target (*: TARGET*) =
 
       | Paddw (rd, rs1, rs2) ->
          fprintf oc "	addw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+      | Paddxw (s14, rd, rs1, rs2) ->
+         fprintf oc "	addx%dw	%a = %a, %a\n" (scale_of_shift1_4 s14)
+           ireg rd ireg rs1 ireg rs2
       | Psubw (rd, rs1, rs2) ->
          fprintf oc "	sbfw	%a = %a, %a\n" ireg rd ireg rs2 ireg rs1
+      | Prevsubxw (s14, rd, rs1, rs2) ->
+         fprintf oc "	subx%dw	%a = %a, %a\n" (scale_of_shift1_4 s14)
+           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) ->
@@ -558,22 +570,30 @@ 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 (s14, rd, rs1, rs2) ->
+         fprintf oc "	addx%dd	%a = %a, %a\n" (scale_of_shift1_4 s14)
+           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;
+      | Prevsubxl (s14, rd, rs1, rs2) ->
+         fprintf oc "	sbfx%dd	%a = %a, %a\n" (scale_of_shift1_4 s14)
+           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
@@ -591,6 +611,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
@@ -610,6 +632,14 @@ 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 (s14, rd, rs, imm) ->
+         fprintf oc "	addx%dw	%a = %a, %a\n"  (scale_of_shift1_4 s14)
+           ireg rd ireg rs coqint imm
+      | Prevsubiw (rd, rs, imm) ->
+         fprintf oc "	sbfw	%a = %a, %a\n" ireg rd ireg rs coqint imm
+      | Prevsubxiw (s14, rd, rs, imm) ->
+         fprintf oc "	sbfx%dw	%a = %a, %a\n"  (scale_of_shift1_4 s14)
+           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) ->
@@ -655,6 +685,14 @@ 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 (s14, rd, rs, imm) ->
+         fprintf oc "	addx%dd	%a = %a, %a\n"  (scale_of_shift1_4 s14)
+           ireg rd ireg rs coqint imm
+      | Prevsubil (rd, rs, imm) ->
+         fprintf oc "	sbfd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+      | Prevsubxil (s14, rd, rs, imm) ->
+         fprintf oc "	sbfx%dd	%a = %a, %a\n"  (scale_of_shift1_4 s14)
+           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;
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 643cca0c..f41dae63 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -161,8 +161,13 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Ocast16signed, v1 :: nil => sign_ext 16 v1
   | Oadd, v1::v2::nil => add v1 v2
   | Oaddimm n, v1::nil => add v1 (I n)
+  | Oaddx shift, v1::v2::nil => add v2 (shl v1 (I (int_of_shift1_4 shift)))
+  | Oaddximm shift n, v1::nil => add (I n) (shl v1 (I (int_of_shift1_4 shift)))
   | Oneg, v1::nil => neg v1
   | Osub, v1::v2::nil => sub v1 v2
+  | Orevsubx shift, v1::v2::nil => sub v2 (shl v1 (I (int_of_shift1_4 shift)))
+  | Orevsubimm n, v1::nil => sub (I n) v1
+  | Orevsubximm shift n, v1::nil => sub (I n) (shl v1 (I (int_of_shift1_4 shift)))
   | Omul, v1::v2::nil => mul v1 v2
   | Omulimm n, v1::nil => mul v1 (I n)
   | Omulhs, v1::v2::nil => mulhs v1 v2
@@ -198,6 +203,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Oshrximm n, v1::nil => shrx v1 (I n)
   | Omadd, v1::v2::v3::nil => add v1 (mul v2 v3)
   | Omaddimm n, v1::v2::nil => add v1 (mul v2 (I n))
+  | Omsub, v1::v2::v3::nil => sub v1 (mul v2 v3)
   | Omakelong, v1::v2::nil => longofwords v1 v2
   | Olowlong, v1::nil => loword v1
   | Ohighlong, v1::nil => hiword v1
@@ -205,8 +211,13 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Ocast32unsigned, v1::nil => longofintu v1
   | Oaddl, v1::v2::nil => addl v1 v2
   | Oaddlimm n, v1::nil => addl v1 (L n)
+  | Oaddxl shift, v1::v2::nil => addl v2 (shll v1 (I (int_of_shift1_4 shift)))
+  | Oaddxlimm shift n, v1::nil => addl (L n) (shll v1 (I (int_of_shift1_4 shift))) 
   | Onegl, v1::nil => negl v1
   | Osubl, v1::v2::nil => subl v1 v2
+  | Orevsubxl shift, v1::v2::nil => subl v2 (shll v1 (I (int_of_shift1_4 shift)))
+  | Orevsublimm n, v1::nil => subl (L n) v1
+  | Orevsubxlimm shift n, v1::nil => subl (L n) (shll v1 (I (int_of_shift1_4 shift)))
   | Omull, v1::v2::nil => mull v1 v2
   | Omullimm n, v1::nil => mull v1 (L n)
   | Omullhs, v1::v2::nil => mullhs v1 v2
@@ -241,6 +252,7 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Oshrxlimm n, v1::nil => shrxl v1 (I n)
   | Omaddl, v1::v2::v3::nil => addl v1 (mull v2 v3)
   | Omaddlimm n, v1::v2::nil => addl v1 (mull v2 (L n))
+  | Omsubl, v1::v2::v3::nil => subl v1 (mull v2 v3)
   | Onegf, v1::nil => negf v1
   | Oabsf, v1::nil => absf v1
   | Oaddf, v1::v2::nil => addf v1 v2
@@ -359,12 +371,46 @@ Theorem eval_static_operation_sound:
   list_forall2 (vmatch bc) vargs aargs ->
   vmatch bc vres (eval_static_operation op aargs).
 Proof.
-  unfold eval_operation, eval_static_operation, eval_static_select, eval_static_selectl, eval_static_selectf, eval_static_selectfs; intros;
+  unfold eval_operation, eval_static_operation, eval_static_select, eval_static_selectl, eval_static_selectf, eval_static_selectfs, addx, revsubx, addxl, revsubxl; intros.
   destruct op; InvHyps; eauto with va.
-  destruct (propagate_float_constants tt); constructor.
-  destruct (propagate_float_constants tt); constructor.
-  rewrite Ptrofs.add_zero_l; eauto with va.
-  apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
+  - destruct (propagate_float_constants tt); constructor.
+  - destruct (propagate_float_constants tt); constructor.
+  - rewrite Ptrofs.add_zero_l; eauto with va.
+  - replace(match Val.shl a1 (Vint (int_of_shift1_4 shift)) with
+    | Vint n2 => Vint (Int.add n n2)
+    | Vptr b2 ofs2 =>
+        if Archi.ptr64
+        then Vundef
+        else Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int n))
+    | _ => Vundef
+    end)  with (Val.add (Vint n) (Val.shl a1 (Vint (int_of_shift1_4 shift)))).
+    + eauto with va.
+    + destruct a1; destruct shift; reflexivity.
+  - (*revsubimm*) inv H1; constructor.
+  - replace (match Val.shl a1 (Vint (int_of_shift1_4 shift)) with
+   | Vint n2 => Vint (Int.sub n n2)
+   | _ => Vundef
+             end) with (Val.sub (Vint n) (Val.shl a1 (Vint (int_of_shift1_4 shift)))).
+    + eauto with va.
+    + destruct n; destruct shift; reflexivity.
+  - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with
+    | Vlong n2 => Vlong (Int64.add n n2)
+    | Vptr b2 ofs2 =>
+        if Archi.ptr64
+        then Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int64 n))
+        else Vundef
+    | _ => Vundef
+             end) with (Val.addl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))).
+    + eauto with va.
+    + destruct a1; destruct shift; reflexivity.
+  - inv H1; constructor.
+  - replace (match Val.shll a1 (Vint (int_of_shift1_4 shift)) with
+    | Vlong n2 => Vlong (Int64.sub n n2)
+    | _ => Vundef
+             end) with (Val.subl (Vlong n) (Val.shll a1 (Vint (int_of_shift1_4 shift)))).
+    + eauto with va.
+    + destruct a1; destruct shift; reflexivity.
+  - apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
   (* select *)
   - assert (Hcond : (cmatch (eval_condition0 cond a2 m) (eval_static_condition0 cond b2))) by (apply eval_static_condition0_sound; assumption).
     rewrite eval_select_to2.
diff --git a/test/monniaux/bitsliced-aes/bs.c b/test/monniaux/bitsliced-aes/bs.c
index 083a8fc5..3132e1d9 100644
--- a/test/monniaux/bitsliced-aes/bs.c
+++ b/test/monniaux/bitsliced-aes/bs.c
@@ -3,7 +3,11 @@
 #include "bs.h"
 #include "../ternary.h"
 
+/* TEMPORARY */
+#define TERNARY(x, v0, v1) ((x) ? (v0) : (v1))
+/*
 #define TERNARY(x, v0, v1) TERNARY64(x, v1, v0)
+*/
 
 #if (defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__) ||\
         defined(__amd64__) || defined(__amd32__)|| defined(__amd16__)