nxor

13 files changed, 64 insertions, 4 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 3e4e4db7..2fd46689 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -142,6 +142,7 @@ Inductive instruction : Type :=
   | Porw                (rd rs1 rs2: ireg)          (**r or word *)

   | Pnorw               (rd rs1 rs2: ireg)          (**r nor word *)

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

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

@@ -172,6 +173,7 @@ Inductive instruction : Type :=
   | Poriw               (rd rs: ireg) (imm: int)    (**r or imm word *)

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

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

@@ -267,6 +269,7 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRR Asmblock.Porw rd rs1 rs2        => Porw rd rs1 rs2

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

@@ -296,6 +299,7 @@ Definition basic_to_instruction (b: basic) :=
   | PArithRRI32 Asmblock.Poriw rd rs imm        => Poriw rd rs imm

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

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 66878a94..6e55b074 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -342,6 +342,7 @@ Inductive arith_name_rrr : Type :=
   | Porw                                            (**r or word *)
   | Pnorw                                           (**r nor word *)
   | Pxorw                                           (**r xor word *)
+  | Pnxorw                                          (**r nxor word *)
   | Psraw                                           (**r shift right arithmetic word *)
   | Psrlw                                           (**r shift right logical word *)
   | Psllw                                           (**r shift left logical word *)
@@ -373,6 +374,7 @@ Inductive arith_name_rri32 : Type :=
   | Poriw                                           (**r or imm word *)
   | Pnoriw                                          (**r nor imm word *)
   | Pxoriw                                          (**r xor imm word *)
+  | Pnxoriw                                         (**r nxor imm word *)
   | Psraiw                                          (**r shift right arithmetic imm word *)
   | Psrliw                                          (**r shift right logical imm word *)
   | Pslliw                                          (**r shift left logical imm word *)
@@ -1099,6 +1101,7 @@ Definition arith_eval_rrr n v1 v2 :=
   | Porw   => Val.or   v1 v2
   | Pnorw  => Val.notint (Val.or v1 v2)
   | Pxorw  => Val.xor  v1 v2
+  | Pnxorw => Val.notint (Val.xor v1 v2)
   | Psrlw  => Val.shru v1 v2
   | Psraw  => Val.shr  v1 v2
   | Psllw  => Val.shl  v1 v2
@@ -1130,6 +1133,7 @@ Definition arith_eval_rri32 n v i :=
   | Poriw   => Val.or    v (Vint i)
   | Pnoriw  => Val.notint (Val.or v (Vint i))
   | Pxoriw  => Val.xor   v (Vint i)
+  | Pnxoriw => Val.notint (Val.xor v (Vint i))
   | Psraiw  => Val.shr   v (Vint i)
   | Psrliw  => Val.shru  v (Vint i)
   | Pslliw  => Val.shl   v (Vint i)
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 0694c22f..9266a09b 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -1304,6 +1304,7 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring :=
   | Porw => "Porw"
   | Pnorw => "Pnorw"
   | Pxorw => "Pxorw"
+  | Pnxorw => "Pnxorw"
   | Psraw => "Psraw"
   | Psrlw => "Psrlw"
   | Psllw => "Psllw"
@@ -1333,6 +1334,7 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring :=
   | Poriw => "Poriw"
   | Pnoriw => "Pnoriw"
   | Pxoriw => "Pxoriw"
+  | Pnxoriw => "Pnxoriw"
   | Psraiw => "Psraiw"
   | Psrliw => "Psrliw"
   | Pslliw => "Pslliw"
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 9b9e9a12..f32d14bb 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -90,6 +90,7 @@ Definition nandimm32 := opimm32 Pnandw Pnandiw.
 Definition orimm32  := opimm32 Porw Poriw.
 Definition norimm32 := opimm32 Pnorw Pnoriw.
 Definition xorimm32 := opimm32 Pxorw Pxoriw.
+Definition nxorimm32 := opimm32 Pnxorw Pnxoriw.
 (*
 Definition sltimm32 := opimm32 Psltw Psltiw.
 Definition sltuimm32 := opimm32 Psltuw Psltiuw.
@@ -460,6 +461,12 @@ Definition transl_op
   | Oxorimm n, a1 :: nil =>
       do rd  <- ireg_of res; do rs <- ireg_of a1;
       OK (xorimm32 rd rs n ::i k)
+  | Onxor, a1 :: a2 :: nil =>
+      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      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)
   | 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)
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index 3442e3c1..b8f120f5 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -55,6 +55,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Onorimm n => op1 (orimm nv n)
   | Oxor => op2 (bitwise nv)
   | Oxorimm n => op1 (bitwise nv)
