From 3916ecbc8c77c99bab0bd69de184ae432fd9d3f4 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 3 May 2019 16:48:07 +0200
Subject: Lq finished ?

---
 mppa_k1c/Asmblockdeps.v              | 31 ++++++++++++++++---------------
 mppa_k1c/Peephole.v                  | 11 +++++++++++
 mppa_k1c/PostpassSchedulingOracle.ml |  7 ++++---
 3 files changed, 31 insertions(+), 18 deletions(-)

(limited to 'mppa_k1c')

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index ee4a9b51..225c3e98 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -366,10 +366,23 @@ Qed.
 Hint Resolve arith_op_eq_correct: wlp.
 Opaque arith_op_eq_correct.
 
+Definition offset_eq (ofs1 ofs2 : offset): ?? bool :=
+  RET (Ptrofs.eq ofs1 ofs2).
+
+Lemma offset_eq_correct ofs1 ofs2:
+  WHEN offset_eq ofs1 ofs2 ~> b THEN b = true -> ofs1 = ofs2.
+Proof.
+  wlp_simplify.
+  pose (Ptrofs.eq_spec ofs1 ofs2).
+  rewrite H in *.
+  trivial.
+Qed.
+Hint Resolve offset_eq_correct: wlp.
+
 Definition load_op_eq (o1 o2: load_op): ?? bool :=
   match o1 with
   | OLoadRRO n1 ofs1 =>
-     match o2 with OLoadRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) | _ => RET false end
+     match o2 with OLoadRRO n2 ofs2 => iandb (phys_eq n1 n2) (offset_eq ofs1 ofs2) | _ => RET false end
   | OLoadRRR n1 =>
      match o2 with OLoadRRR n2 => phys_eq n1 n2 | _ => RET false end
   | OLoadRRRXS n1 =>
@@ -380,26 +393,14 @@ Lemma load_op_eq_correct o1 o2:
   WHEN load_op_eq o1 o2 ~> b THEN b = true -> o1 = o2.
 Proof.
   destruct o1, o2; wlp_simplify; try discriminate.
-  - congruence.
+  - f_equal. pose (Ptrofs.eq_spec ofs ofs0).
+    rewrite H in *. trivial.
   - congruence.
   - congruence.
 Qed.
 Hint Resolve load_op_eq_correct: wlp.
 Opaque load_op_eq_correct.
 
-Definition offset_eq (ofs1 ofs2 : offset): ?? bool :=
-  RET (Ptrofs.eq ofs1 ofs2).
-
-Lemma offset_eq_correct ofs1 ofs2:
-  WHEN offset_eq ofs1 ofs2 ~> b THEN b = true -> ofs1 = ofs2.
-Proof.
-  wlp_simplify.
-  pose (Ptrofs.eq_spec ofs1 ofs2).
-  rewrite H in *.
-  trivial.
-Qed.
-Hint Resolve offset_eq_correct: wlp.
-
 Definition store_op_eq (o1 o2: store_op): ?? bool :=
   match o1 with
   | OStoreRRO n1 ofs1 =>
diff --git a/mppa_k1c/Peephole.v b/mppa_k1c/Peephole.v
index 6e06e7ea..3603c1d8 100644
--- a/mppa_k1c/Peephole.v
+++ b/mppa_k1c/Peephole.v
@@ -46,6 +46,17 @@ Fixpoint coalesce_mem (insns : list basic) : list basic :=
             else h0 :: (coalesce_mem t0)
           | None => h0 :: (coalesce_mem t0)
           end
+        | (PLoadRRO Pld_a rd0 ra0 ofs0),
+          (PLoadRRO Pld_a rd1 ra1 ofs1) =>
+          match gpreg_q_search rd0 rd1 with
+          | Some rd0rd1 =>
+            let zofs0 := Ptrofs.signed ofs0 in
+            let zofs1 := Ptrofs.signed ofs1 in
+            if (zofs1 =? zofs0 + 8) && (ireg_eq ra0 ra1) && negb (ireg_eq ra0 rd0)
+            then (PLoad (PLoadQRRO rd0rd1 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
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index e3d43237..d3f16366 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -448,7 +448,7 @@ type real_instruction =
   | Maddw | Maddd | Cmoved
   | Make | Nop | Extfz | Extfs | Insf
   (* LSU *)
-  | Lbs | Lbz | Lhs | Lhz | Lws | Ld
+  | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq
   | Sb | Sh | Sw | Sd | Sq
   (* BCU *)
   | Icall | Call | Cb | Igoto | Goto | Ret | Get | Set
@@ -521,6 +521,7 @@ let ab_inst_to_real = function
   | "Plhu" -> Lhz 
   | "Plw" | "Plw_a" | "Pfls" -> Lws 
   | "Pld" | "Pfld" | "Pld_a" -> Ld
+  | "Plq" -> Lq
 
   | "Psb" -> Sb
   | "Psh" -> Sh 
@@ -598,7 +599,7 @@ let rec_to_usage r =
   | Rorw -> (match encoding with None | Some U6 -> alu_lite | _ -> raise InvalidEncoding)
   | Extfz | Extfs | Insf -> (match encoding with None -> alu_lite | _ -> raise InvalidEncoding)
   | Fixeduwz | Fixedwz | Floatwz | Floatuwz | Fixeddz | Fixedudz | Floatdz | Floatudz -> mau
-  | Lbs | Lbz | Lhs | Lhz | Lws | Ld -> 
+  | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq -> 
       (match encoding with None | Some U6 | Some S10 -> lsu_data 
                           | Some U27L5 | Some U27L10 -> lsu_data_x 
                           | Some E27U27L10 -> lsu_data_y)
@@ -623,7 +624,7 @@ let real_inst_to_latency = function
         -> 1
   | Floatwz | Floatuwz | Fixeduwz | Fixedwz | Floatdz | Floatudz | Fixeddz | Fixedudz -> 4
   | Mulw | Muld | Maddw | Maddd -> 2 (* FIXME - WORST CASE. If it's S10 then it's only 1 *)
-  | Lbs | Lbz | Lhs | Lhz | Lws | Ld -> 3
+  | Lbs | Lbz | Lhs | Lhz | Lws | Ld | Lq -> 3
   | Sb | Sh | Sw | Sd | Sq -> 1 (* See k1c-Optimization.pdf page 19 *)
   | Get -> 1
   | Set -> 4 (* According to the manual should be 3, but I measured 4 *)
-- 
cgit