diff options
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asm.v | 3 | ||||
-rw-r--r-- | mppa_k1c/Asmblock.v | 3 | ||||
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 1 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 5 | ||||
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 8 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 3 |
6 files changed, 17 insertions, 6 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 31bc855d..5ed54a2b 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -171,7 +171,7 @@ Inductive instruction : Type := | 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 *)
-
+ | Proriw (rd rs: ireg) (imm: int) (**r rotate right imm word *)
| Psllil (rd rs: ireg) (imm: int) (**r shift left logical immediate long *)
| Psrlil (rd rs: ireg) (imm: int) (**r shift right logical immediate long *)
| Psrail (rd rs: ireg) (imm: int) (**r shift right arithmetic immediate long *)
@@ -291,6 +291,7 @@ Definition basic_to_instruction (b: basic) := | 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
+ | PArithRRI32 Asmblock.Proriw rd rs imm => Proriw rd rs imm
| PArithRRI32 Asmblock.Psllil rd rs imm => Psllil rd rs imm
| PArithRRI32 Asmblock.Psrlil rd rs imm => Psrlil rd rs imm
| PArithRRI32 Asmblock.Psrail rd rs imm => Psrail rd rs imm
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index 621ed8a7..883cfb94 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -372,7 +372,7 @@ Inductive arith_name_rri32 : Type := | Psraiw (**r shift right arithmetic imm word *) | Psrliw (**r shift right logical imm word *) | Pslliw (**r shift left logical imm word *) - + | Proriw (**r rotate right imm word *) | Psllil (**r shift left logical immediate long *) | Psrlil (**r shift right logical immediate long *) | Psrail (**r shift right arithmetic immediate long *) @@ -1125,6 +1125,7 @@ Definition arith_eval_rri32 n v i := | Psraiw => Val.shr v (Vint i) | Psrliw => Val.shru v (Vint i) | Pslliw => Val.shl v (Vint i) + | Proriw => Val.ror v (Vint i) | Psllil => Val.shll v (Vint i) | Psrlil => Val.shrlu v (Vint i) | Psrail => Val.shrl v (Vint i) diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index c6052337..19fca6c1 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1332,6 +1332,7 @@ Definition string_of_name_rri32 (n: arith_name_rri32): pstring := | Psraiw => "Psraiw" | Psrliw => "Psrliw" | Pslliw => "Pslliw" + | Proriw => "Proriw" | Psllil => "Psllil" | Psrlil => "Psrlil" | Psrail => "Psrail" diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 1c176538..26b1c6c1 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -471,7 +471,10 @@ Definition transl_op Psrliw RTMP RTMP (Int.sub Int.iwordsize n) ::i Paddw RTMP rs RTMP ::i Psraiw rd RTMP n ::i k) - + | Ororimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Proriw rd rs n ::i k) + (* [Omakelong], [Ohighlong] should not occur *) | Olowlong, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 9700776c..97108a90 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -91,6 +91,7 @@ let arith_rri32_str = function | Psraiw -> "Psraiw" | Psrliw -> "Psrliw" | Pslliw -> "Pslliw" + | Proriw -> "Proriw" | Psllil -> "Psllil" | Psrlil -> "Psrlil" | Psrail -> "Psrail" @@ -375,7 +376,7 @@ let lsu_data_y : int array = let resmap = fun r -> match r with type real_instruction = (* ALU *) - | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw + | Addw | Andw | Compw | Mulw | Orw | Sbfw | Sraw | Srlw | Sllw | Rorw | Xorw | Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Xord | Make | Nop | Sxwd | Zxwd (* LSU *) @@ -409,6 +410,7 @@ let ab_inst_to_real = function | "Psrlw" | "Psrliw" -> Srlw | "Psrll" | "Psrlil" -> Srld | "Psllw" | "Pslliw" -> Sllw + | "Proriw" -> Rorw | "Pslll" | "Psllil" -> Slld | "Pxorw" | "Pxoriw" -> Xorw | "Pxorl" | "Pxoril" -> Xord @@ -504,7 +506,7 @@ let rec_to_usage r = | Some U27L5 | Some U27L10 -> mau_x | Some E27U27L10 -> mau_y) | Nop -> alu_nop - | Sraw | Srlw | Sllw | Srad | Srld | Slld -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding) + | Sraw | Srlw | Sllw | Rorw | Srad | Srld | Slld -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding) | Sxwd | Zxwd -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding) | Fixeduwz | Fixedwz | Floatwz | Floatuwz | Fixeddz | Fixedudz | Floatdz | Floatudz -> mau | Lbs | Lbz | Lhs | Lhz | Lws | Ld -> @@ -523,7 +525,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 + | Addw | Andw | Compw | Orw | Sbfw | Sraw | Srlw | Sllw | Xorw | Rorw | 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 70d9ff6c..810808c2 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -430,6 +430,9 @@ module Target (*: TARGET*) = fprintf oc " srlw %a = %a, %a\n" ireg rd ireg rs coqint imm | Pslliw (rd, rs, imm) -> fprintf oc " sllw %a = %a, %a\n" ireg rd ireg rs coqint imm + | Proriw (rd, rs, imm) -> + fprintf oc " rorw %a = %a, %a\n" ireg rd ireg rs coqint imm + | Psllil (rd, rs, imm) -> fprintf oc " slld %a = %a, %a\n" ireg rd ireg rs coqint64 imm | Psrlil (rd, rs, imm) -> |