long nand, nor, nxor

11 files changed, 144 insertions, 7 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 2fd46689..354840d4 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -150,8 +150,11 @@ Inductive instruction : Type :=
   | Paddl               (rd rs1 rs2: ireg)          (**r add long *)

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

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

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

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

+  | Pnorl               (rd rs1 rs2: ireg)          (**r nor long *)

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

+  | Pnxorl              (rd rs1 rs2: ireg)          (**r nxor 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 *)

@@ -186,8 +189,11 @@ Inductive instruction : Type :=
   | Pcompil (it: itest) (rd rs: ireg) (imm: int64)  (**r comparison imm long *)

   | Paddil              (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 *) 

   | Poril               (rd rs: ireg) (imm: int64)  (**r or immediate long *) 

+  | 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 *)

   .

 

 (** Correspondance between Asmblock and Asm *)

@@ -277,8 +283,11 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRR Asmblock.Paddl rd rs1 rs2       => Paddl rd rs1 rs2

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

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

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

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

+  | 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.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

@@ -312,8 +321,11 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRI64 (Asmblock.Pcompil it) rd rs imm => Pcompil it rd rs imm

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

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

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

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

+  | 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

 

   (** Load *)

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

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 6e55b074..5279bd29 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -350,8 +350,11 @@ Inductive arith_name_rrr : Type :=
   | Paddl                                           (**r add long *)
   | Psubl                                           (**r sub long *)
   | Pandl                                           (**r and long *)
+  | Pnandl                                          (**r nand long *)
   | Porl                                            (**r or long *)
+  | Pnorl                                           (**r nor long *)
   | Pxorl                                           (**r xor long *)
+  | Pnxorl                                          (**r nxor long *)
   | Pmull                                           (**r mul long (low part) *)
   | Pslll                                           (**r shift left logical long *)
   | Psrll                                           (**r shift right logical long *)
@@ -388,8 +391,11 @@ Inductive arith_name_rri64 : Type :=
   | Pcompil (it: itest)                             (**r comparison imm long *)
   | Paddil                                          (**r add immediate long *) 
   | Pandil                                          (**r and immediate long *) 
+  | Pnandil                                         (**r nand immediate long *) 
   | Poril                                           (**r or immediate long *) 
+  | Pnoril                                          (**r nor immediate long *) 
   | Pxoril                                          (**r xor immediate long *) 
+  | Pnxoril                                         (**r nxor immediate long *) 
 .
 
 Inductive ar_instruction : Type :=
@@ -1109,8 +1115,11 @@ Definition arith_eval_rrr n v1 v2 :=
   | Paddl => Val.addl v1 v2
   | Psubl => Val.subl v1 v2
   | Pandl => Val.andl v1 v2
+  | Pnandl => Val.notl (Val.andl v1 v2)
   | Porl  => Val.orl  v1 v2
+  | Pnorl  => Val.notl (Val.orl  v1 v2)
   | Pxorl  => Val.xorl  v1 v2
+  | Pnxorl  => Val.notl (Val.xorl  v1 v2)
   | Pmull => Val.mull v1 v2
   | Pslll => Val.shll v1 v2
   | Psrll => Val.shrlu v1 v2
@@ -1148,8 +1157,11 @@ Definition arith_eval_rri64 n v i :=
   | Pcompil c => compare_long c v (Vlong i)
   | Paddil  => Val.addl v (Vlong i)
   | Pandil  => Val.andl v (Vlong i)
+  | Pnandil  => Val.notl (Val.andl v (Vlong i))
   | Poril   => Val.orl  v (Vlong i)
+  | Pnoril   => Val.notl (Val.orl  v (Vlong i))
   | Pxoril  => Val.xorl  v (Vlong i)
