diff options
-rw-r--r-- | mppa_k1c/Asm.v | 4 | ||||
-rw-r--r-- | mppa_k1c/Asmblock.v | 4 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 2 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 7 | ||||
-rw-r--r-- | mppa_k1c/NeedOp.v | 4 | ||||
-rw-r--r-- | mppa_k1c/Op.v | 12 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 9 | ||||
-rw-r--r-- | mppa_k1c/SelectOp.v | 10 | ||||
-rw-r--r-- | mppa_k1c/SelectOp.vp | 2 | ||||
-rw-r--r-- | mppa_k1c/SelectOpproof.v | 2 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 4 | ||||
-rw-r--r-- | mppa_k1c/ValueAOp.v | 2 | ||||
-rw-r--r-- | test/monniaux/nand/nand.c | 6 |
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)); } |