Merge branch 'mppa_postpass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa_postpass

14 files changed, 257 insertions, 18 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 354840d4..8486e25d 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -143,6 +143,8 @@ Inductive instruction : Type :=
   | Pnorw               (rd rs1 rs2: ireg)          (**r nor word *)

   | Pxorw               (rd rs1 rs2: ireg)          (**r xor word *)

   | Pnxorw              (rd rs1 rs2: ireg)          (**r xor word *)

+  | Pandnw              (rd rs1 rs2: ireg)          (**r andn word *)

+  | Pornw               (rd rs1 rs2: ireg)          (**r orn word *)

   | Psraw               (rd rs1 rs2: ireg)          (**r shift right arithmetic word *)

   | Psrlw               (rd rs1 rs2: ireg)          (**r shift right logical word *)

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

@@ -155,6 +157,8 @@ Inductive instruction : Type :=
   | Pnorl               (rd rs1 rs2: ireg)          (**r nor long *)

   | Pxorl               (rd rs1 rs2: ireg)          (**r xor long *)

   | Pnxorl              (rd rs1 rs2: ireg)          (**r nxor long *)

+  | Pandnl              (rd rs1 rs2: ireg)          (**r andn long *)

+  | Pornl               (rd rs1 rs2: ireg)          (**r orn long *)

   | Pmull               (rd rs1 rs2: ireg)          (**r mul long (low part) *)

   | Pslll               (rd rs1 rs2: ireg)          (**r shift left logical long *)

   | Psrll               (rd rs1 rs2: ireg)          (**r shift right logical long *)

@@ -177,6 +181,8 @@ Inductive instruction : Type :=
   | Pnoriw              (rd rs: ireg) (imm: int)    (**r nor imm word *)

   | Pxoriw              (rd rs: ireg) (imm: int)    (**r xor imm word *)

   | Pnxoriw             (rd rs: ireg) (imm: int)    (**r nxor imm word *)

+  | Pandniw             (rd rs: ireg) (imm: int)    (**r andn imm word *)

+  | Porniw              (rd rs: ireg) (imm: int)    (**r orn imm word *)

   | Psraiw              (rd rs: ireg) (imm: int)    (**r shift right arithmetic imm word *)

   | Psrliw              (rd rs: ireg) (imm: int)    (**r shift right logical imm word *)

   | Pslliw              (rd rs: ireg) (imm: int)    (**r shift left logical imm word *)

@@ -194,6 +200,8 @@ Inductive instruction : Type :=
   | Pnoril              (rd rs: ireg) (imm: int64)  (**r and immediate long *) 

   | Pxoril              (rd rs: ireg) (imm: int64)  (**r xor immediate long *)

   | Pnxoril             (rd rs: ireg) (imm: int64)  (**r xor immediate long *)

+  | Pandnil             (rd rs: ireg) (imm: int64)  (**r andn long *)

+  | Pornil              (rd rs: ireg) (imm: int64)  (**r orn long *)

   .

 

 (** Correspondance between Asmblock and Asm *)

@@ -276,6 +284,8 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRR Asmblock.Pnorw rd rs1 rs2       => Pnorw rd rs1 rs2

   | PArithRRR Asmblock.Pxorw rd rs1 rs2       => Pxorw rd rs1 rs2

   | PArithRRR Asmblock.Pnxorw rd rs1 rs2      => Pnxorw rd rs1 rs2

+  | PArithRRR Asmblock.Pandnw rd rs1 rs2      => Pandnw rd rs1 rs2

+  | PArithRRR Asmblock.Pornw rd rs1 rs2       => Pornw rd rs1 rs2

   | PArithRRR Asmblock.Psraw rd rs1 rs2       => Psraw rd rs1 rs2

   | PArithRRR Asmblock.Psrlw rd rs1 rs2       => Psrlw rd rs1 rs2

   | PArithRRR Asmblock.Psllw rd rs1 rs2       => Psllw rd rs1 rs2

@@ -288,6 +298,8 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRR Asmblock.Pnorl rd rs1 rs2       => Pnorl rd rs1 rs2

   | PArithRRR Asmblock.Pxorl rd rs1 rs2       => Pxorl rd rs1 rs2

   | PArithRRR Asmblock.Pnxorl rd rs1 rs2      => Pnxorl rd rs1 rs2

+  | PArithRRR Asmblock.Pandnl rd rs1 rs2      => Pandnl rd rs1 rs2

+  | PArithRRR Asmblock.Pornl rd rs1 rs2       => Pornl rd rs1 rs2

   | PArithRRR Asmblock.Pmull rd rs1 rs2       => Pmull rd rs1 rs2

   | PArithRRR Asmblock.Pslll rd rs1 rs2       => Pslll rd rs1 rs2

   | PArithRRR Asmblock.Psrll rd rs1 rs2       => Psrll rd rs1 rs2

@@ -309,6 +321,8 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRI32 Asmblock.Pnoriw rd rs imm       => Pnoriw rd rs imm

   | PArithRRI32 Asmblock.Pxoriw rd rs imm       => Pxoriw rd rs imm

   | PArithRRI32 Asmblock.Pnxoriw rd rs imm      => Pnxoriw rd rs imm

+  | PArithRRI32 Asmblock.Pandniw rd rs imm      => Pandniw rd rs imm

+  | PArithRRI32 Asmblock.Porniw rd rs imm       => Porniw rd rs imm

   | PArithRRI32 Asmblock.Psraiw rd rs imm       => Psraiw rd rs imm

   | PArithRRI32 Asmblock.Psrliw rd rs imm       => Psrliw rd rs imm

   | PArithRRI32 Asmblock.Pslliw rd rs imm       => Pslliw rd rs imm

@@ -326,6 +340,8 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRI64 Asmblock.Pnoril rd rs imm       => Pnoril rd rs imm

   | PArithRRI64 Asmblock.Pxoril rd rs imm       => Pxoril rd rs imm

   | PArithRRI64 Asmblock.Pnxoril rd rs imm      => Pnxoril rd rs imm

+  | PArithRRI64 Asmblock.Pandnil rd rs imm      => Pandnil rd rs imm

+  | PArithRRI64 Asmblock.Pornil rd rs imm       => Pornil rd rs imm

 

   (** Load *)

   | PLoadRRO Asmblock.Plb rd ra ofs   => Plb rd ra ofs

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 4757b9fc..4f9fc34d 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -344,6 +344,8 @@ Inductive arith_name_rrr : Type :=
   | Pnorw                                           (**r nor word *)
   | Pxorw                                           (**r xor word *)
   | Pnxorw                                          (**r nxor word *)