+  | Pnxoril  => Val.notl (Val.xorl  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 9266a09b..c5b5bd56 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1311,8 +1311,11 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring :=
   | Paddl => "Paddl"
   | Psubl => "Psubl"
   | Pandl => "Pandl"
+  | Pnandl => "Pnandl"
   | Porl => "Porl"
+  | Pnorl => "Pnorl"
   | Pxorl => "Pxorl"
+  | Pnxorl => "Pnxorl"
   | Pmull => "Pmull"
   | Pslll => "Pslll"
   | Psrll => "Psrll"
@@ -1349,8 +1352,11 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring :=
     Pcompil _ => "Pcompil"
   | Paddil => "Paddil"
   | Pandil => "Pandil"
+  | Pnandil => "Pnandil"
   | Poril => "Poril"
+  | Pnoril => "Pnoril"
   | Pxoril => "Pxoril"
+  | Pnxoril => "Pnxoril"
   end.
 
 Definition string_of_arith (op: arith_op): pstring :=
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index f32d14bb..9d682bed 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -112,6 +112,9 @@ Definition addimm64 := opimm64 Paddl Paddil.
 Definition orimm64  := opimm64 Porl  Poril.
 Definition andimm64 := opimm64 Pandl Pandil.
 Definition xorimm64 := opimm64 Pxorl  Pxoril.
+Definition norimm64  := opimm64 Pnorl  Pnoril.
+Definition nandimm64 := opimm64 Pnandl Pnandil.
+Definition nxorimm64 := opimm64 Pnxorl  Pnxoril.
 
 (*
 Definition sltimm64 := opimm64 Psltl Psltil.
@@ -535,18 +538,36 @@ Definition transl_op
   | Oandlimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (andimm64 rd rs n ::i k)
+  | Onandl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Pnandl rd rs1 rs2 ::i k)
+  | Onandlimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (nandimm64 rd rs n ::i k)
   | Oorl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Porl rd rs1 rs2 ::i k)
   | Oorlimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (orimm64 rd rs n ::i k)
+  | Onorl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Pnorl rd rs1 rs2 ::i k)
+  | Onorlimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (norimm64 rd rs n ::i k)
   | Oxorl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pxorl rd rs1 rs2 ::i k)
   | Oxorlimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (xorimm64 rd rs n ::i k)
