aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asmblockgen.v7
-rw-r--r--mppa_k1c/NeedOp.v4
-rw-r--r--mppa_k1c/Op.v12
-rw-r--r--mppa_k1c/SelectOp.v10
-rw-r--r--mppa_k1c/SelectOp.vp2
-rw-r--r--mppa_k1c/SelectOpproof.v2
-rw-r--r--mppa_k1c/ValueAOp.v2
-rw-r--r--test/monniaux/nand/nand.c6
8 files changed, 44 insertions, 1 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 12dabd88..9b9e9a12 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -88,6 +88,7 @@ Definition addimm32 := opimm32 Paddw Paddiw.
Definition andimm32 := opimm32 Pandw Pandiw.
Definition nandimm32 := opimm32 Pnandw Pnandiw.
Definition orimm32 := opimm32 Porw Poriw.
+Definition norimm32 := opimm32 Pnorw Pnoriw.
Definition xorimm32 := opimm32 Pxorw Pxoriw.
(*
Definition sltimm32 := opimm32 Psltw Psltiw.
@@ -444,9 +445,15 @@ Definition transl_op
| Oor, a1 :: a2 :: nil =>
do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
OK (Porw rd rs1 rs2 ::i k)
+ | Onor, a1 :: a2 :: nil =>
+ do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+ OK (Pnorw rd rs1 rs2 ::i k)
| Oorimm n, a1 :: nil =>
do rd <- ireg_of res; do rs <- ireg_of a1;
OK (orimm32 rd rs n ::i k)
+ | Onorimm n, a1 :: nil =>
+ do rd <- ireg_of res; do rs <- ireg_of a1;
+ OK (norimm32 rd rs n ::i k)
| Oxor, a1 :: a2 :: nil =>
do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
OK (Pxorw rd rs1 rs2 ::i k)
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index c5d9e58f..3442e3c1 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -51,6 +51,8 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| Onandimm n => op1 (andimm nv n)
| Oor => op2 (bitwise nv)
| Oorimm n => op1 (orimm nv n)
+ | Onor => op2 (bitwise nv)
+ | Onorimm n => op1 (orimm nv n)
| Oxor => op2 (bitwise nv)
| Oxorimm n => op1 (bitwise nv)
| Oshl | Oshr | Oshru => op2 (default nv)
@@ -154,6 +156,8 @@ Proof.
- apply notint_sound; apply andimm_sound; auto.
- apply or_sound; auto.
- apply orimm_sound; auto.
+- apply notint_sound; apply or_sound; auto.
+- apply notint_sound; apply orimm_sound; auto.
- apply xor_sound; auto.
- apply xor_sound; auto with na.
- apply shlimm_sound; auto.
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 8c5f01cd..275613bb 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -82,6 +82,8 @@ Inductive operation : Type :=
| Onandimm (n: int) (**r [rd = ~(r1 & n)] *)
| Oor (**r [rd = r1 | r2] *)
| Oorimm (n: int) (**r [rd = r1 | n] *)
+ | Onor (**r [rd = r1 | r2] *)
+ | Onorimm (n: int) (**r [rd = r1 | n] *)
| Oxor (**r [rd = r1 ^ r2] *)
| Oxorimm (n: int) (**r [rd = r1 ^ n] *)
| Oshl (**r [rd = r1 << r2] *)
@@ -254,6 +256,8 @@ Definition eval_operation
| 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))
+ | Onor, v1 :: v2 :: nil => Some (Val.notint (Val.or v1 v2))
+ | 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))
| Oshl, v1 :: v2 :: nil => Some (Val.shl v1 v2)
@@ -413,6 +417,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
| Onandimm _ => (Tint :: nil, Tint)
| Oor => (Tint :: Tint :: nil, Tint)
| Oorimm _ => (Tint :: nil, Tint)
+ | Onor => (Tint :: Tint :: nil, Tint)
+ | Onorimm _ => (Tint :: nil, Tint)
| Oxor => (Tint :: Tint :: nil, Tint)
| Oxorimm _ => (Tint :: nil, Tint)
| Oshl => (Tint :: Tint :: nil, Tint)
@@ -564,6 +570,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
(* or, orimm *)
- destruct v0; destruct v1...
- destruct v0...
+ (* nor, norimm *)
+ - destruct v0; destruct v1...
+ - destruct v0...
(* xor, xorimm *)
- destruct v0; destruct v1...
- destruct v0...
@@ -1031,6 +1040,9 @@ Proof.
(* or, orimm *)
- inv H4; inv H2; simpl; auto.
- inv H4; simpl; auto.
+ (* nor, norimm *)
+ - inv H4; inv H2; simpl; auto.
+ - inv H4; simpl; auto.
(* xor, xorimm *)
- inv H4; inv H2; simpl; auto.
- inv H4; simpl; auto.
diff --git a/mppa_k1c/SelectOp.v b/mppa_k1c/SelectOp.v
index 4d3d5ad0..028c2eb1 100644
--- a/mppa_k1c/SelectOp.v
+++ b/mppa_k1c/SelectOp.v
@@ -726,6 +726,8 @@ Nondetfunction notint (e: expr) :=
match e with
| Eop Oand (e1:::e2:::Enil) => Eop Onand (e1:::e2:::Enil)
| 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)
| _ => xorimm Int.mone e
end.
>>
@@ -734,12 +736,16 @@ Nondetfunction notint (e: expr) :=
Inductive notint_cases: forall (e: expr), Type :=
| notint_case1: forall e1 e2, notint_cases (Eop Oand (e1:::e2:::Enil))
| 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_default: forall (e: expr), notint_cases e.
Definition notint_match (e: expr) :=
match e as zz1 return notint_cases zz1 with
| Eop Oand (e1:::e2:::Enil) => notint_case1 e1 e2
| 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
| e => notint_default e
end.
@@ -749,6 +755,10 @@ Definition notint (e: expr) :=
Eop Onand (e1:::e2:::Enil)
| notint_case2 n e1 => (* Eop (Oandimm n) (e1:::Enil) *)
Eop (Onandimm n) (e1:::Enil)
+ | notint_case3 e1 e2 => (* Eop Oor (e1:::e2:::Enil) *)
+ Eop Onor (e1:::e2:::Enil)
+ | notint_case4 n e1 => (* Eop (Oorimm n) (e1:::Enil) *)
+ Eop (Onorimm n) (e1:::Enil)
| notint_default e =>
xorimm Int.mone e
end.
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 4b64e495..3f806dda 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -279,6 +279,8 @@ Nondetfunction notint (e: expr) :=
match e with
| Eop Oand (e1:::e2:::Enil) => Eop Onand (e1:::e2:::Enil)
| 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)
| _ => xorimm Int.mone e
end.
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index c14a622a..59ea598a 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -529,6 +529,8 @@ Proof.
unfold notint; red; intros until x; case (notint_match a); intros; InvEval.
- TrivialExists; simpl; congruence.
- TrivialExists; simpl; congruence.
+ - TrivialExists; simpl; congruence.
+ - TrivialExists; simpl; congruence.
- apply eval_xorimm; assumption.
Qed.
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index a78857b3..b9319a82 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -69,6 +69,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
| Onandimm n, v1::nil => notint (and v1 (I n))
| Oor, v1::v2::nil => or v1 v2
| Oorimm n, v1::nil => or v1 (I n)
+ | Onor, v1::v2::nil => notint (or v1 v2)
+ | Onorimm n, v1::nil => notint (or v1 (I n))
| Oxor, v1::v2::nil => xor v1 v2
| Oxorimm n, v1::nil => xor v1 (I n)
| Oshl, v1::v2::nil => shl v1 v2
diff --git a/test/monniaux/nand/nand.c b/test/monniaux/nand/nand.c
index bcd30396..86cf84bd 100644
--- a/test/monniaux/nand/nand.c
+++ b/test/monniaux/nand/nand.c
@@ -8,7 +8,11 @@ unsigned nand(unsigned x, unsigned y) {
return ~(x & y);
}
+unsigned nor(unsigned x, unsigned y) {
+ return ~(x | y);
+}
+
int main() {
unsigned x = 0xF4, y = 0x33;
- printf("%X\n", nand(x, y));
+ printf("%X\n", nor(x, y));
}
generated by cgit (git 2.34.1) at 2024-07-02 00:33:25 +0000