+  | Pandnw                                          (**r andn word *)
+  | Pornw                                           (**r orn word *)
   | Psraw                                           (**r shift right arithmetic word *)
   | Psrlw                                           (**r shift right logical word *)
   | Psllw                                           (**r shift left logical word *)
@@ -356,6 +358,8 @@ Inductive arith_name_rrr : Type :=
   | Pnorl                                           (**r nor long *)
   | Pxorl                                           (**r xor long *)
   | Pnxorl                                          (**r nxor long *)
+  | Pandnl                                          (**r andn long *)
+  | Pornl                                           (**r orn long *)
   | Pmull                                           (**r mul long (low part) *)
   | Pslll                                           (**r shift left logical long *)
   | Psrll                                           (**r shift right logical long *)
@@ -379,6 +383,8 @@ Inductive arith_name_rri32 : Type :=
   | Pnoriw                                          (**r nor imm word *)
   | Pxoriw                                          (**r xor imm word *)
   | Pnxoriw                                         (**r nxor imm word *)
+  | Pandniw                                         (**r andn word *)
+  | Porniw                                          (**r orn word *)
   | Psraiw                                          (**r shift right arithmetic imm word *)
   | Psrliw                                          (**r shift right logical imm word *)
   | Pslliw                                          (**r shift left logical imm word *)
@@ -397,6 +403,8 @@ Inductive arith_name_rri64 : Type :=
   | Pnoril                                          (**r nor immediate long *) 
   | Pxoril                                          (**r xor immediate long *) 
   | Pnxoril                                         (**r nxor immediate long *) 
+  | Pandnil                                         (**r andn immediate long *)
+  | Pornil                                          (**r orn immediate long *)
 .
 
 Inductive ar_instruction : Type :=
@@ -1109,6 +1117,8 @@ Definition arith_eval_rrr n v1 v2 :=
   | Pnorw  => Val.notint (Val.or v1 v2)
   | Pxorw  => Val.xor  v1 v2
   | Pnxorw => Val.notint (Val.xor v1 v2)
+  | Pandnw => Val.and (Val.notint v1) v2
+  | Pornw  => Val.or (Val.notint v1) v2
   | Psrlw  => Val.shru v1 v2
   | Psraw  => Val.shr  v1 v2
   | Psllw  => Val.shl  v1 v2
@@ -1121,6 +1131,8 @@ Definition arith_eval_rrr n v1 v2 :=
   | Pnorl  => Val.notl (Val.orl  v1 v2)
   | Pxorl  => Val.xorl  v1 v2
   | Pnxorl  => Val.notl (Val.xorl  v1 v2)
+  | Pandnl => Val.andl (Val.notl v1) v2
+  | Pornl  => Val.orl (Val.notl v1) v2
   | Pmull => Val.mull v1 v2
   | Pslll => Val.shll v1 v2
   | Psrll => Val.shrlu v1 v2
@@ -1144,6 +1156,8 @@ Definition arith_eval_rri32 n v i :=
   | Pnoriw  => Val.notint (Val.or v (Vint i))
   | Pxoriw  => Val.xor   v (Vint i)
   | Pnxoriw => Val.notint (Val.xor v (Vint i))
+  | Pandniw => Val.and (Val.notint v) (Vint i)
+  | Porniw  => Val.or (Val.notint v) (Vint i)
   | Psraiw  => Val.shr   v (Vint i)
   | Psrliw  => Val.shru  v (Vint i)
   | Pslliw  => Val.shl   v (Vint i)
@@ -1163,6 +1177,8 @@ Definition arith_eval_rri64 n v i :=
   | Pnoril   => Val.notl (Val.orl  v (Vlong i))
   | Pxoril  => Val.xorl  v (Vlong 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)
   end.
 
 Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset :=
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index b77fa47d..a2d75b27 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1305,6 +1305,8 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring :=
   | Pnorw => "Pnorw"
   | Pxorw => "Pxorw"
   | Pnxorw => "Pnxorw"
+  | Pandnw => "Pandnw"
+  | Pornw => "Pornw"
   | Psraw => "Psraw"
   | Psrlw => "Psrlw"
   | Psllw => "Psllw"
@@ -1316,6 +1318,8 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring :=
   | Pnorl => "Pnorl"
   | Pxorl => "Pxorl"
   | Pnxorl => "Pnxorl"
+  | Pandnl => "Pandnl"
+  | Pornl => "Pornl"
   | Pmull => "Pmull"
   | Pslll => "Pslll"
   | Psrll => "Psrll"
@@ -1338,6 +1342,8 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring :=
   | Pnoriw => "Pnoriw"
   | Pxoriw => "Pxoriw"
   | Pnxoriw => "Pnxoriw"
+  | Pandniw => "Pandniw"
+  | Porniw => "Porniw"
   | Psraiw => "Psraiw"
   | Psrliw => "Psrliw"
   | Pslliw => "Pslliw"
@@ -1357,6 +1363,8 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring :=
   | Pnoril => "Pnoril"
   | Pxoril => "Pxoril"
   | Pnxoril => "Pnxoril"
+  | Pandnil => "Pandnil"
+  | Pornil => "Pornil"
   end.
 
 Definition string_of_arith (op: arith_op): pstring :=
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index f28102f8..4b168eec 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -467,7 +467,22 @@ Definition transl_op
       OK (Pnxorw rd rs1 rs2 ::i k)
   | Onxorimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
-      OK (nxorimm32 rd rs n ::i k)
+        OK (nxorimm32 rd rs n ::i k)
+  | Onot, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+        OK (xorimm32 rd rs Int.mone ::i k)
+  | Oandn, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Pandnw rd rs1 rs2 ::i k)
+  | Oandnimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (Pandniw rd rs n ::i k)
+  | Oorn, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Pornw rd rs1 rs2 ::i k)
+  | Oornimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (Porniw rd rs n ::i k)
   | Oshl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Psllw rd rs1 rs2 ::i k)
@@ -530,6 +545,9 @@ Definition transl_op
   | Odivlu, _ => Error (msg "Asmblockgen.transl_op: Odivlu") (* Géré par fonction externe *)
   | Omodl, _ => Error (msg "Asmblockgen.transl_op: Omodl") (* Géré par fonction externe *)
   | Omodlu, _ => Error (msg "Asmblockgen.transl_op: Omodlu") (* Géré par fonction externe *)