+  | Onxorl, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Pnxorl rd rs1 rs2 ::i k)
+  | Onxorlimm n, a1 :: nil =>
+      do rd  <- ireg_of res; do rs <- ireg_of a1;
+      OK (nxorimm64 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 b8f120f5..f7b13cad 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -75,10 +75,16 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Omullhs | Omullhu | Odivl | Odivlu | Omodl | Omodlu => op2 (default nv)
   | Oandl => op2 (default nv)
   | Oandlimm n => op1 (default nv)
+  | Onandl => op2 (default nv)
+  | Onandlimm n => op1 (default nv)
   | Oorl => op2 (default nv)
   | Oorlimm n => op1 (default nv)
+  | Onorl => op2 (default nv)
+  | Onorlimm n => op1 (default nv)
   | Oxorl => op2 (default nv)
   | Oxorlimm n => op1 (default nv)
+  | Onxorl => op2 (default nv)
+  | Onxorlimm n => op1 (default nv)
   | Oshll | Oshrl | Oshrlu => op2 (default nv)
   | Oshllimm n => op1 (default nv)
   | Oshrlimm n => op1 (default nv)
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index a67fa27f..bf42b65f 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -115,10 +115,16 @@ Inductive operation : Type :=
   | Omodlu                   (**r [rd = r1 % r2] (unsigned) *)
   | Oandl                    (**r [rd = r1 & r2] *)
   | Oandlimm (n: int64)      (**r [rd = r1 & n] *)
+  | Onandl                   (**r [rd = ~(r1 & r2)] *)
+  | Onandlimm (n: int64)     (**r [rd = ~(r1 & n)] *)
   | Oorl                     (**r [rd = r1 | r2] *)
   | Oorlimm (n: int64)       (**r [rd = r1 | n] *)
+  | Onorl                    (**r [rd = ~(r1 | r2)] *)
+  | Onorlimm (n: int64)      (**r [rd = ~(r1 | n)] *)
   | Oxorl                    (**r [rd = r1 ^ r2] *)
   | Oxorlimm (n: int64)      (**r [rd = r1 ^ n] *)
+  | Onxorl                   (**r [rd = ~(r1 ^ r2)] *)
+  | Onxorlimm (n: int64)     (**r [rd = ~(r1 ^ n)] *)
   | Oshll                    (**r [rd = r1 << r2] *)
   | Oshllimm (n: int)        (**r [rd = r1 << n] *)
   | Oshrl                    (**r [rd = r1 >> r2] (signed) *)
@@ -290,10 +296,16 @@ Definition eval_operation
   | Omodlu, v1::v2::nil => Val.modlu v1 v2
   | Oandl, v1::v2::nil => Some(Val.andl v1 v2)
   | Oandlimm n, v1::nil => Some (Val.andl v1 (Vlong n))
+  | Onandl, v1::v2::nil => Some(Val.notl (Val.andl v1 v2))
+  | Onandlimm n, v1::nil => Some(Val.notl (Val.andl v1 (Vlong n)))
   | Oorl, v1::v2::nil => Some(Val.orl v1 v2)
   | Oorlimm n, v1::nil => Some (Val.orl v1 (Vlong n))
+  | Onorl, v1::v2::nil => Some(Val.notl (Val.orl v1 v2))
+  | Onorlimm n, v1::nil => Some(Val.notl (Val.orl v1 (Vlong n)))
   | Oxorl, v1::v2::nil => Some(Val.xorl v1 v2)
   | 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)))
   | 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)
@@ -453,10 +465,16 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Omodlu => (Tlong :: Tlong :: nil, Tlong)
   | Oandl => (Tlong :: Tlong :: nil, Tlong)
   | Oandlimm _ => (Tlong :: nil, Tlong)
+  | Onandl => (Tlong :: Tlong :: nil, Tlong)
+  | Onandlimm _ => (Tlong :: nil, Tlong)
   | Oorl => (Tlong :: Tlong :: nil, Tlong)
   | Oorlimm _ => (Tlong :: nil, Tlong)
+  | Onorl => (Tlong :: Tlong :: nil, Tlong)
+  | Onorlimm _ => (Tlong :: nil, Tlong)
   | Oxorl => (Tlong :: Tlong :: nil, Tlong)
   | Oxorlimm _ => (Tlong :: nil, Tlong)
+  | Onxorl => (Tlong :: Tlong :: nil, Tlong)
+  | Onxorlimm _ => (Tlong :: nil, Tlong)
   | Oshll => (Tlong :: Tint :: nil, Tlong)
   | Oshllimm _ => (Tlong :: nil, Tlong)
   | Oshrl => (Tlong :: Tint :: nil, Tlong)
@@ -630,12 +648,21 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* andl, andlimm *)
   - destruct v0; destruct v1...
   - destruct v0...
+  (* nandl, nandlimm *)
+  - destruct v0; destruct v1...
+  - destruct v0...
   (* orl, orlimm *)
   - destruct v0; destruct v1...
   - destruct v0...
+  (* norl, norlimm *)
+  - destruct v0; destruct v1...
+  - destruct v0...
   (* xorl, xorlimm *)
   - destruct v0; destruct v1...
   - destruct v0...