+  | Onxor => op2 (bitwise nv)
+  | Onxorimm n => op1 (bitwise nv)
   | Oshl | Oshr | Oshru => op2 (default nv)
   | Oshlimm n => op1 (shlimm nv n)
   | Oshrimm n => op1 (shrimm nv n)
@@ -160,6 +162,8 @@ Proof.
 - apply notint_sound; apply orimm_sound; auto.
 - apply xor_sound; auto.
 - apply xor_sound; auto with na.
+- apply notint_sound; apply xor_sound; auto.
+- apply notint_sound; apply xor_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 275613bb..a67fa27f 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -86,6 +86,8 @@ Inductive operation : Type :=
   | Onorimm (n: int)         (**r [rd = r1 | n] *)
   | Oxor                     (**r [rd = r1 ^ r2] *)
   | Oxorimm (n: int)         (**r [rd = r1 ^ n] *)
+  | Onxor                    (**r [rd = ~(r1 ^ r2)] *)
+  | Onxorimm (n: int)        (**r [rd = ~(r1 ^ n)] *)
   | Oshl                     (**r [rd = r1 << r2] *)
   | Oshlimm (n: int)         (**r [rd = r1 << n] *)
   | Oshr                     (**r [rd = r1 >> r2] (signed) *)
@@ -260,6 +262,8 @@ Definition eval_operation
   | Onorimm n, v1 :: nil => Some (Val.notint (Val.or v1 (Vint n)))
   | Oxor, v1 :: v2 :: nil => Some (Val.xor v1 v2)
   | 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)))
   | 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)
@@ -421,6 +425,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Onorimm _ => (Tint :: nil, Tint)
   | Oxor => (Tint :: Tint :: nil, Tint)
   | Oxorimm _ => (Tint :: nil, Tint)
+  | Onxor => (Tint :: Tint :: nil, Tint)
+  | Onxorimm _ => (Tint :: nil, Tint)
   | Oshl => (Tint :: Tint :: nil, Tint)
   | Oshlimm _ => (Tint :: nil, Tint)
   | Oshr => (Tint :: Tint :: nil, Tint)
@@ -576,6 +582,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* xor, xorimm *)
   - destruct v0; destruct v1...
   - destruct v0...