+  | Onotl, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+        OK (xorimm64 rd rs Int64.mone ::i k)
   | Oandl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pandl rd rs1 rs2 ::i k)
@@ -566,6 +584,18 @@ Definition transl_op
   | Onxorlimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (nxorimm64 rd rs n ::i k)
+  | Oandnl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Pandnl rd rs1 rs2 ::i k)
+  | Oandnlimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (Pandnil rd rs n ::i k)
+  | Oornl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Pornl rd rs1 rs2 ::i k)
+  | Oornlimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (Pornil rd rs n ::i k)
   | Oshll, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pslll rd rs1 rs2 ::i k)
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index f7b13cad..12d7a4f7 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -57,6 +57,11 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Oxorimm n => op1 (bitwise nv)
   | Onxor => op2 (bitwise nv)
   | Onxorimm n => op1 (bitwise nv)
+  | Onot => op1 (bitwise nv)
+  | Oandn => op2 (bitwise nv)
+  | Oandnimm n => op1 (andimm nv n)
+  | Oorn => op2 (bitwise nv)
+  | Oornimm n => op1 (orimm nv n)
   | Oshl | Oshr | Oshru => op2 (default nv)
   | Oshlimm n => op1 (shlimm nv n)
   | Oshrimm n => op1 (shrimm nv n)
@@ -85,6 +90,11 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Oxorlimm n => op1 (default nv)
   | Onxorl => op2 (default nv)
   | Onxorlimm n => op1 (default nv)
+  | Onotl => op1 (default nv)
+  | Oandnl => op2 (default nv)
+  | Oandnlimm n => op1 (default nv)
+  | Oornl => op2 (default nv)
+  | Oornlimm n => op1 (default nv)
   | Oshll | Oshrl | Oshrlu => op2 (default nv)
   | Oshllimm n => op1 (default nv)
   | Oshrlimm n => op1 (default nv)
@@ -170,6 +180,11 @@ Proof.
 - apply xor_sound; auto with na.
 - apply notint_sound; apply xor_sound; auto.
 - apply notint_sound; apply xor_sound; auto with na.
+- apply notint_sound; auto.
+- apply and_sound; try apply notint_sound; auto with na.
+- apply andimm_sound; try apply notint_sound; auto with na.
+- apply or_sound; try apply notint_sound; auto with na.
+- apply orimm_sound; try apply notint_sound; auto with na.
 - apply shlimm_sound; auto.
 - apply shrimm_sound; auto.
 - apply shruimm_sound; auto.
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index bf42b65f..04ea8945 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -88,6 +88,11 @@ Inductive operation : Type :=
   | Oxorimm (n: int)         (**r [rd = r1 ^ n] *)
   | Onxor                    (**r [rd = ~(r1 ^ r2)] *)
   | Onxorimm (n: int)        (**r [rd = ~(r1 ^ n)] *)
+  | Onot                     (**r [rd = ~r1] *)
+  | Oandn                    (**r [rd = (~r1) ^ r2] *)
+  | Oandnimm (n: int)        (**r [rd = (~r1) ^ n] *)
+  | Oorn                     (**r [rd = (~r1) | r2] *)
+  | Oornimm (n: int)         (**r [rd = (~r1) | n] *)
   | Oshl                     (**r [rd = r1 << r2] *)
   | Oshlimm (n: int)         (**r [rd = r1 << n] *)
   | Oshr                     (**r [rd = r1 >> r2] (signed) *)
@@ -125,6 +130,11 @@ Inductive operation : Type :=
   | Oxorlimm (n: int64)      (**r [rd = r1 ^ n] *)
   | Onxorl                   (**r [rd = ~(r1 ^ r2)] *)
   | Onxorlimm (n: int64)     (**r [rd = ~(r1 ^ n)] *)
+  | Onotl                    (**r [rd = ~r1] *)
+  | Oandnl                   (**r [rd = (~r1) ^ r2] *)
+  | Oandnlimm (n: int64)     (**r [rd = (~r1) ^ n] *)
+  | Oornl                    (**r [rd = (~r1) | r2] *)
+  | Oornlimm (n: int64)      (**r [rd = (~r1) | n] *)
   | Oshll                    (**r [rd = r1 << r2] *)
   | Oshllimm (n: int)        (**r [rd = r1 << n] *)
   | Oshrl                    (**r [rd = r1 >> r2] (signed) *)
@@ -270,6 +280,11 @@ Definition eval_operation
   | Oxorimm n, v1 :: nil => Some (Val.xor v1 (Vint n))
   | Onxor, v1 :: v2 :: nil => Some (Val.notint (Val.xor v1 v2))
   | Onxorimm n, v1 :: nil => Some (Val.notint (Val.xor v1 (Vint n)))
+  | Onot, v1 :: nil => Some (Val.notint v1)
+  | Oandn, v1 :: v2 :: nil => Some (Val.and (Val.notint v1) v2)
+  | Oandnimm n, v1 :: nil => Some (Val.and (Val.notint v1) (Vint n))
+  | Oorn, v1 :: v2 :: nil => Some (Val.or (Val.notint v1) v2)
+  | Oornimm n, v1 :: nil => Some (Val.or (Val.notint v1) (Vint n))
   | Oshl, v1 :: v2 :: nil => Some (Val.shl v1 v2)
   | Oshlimm n, v1 :: nil => Some (Val.shl v1 (Vint n))
   | Oshr, v1 :: v2 :: nil => Some (Val.shr v1 v2)
@@ -306,6 +321,11 @@ Definition eval_operation
   | Oxorlimm n, v1::nil => Some (Val.xorl v1 (Vlong n))
   | Onxorl, v1::v2::nil => Some(Val.notl (Val.xorl v1 v2))
   | Onxorlimm n, v1::nil => Some(Val.notl (Val.xorl v1 (Vlong n)))
+  | Onotl, v1 :: nil => Some (Val.notl v1)
+  | Oandnl, v1 :: v2 :: nil => Some (Val.andl (Val.notl v1) v2)
+  | Oandnlimm n, v1 :: nil => Some (Val.andl (Val.notl v1) (Vlong n))
+  | Oornl, v1 :: v2 :: nil => Some (Val.orl (Val.notl v1) v2)
+  | Oornlimm n, v1 :: nil => Some (Val.orl (Val.notl v1) (Vlong n))
   | Oshll, v1::v2::nil => Some (Val.shll v1 v2)
   | Oshllimm n, v1::nil => Some (Val.shll v1 (Vint n))
   | Oshrl, v1::v2::nil => Some (Val.shrl v1 v2)
