aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--mppa_k1c/Asm.v7
-rw-r--r--mppa_k1c/Asmblockdeps.v20
-rw-r--r--mppa_k1c/Asmvliw.v18
-rw-r--r--mppa_k1c/PostpassSchedulingOracle.ml15
-rw-r--r--mppa_k1c/TargetPrinter.ml2
5 files changed, 55 insertions, 7 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 609bf93e..f1ccc126 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -137,6 +137,9 @@ Inductive instruction : Type :=
| Pextfzl (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields unsigned *)
| Pextfsl (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields signed *)
+ | Pinsf (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r insert bitfield *)
+ | Pinsfl (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r insert bitfield *)
+
| Pfabsd (rd rs: ireg) (**r float absolute double *)
| Pfabsw (rd rs: ireg) (**r float absolute word *)
| Pfnegd (rd rs: ireg) (**r float negate double *)
@@ -404,6 +407,10 @@ Definition basic_to_instruction (b: basic) :=
| PArithARRR (Asmvliw.Pcmove cond) rd rs1 rs2=> Pcmove cond rd rs1 rs2
| PArithARRR (Asmvliw.Pcmoveu cond) rd rs1 rs2=> Pcmoveu cond rd rs1 rs2
+ (** ARR *)
+ | PArithARR (Asmvliw.Pinsf stop start) rd rs => Pinsf rd rs stop start
+ | PArithARR (Asmvliw.Pinsfl stop start) rd rs => Pinsfl rd rs stop start
+
(** ARRI32 *)
| PArithARRI32 Asmvliw.Pmaddiw rd rs1 imm => Pmaddiw rd rs1 imm
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index a1a11701..8fccdd99 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -57,6 +57,7 @@ Inductive arith_op :=
| OArithRRI32 (n: arith_name_rri32) (imm: int)
| OArithRRI64 (n: arith_name_rri64) (imm: int64)
| OArithARRR (n: arith_name_arrr)
+ | OArithARR (n: arith_name_arr)
| OArithARRI32 (n: arith_name_arri32) (imm: int)
| OArithARRI64 (n: arith_name_arri64) (imm: int64)
.
@@ -121,6 +122,7 @@ Definition arith_eval (ao: arith_op) (l: list value) :=
| OArithRRI32 n i, [Val v] => Some (Val (arith_eval_rri32 n v i))
| OArithRRI64 n i, [Val v] => Some (Val (arith_eval_rri64 n v i))
+ | OArithARR n, [Val v1; Val v2] => Some (Val (arith_eval_arr n v1 v2))
| OArithARRR n, [Val v1; Val v2; Val v3] => Some (Val (arith_eval_arrr n v1 v2 v3))
| OArithARRI32 n i, [Val v1; Val v2] => Some (Val (arith_eval_arri32 n v1 v2 i))
| OArithARRI64 n i, [Val v1; Val v2] => Some (Val (arith_eval_arri64 n v1 v2 i))
@@ -329,6 +331,8 @@ Definition arith_op_eq (o1 o2: arith_op): ?? bool :=
match o2 with OArithRRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
| OArithARRR n1 =>
match o2 with OArithARRR n2 => phys_eq n1 n2 | _ => RET false end
+ | OArithARR n1 =>
+ match o2 with OArithARR n2 => phys_eq n1 n2 | _ => RET false end
| OArithARRI32 n1 i1 =>
match o2 with OArithARRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end
| OArithARRI64 n1 i1 =>
@@ -597,6 +601,7 @@ Definition trans_arith (ai: ar_instruction) : inst :=
| PArithRRI32 n d s i => [(#d, Op (Arith (OArithRRI32 n i)) (PReg(#s) @ Enil))]
| PArithRRI64 n d s i => [(#d, Op (Arith (OArithRRI64 n i)) (PReg(#s) @ Enil))]
| PArithARRR n d s1 s2 => [(#d, Op (Arith (OArithARRR n)) (PReg(#d) @ PReg(#s1) @ PReg(#s2) @ Enil))]
+ | PArithARR n d s => [(#d, Op (Arith (OArithARR n)) (PReg(#d) @ PReg(#s) @ Enil))]
| PArithARRI32 n d s i => [(#d, Op (Arith (OArithARRI32 n i)) (PReg(#d) @ PReg(#s) @ Enil))]
| PArithARRI64 n d s i => [(#d, Op (Arith (OArithARRI64 n i)) (PReg(#d) @ PReg(#s) @ Enil))]
end.
@@ -776,6 +781,12 @@ Proof.
* Simpl.
* intros rr; destruct rr; Simpl.
destruct (ireg_eq g rd); subst; Simpl.
+(* PArithARR *)
+ - eexists; split; [|split].
+ * simpl. rewrite (H0 rd). rewrite (H0 rs). reflexivity.
+ * Simpl.
+ * intros rr; destruct rr; Simpl.
+ destruct (ireg_eq g rd); subst; Simpl.
(* PArithARRI32 *)
- eexists; split; [|split].
* simpl. rewrite (H0 rd). rewrite (H0 rs). reflexivity.
@@ -1344,6 +1355,12 @@ Definition string_of_name_arrr (n: arith_name_arrr): pstring :=
| Pcmoveu _ => "Pcmoveu"
end.
+Definition string_of_name_arr (n: arith_name_arr): pstring :=
+ match n with
+ | Pinsf _ _ => "Pinsf"
+ | Pinsfl _ _ => "Pinsfl"
+ end.
+
Definition string_of_name_arri32 (n: arith_name_arri32): pstring :=
match n with
| Pmaddiw => "Pmaddw"
@@ -1366,6 +1383,7 @@ Definition string_of_arith (op: arith_op): pstring :=
| OArithRRI32 n _ => string_of_name_rri32 n
| OArithRRI64 n _ => string_of_name_rri64 n
| OArithARRR n => string_of_name_arrr n
+ | OArithARR n => string_of_name_arr n
| OArithARRI32 n _ => string_of_name_arri32 n
| OArithARRI64 n _ => string_of_name_arri64 n
end.
@@ -1470,5 +1488,3 @@ Definition bblock_equiv_eq := pure_bblock_eq_test_correct true.
End SECT_BBLOCK_EQUIV.
-
-
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 6442cecc..0427d93c 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -312,7 +312,7 @@ Inductive arith_name_rr : Type :=
| Pextfs (stop : Z) (start : Z) (**r extract bit field, signed *)
| Pextfzl (stop : Z) (start : Z) (**r extract bit field, unsigned *)
| Pextfsl (stop : Z) (start : Z) (**r extract bit field, signed *)
-
+
| Pfabsd (**r float absolute double *)
| Pfabsw (**r float absolute word *)
| Pfnegd (**r float negate double *)
@@ -444,6 +444,11 @@ Inductive arith_name_arri64 : Type :=
| Pmaddil (**r multiply add long *)
.
+Inductive arith_name_arr : Type :=
+ | Pinsf (stop : Z) (start : Z) (**r insert bit field *)
+ | Pinsfl (stop : Z) (start : Z) (**r insert bit field *)
+.
+
Inductive ar_instruction : Type :=
| PArithR (i: arith_name_r) (rd: ireg)
| PArithRR (i: arith_name_rr) (rd rs: ireg)
@@ -455,6 +460,7 @@ Inductive ar_instruction : Type :=
| PArithRRI32 (i: arith_name_rri32) (rd rs: ireg) (imm: int)
| PArithRRI64 (i: arith_name_rri64) (rd rs: ireg) (imm: int64)
| PArithARRR (i: arith_name_arrr) (rd rs1 rs2: ireg)
+ | PArithARR (i: arith_name_arr) (rd rs: ireg)
| PArithARRI32 (i: arith_name_arri32) (rd rs: ireg) (imm: int)
| PArithARRI64 (i: arith_name_arri64) (rd rs: ireg) (imm: int64)
.
@@ -468,7 +474,8 @@ Coercion PArithRF64: arith_name_rf64 >-> Funclass.
Coercion PArithRRR: arith_name_rrr >-> Funclass.
Coercion PArithRRI32: arith_name_rri32 >-> Funclass.
Coercion PArithRRI64: arith_name_rri64 >-> Funclass.
-Coercion PArithARRR: arith_name_arrr >-> Funclass.
+Coercion PArithARRR: arith_name_arrr >-> Funclass.
+Coercion PArithARR: arith_name_arr >-> Funclass.
Coercion PArithARRI32: arith_name_arri32 >-> Funclass.
Coercion PArithARRI64: arith_name_arri64 >-> Funclass.
@@ -1048,6 +1055,12 @@ Definition arith_eval_arrr n v1 v2 v3 :=
end
end.
+Definition arith_eval_arr n v1 v2 :=
+ match n with
+ | Pinsf stop start => ExtValues.insf stop start v1 v2
+ | Pinsfl stop start => ExtValues.insfl stop start v1 v2
+ end.
+
Definition arith_eval_arri32 n v1 v2 v3 :=
match n with
| Pmaddiw => Val.add v1 (Val.mul v2 (Vint v3))
@@ -1074,6 +1087,7 @@ Definition parexec_arith_instr (ai: ar_instruction) (rsr rsw: regset): regset :=
| PArithRRI64 n d s i => rsw#d <- (arith_eval_rri64 n rsr#s i)
| PArithARRR n d s1 s2 => rsw#d <- (arith_eval_arrr n rsr#d rsr#s1 rsr#s2)
+ | PArithARR n d s => rsw#d <- (arith_eval_arr n rsr#d rsr#s)
| PArithARRI32 n d s i => rsw#d <- (arith_eval_arri32 n rsr#d rsr#s i)
| PArithARRI64 n d s i => rsw#d <- (arith_eval_arri64 n rsr#d rsr#s i)
end.
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index b9344116..e0ad2357 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -130,6 +130,11 @@ let arith_rri64_str = function
| Pandnil -> "Pandnil"
| Pornil -> "Pornil"
+
+let arith_arr_str = function
+ | Pinsf (_, _) -> "Pinsf"
+ | Pinsfl (_, _) -> "Pinsfl"
+
let arith_arrr_str = function
| Pmaddw -> "Pmaddw"
| Pmaddl -> "Pmaddl"
@@ -179,6 +184,8 @@ let arith_arri32_rec i rd rs imm32 = { inst = "Pmaddiw"; write_locs = [Reg rd];
let arith_arri64_rec i rd rs imm64 = { inst = "Pmaddil"; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs]; imm = imm64; is_control = false }
+let arith_arr_rec i rd rs = { inst = arith_arr_str i; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs]; imm = None; is_control = false}
+
let arith_arrr_rec i rd rs1 rs2 = { inst = arith_arrr_str i; write_locs = [Reg rd]; read_locs = [Reg rd; Reg rs1; Reg rs2]; imm = None; is_control = false}
let arith_rr_rec i rd rs = { inst = arith_rr_str i; write_locs = [Reg rd]; read_locs = [Reg rs]; imm = None; is_control = false}
@@ -192,6 +199,7 @@ let arith_rec i =
| PArithRRI32 (i, rd, rs, imm32) -> arith_rri32_rec i (IR rd) (IR rs) (Some (I32 imm32))
| PArithRRI64 (i, rd, rs, imm64) -> arith_rri64_rec i (IR rd) (IR rs) (Some (I64 imm64))
| PArithRRR (i, rd, rs1, rs2) -> arith_rrr_rec i (IR rd) (IR rs1) (IR rs2)
+ | PArithARR (i, rd, rs) -> arith_arr_rec i (IR rd) (IR rs)
(* Seems like single constant constructor types are elided *)
| PArithARRI32 ((* i,*) rd, rs, imm32) -> arith_arri32_rec () (IR rd) (IR rs) (Some (I32 imm32))
| PArithARRI64 ((* i,*) rd, rs, imm64) -> arith_arri64_rec () (IR rd) (IR rs) (Some (I64 imm64))
@@ -428,7 +436,7 @@ type real_instruction =
| Addd | Andd | Compd | Muld | Ord | Sbfd | Srad | Srld | Slld | Xord
| Nandw | Norw | Nxorw | Nandd | Nord | Nxord | Andnw | Ornw | Andnd | Ornd
| Maddw | Maddd | Cmoved
- | Make | Nop | Extfz | Extfs
+ | Make | Nop | Extfz | Extfs | Insf
(* LSU *)
| Lbs | Lbz | Lhs | Lhz | Lws | Ld
| Sb | Sh | Sw | Sd
@@ -480,6 +488,7 @@ let ab_inst_to_real = function
| "Pnop" | "Pcvtw2l" -> Nop
| "Pextfz" | "Pextfzl" | "Pzxwd" -> Extfz
| "Pextfs" | "Pextfsl" | "Psxwd" -> Extfs
+ | "Insf" | "Insfl" -> Insf
| "Pfnarrowdw" -> Fnarrowdw
| "Pfwidenlwd" -> Fwidenlwd
| "Pfloatwrnsz" -> Floatwz
@@ -574,7 +583,7 @@ let rec_to_usage r =
| Sraw | Srlw | Sllw | Srad | Srld | Slld -> (match encoding with None | Some U6 -> alu_tiny | _ -> raise InvalidEncoding)
(* TODO: check *)
| Rorw -> (match encoding with None | Some U6 -> alu_lite | _ -> raise InvalidEncoding)
- | Extfz | Extfs -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding)
+ | Extfz | Extfs | Insf -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding)
| Fixeduwz | Fixedwz | Floatwz | Floatuwz | Fixeddz | Fixedudz | Floatdz | Floatudz -> mau
| Lbs | Lbz | Lhs | Lhz | Lws | Ld ->
(match encoding with None | Some U6 | Some S10 -> lsu_data
@@ -597,7 +606,7 @@ let real_inst_to_latency = function
| Rorw | Nandw | Norw | Nxorw | Ornw | Andnw
| Nandd | Nord | Nxord | Ornd | Andnd
| Addd | Andd | Compd | Ord | Sbfd | Srad | Srld | Slld | Xord | Make
- | Extfs | Extfz | Fcompw | Fcompd | Cmoved
+ | Extfs | Extfz | Insf | Fcompw | Fcompd | Cmoved
-> 1
| Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4
| Mulw | Muld | Maddw | Maddd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *)
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index f986db39..99c89804 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -381,6 +381,8 @@ module Target (*: TARGET*) =
fprintf oc " extfz %a = %a, %ld, %ld\n" ireg rd ireg rs (camlint_of_coqint stop) (camlint_of_coqint start)
| Pextfs(rd, rs, stop, start) | Pextfsl(rd, rs, stop, start) ->
fprintf oc " extfs %a = %a, %ld, %ld\n" ireg rd ireg rs (camlint_of_coqint stop) (camlint_of_coqint start)
+ | Pinsf(rd, rs, stop, start) | Pinsfl(rd, rs, stop, start) ->
+ fprintf oc " insf %a = %a, %ld, %ld\n" ireg rd ireg rs (camlint_of_coqint stop) (camlint_of_coqint start)
| Pfabsd(rd, rs) ->
fprintf oc " fabsd %a = %a\n" ireg rd ireg rs
| Pfabsw(rd, rs) ->
generated by cgit (git 2.34.1) at 2024-07-07 04:27:37 +0000