+  (* nxor, nxorimm *)
+  - 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)...
@@ -1046,6 +1055,9 @@ Proof.
   (* xor, xorimm *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
+  (* nxor, nxorimm *)
+  - 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.
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index c674bf3e..2d25c281 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -65,6 +65,7 @@ let arith_rrr_str = function
   | Porw -> "Porw"
   | Pnorw -> "Pnorw"
   | Pxorw -> "Pxorw"
+  | Pnxorw -> "Pnxorw"
   | Psraw -> "Psraw"
   | Psrlw -> "Psrlw"
   | Psllw -> "Psllw"
@@ -92,6 +93,7 @@ let arith_rri32_str = function
   | Poriw -> "Poriw"
   | Pnoriw -> "Pnoriw"
   | Pxoriw -> "Pxoriw"
+  | Pnxoriw -> "Pnxoriw"
   | Psraiw -> "Psraiw"
   | Psrliw -> "Psrliw"
   | Pslliw -> "Pslliw"
@@ -382,7 +384,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                                                               
+  | Nandw | Norw | Nxorw                                                        
   | Make | Nop  | Sxwd  | Zxwd
   (* LSU *)
   | Lbs | Lbz | Lhs | Lhz | Lws | Ld
@@ -420,6 +422,7 @@ let ab_inst_to_real = function
   | "Proriw" -> Rorw
   | "Pslll" | "Psllil" -> Slld
   | "Pxorw" | "Pxoriw" -> Xorw
+  | "Pnxorw" | "Pnxoriw" -> Nxorw
   | "Pxorl" | "Pxoril" -> Xord
   | "Pmake" | "Pmakel" | "Pmakefs" | "Pmakef" | "Ploadsymbol" -> Make
   | "Pnop" | "Pcvtw2l" -> Nop
@@ -482,7 +485,7 @@ 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 -> 
+  | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw | Nxorw -> 
       (match encoding with None | Some U6 | Some S10 -> alu_tiny 
                           | Some U27L5 | Some U27L10 -> alu_tiny_x
                           | _ -> raise InvalidEncoding)
@@ -535,7 +538,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
+  | Rorw | Nandw | Norw | Nxorw
   | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make
   | Sxwd | Zxwd | Fcompw | Fcompd
         -> 1
diff --git a/mppa_k1c/SelectOp.v b/mppa_k1c/SelectOp.v
index 028c2eb1..109d447b 100644
--- a/mppa_k1c/SelectOp.v
+++ b/mppa_k1c/SelectOp.v
@@ -728,6 +728,8 @@ Nondetfunction notint (e: expr) :=
   | Eop (Oandimm n) (e1:::Enil) => Eop (Onandimm n) (e1:::Enil)
   | Eop Oor (e1:::e2:::Enil) => Eop Onor (e1:::e2:::Enil)
   | 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
   end.
 >>
@@ -738,6 +740,8 @@ Inductive notint_cases: forall (e: expr), Type :=
   | notint_case2: forall n e1, notint_cases (Eop (Oandimm n) (e1:::Enil))
   | notint_case3: forall e1 e2, notint_cases (Eop Oor (e1:::e2:::Enil))
   | notint_case4: forall n e1, notint_cases (Eop (Oorimm n) (e1:::Enil))
+  | notint_case5: forall e1 e2, notint_cases (Eop Oxor (e1:::e2:::Enil))
+  | notint_case6: forall n e1, notint_cases (Eop (Oxorimm n) (e1:::Enil))
   | notint_default: forall (e: expr), notint_cases e.
 
 Definition notint_match (e: expr) :=
@@ -746,6 +750,8 @@ Definition notint_match (e: expr) :=
   | Eop (Oandimm n) (e1:::Enil) => notint_case2 n e1
   | Eop Oor (e1:::e2:::Enil) => notint_case3 e1 e2
   | Eop (Oorimm n) (e1:::Enil) => notint_case4 n e1
+  | Eop Oxor (e1:::e2:::Enil) => notint_case5 e1 e2
+  | Eop (Oxorimm n) (e1:::Enil) => notint_case6 n e1
   | e => notint_default e
   end.
 
@@ -759,6 +765,10 @@ Definition notint (e: expr) :=
       Eop Onor (e1:::e2:::Enil)
   | notint_case4 n e1 => (* Eop (Oorimm n) (e1:::Enil) *) 
       Eop (Onorimm n) (e1:::Enil)
+  | notint_case5 e1 e2 => (* Eop Oxor (e1:::e2:::Enil) *) 
+      Eop Onxor (e1:::e2:::Enil)
+  | notint_case6 n e1 => (* Eop (Oxorimm n) (e1:::Enil) *) 
+      Eop (Onxorimm n) (e1:::Enil)
   | notint_default e =>
       xorimm Int.mone e
   end.
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 3f806dda..a45e3403 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -281,6 +281,8 @@ Nondetfunction notint (e: expr) :=
   | Eop (Oandimm n) (e1:::Enil) => Eop (Onandimm n) (e1:::Enil)
   | Eop Oor (e1:::e2:::Enil) => Eop Onor (e1:::e2:::Enil)
   | 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
   end.
 
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 59ea598a..73b345d3 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -531,6 +531,8 @@ Proof.
   - TrivialExists; simpl; congruence.
   - TrivialExists; simpl; congruence.
   - TrivialExists; simpl; congruence.
+  - TrivialExists; simpl; congruence.
+  - TrivialExists; simpl; congruence.
   - apply eval_xorimm; assumption.
 Qed.
 
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 07663074..49ea53b9 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -378,6 +378,8 @@ module Target (*: TARGET*) =
          fprintf oc "	norw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Pxorw (rd, rs1, rs2) -> 
          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
       | Psraw (rd, rs1, rs2) ->
          fprintf oc "	sraw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
       | Psrlw (rd, rs1, rs2) ->
@@ -432,6 +434,8 @@ module Target (*: TARGET*) =
          fprintf oc "	norw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Pxoriw (rd, rs, imm) -> 
          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
       | Psraiw (rd, rs, imm) ->
          fprintf oc "	sraw	%a = %a, %a\n" ireg rd ireg rs coqint imm
       | Psrliw (rd, rs, imm) ->
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index b9319a82..15378811 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -73,6 +73,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Onorimm n, v1::nil => notint (or v1 (I n))
   | Oxor, v1::v2::nil => xor v1 v2
   | 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))
   | Oshl, v1::v2::nil => shl v1 v2
   | Oshlimm n, v1::nil => shl v1 (I n)
   | Oshr, v1::v2::nil => shr v1 v2
diff --git a/test/monniaux/nand/nand.c b/test/monniaux/nand/nand.c
index 86cf84bd..f808f311 100644
--- a/test/monniaux/nand/nand.c
+++ b/test/monniaux/nand/nand.c
@@ -12,7 +12,11 @@ unsigned nor(unsigned x, unsigned y) {
   return ~(x | y);
 }
 
+unsigned nxor(unsigned x, unsigned y) {
+  return ~(x ^ y);
+}
+
 int main() {
   unsigned x = 0xF4, y = 0x33;
-  printf("%X\n", nor(x, y));
+  printf("%X\n", nxor(x, y));
 }