diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 18:01:25 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-16 18:01:25 +0100 |
commit | fb02f9116621a0bcb9bb2c334ad782fee5887d0e (patch) | |
tree | bce5373f7b3e1c88c4ca69b83da7f420840a5cba /mppa_k1c | |
parent | 8155320553564674b7481b325c33845439b46b95 (diff) | |
download | compcert-kvx-fb02f9116621a0bcb9bb2c334ad782fee5887d0e.tar.gz compcert-kvx-fb02f9116621a0bcb9bb2c334ad782fee5887d0e.zip |
partial norw
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asm.v | 8 | ||||
-rw-r--r-- | mppa_k1c/Asmblock.v | 10 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 2 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 11 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 4 |
5 files changed, 26 insertions, 9 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index ee3fd198..3e4e4db7 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -138,8 +138,9 @@ Inductive instruction : Type := | Psubw (rd rs1 rs2: ireg) (**r sub word *)
| Pmulw (rd rs1 rs2: ireg) (**r mul word *)
| Pandw (rd rs1 rs2: ireg) (**r and word *)
- | Pnandw (rd rs1 rs2: ireg) (**r and word *)
+ | Pnandw (rd rs1 rs2: ireg) (**r nand word *)
| Porw (rd rs1 rs2: ireg) (**r or word *)
+ | Pnorw (rd rs1 rs2: ireg) (**r nor word *)
| Pxorw (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 *)
@@ -167,8 +168,9 @@ Inductive instruction : Type := | Paddiw (rd rs: ireg) (imm: int) (**r add imm word *)
| Pandiw (rd rs: ireg) (imm: int) (**r and imm word *)
- | Pnandiw (rd rs: ireg) (imm: int) (**r and imm word *)
+ | Pnandiw (rd rs: ireg) (imm: int) (**r nand imm word *)
| 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 *)
| Psraiw (rd rs: ireg) (imm: int) (**r shift right arithmetic imm word *)
| Psrliw (rd rs: ireg) (imm: int) (**r shift right logical imm word *)
@@ -263,6 +265,7 @@ Definition basic_to_instruction (b: basic) := | PArithRRR Asmblock.Pandw rd rs1 rs2 => Pandw rd rs1 rs2
| PArithRRR Asmblock.Pnandw rd rs1 rs2 => Pnandw rd rs1 rs2
| 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.Psraw rd rs1 rs2 => Psraw rd rs1 rs2
| PArithRRR Asmblock.Psrlw rd rs1 rs2 => Psrlw rd rs1 rs2
@@ -291,6 +294,7 @@ Definition basic_to_instruction (b: basic) := | PArithRRI32 Asmblock.Pandiw rd rs imm => Pandiw rd rs imm
| PArithRRI32 Asmblock.Pnandiw rd rs imm => Pnandiw rd rs imm
| 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.Psraiw rd rs imm => Psraiw rd rs imm
| PArithRRI32 Asmblock.Psrliw rd rs imm => Psrliw rd rs imm
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index ca9a96a5..66878a94 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -338,8 +338,9 @@ Inductive arith_name_rrr : Type := | Psubw (**r sub word *) | Pmulw (**r mul word *) | Pandw (**r and word *) - | Pnandw (**r and word *) + | Pnandw (**r nand word *) | Porw (**r or word *) + | Pnorw (**r nor word *) | Pxorw (**r xor word *) | Psraw (**r shift right arithmetic word *) | Psrlw (**r shift right logical word *) @@ -368,8 +369,9 @@ Inductive arith_name_rri32 : Type := | Paddiw (**r add imm word *) | Pandiw (**r and imm word *) - | Pnandiw (**r and imm word *) + | Pnandiw (**r nand imm word *) | Poriw (**r or imm word *) + | Pnoriw (**r nor imm word *) | Pxoriw (**r xor imm word *) | Psraiw (**r shift right arithmetic imm word *) | Psrliw (**r shift right logical imm word *) @@ -1095,6 +1097,7 @@ Definition arith_eval_rrr n v1 v2 := | Pandw => Val.and v1 v2 | Pnandw => Val.notint (Val.and v1 v2) | Porw => Val.or v1 v2 + | Pnorw => Val.notint (Val.or v1 v2) | Pxorw => Val.xor v1 v2 | Psrlw => Val.shru v1 v2 | Psraw => Val.shr v1 v2 @@ -1123,8 +1126,9 @@ Definition arith_eval_rri32 n v i := | Pcompiw c => compare_int c v (Vint i) | Paddiw => Val.add v (Vint i) | Pandiw => Val.and v (Vint i) - | Pnandiw => Val.notint(Val.and v (Vint i)) + | Pnandiw => Val.notint (Val.and v (Vint i)) | Poriw => Val.or v (Vint i) + | Pnoriw => Val.notint (Val.or v (Vint i)) | Pxoriw => Val.xor v (Vint i) | Psraiw => Val.shr v (Vint i) | Psrliw => Val.shru v (Vint i) diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index 499b0d66..0694c22f 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1302,6 +1302,7 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Pandw => "Pandw" | Pnandw => "Pnandw" | Porw => "Porw" + | Pnorw => "Pnorw" | Pxorw => "Pxorw" | Psraw => "Psraw" | Psrlw => "Psrlw" @@ -1330,6 +1331,7 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := | Pandiw => "Pandiw" | Pnandiw => "Pnandiw" | Poriw => "Poriw" + | Pnoriw => "Pnoriw" | Pxoriw => "Pxoriw" | Psraiw => "Psraiw" | Psrliw => "Psrliw" diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 791936f3..c674bf3e 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -63,6 +63,7 @@ let arith_rrr_str = function | Pandw -> "Pandw" | Pnandw -> "Pnandw" | Porw -> "Porw" + | Pnorw -> "Pnorw" | Pxorw -> "Pxorw" | Psraw -> "Psraw" | Psrlw -> "Psrlw" @@ -89,6 +90,7 @@ let arith_rri32_str = function | Pandiw -> "Pandiw" | Pnandiw -> "Pnandiw" | Poriw -> "Poriw" + | Pnoriw -> "Pnoriw" | Pxoriw -> "Pxoriw" | Psraiw -> "Psraiw" | Psrliw -> "Psrliw" @@ -380,7 +382,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 + | Nandw | Norw | Make | Nop | Sxwd | Zxwd (* LSU *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld @@ -406,6 +408,7 @@ let ab_inst_to_real = function | "Pmulw" -> Mulw | "Pmull" -> Muld | "Porw" | "Poriw" -> Orw + | "Pnorw" | "Pnoriw" -> Norw | "Porl" | "Poril" -> Ord | "Psubw" | "Pnegw" -> Sbfw | "Psubl" | "Pnegl" -> Sbfd @@ -469,7 +472,7 @@ let ab_inst_to_real = function | "Pfmuld" -> Fmuld | "Pfmulw" -> Fmulw | s -> failwith @@ sprintf "ab_inst_to_real: unrecognized instruction: %s" s - + exception InvalidEncoding let rec_to_usage r = @@ -479,7 +482,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 | Sbfw | Xorw -> + | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw -> (match encoding with None | Some U6 | Some S10 -> alu_tiny | Some U27L5 | Some U27L10 -> alu_tiny_x | _ -> raise InvalidEncoding) @@ -532,7 +535,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 + | Rorw | Nandw | Norw | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make | Sxwd | Zxwd | Fcompw | Fcompd -> 1 diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 9ab09866..07663074 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -374,6 +374,8 @@ module Target (*: TARGET*) = fprintf oc " nandw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 | Porw (rd, rs1, rs2) -> fprintf oc " orw %a = %a, %a\n" ireg rd ireg rs1 ireg rs2 + | Pnorw (rd, rs1, rs2) -> + 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 | Psraw (rd, rs1, rs2) -> @@ -426,6 +428,8 @@ module Target (*: TARGET*) = fprintf oc " nandw %a = %a, %a\n" ireg rd ireg rs coqint imm | Poriw (rd, rs, imm) -> fprintf oc " orw %a = %a, %a\n" ireg rd ireg rs coqint imm + | Pnoriw (rd, rs, imm) -> + 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 | Psraiw (rd, rs, imm) -> |