@@ -439,6 +459,11 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Oxorimm _ => (Tint :: nil, Tint)
   | Onxor => (Tint :: Tint :: nil, Tint)
   | Onxorimm _ => (Tint :: nil, Tint)
+  | Onot => (Tint :: nil, Tint)
+  | Oandn => (Tint :: Tint :: nil, Tint)
+  | Oandnimm _ => (Tint :: nil, Tint)
+  | Oorn => (Tint :: Tint :: nil, Tint)
+  | Oornimm _ => (Tint :: nil, Tint)
   | Oshl => (Tint :: Tint :: nil, Tint)
   | Oshlimm _ => (Tint :: nil, Tint)
   | Oshr => (Tint :: Tint :: nil, Tint)
@@ -475,6 +500,11 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Oxorlimm _ => (Tlong :: nil, Tlong)
   | Onxorl => (Tlong :: Tlong :: nil, Tlong)
   | Onxorlimm _ => (Tlong :: nil, Tlong)
+  | Onotl => (Tlong :: nil, Tlong)
+  | Oandnl => (Tlong :: Tlong :: nil, Tlong)
+  | Oandnlimm _ => (Tlong :: nil, Tlong)
+  | Oornl => (Tlong :: Tlong :: nil, Tlong)
+  | Oornlimm _ => (Tlong :: nil, Tlong)
   | Oshll => (Tlong :: Tint :: nil, Tlong)
   | Oshllimm _ => (Tlong :: nil, Tlong)
   | Oshrl => (Tlong :: Tint :: nil, Tlong)
@@ -603,6 +633,14 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* nxor, nxorimm *)
   - destruct v0; destruct v1...
   - destruct v0...
+  (* not *)
+  - destruct v0...
+  (* andn, andnimm *)
+  - destruct v0; destruct v1...
+  - destruct v0...
+  (* orn, ornimm *)
+  - destruct v0; destruct v1...
+  - destruct v0...
   (* shl, shlimm *)
   - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int.iwordsize)...
   - destruct v0; simpl... destruct (Int.ltu n Int.iwordsize)...
@@ -663,6 +701,14 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* nxorl, nxorlimm *)
   - destruct v0; destruct v1...
   - destruct v0...
