diff options
| -rw-r--r-- | mppa_k1c/Peephole.v | 39 |
1 files changed, 38 insertions, 1 deletions
diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v index 3603c1d8..9fb0d898 100644 --- a/mppa_k1c/Peephole.v +++ b/mppa_k1c/Peephole.v @@ -13,6 +13,12 @@ R0R1 :: R2R3 :: R4R5 :: R6R7 :: R8R9 :: R50R51 :: R52R53 :: R54R55 :: R56R57 :: R58R59 :: R60R61 :: R62R63 :: nil. +Definition gpreg_o_list : list gpreg_o := +R0R1R2R3 :: R4R5R6R7 :: R8R9R10R11 :: R12R13R14R15 +:: R16R17R18R19 :: R20R21R22R23 :: R24R25R26R27 :: R28R29R30R31 +:: R32R33R34R35 :: R36R37R38R39 :: R40R41R42R43 :: R44R45R46R47 +:: R48R49R50R51 :: R52R53R54R55 :: R56R57R58R59 :: R60R61R62R63 :: nil. + Fixpoint gpreg_q_search_rec r0 r1 l := match l with | h :: t => @@ -23,9 +29,25 @@ Fixpoint gpreg_q_search_rec r0 r1 l := | nil => None end. +Fixpoint gpreg_o_search_rec r0 r1 r2 r3 l := + match l with + | h :: t => + match gpreg_o_expand h with + | (((s0, s1), s2), s3) => + if (gpreg_eq r0 s0) && (gpreg_eq r1 s1) && + (gpreg_eq r2 s2) && (gpreg_eq r3 s3) + then Some h + else gpreg_o_search_rec r0 r1 r2 r3 t + end + | nil => None + end. + Definition gpreg_q_search (r0 : gpreg) (r1 : gpreg) : option gpreg_q := gpreg_q_search_rec r0 r1 gpreg_q_list. +Definition gpreg_o_search r0 r1 r2 r3 : option gpreg_o := + gpreg_o_search_rec r0 r1 r2 r3 gpreg_o_list. + Parameter print_found_store: forall A, Z -> A -> A. Fixpoint coalesce_mem (insns : list basic) : list basic := @@ -42,7 +64,22 @@ Fixpoint coalesce_mem (insns : list basic) : list basic := let zofs0 := Ptrofs.signed ofs0 in let zofs1 := Ptrofs.signed ofs1 in if (zofs1 =? zofs0 + 8) && (ireg_eq ra0 ra1) - then (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1) + then + match t1 with + | (PStoreRRO Psd_a rs2 ra2 ofs2) :: + (PStoreRRO Psd_a rs3 ra3 ofs3) :: t3 => + match gpreg_o_search rs0 rs1 rs2 rs3 with + | Some octuple => + let zofs2 := Ptrofs.signed ofs2 in + let zofs3 := Ptrofs.signed ofs3 in + if (zofs2 =? zofs0 + 16) && (ireg_eq ra0 ra2) && + (zofs3 =? zofs0 + 24) && (ireg_eq ra0 ra3) + then (PStore (PStoreORRO octuple ra0 ofs0)) :: Pnop :: Pnop :: Pnop :: (coalesce_mem t3) + else (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1) + | None => (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1) + end + | _ => (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1) + end else h0 :: (coalesce_mem t0) | None => h0 :: (coalesce_mem t0) end |