From 0d66eae95a8905ff985cd4738808fc93215a4904 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 16 Mar 2019 16:16:42 +0100
Subject: nand debut

---
 mppa_k1c/NeedOp.v   |  4 ++++
 mppa_k1c/Op.v       | 12 ++++++++++++
 mppa_k1c/ValueAOp.v |  2 ++
 3 files changed, 18 insertions(+)

diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index 5f8648d3..c5d9e58f 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -47,6 +47,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
   | Omulhs | Omulhu | Odiv | Odivu | Omod | Omodu => op2 (default nv)
   | Oand => op2 (bitwise nv)
   | Oandimm n => op1 (andimm nv n)
+  | Onand => op2 (bitwise nv)
+  | Onandimm n => op1 (andimm nv n)
   | Oor => op2 (bitwise nv)
   | Oorimm n => op1 (orimm nv n)
   | Oxor => op2 (bitwise nv)
@@ -148,6 +150,8 @@ Proof.
 - apply mul_sound; auto.
 - apply and_sound; auto.
 - apply andimm_sound; auto.
+- apply notint_sound; apply and_sound; auto.
+- apply notint_sound; apply andimm_sound; auto.
 - apply or_sound; auto.
 - apply orimm_sound; auto.
 - apply xor_sound; auto.
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 3a006fb2..8c5f01cd 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -78,6 +78,8 @@ Inductive operation : Type :=
   | Omodu                    (**r [rd = r1 % r2] (unsigned) *)
   | Oand                     (**r [rd = r1 & r2] *)
   | Oandimm (n: int)         (**r [rd = r1 & n] *)
+  | Onand                    (**r [rd = ~(r1 & r2)] *)
+  | Onandimm (n: int)        (**r [rd = ~(r1 & n)] *)
   | Oor                      (**r [rd = r1 | r2] *)
   | Oorimm (n: int)          (**r [rd = r1 | n] *)
   | Oxor                     (**r [rd = r1 ^ r2] *)
@@ -248,6 +250,8 @@ Definition eval_operation
   | Omodu, v1 :: v2 :: nil => Val.modu v1 v2
   | Oand, v1 :: v2 :: nil => Some (Val.and v1 v2)
   | Oandimm n, v1 :: nil => Some (Val.and v1 (Vint n))
+  | Onand, v1 :: v2 :: nil => Some (Val.notint (Val.and v1 v2))
+  | Onandimm n, v1 :: nil => Some (Val.notint (Val.and v1 (Vint n)))
   | Oor, v1 :: v2 :: nil => Some (Val.or v1 v2)
   | Oorimm n, v1 :: nil => Some (Val.or v1 (Vint n))
   | Oxor, v1 :: v2 :: nil => Some (Val.xor v1 v2)
@@ -405,6 +409,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Omodu => (Tint :: Tint :: nil, Tint)
   | Oand => (Tint :: Tint :: nil, Tint)
   | Oandimm _ => (Tint :: nil, Tint)
+  | Onand => (Tint :: Tint :: nil, Tint)
+  | Onandimm _ => (Tint :: nil, Tint)
   | Oor => (Tint :: Tint :: nil, Tint)
   | Oorimm _ => (Tint :: nil, Tint)
   | Oxor => (Tint :: Tint :: nil, Tint)
@@ -552,6 +558,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* and, andimm *)
   - destruct v0; destruct v1...
   - destruct v0...
+  (* nand, nandimm *)
+  - destruct v0; destruct v1...
+  - destruct v0...
   (* or, orimm *)
   - destruct v0; destruct v1...
   - destruct v0...
@@ -1016,6 +1025,9 @@ Proof.
   (* and, andimm *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
+  (* nand, nandimm *)
+  - inv H4; inv H2; simpl; auto.
+  - inv H4; simpl; auto.
   (* or, orimm *)
   - inv H4; inv H2; simpl; auto.
   - inv H4; simpl; auto.
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 26a49135..a78857b3 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -65,6 +65,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
   | Omodu, v1::v2::nil => modu v1 v2
   | Oand, v1::v2::nil => and v1 v2
   | Oandimm n, v1::nil => and v1 (I n)
+  | Onand, v1::v2::nil => notint (and v1 v2)
+  | Onandimm n, v1::nil => notint (and v1 (I n))
   | Oor, v1::v2::nil => or v1 v2
   | Oorimm n, v1::nil => or v1 (I n)
   | Oxor, v1::v2::nil => xor v1 v2
-- 
cgit