+  (* nxorl, nxorlimm *)
+  - 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')...
@@ -1106,12 +1133,21 @@ Proof.
   (* andl, andlimm *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
+  (* nandl, nandlimm *)
+  - inv H4; inv H2; simpl; auto.
+  - inv H4; simpl; auto.
   (* orl, orlimm *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
+  (* norl, norlimm *)
+  - inv H4; inv H2; simpl; auto.
+  - inv H4; simpl; auto.
   (* xorl, xorlimm *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
+  (* nxorl, nxorlimm *)
+  - 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 2d25c281..3c242441 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -72,8 +72,11 @@ let arith_rrr_str = function
   | Paddl -> "Paddl"
   | Psubl -> "Psubl"
   | Pandl -> "Pandl"
+  | Pnandl -> "Pnandl"
   | Porl -> "Porl"
+  | Pnorl -> "Pnorl"
   | Pxorl -> "Pxorl"
+  | Pnxorl -> "Pnxorl"
   | Pmull -> "Pmull"
   | Pslll -> "Pslll"
   | Psrll -> "Psrll"
@@ -106,8 +109,11 @@ let arith_rri64_str = function
   | Pcompil it -> "Pcompil"
   | Paddil -> "Paddil"
   | Pandil -> "Pandil"
+  | Pnandil -> "Pnandil"
   | Poril -> "Poril"
+  | Pnoril -> "Pnoril"
   | Pxoril -> "Pxoril"
+  | Pnxoril -> "Pnxoril"
 
 let arith_ri32_str = "Pmake"
 
@@ -384,7 +390,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                                                        
+  | Nandw | Norw | Nxorw | Nandd | Nord | Nxord                                                      
   | Make | Nop  | Sxwd  | Zxwd
   (* LSU *)
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld
@@ -403,6 +409,7 @@ let ab_inst_to_real = function
   | "Pandw" | "Pandiw" -> Andw
   | "Pnandw" | "Pnandiw" -> Nandw
   | "Pandl" | "Pandil" -> Andd
+  | "Pnandl" | "Pnandil" -> Nandd
   | "Pcompw" | "Pcompiw" -> Compw
   | "Pcompl" | "Pcompil" -> Compd
   | "Pfcompw" -> Fcompw
@@ -412,6 +419,7 @@ let ab_inst_to_real = function
   | "Porw" | "Poriw" -> Orw
   | "Pnorw" | "Pnoriw" -> Norw
   | "Porl" | "Poril" -> Ord
+  | "Pnorl" | "Pnoril" -> Nord
   | "Psubw" | "Pnegw" -> Sbfw
   | "Psubl" | "Pnegl" -> Sbfd
   | "Psraw" | "Psraiw" -> Sraw
@@ -424,6 +432,7 @@ let ab_inst_to_real = function
   | "Pxorw" | "Pxoriw" -> Xorw
   | "Pnxorw" | "Pnxoriw" -> Nxorw
   | "Pxorl" | "Pxoril" -> Xord
+  | "Pnxorl" | "Pnxoril" -> Nxord
   | "Pmake" | "Pmakel" | "Pmakefs" | "Pmakef" | "Ploadsymbol" -> Make
   | "Pnop" | "Pcvtw2l" -> Nop
   | "Psxwd" -> Sxwd
@@ -489,7 +498,7 @@ let rec_to_usage r =
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | _ -> raise InvalidEncoding)
-  | Addd | Andd | Ord | Sbfd | Xord -> 
+  | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord | Nxord -> 
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | Some E27U27L10 -> alu_tiny_y)
@@ -538,7 +547,7 @@ 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
+  | Rorw | Nandw | Norw | Nxorw | Nandd | Nord | Nxord
   | 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 5e94fbb5..cc266abd 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -287,8 +287,17 @@ Nondetfunction xorl (e1: expr) (e2: expr) :=
 
 (** ** Integer logical negation *)
 
-Definition notl (e: expr) :=
-  if Archi.splitlong then SplitLong.notl e else xorlimm Int64.mone e.
+Nondetfunction notl (e: expr) :=
+  match e with
+  | Eop Oandl (e1:::e2:::Enil) => Eop Onandl (e1:::e2:::Enil)
+  | Eop (Oandlimm n) (e1:::Enil) => Eop (Onandlimm n) (e1:::Enil)
+  | Eop Oorl (e1:::e2:::Enil) => Eop Onorl (e1:::e2:::Enil)
+  | 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
+  end.
+(* old:  if Archi.splitlong then SplitLong.notl e else xorlimm Int64.mone e. *)
 
 (** ** Integer division and modulus *)
 
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 44846a6f..a8a6bc9c 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -441,8 +441,16 @@ Qed.
 
 Theorem eval_notl: unary_constructor_sound notl Val.notl.
 Proof.
-  unfold notl; destruct Archi.splitlong. apply SplitLongproof.eval_notl.
-  red; intros. rewrite Val.notl_xorl. apply eval_xorlimm; auto.
+  assert (forall v, Val.lessdef (Val.notl (Val.notl v)) v).
+    destruct v; simpl; auto. rewrite Int64.not_involutive; auto.
+  unfold notl; red; intros until x; case (notl_match a); intros; InvEval.
+  - TrivialExists; simpl; congruence.
+  - TrivialExists; simpl; congruence.
+  - TrivialExists; simpl; congruence.
+  - TrivialExists; simpl; congruence.
+  - TrivialExists; simpl; congruence.
+  - TrivialExists; simpl; congruence.
+  - apply eval_xorlimm; assumption.
 Qed.
 
 Theorem eval_divls_base: partial_binary_constructor_sound divls_base Val.divls.
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 49ea53b9..d30d62a2 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -393,10 +393,16 @@ module Target (*: TARGET*) =
          fprintf oc "	sbfd	%a = %a, %a\n" ireg rd ireg rs2 ireg rs1
       | Pandl (rd, rs1, rs2) -> assert Archi.ptr64;
          fprintf oc "	andd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+      | Pnandl (rd, rs1, rs2) -> assert Archi.ptr64;
+         fprintf oc "	nandd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Porl (rd, rs1, rs2) -> assert Archi.ptr64;
          fprintf oc "	ord	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+      | Pnorl (rd, rs1, rs2) -> assert Archi.ptr64;
+         fprintf oc "	nord	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Pxorl (rd, rs1, rs2) -> assert Archi.ptr64;
          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
       | Pmull (rd, rs1, rs2) ->
          fprintf oc "	muld	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Pslll  (rd, rs1, rs2) ->
@@ -459,10 +465,16 @@ module Target (*: TARGET*) =
          fprintf oc "	addd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
       | Pandil (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	andd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+      | Pnandil (rd, rs, imm) -> assert Archi.ptr64;
+         fprintf oc "	andd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
       | Poril (rd, rs, imm) -> assert Archi.ptr64;
          fprintf oc "	ord	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+      | Pnoril (rd, rs, imm) -> assert Archi.ptr64;
+         fprintf oc "	nord	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
       | Pxoril (rd, rs, imm) -> assert Archi.ptr64;
          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
 
     let get_section_names name =
       let (text, lit) =
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 15378811..33f4d8a9 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -101,10 +101,16 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Omodlu, v1::v2::nil => modlu v1 v2
   | Oandl, v1::v2::nil => andl v1 v2
   | Oandlimm n, v1::nil => andl v1 (L n)
+  | Onandl, v1::v2::nil => notl (andl v1 v2)
+  | Onandlimm n, v1::nil => notl (andl v1 (L n))
   | Oorl, v1::v2::nil => orl v1 v2
   | Oorlimm n, v1::nil => orl v1 (L n)
+  | Onorl, v1::v2::nil => notl (orl v1 v2)
+  | Onorlimm n, v1::nil => notl (orl v1 (L n))
   | Oxorl, v1::v2::nil => xorl v1 v2
   | 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))
   | Oshll, v1::v2::nil => shll v1 v2
   | Oshllimm n, v1::nil => shll v1 (I n)
   | Oshrl, v1::v2::nil => shrl v1 v2