diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 11:34:22 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 11:34:22 +0200 |
commit | ad8f16390a68b0cf8e4da39d2ae5d1ad30026803 (patch) | |
tree | 5f0e12eccd40bcc688408cb5d07dc8d850832384 /mppa_k1c/Peephole.v | |
parent | fb77ce264f957a1ee3f87e537b55afbb10785ecf (diff) | |
parent | cba53c98b999eea7984e4ffd24a9449abea3e0e2 (diff) | |
download | compcert-kvx-ad8f16390a68b0cf8e4da39d2ae5d1ad30026803.tar.gz compcert-kvx-ad8f16390a68b0cf8e4da39d2ae5d1ad30026803.zip |
Merge remote-tracking branch 'origin/mppa-peephole' into mppa-work
Diffstat (limited to 'mppa_k1c/Peephole.v')
-rw-r--r-- | mppa_k1c/Peephole.v | 70 |
1 files changed, 70 insertions, 0 deletions
diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v new file mode 100644 index 00000000..6e06e7ea --- /dev/null +++ b/mppa_k1c/Peephole.v @@ -0,0 +1,70 @@ +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 +:: 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, Z -> A -> A. + +Fixpoint coalesce_mem (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 ofs0), + (PStoreRRO Psd_a rs1 ra1 ofs1) => + 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 (PStore (PStoreQRRO rs0rs1 ra0 ofs0)) :: Pnop :: (coalesce_mem t1) + else h0 :: (coalesce_mem t0) + | None => h0 :: (coalesce_mem t0) + end + | _, _ => 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 + {| 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. |