find consecutive writes

1 files changed, 32 insertions, 6 deletions

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