From 54eb8e20fb0172aa47d1045ae56eb8fd2afe9d36 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 27 Apr 2019 21:32:15 +0200 Subject: begin add bitfield insertion --- mppa_k1c/Asm.v | 7 +++++++ mppa_k1c/Asmblockdeps.v | 20 ++++++++++++++++++-- mppa_k1c/Asmvliw.v | 18 ++++++++++++++++-- mppa_k1c/PostpassSchedulingOracle.ml | 15 ++++++++++++--- mppa_k1c/TargetPrinter.ml | 2 ++ 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) -> -- cgit