From cfc949a5fce43f2d4e094b52ea42d619f64692c1 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 18 Mar 2019 11:22:49 +0100
Subject: andn / orn suite

---
 mppa_k1c/Asmblockgen.v     | 29 ++++++++++++++++++++++++++++-
 mppa_k1c/SelectLong.vp     |  2 +-
 mppa_k1c/SelectLongproof.v |  2 +-
 mppa_k1c/SelectOp.v        |  4 ++--
 mppa_k1c/SelectOp.vp       |  2 +-
 mppa_k1c/SelectOpproof.v   |  2 +-
 6 files changed, 34 insertions(+), 7 deletions(-)

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 9d682bed..c3ac217b 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -469,7 +469,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)
@@ -568,6 +583,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/SelectLong.vp b/mppa_k1c/SelectLong.vp
index cc266abd..dbd14b99 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -295,7 +295,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..27052edc 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -450,7 +450,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..78ab6261 100644
--- a/mppa_k1c/SelectOp.v
+++ b/mppa_k1c/SelectOp.v
@@ -730,7 +730,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 +770,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..2878da1a 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -283,7 +283,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..26df4fc7 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -533,7 +533,7 @@ Proof.
   - TrivialExists; simpl; congruence.
   - TrivialExists; simpl; congruence.
   - TrivialExists; simpl; congruence.
-  - apply eval_xorimm; assumption.
+  - TrivialExists.
 Qed.
 
 Theorem eval_divs_base:
-- 
cgit