+  (* notl *)
+  - destruct v0...
+  (* andnl, andnlimm *)
+  - destruct v0; destruct v1...
+  - destruct v0...
+  (* ornl, ornlimm *)
+  - destruct v0; destruct v1...
+  - destruct v0...
   (* shll, shllimm *)
   - destruct v0; destruct v1; simpl... destruct (Int.ltu i0 Int64.iwordsize')...
   - destruct v0; simpl... destruct (Int.ltu n Int64.iwordsize')...
@@ -1085,6 +1131,14 @@ Proof.
   (* nxor, nxorimm *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
+  (* not *)
+  - inv H4; simpl; auto.
+  (* andn, andnimm *)
+  - inv H4; inv H2; simpl; auto.
+  - inv H4; simpl; auto.
+  (* orn, ornimm *)
+  - inv H4; inv H2; simpl; auto.
+  - inv H4; simpl; auto.
   (* shl, shlimm *)
   - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int.iwordsize); auto.
   - inv H4; simpl; auto. destruct (Int.ltu n Int.iwordsize); auto.
@@ -1148,6 +1202,14 @@ Proof.
   (* nxorl, nxorlimm *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
+  (* notl *)
+  - inv H4; simpl; auto.
+  (* andnl, andnlimm *)
+  - inv H4; inv H2; simpl; auto.
+  - inv H4; simpl; auto.
+  (* ornl, ornlimm *)
+  - inv H4; inv H2; simpl; auto.
+  - inv H4; simpl; auto.
   (* shll, shllimm *)
   - inv H4; inv H2; simpl; auto. destruct (Int.ltu i0 Int64.iwordsize'); auto.
   - inv H4; simpl; auto. destruct (Int.ltu n Int64.iwordsize'); auto.
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index 3c242441..ce2fb2ae 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -66,6 +66,8 @@ let arith_rrr_str = function
   | Pnorw -> "Pnorw"
   | Pxorw -> "Pxorw"
   | Pnxorw -> "Pnxorw"
+  | Pandnw -> "Pandnw"
+  | Pornw -> "Pornw"
   | Psraw -> "Psraw"
   | Psrlw -> "Psrlw"
   | Psllw -> "Psllw"
@@ -77,6 +79,8 @@ let arith_rrr_str = function
   | Pnorl -> "Pnorl"
   | Pxorl -> "Pxorl"
   | Pnxorl -> "Pnxorl"
+  | Pandnl -> "Pandnl"
+  | Pornl -> "Pornl"
   | Pmull -> "Pmull"
   | Pslll -> "Pslll"
   | Psrll -> "Psrll"
@@ -97,6 +101,8 @@ let arith_rri32_str = function
   | Pnoriw -> "Pnoriw"
   | Pxoriw -> "Pxoriw"
   | Pnxoriw -> "Pnxoriw"
+  | Pandniw -> "Pandniw"
+  | Porniw -> "Porniw"
   | Psraiw -> "Psraiw"
   | Psrliw -> "Psrliw"
   | Pslliw -> "Pslliw"
@@ -114,6 +120,8 @@ let arith_rri64_str = function
   | Pnoril -> "Pnoril"
   | Pxoril -> "Pxoril"
   | Pnxoril -> "Pnxoril"
+  | Pandnil -> "Pandnil"
+  | Pornil -> "Pornil"
 
 let arith_ri32_str = "Pmake"
 
@@ -390,7 +398,7 @@ type real_instruction =
   (* ALU *) 
   | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Rorw | Xorw
   | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Xord
-  | Nandw | Norw | Nxorw | Nandd | Nord | Nxord                                                      
+  | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd
   | Make | Nop  | Sxwd  | Zxwd
   (* LSU *)
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld
@@ -431,8 +439,12 @@ let ab_inst_to_real = function
   | "Pslll" | "Psllil" -> Slld
   | "Pxorw" | "Pxoriw" -> Xorw
   | "Pnxorw" | "Pnxoriw" -> Nxorw
+  | "Pandnw" | "Pandniw" -> Andnw
+  | "Pornw" | "Porniw" -> Ornw
   | "Pxorl" | "Pxoril" -> Xord
   | "Pnxorl" | "Pnxoril" -> Nxord
+  | "Pandnl" | "Pandnil" -> Andnd
+  | "Pornl" | "Pornil" -> Ornd
   | "Pmake" | "Pmakel" | "Pmakefs" | "Pmakef" | "Ploadsymbol" -> Make
   | "Pnop" | "Pcvtw2l" -> Nop
   | "Psxwd" -> Sxwd
@@ -494,11 +506,11 @@ let rec_to_usage r =
                                   (* I do not know yet in which context Ofslow can be used by CompCert *)
   and real_inst = ab_inst_to_real r.inst
   in match real_inst with
-  | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw | Nxorw -> 
+  | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw | Nxorw | Andnw | Ornw -> 
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | _ -> raise InvalidEncoding)
-  | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord | Nxord -> 
+  | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord | Nxord | Andnd | Ornd -> 
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | Some E27U27L10 -> alu_tiny_y)
@@ -547,7 +559,9 @@ let rec_to_usage r =
 let real_inst_to_latency = function
   | Nop -> 0 (* Only goes through ID *)
   | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw
-  | Rorw | Nandw | Norw | Nxorw | Nandd | Nord | Nxord
+    (* TODO check rorw *)
+  | Rorw | Nandw | Norw | Nxorw | Ornw | Andnw
+  | Nandd | Nord | Nxord | Ornd | Andnd
   | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make
   | Sxwd | Zxwd | Fcompw | Fcompd
         -> 1
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp
index cc266abd..07ebf1a2 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -238,6 +238,7 @@ Nondetfunction andlimm (n1: int64) (e2: expr) :=
       longconst (Int64.and n1 n2)
   | Eop (Oandlimm n2) (t2:::Enil) =>
       Eop (Oandlimm (Int64.and n1 n2)) (t2:::Enil)
+  | Eop Onotl (t2:::Enil) => Eop (Oandnlimm n1) (t2:::Enil)
   | _ =>
       Eop (Oandlimm n1) (e2:::Enil)
   end.
@@ -247,6 +248,8 @@ Nondetfunction andl (e1: expr) (e2: expr) :=
   match e1, e2 with
   | Eop (Olongconst n1) Enil, t2 => andlimm n1 t2
   | t1, Eop (Olongconst n2) Enil => andlimm n2 t1
+  | (Eop Onotl (t1:::Enil)), t2 => Eop Oandnl (t1:::t2:::Enil) 
+  | t1, (Eop Onotl (t2:::Enil)) => Eop Oandnl (t2:::t1:::Enil) 
   | _, _ => Eop Oandl (e1:::e2:::Enil)
   end.
 
@@ -264,6 +267,8 @@ Nondetfunction orl (e1: expr) (e2: expr) :=
   match e1, e2 with
   | Eop (Olongconst n1) Enil, t2 => orlimm n1 t2
   | t1, Eop (Olongconst n2) Enil => orlimm n2 t1
+  | (Eop Onotl (t1:::Enil)), t2 => Eop Oornl (t1:::t2:::Enil) 
+  | t1, (Eop Onotl (t2:::Enil))  => Eop Oornl (t2:::t1:::Enil) 
   | _, _ => Eop Oorl (e1:::e2:::Enil)
   end.
 
@@ -295,7 +300,7 @@ Nondetfunction notl (e: expr) :=
   | Eop (Oorlimm n) (e1:::Enil) => Eop (Onorlimm n) (e1:::Enil)
   | Eop Oxorl (e1:::e2:::Enil) => Eop Onxorl (e1:::e2:::Enil)
   | Eop (Oxorlimm n) (e1:::Enil) => Eop (Onxorlimm n) (e1:::Enil)
-  | _ => xorlimm Int64.mone e
+  | _ => Eop Onotl (e:::Enil) 
   end.
 (* old:  if Archi.splitlong then SplitLong.notl e else xorlimm Int64.mone e. *)
 
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index a8a6bc9c..27681875 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -382,6 +382,7 @@ Proof.
 - econstructor; split. apply eval_longconst. simpl. rewrite Int64.and_commut; auto.
 - TrivialExists. simpl. rewrite Val.andl_assoc. rewrite Int64.and_commut; auto.
 - TrivialExists.
+- TrivialExists.
 Qed.
 
 Theorem eval_andl: binary_constructor_sound andl Val.andl.
@@ -390,6 +391,8 @@ Proof.
   red; intros. destruct (andl_match a b).
 - InvEval. rewrite Val.andl_commut. apply eval_andlimm; auto.
 - InvEval. apply eval_andlimm; auto.
+- (*andn*) InvEval. TrivialExists. simpl. congruence.
+- (*andn reverse*) InvEval. rewrite Val.andl_commut. TrivialExists; simpl. congruence.
 - TrivialExists.
 Qed.
 
@@ -413,6 +416,8 @@ Proof.
   destruct (orl_match a b).
 - InvEval. rewrite Val.orl_commut. apply eval_orlimm; auto.
 - InvEval. apply eval_orlimm; auto.
+- (*orn*) InvEval. TrivialExists; simpl; congruence.
+- (*orn reversed*) InvEval. rewrite Val.orl_commut. TrivialExists; simpl; congruence.
 - TrivialExists.
 Qed.
 
@@ -450,7 +455,7 @@ Proof.
   - TrivialExists; simpl; congruence.
   - TrivialExists; simpl; congruence.
   - TrivialExists; simpl; congruence.
-  - apply eval_xorlimm; assumption.
+  - TrivialExists.
 Qed.
 
 Theorem eval_divls_base: partial_binary_constructor_sound divls_base Val.divls.
diff --git a/mppa_k1c/SelectOp.v b/mppa_k1c/SelectOp.v
index 109d447b..edb07e5f 100644
--- a/mppa_k1c/SelectOp.v
+++ b/mppa_k1c/SelectOp.v
@@ -493,6 +493,7 @@ Nondetfunction andimm (n1: int) (e2: expr) :=
   else match e2 with
   | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.and n1 n2)) Enil
   | Eop (Oandimm n2) (t2:::Enil) => Eop (Oandimm (Int.and n1 n2)) (t2:::Enil)
+  | Eop Onot (t2:::Enil) => Eop (Oandnimm n1) (t2:::Enil)
   | _ => Eop (Oandimm n1) (e2:::Enil)
   end.
 >>
@@ -501,12 +502,14 @@ Nondetfunction andimm (n1: int) (e2: expr) :=
 Inductive andimm_cases: forall (e2: expr), Type :=
   | andimm_case1: forall n2, andimm_cases (Eop (Ointconst n2) Enil)
   | andimm_case2: forall n2 t2, andimm_cases (Eop (Oandimm n2) (t2:::Enil))
+  | andimm_case3: forall t2, andimm_cases (Eop Onot (t2:::Enil))
   | andimm_default: forall (e2: expr), andimm_cases e2.
 
 Definition andimm_match (e2: expr) :=
   match e2 as zz1 return andimm_cases zz1 with
   | Eop (Ointconst n2) Enil => andimm_case1 n2
   | Eop (Oandimm n2) (t2:::Enil) => andimm_case2 n2 t2
+  | Eop Onot (t2:::Enil) => andimm_case3 t2
   | e2 => andimm_default e2
   end.
 
@@ -516,6 +519,8 @@ Definition andimm (n1: int) (e2: expr) :=
       Eop (Ointconst (Int.and n1 n2)) Enil
   | andimm_case2 n2 t2 => (* Eop (Oandimm n2) (t2:::Enil) *) 
       Eop (Oandimm (Int.and n1 n2)) (t2:::Enil)
+  | andimm_case3 t2 => (* Eop Onot (t2:::Enil) *) 
+      Eop (Oandnimm n1) (t2:::Enil)
   | andimm_default e2 =>
       Eop (Oandimm n1) (e2:::Enil)
   end.
@@ -527,6 +532,8 @@ Nondetfunction and (e1: expr) (e2: expr) :=
   match e1, e2 with
   | Eop (Ointconst n1) Enil, t2 => andimm n1 t2
   | t1, Eop (Ointconst n2) Enil => andimm n2 t1
+  | (Eop Onot (t1:::Enil)), t2 => Eop Oandn (t1:::t2:::Enil) 
+  | t1, (Eop Onot (t2:::Enil)) => Eop Oandn (t2:::t1:::Enil) 
   | _, _ => Eop Oand (e1:::e2:::Enil)
   end.
 >>
@@ -535,12 +542,16 @@ Nondetfunction and (e1: expr) (e2: expr) :=
 Inductive and_cases: forall (e1: expr) (e2: expr), Type :=
   | and_case1: forall n1 t2, and_cases (Eop (Ointconst n1) Enil) (t2)
   | and_case2: forall t1 n2, and_cases (t1) (Eop (Ointconst n2) Enil)
+  | and_case3: forall t1 t2, and_cases ((Eop Onot (t1:::Enil))) (t2)
+  | and_case4: forall t1 t2, and_cases (t1) ((Eop Onot (t2:::Enil)))
   | and_default: forall (e1: expr) (e2: expr), and_cases e1 e2.
 
 Definition and_match (e1: expr) (e2: expr) :=
   match e1 as zz1, e2 as zz2 return and_cases zz1 zz2 with
   | Eop (Ointconst n1) Enil, t2 => and_case1 n1 t2
   | t1, Eop (Ointconst n2) Enil => and_case2 t1 n2
+  | (Eop Onot (t1:::Enil)), t2 => and_case3 t1 t2
+  | t1, (Eop Onot (t2:::Enil)) => and_case4 t1 t2
   | e1, e2 => and_default e1 e2
   end.
 
@@ -550,6 +561,10 @@ Definition and (e1: expr) (e2: expr) :=
       andimm n1 t2
   | and_case2 t1 n2 => (* t1, Eop (Ointconst n2) Enil *) 
       andimm n2 t1
+  | and_case3 t1 t2 => (* (Eop Onot (t1:::Enil)), t2 *) 
+      Eop Oandn (t1:::t2:::Enil)
+  | and_case4 t1 t2 => (* t1, (Eop Onot (t2:::Enil)) *) 
+      Eop Oandn (t2:::t1:::Enil)
   | and_default e1 e2 =>
       Eop Oand (e1:::e2:::Enil)
   end.
@@ -563,6 +578,7 @@ Nondetfunction orimm (n1: int) (e2: expr) :=
   else match e2 with
        | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.or n1 n2)) Enil
        | Eop (Oorimm n2) (t2:::Enil) => Eop (Oorimm (Int.or n1 n2)) (t2:::Enil)
