diff options
Diffstat (limited to 'mppa_k1c')
| -rw-r--r-- | mppa_k1c/Asmvliw.v | 51 | ||||
| -rw-r--r-- | mppa_k1c/Peephole.v | 38 |
2 files changed, 83 insertions, 6 deletions
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index e460727c..0cbe27e1 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -66,12 +66,63 @@ Inductive gpreg: Type := Definition ireg := gpreg. Definition freg := gpreg. +Lemma gpreg_eq: forall (x y: gpreg), {x=y} + {x<>y}. +Proof. decide equality. Defined. + Lemma ireg_eq: forall (x y: ireg), {x=y} + {x<>y}. Proof. decide equality. Defined. Lemma freg_eq: forall (x y: freg), {x=y} + {x<>y}. Proof. decide equality. Defined. +Inductive gpreg_q : Type := +| R0R1 | R2R3 | R4R5 | R6R7 | R8R9 +| R10R11 | R12R13 | R14R15 | R16R17 | R18R19 +| R20R21 | R22R23 | R24R25 | R26R27 | R28R29 +| R30R31 | R32R33 | R34R35 | R36R37 | R38R39 +| R40R41 | R42R43 | R44R45 | R46R47 | R48R49 +| R50R51 | R52R53 | R54R55 | R56R57 | R58R59 +| R60R61 | R62R63. + +Lemma gpreg_q_eq : forall (x y : gpreg_q), {x=y} + {x<>y}. +Proof. decide equality. Defined. + +Definition gpreg_q_expand (x : gpreg_q) : gpreg * gpreg := + match x with + | R0R1 => (GPR0, GPR1) + | R2R3 => (GPR2, GPR3) + | R4R5 => (GPR4, GPR5) + | R6R7 => (GPR6, GPR7) + | R8R9 => (GPR8, GPR9) + | R10R11 => (GPR10, GPR11) + | R12R13 => (GPR12, GPR13) + | R14R15 => (GPR14, GPR15) + | R16R17 => (GPR16, GPR17) + | R18R19 => (GPR18, GPR19) + | R20R21 => (GPR20, GPR21) + | R22R23 => (GPR22, GPR23) + | R24R25 => (GPR24, GPR25) + | R26R27 => (GPR26, GPR27) + | R28R29 => (GPR28, GPR29) + | R30R31 => (GPR30, GPR31) + | R32R33 => (GPR32, GPR33) + | R34R35 => (GPR34, GPR35) + | R36R37 => (GPR36, GPR37) + | R38R39 => (GPR38, GPR39) + | R40R41 => (GPR40, GPR41) + | R42R43 => (GPR42, GPR43) + | R44R45 => (GPR44, GPR45) + | R46R47 => (GPR46, GPR47) + | R48R49 => (GPR48, GPR49) + | R50R51 => (GPR50, GPR51) + | R52R53 => (GPR52, GPR53) + | R54R55 => (GPR54, GPR55) + | R56R57 => (GPR56, GPR57) + | R58R59 => (GPR58, GPR59) + | R60R61 => (GPR60, GPR61) + | R62R63 => (GPR62, GPR63) + end. + (** We model the following registers of the RISC-V architecture. *) (** basic register *) diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v index 47e04aec..2c73bb63 100644 --- a/mppa_k1c/Peephole.v +++ b/mppa_k1c/Peephole.v @@ -3,6 +3,28 @@ Require Import Asmvliw. Require Import Values. Require Import Integers. +Definition gpreg_q_list : list gpreg_q := +R0R1 :: R2R3 :: R4R5 :: R6R7 :: R8R9 +:: R10R11 :: R12R13 :: R14R15 :: R16R17 :: R18R19 +:: R20R21 :: R22R23 :: R24R25 :: R26R27 :: R28R29 +:: R30R31 :: R32R33 :: R34R35 :: R36R37 :: R38R39 +:: R40R41 :: R42R43 :: R44R45 :: R46R47 :: R48R49 +:: R50R51 :: R52R53 :: R54R55 :: R56R57 :: R58R59 +:: R60R61 :: R62R63 :: nil. + +Fixpoint gpreg_q_search_rec r0 r1 l := + match l with + | h :: t => + let (s0, s1) := gpreg_q_expand h in + if (gpreg_eq r0 s0) && (gpreg_eq r1 s1) + then Some h + else gpreg_q_search_rec r0 r1 t + | nil => None + end. + +Definition gpreg_q_search (r0 : gpreg) (r1 : gpreg) : option gpreg_q := + gpreg_q_search_rec r0 r1 gpreg_q_list. + Parameter print_found_store : forall A : Type, Z -> A -> A. Fixpoint optimize_body (insns : list basic) : list basic := @@ -14,12 +36,16 @@ Fixpoint optimize_body (insns : list basic) : list basic := match h0, h1 with | (PStoreRRO Psd_a rs0 ra0 (Ofsimm ofs0)), (PStoreRRO Psd_a rs1 ra1 (Ofsimm ofs1)) => - let zofs0 := Ptrofs.signed ofs0 in - let zofs1 := Ptrofs.signed ofs1 in - if zofs1 =? zofs0 + 8 - then let h0' := print_found_store basic zofs0 h0 in - h0' :: (optimize_body t0) - else h0 :: (optimize_body t0) + match gpreg_q_search rs0 rs1 with + | Some rs0rs1 => + let zofs0 := Ptrofs.signed ofs0 in + let zofs1 := Ptrofs.signed ofs1 in + if (zofs1 =? zofs0 + 8) && (ireg_eq ra0 ra1) + then let h0' := print_found_store basic zofs0 h0 in + h0' :: (optimize_body t0) + else h0 :: (optimize_body t0) + | None => h0 :: (optimize_body t0) + end | _, _ => h0 :: (optimize_body t0) end | nil => h0 :: nil |