From df9f42773b48270e77d1760719b1d8399062c2ea Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 2 May 2019 20:23:56 +0200 Subject: seems to work --- mppa_k1c/Peephole.v | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 mppa_k1c/Peephole.v (limited to 'mppa_k1c/Peephole.v') diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v new file mode 100644 index 00000000..56e547e5 --- /dev/null +++ b/mppa_k1c/Peephole.v @@ -0,0 +1,15 @@ +Require Import Asmvliw. + +Definition optimize_body (insns : list basic) := insns. + +Program Definition optimize_bblock (bb : bblock) := + let optimized := optimize_body (body bb) in + let wf_ok := wf_bblockb optimized (exit bb) in + {| header := header bb; + body := if wf_ok then optimized else (body bb); + exit := exit bb |}. +Next Obligation. + destruct (wf_bblockb (optimize_body (body bb))) eqn:Rwf. + - rewrite Rwf. simpl. trivial. + - exact (correct bb). +Qed. -- cgit From ec84544fb9f842caf98ca61669a8fb3024504ae2 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 2 May 2019 21:14:48 +0200 Subject: found peephole --- mppa_k1c/Peephole.v | 22 +++++++++++++++++++++- 1 file changed, 21 insertions(+), 1 deletion(-) (limited to 'mppa_k1c/Peephole.v') diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v index 56e547e5..b7931aca 100644 --- a/mppa_k1c/Peephole.v +++ b/mppa_k1c/Peephole.v @@ -1,6 +1,26 @@ +Require Import Coqlib. Require Import Asmvliw. +Require Import Values. +Require Import Integers. -Definition optimize_body (insns : list basic) := insns. +Parameter print_found_store : forall A : Type, Z -> A -> A. + +Fixpoint optimize_body (insns : list basic) : list basic := + match insns with + | nil => nil + | h0 :: t0 => + match t0 with + | h1 :: t1 => + match h0, h1 with + | (PStoreRRO Psd_a rs0 ra0 (Ofsimm ofs0)), + (PStoreRRO Psd_a rs1 ra1 (Ofsimm ofs1)) => + let h0' := print_found_store basic (Ptrofs.signed ofs0) h0 in + h0' :: (optimize_body t0) + | _, _ => h0 :: (optimize_body t0) + end + | nil => h0 :: nil + end + end. Program Definition optimize_bblock (bb : bblock) := let optimized := optimize_body (body bb) in -- cgit From 56ab9fea6dc937dac56e883a64f06cae3c931551 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 2 May 2019 21:20:14 +0200 Subject: detect consecutive ones --- mppa_k1c/Peephole.v | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'mppa_k1c/Peephole.v') diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v index b7931aca..47e04aec 100644 --- a/mppa_k1c/Peephole.v +++ b/mppa_k1c/Peephole.v @@ -14,8 +14,12 @@ 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 h0' := print_found_store basic (Ptrofs.signed ofs0) h0 in - h0' :: (optimize_body t0) + 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) | _, _ => h0 :: (optimize_body t0) end | nil => h0 :: nil -- cgit From 5d09dd8f3194ecc90137178d6b5d18b9ad31aabf Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 2 May 2019 21:58:47 +0200 Subject: find consecutive writes --- mppa_k1c/Peephole.v | 38 ++++++++++++++++++++++++++++++++------ 1 file changed, 32 insertions(+), 6 deletions(-) (limited to 'mppa_k1c/Peephole.v') 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 -- cgit From e1c864b670812eda55e0ee129855c69d32c8b84a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 3 May 2019 10:34:58 +0200 Subject: it compiles --- mppa_k1c/Peephole.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'mppa_k1c/Peephole.v') diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v index 2c73bb63..91936ac6 100644 --- a/mppa_k1c/Peephole.v +++ b/mppa_k1c/Peephole.v @@ -34,8 +34,8 @@ Fixpoint optimize_body (insns : list basic) : list basic := match t0 with | h1 :: t1 => match h0, h1 with - | (PStoreRRO Psd_a rs0 ra0 (Ofsimm ofs0)), - (PStoreRRO Psd_a rs1 ra1 (Ofsimm ofs1)) => + | (PStoreRRO Psd_a rs0 ra0 ofs0), + (PStoreRRO Psd_a rs1 ra1 ofs1) => match gpreg_q_search rs0 rs1 with | Some rs0rs1 => let zofs0 := Ptrofs.signed ofs0 in -- cgit From a289d73e791be5a760c8a9b2f3de2064f001a770 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 3 May 2019 11:17:57 +0200 Subject: use sq to save pairs of registers --- mppa_k1c/Peephole.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mppa_k1c/Peephole.v') diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v index 91936ac6..3e0d9ae9 100644 --- a/mppa_k1c/Peephole.v +++ b/mppa_k1c/Peephole.v @@ -42,7 +42,7 @@ Fixpoint optimize_body (insns : list basic) : list basic := 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) + (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (optimize_body t1) else h0 :: (optimize_body t0) | None => h0 :: (optimize_body t0) end -- cgit From cba53c98b999eea7984e4ffd24a9449abea3e0e2 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 3 May 2019 11:29:40 +0200 Subject: -fcoalesce-mem --- mppa_k1c/Peephole.v | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) (limited to 'mppa_k1c/Peephole.v') diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v index 3e0d9ae9..6e06e7ea 100644 --- a/mppa_k1c/Peephole.v +++ b/mppa_k1c/Peephole.v @@ -2,6 +2,7 @@ Require Import Coqlib. Require Import Asmvliw. Require Import Values. Require Import Integers. +Require Compopts. Definition gpreg_q_list : list gpreg_q := R0R1 :: R2R3 :: R4R5 :: R6R7 :: R8R9 @@ -25,9 +26,9 @@ Fixpoint gpreg_q_search_rec r0 r1 l := 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. +Parameter print_found_store: forall A, Z -> A -> A. -Fixpoint optimize_body (insns : list basic) : list basic := +Fixpoint coalesce_mem (insns : list basic) : list basic := match insns with | nil => nil | h0 :: t0 => @@ -41,17 +42,21 @@ Fixpoint optimize_body (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 let h0' := print_found_store basic zofs0 h0 in - (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (optimize_body t1) - else h0 :: (optimize_body t0) - | None => h0 :: (optimize_body t0) + then (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1) + else h0 :: (coalesce_mem t0) + | None => h0 :: (coalesce_mem t0) end - | _, _ => h0 :: (optimize_body t0) + | _, _ => h0 :: (coalesce_mem t0) end | nil => h0 :: nil end end. +Definition optimize_body (insns : list basic) := + if Compopts.optim_coalesce_mem tt + then coalesce_mem insns + else insns. + Program Definition optimize_bblock (bb : bblock) := let optimized := optimize_body (body bb) in let wf_ok := wf_bblockb optimized (exit bb) in -- cgit