+       | Eop Onot (t2:::Enil) => Eop (Oornimm n1) (t2:::Enil)
        | _ => Eop (Oorimm n1) (e2:::Enil)
   end.
 >>
@@ -571,12 +587,14 @@ Nondetfunction orimm (n1: int) (e2: expr) :=
 Inductive orimm_cases: forall (e2: expr), Type :=
   | orimm_case1: forall n2, orimm_cases (Eop (Ointconst n2) Enil)
   | orimm_case2: forall n2 t2, orimm_cases (Eop (Oorimm n2) (t2:::Enil))
+  | orimm_case3: forall t2, orimm_cases (Eop Onot (t2:::Enil))
   | orimm_default: forall (e2: expr), orimm_cases e2.
 
 Definition orimm_match (e2: expr) :=
   match e2 as zz1 return orimm_cases zz1 with
   | Eop (Ointconst n2) Enil => orimm_case1 n2
   | Eop (Oorimm n2) (t2:::Enil) => orimm_case2 n2 t2
+  | Eop Onot (t2:::Enil) => orimm_case3 t2
   | e2 => orimm_default e2
   end.
 
@@ -586,6 +604,8 @@ Definition orimm (n1: int) (e2: expr) :=
       Eop (Ointconst (Int.or n1 n2)) Enil
   | orimm_case2 n2 t2 => (* Eop (Oorimm n2) (t2:::Enil) *) 
       Eop (Oorimm (Int.or n1 n2)) (t2:::Enil)
+  | orimm_case3 t2 => (* Eop Onot (t2:::Enil) *) 
+      Eop (Oornimm n1) (t2:::Enil)
   | orimm_default e2 =>
       Eop (Oorimm n1) (e2:::Enil)
   end.
