diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-18 11:01:43 +0100 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-18 11:01:43 +0100 |
commit | 4bd693ddb0f1489c301927fd0eb521cf3505ac2b (patch) | |
tree | 7ffd9d04ba8dd43c578ff3d30330f381b928e35f /mppa_k1c | |
parent | 6ecca2e4797af8effde673b8f188d562fdfc89a6 (diff) | |
download | compcert-kvx-4bd693ddb0f1489c301927fd0eb521cf3505ac2b.tar.gz compcert-kvx-4bd693ddb0f1489c301927fd0eb521cf3505ac2b.zip |
orn / andn in asm
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asm.v | 8 | ||||
-rw-r--r-- | mppa_k1c/Asmblock.v | 16 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 8 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 22 |
4 files changed, 50 insertions, 4 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index e07b1190..8486e25d 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -284,6 +284,8 @@ Definition basic_to_instruction (b: basic) := | 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.Pandnw rd rs1 rs2 => Pandnw rd rs1 rs2
+ | PArithRRR Asmblock.Pornw rd rs1 rs2 => Pornw 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 +298,8 @@ Definition basic_to_instruction (b: basic) := | PArithRRR Asmblock.Pnorl rd rs1 rs2 => Pnorl rd rs1 rs2
| PArithRRR Asmblock.Pxorl rd rs1 rs2 => Pxorl rd rs1 rs2
| PArithRRR Asmblock.Pnxorl rd rs1 rs2 => Pnxorl rd rs1 rs2
+ | PArithRRR Asmblock.Pandnl rd rs1 rs2 => Pandnl rd rs1 rs2
+ | PArithRRR Asmblock.Pornl rd rs1 rs2 => Pornl rd rs1 rs2
| PArithRRR Asmblock.Pmull rd rs1 rs2 => Pmull rd rs1 rs2
| PArithRRR Asmblock.Pslll rd rs1 rs2 => Pslll rd rs1 rs2
| PArithRRR Asmblock.Psrll rd rs1 rs2 => Psrll rd rs1 rs2
@@ -317,6 +321,8 @@ Definition basic_to_instruction (b: basic) := | 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.Pandniw rd rs imm => Pandniw rd rs imm
+ | PArithRRI32 Asmblock.Porniw rd rs imm => Porniw 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
@@ -334,6 +340,8 @@ Definition basic_to_instruction (b: basic) := | PArithRRI64 Asmblock.Pnoril rd rs imm => Pnoril rd rs imm
| PArithRRI64 Asmblock.Pxoril rd rs imm => Pxoril rd rs imm
| PArithRRI64 Asmblock.Pnxoril rd rs imm => Pnxoril rd rs imm
+ | PArithRRI64 Asmblock.Pandnil rd rs imm => Pandnil rd rs imm
+ | PArithRRI64 Asmblock.Pornil rd rs imm => Pornil rd rs imm
(** Load *)
| PLoadRRO Asmblock.Plb rd ra ofs => Plb rd ra ofs
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 5279bd29..cdbe4eb3 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -343,6 +343,8 @@ Inductive arith_name_rrr : Type := | Pnorw (**r nor word *) | Pxorw (**r xor word *) | Pnxorw (**r nxor word *) + | Pandnw (**r andn word *) + | Pornw (**r orn word *) | Psraw (**r shift right arithmetic word *) | Psrlw (**r shift right logical word *) | Psllw (**r shift left logical word *) @@ -355,6 +357,8 @@ Inductive arith_name_rrr : Type := | Pnorl (**r nor long *) | Pxorl (**r xor long *) | Pnxorl (**r nxor long *) + | Pandnl (**r andn long *) + | Pornl (**r orn long *) | Pmull (**r mul long (low part) *) | Pslll (**r shift left logical long *) | Psrll (**r shift right logical long *) @@ -378,6 +382,8 @@ Inductive arith_name_rri32 : Type := | Pnoriw (**r nor imm word *) | Pxoriw (**r xor imm word *) | Pnxoriw (**r nxor imm word *) + | Pandniw (**r andn word *) + | Porniw (**r orn word *) | Psraiw (**r shift right arithmetic imm word *) | Psrliw (**r shift right logical imm word *) | Pslliw (**r shift left logical imm word *) @@ -396,6 +402,8 @@ Inductive arith_name_rri64 : Type := | Pnoril (**r nor immediate long *) | Pxoril (**r xor immediate long *) | Pnxoril (**r nxor immediate long *) + | Pandnil (**r andn immediate long *) + | Pornil (**r orn immediate long *) . Inductive ar_instruction : Type := @@ -1108,6 +1116,8 @@ Definition arith_eval_rrr n v1 v2 := | Pnorw => Val.notint (Val.or v1 v2) | Pxorw => Val.xor v1 v2 | Pnxorw => Val.notint (Val.xor v1 v2) + | Pandnw => Val.and (Val.notint v1) v2 + | Pornw => Val.or (Val.notint v1) v2 | Psrlw => Val.shru v1 v2 | Psraw => Val.shr v1 v2 | Psllw => Val.shl v1 v2 @@ -1120,6 +1130,8 @@ Definition arith_eval_rrr n v1 v2 := | Pnorl => Val.notl (Val.orl v1 v2) | Pxorl => Val.xorl v1 v2 | Pnxorl => Val.notl (Val.xorl v1 v2) + | Pandnl => Val.andl (Val.notl v1) v2 + | Pornl => Val.orl (Val.notl v1) v2 | Pmull => Val.mull v1 v2 | Pslll => Val.shll v1 v2 | Psrll => Val.shrlu v1 v2 @@ -1143,6 +1155,8 @@ Definition arith_eval_rri32 n v i := | Pnoriw => Val.notint (Val.or v (Vint i)) | Pxoriw => Val.xor v (Vint i) | Pnxoriw => Val.notint (Val.xor v (Vint i)) + | Pandniw => Val.and (Val.notint v) (Vint i) + | Porniw => Val.or (Val.notint v) (Vint i) | Psraiw => Val.shr v (Vint i) | Psrliw => Val.shru v (Vint i) | Pslliw => Val.shl v (Vint i) @@ -1162,6 +1176,8 @@ Definition arith_eval_rri64 n v i := | Pnoril => Val.notl (Val.orl v (Vlong i)) | Pxoril => Val.xorl v (Vlong i) | Pnxoril => Val.notl (Val.xorl v (Vlong i)) + | Pandnil => Val.andl (Val.notl v) (Vlong i) + | Pornil => Val.orl (Val.notl v) (Vlong i) end. Definition exec_arith_instr (ai: ar_instruction) (rs: regset): regset := diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index c5b5bd56..d69903b4 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1305,6 +1305,8 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Pnorw => "Pnorw" | Pxorw => "Pxorw" | Pnxorw => "Pnxorw" + | Pandnw => "Pandnw" + | Pornw => "Pornw" | Psraw => "Psraw" | Psrlw => "Psrlw" | Psllw => "Psllw" @@ -1316,6 +1318,8 @@ Definition string_of_name_rrr (n: arith_name_rrr): pstring := | Pnorl => "Pnorl" | Pxorl => "Pxorl" | Pnxorl => "Pnxorl" + | Pandnl => "Pandnl" + | Pornl => "Pornl" | Pmull => "Pmull" | Pslll => "Pslll" | Psrll => "Psrll" @@ -1338,6 +1342,8 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := | Pnoriw => "Pnoriw" | Pxoriw => "Pxoriw" | Pnxoriw => "Pnxoriw" + | Pandniw => "Pandniw" + | Porniw => "Porniw" | Psraiw => "Psraiw" | Psrliw => "Psrliw" | Pslliw => "Pslliw" @@ -1357,6 +1363,8 @@ Definition string_of_name_rri64 (n: arith_name_rri64): pstring := | Pnoril => "Pnoril" | Pxoril => "Pxoril" | Pnxoril => "Pnxoril" + | Pandnil => "Pandnil" + | Pornil => "Pornil" end. Definition string_of_arith (op: arith_op): pstring := diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 3c242441..ce2fb2ae 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -66,6 +66,8 @@ let arith_rrr_str = function | Pnorw -> "Pnorw" | Pxorw -> "Pxorw" | Pnxorw -> "Pnxorw" + | Pandnw -> "Pandnw" + | Pornw -> "Pornw" | Psraw -> "Psraw" | Psrlw -> "Psrlw" | Psllw -> "Psllw" @@ -77,6 +79,8 @@ let arith_rrr_str = function | Pnorl -> "Pnorl" | Pxorl -> "Pxorl" | Pnxorl -> "Pnxorl" + | Pandnl -> "Pandnl" + | Pornl -> "Pornl" | Pmull -> "Pmull" | Pslll -> "Pslll" | Psrll -> "Psrll" @@ -97,6 +101,8 @@ let arith_rri32_str = function | Pnoriw -> "Pnoriw" | Pxoriw -> "Pxoriw" | Pnxoriw -> "Pnxoriw" + | Pandniw -> "Pandniw" + | Porniw -> "Porniw" | Psraiw -> "Psraiw" | Psrliw -> "Psrliw" | Pslliw -> "Pslliw" @@ -114,6 +120,8 @@ let arith_rri64_str = function | Pnoril -> "Pnoril" | Pxoril -> "Pxoril" | Pnxoril -> "Pnxoril" + | Pandnil -> "Pandnil" + | Pornil -> "Pornil" let arith_ri32_str = "Pmake" @@ -390,7 +398,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 | Nxorw | Nandd | Nord | Nxord + | Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd | Make | Nop | Sxwd | Zxwd (* LSU *) | Lbs | Lbz | Lhs | Lhz | Lws | Ld @@ -431,8 +439,12 @@ let ab_inst_to_real = function | "Pslll" | "Psllil" -> Slld | "Pxorw" | "Pxoriw" -> Xorw | "Pnxorw" | "Pnxoriw" -> Nxorw + | "Pandnw" | "Pandniw" -> Andnw + | "Pornw" | "Porniw" -> Ornw | "Pxorl" | "Pxoril" -> Xord | "Pnxorl" | "Pnxoril" -> Nxord + | "Pandnl" | "Pandnil" -> Andnd + | "Pornl" | "Pornil" -> Ornd | "Pmake" | "Pmakel" | "Pmakefs" | "Pmakef" | "Ploadsymbol" -> Make | "Pnop" | "Pcvtw2l" -> Nop | "Psxwd" -> Sxwd @@ -494,11 +506,11 @@ 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 | Nxorw -> + | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw | Nxorw | Andnw | Ornw -> (match encoding with None | Some U6 | Some S10 -> alu_tiny | Some U27L5 | Some U27L10 -> alu_tiny_x | _ -> raise InvalidEncoding) - | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord | Nxord -> + | Addd | Andd | Nandd | Ord | Nord | Sbfd | Xord | Nxord | Andnd | Ornd -> (match encoding with None | Some U6 | Some S10 -> alu_tiny | Some U27L5 | Some U27L10 -> alu_tiny_x | Some E27U27L10 -> alu_tiny_y) @@ -547,7 +559,9 @@ 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 | Nxorw | Nandd | Nord | Nxord + (* TODO check rorw *) + | Rorw | Nandw | Norw | Nxorw | Ornw | Andnw + | Nandd | Nord | Nxord | Ornd | Andnd | Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make | Sxwd | Zxwd | Fcompw | Fcompd -> 1 |