@@ -611,6 +631,8 @@ Nondetfunction or (e1: expr) (e2: expr) :=
       if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2
       then Eop (Ororimm n2) (t1:::Enil)
       else Eop Oor (e1:::e2:::Enil)
+  | (Eop Onot (t1:::Enil)), t2 => Eop Oorn (t1:::t2:::Enil) 
+  | t1, (Eop Onot (t2:::Enil))  => Eop Oorn (t2:::t1:::Enil) 
   | _, _ => Eop Oor (e1:::e2:::Enil)
   end.
 >>
@@ -621,6 +643,8 @@ Inductive or_cases: forall (e1: expr) (e2: expr), Type :=
   | or_case2: forall t1 n2, or_cases (t1) (Eop (Ointconst n2) Enil)
   | or_case3: forall n1 t1 n2 t2, or_cases (Eop (Oshlimm n1) (t1:::Enil)) (Eop (Oshruimm n2) (t2:::Enil))
   | or_case4: forall n2 t2 n1 t1, or_cases (Eop (Oshruimm n2) (t2:::Enil)) (Eop (Oshlimm n1) (t1:::Enil))
+  | or_case5: forall t1 t2, or_cases ((Eop Onot (t1:::Enil))) (t2)
+  | or_case6: forall t1 t2, or_cases (t1) ((Eop Onot (t2:::Enil)))
   | or_default: forall (e1: expr) (e2: expr), or_cases e1 e2.
 
 Definition or_match (e1: expr) (e2: expr) :=
@@ -629,6 +653,8 @@ Definition or_match (e1: expr) (e2: expr) :=
   | t1, Eop (Ointconst n2) Enil => or_case2 t1 n2
   | Eop (Oshlimm n1) (t1:::Enil), Eop (Oshruimm n2) (t2:::Enil) => or_case3 n1 t1 n2 t2
   | Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) => or_case4 n2 t2 n1 t1
+  | (Eop Onot (t1:::Enil)), t2 => or_case5 t1 t2
+  | t1, (Eop Onot (t2:::Enil)) => or_case6 t1 t2
   | e1, e2 => or_default e1 e2
   end.
 
@@ -642,6 +668,10 @@ Definition or (e1: expr) (e2: expr) :=
       if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2 then Eop (Ororimm n2) (t1:::Enil) else Eop Oor (e1:::e2:::Enil)
   | or_case4 n2 t2 n1 t1 => (* Eop (Oshruimm n2) (t2:::Enil), Eop (Oshlimm n1) (t1:::Enil) *) 
       if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2 then Eop (Ororimm n2) (t1:::Enil) else Eop Oor (e1:::e2:::Enil)
+  | or_case5 t1 t2 => (* (Eop Onot (t1:::Enil)), t2 *) 
+      Eop Oorn (t1:::t2:::Enil)
+  | or_case6 t1 t2 => (* t1, (Eop Onot (t2:::Enil)) *) 
+      Eop Oorn (t2:::t1:::Enil)
   | or_default e1 e2 =>
       Eop Oor (e1:::e2:::Enil)
   end.
@@ -730,7 +760,7 @@ Nondetfunction notint (e: expr) :=
   | Eop (Oorimm n) (e1:::Enil) => Eop (Onorimm n) (e1:::Enil)
   | Eop Oxor (e1:::e2:::Enil) => Eop Onxor (e1:::e2:::Enil)
   | Eop (Oxorimm n) (e1:::Enil) => Eop (Onxorimm n) (e1:::Enil)
-  | _ => xorimm Int.mone e
+  | _ => Eop Onot (e:::Enil)
   end.
 >>
 *)
@@ -770,7 +800,7 @@ Definition notint (e: expr) :=
   | notint_case6 n e1 => (* Eop (Oxorimm n) (e1:::Enil) *) 
       Eop (Onxorimm n) (e1:::Enil)
   | notint_default e =>
-      xorimm Int.mone e
+      Eop Onot (e:::Enil)
   end.
 
 
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index a45e3403..7ec694e2 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -216,6 +216,7 @@ Nondetfunction andimm (n1: int) (e2: expr) :=
   else match e2 with
   | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.and n1 n2)) Enil
   | Eop (Oandimm n2) (t2:::Enil) => Eop (Oandimm (Int.and n1 n2)) (t2:::Enil)
+  | Eop Onot (t2:::Enil) => Eop (Oandnimm n1) (t2:::Enil)
   | _ => Eop (Oandimm n1) (e2:::Enil)
   end.
 
@@ -223,6 +224,8 @@ Nondetfunction and (e1: expr) (e2: expr) :=
   match e1, e2 with
   | Eop (Ointconst n1) Enil, t2 => andimm n1 t2
   | t1, Eop (Ointconst n2) Enil => andimm n2 t1
+  | (Eop Onot (t1:::Enil)), t2 => Eop Oandn (t1:::t2:::Enil) 
+  | t1, (Eop Onot (t2:::Enil)) => Eop Oandn (t2:::t1:::Enil) 
   | _, _ => Eop Oand (e1:::e2:::Enil)
   end.
 
@@ -232,6 +235,7 @@ Nondetfunction orimm (n1: int) (e2: expr) :=
   else match e2 with
        | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.or n1 n2)) Enil
        | Eop (Oorimm n2) (t2:::Enil) => Eop (Oorimm (Int.or n1 n2)) (t2:::Enil)
+       | Eop Onot (t2:::Enil) => Eop (Oornimm n1) (t2:::Enil)
        | _ => Eop (Oorimm n1) (e2:::Enil)
   end.
 
@@ -253,6 +257,8 @@ Nondetfunction or (e1: expr) (e2: expr) :=
       if Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2
       then Eop (Ororimm n2) (t1:::Enil)
       else Eop Oor (e1:::e2:::Enil)
+  | (Eop Onot (t1:::Enil)), t2 => Eop Oorn (t1:::t2:::Enil) 
+  | t1, (Eop Onot (t2:::Enil))  => Eop Oorn (t2:::t1:::Enil) 
   | _, _ => Eop Oor (e1:::e2:::Enil)
   end.
 
@@ -283,7 +289,7 @@ Nondetfunction notint (e: expr) :=
   | Eop (Oorimm n) (e1:::Enil) => Eop (Onorimm n) (e1:::Enil)
   | Eop Oxor (e1:::e2:::Enil) => Eop Onxor (e1:::e2:::Enil)
   | Eop (Oxorimm n) (e1:::Enil) => Eop (Onxorimm n) (e1:::Enil)
-  | _ => xorimm Int.mone e
+  | _ => Eop Onot (e:::Enil)
   end.
 
 (** ** Integer division and modulus *)
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 73b345d3..57cd3d58 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -422,6 +422,7 @@ Proof.
   case (andimm_match a); intros.
   - InvEval. TrivialExists. simpl. rewrite Int.and_commut; auto.
   - InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists.
+  - InvEval. TrivialExists. simpl; congruence.
   - TrivialExists.
 Qed.
 
@@ -430,6 +431,8 @@ Proof.
   red; intros until y; unfold and; case (and_match a b); intros; InvEval.
   - rewrite Val.and_commut. apply eval_andimm; auto.
   - apply eval_andimm; auto.
+  - (*andn*) TrivialExists; simpl; congruence.
+  - (*andn reverse*) rewrite Val.and_commut. TrivialExists; simpl; congruence.
   - TrivialExists.
 Qed.
 
@@ -449,6 +452,7 @@ Proof.
   destruct (orimm_match a); intros; InvEval.
   - TrivialExists. simpl. rewrite Int.or_commut; auto.
   - subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists.
+  - InvEval. TrivialExists. simpl; congruence.
   - TrivialExists.
 Qed.
 
@@ -493,6 +497,8 @@ Proof.
     destruct (same_expr_pure t1 t2) eqn:?; auto.
     InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst.
     exists (Val.ror v1 (Vint n2)); split. EvalOp. rewrite Val.or_commut. apply ROR; auto.
+  - (*orn*) TrivialExists; simpl; congruence.
+  - (*orn reversed*) rewrite Val.or_commut. TrivialExists; simpl; congruence.
   - apply DEFAULT.
 Qed.
 
@@ -526,14 +532,14 @@ Theorem eval_notint: unary_constructor_sound notint Val.notint.
 Proof.
   assert (forall v, Val.lessdef (Val.notint (Val.notint v)) v).
     destruct v; simpl; auto. rewrite Int.not_involutive; auto.
-  unfold notint; red; intros until x; case (notint_match a); intros; InvEval.
-  - TrivialExists; simpl; congruence.
-  - TrivialExists; simpl; congruence.
-  - TrivialExists; simpl; congruence.
-  - TrivialExists; simpl; congruence.
-  - TrivialExists; simpl; congruence.
-  - TrivialExists; simpl; congruence.
-  - apply eval_xorimm; assumption.
+    unfold notint; red; intros until x; case (notint_match a); intros; InvEval.
+    - TrivialExists; simpl; congruence.
+    - TrivialExists; simpl; congruence.
+    - TrivialExists; simpl; congruence.
+    - TrivialExists; simpl; congruence.
+    - TrivialExists; simpl; congruence.
+    - TrivialExists; simpl; congruence.
+    - TrivialExists.
 Qed.
 
 Theorem eval_divs_base:
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index d30d62a2..511537ce 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -380,6 +380,10 @@ module Target (*: TARGET*) =
          fprintf oc "	xorw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Pnxorw (rd, rs1, rs2) -> 
          fprintf oc "	nxorw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+      | Pandnw (rd, rs1, rs2) -> 
+         fprintf oc "	andnw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+      | Pornw (rd, rs1, rs2) -> 
+         fprintf oc "	ornw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Psraw (rd, rs1, rs2) ->
          fprintf oc "	sraw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Psrlw (rd, rs1, rs2) ->
@@ -403,6 +407,10 @@ module Target (*: TARGET*) =
          fprintf oc "	xord	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Pnxorl (rd, rs1, rs2) -> assert Archi.ptr64;
          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
+      | Pornl (rd, rs1, rs2) -> 
+         fprintf oc "	ornd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Pmull (rd, rs1, rs2) ->
          fprintf oc "	muld	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Pslll  (rd, rs1, rs2) ->
@@ -442,6 +450,10 @@ module Target (*: TARGET*) =
          fprintf oc "	xorw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Pnxoriw (rd, rs, imm) -> 
          fprintf oc "	nxorw	%a = %a, %a\n" ireg rd ireg rs coqint imm
+      | Pandniw (rd, rs, imm) -> 
+         fprintf oc "	andnw	%a = %a, %a\n" ireg rd ireg rs coqint imm
+      | Porniw (rd, rs, imm) -> 
+         fprintf oc "	ornw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Psraiw (rd, rs, imm) ->
          fprintf oc "	sraw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Psrliw (rd, rs, imm) ->
@@ -475,6 +487,10 @@ module Target (*: TARGET*) =
          fprintf oc "	xord	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
       | Pnxoril (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	nxord	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+      | Pandnil (rd, rs, imm) -> 
+         fprintf oc "	andnd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+      | Pornil (rd, rs, imm) -> 
+         fprintf oc "	ornd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
 
     let get_section_names name =
       let (text, lit) =
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 33f4d8a9..57676b35 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -75,6 +75,11 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Oxorimm n, v1::nil => xor v1 (I n)
   | Onxor, v1::v2::nil => notint (xor v1 v2)
   | Onxorimm n, v1::nil => notint (xor v1 (I n))
+  | Onot, v1::nil => notint v1
+  | Oandn, v1::v2::nil => and (notint v1) v2
+  | Oandnimm n, v1::nil => and (notint v1) (I n)
+  | Oorn, v1::v2::nil => or (notint v1) v2
+  | Oornimm n, v1::nil => or (notint v1) (I n)
   | Oshl, v1::v2::nil => shl v1 v2
   | Oshlimm n, v1::nil => shl v1 (I n)
   | Oshr, v1::v2::nil => shr v1 v2
@@ -111,6 +116,11 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Oxorlimm n, v1::nil => xorl v1 (L n)
   | Onxorl, v1::v2::nil => notl (xorl v1 v2)
   | Onxorlimm n, v1::nil => notl (xorl v1 (L n))
+  | Onotl, v1::nil => notl v1
+  | Oandnl, v1::v2::nil => andl (notl v1) v2
+  | Oandnlimm n, v1::nil => andl (notl v1) (L n)
+  | Oornl, v1::v2::nil => orl (notl v1) v2
+  | Oornlimm n, v1::nil => orl (notl v1) (L n)
   | Oshll, v1::v2::nil => shll v1 v2
   | Oshllimm n, v1::nil => shll v1 (I n)
   | Oshrl, v1::v2::nil => shrl v1 v2