MPPA - optimized branch generation for signed long compare to 0

5 files changed, 69 insertions, 23 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 060cffd5..e1359cb0 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -95,13 +95,13 @@ Notation "'SP'" := GPR12 (only parsing) : asm.
 Notation "'RTMP'" := GPR31 (only parsing) : asm.
 
 Inductive btest: Type :=
-(*| BTdnez                              (**r Double Not Equal to Zero *)
+  | BTdnez                              (**r Double Not Equal to Zero *)
   | BTdeqz                              (**r Double Equal to Zero *)
   | BTdltz                              (**r Double Less Than Zero *)
   | BTdgez                              (**r Double Greater Than or Equal to Zero *)
   | BTdlez                              (**r Double Less Than or Equal to Zero *)
   | BTdgtz                              (**r Double Greater Than Zero *)
-  | BTodd                               (**r Odd (LSB Set) *)
+(*| BTodd                               (**r Odd (LSB Set) *)
   | BTeven                              (**r Even (LSB Clear) *)
 *)| BTwnez                              (**r Word Not Equal to Zero *)
   | BTweqz                              (**r Word Equal to Zero *)
@@ -566,6 +566,8 @@ Definition eval_branch (f: function) (l: label) (rs: regset) (m: mem) (res: opti
 
 Inductive signedness: Type := Signed | Unsigned.
 
+Inductive intsize: Type := Int | Long.
+
 Definition itest_for_cmp (c: comparison) (s: signedness) :=
   match c, s with
   | Cne, Signed => ITne
@@ -582,7 +584,7 @@ Definition itest_for_cmp (c: comparison) (s: signedness) :=
   | Cgt, Unsigned => ITgtu
   end.
 
-(* CoMParing Signed Words to Zero *)
+(* CoMPare Signed Words to Zero *)
 Definition btest_for_cmpswz (c: comparison) :=
   match c with
   | Cne => BTwnez
@@ -593,14 +595,32 @@ Definition btest_for_cmpswz (c: comparison) :=
   | Cgt => BTwgtz
   end.
 
+(* CoMPare Signed Doubles to Zero *)
+Definition btest_for_cmpsdz (c: comparison) :=
+  match c with
+  | Cne => BTdnez
+  | Ceq => BTdeqz
+  | Clt => BTdltz
+  | Cge => BTdgez
+  | Cle => BTdlez
+  | Cgt => BTdgtz
+  end.
+
 Definition cmp_for_btest (bt: btest) :=
   match bt with
-  | BTwnez => Some Cne
-  | BTweqz => Some Ceq
-  | BTwltz => Some Clt
-  | BTwgez => Some Cge
-  | BTwlez => Some Cle
-  | BTwgtz => Some Cgt
+  | BTwnez => (Some Cne, Int)
+  | BTweqz => (Some Ceq, Int)
+  | BTwltz => (Some Clt, Int)
+  | BTwgez => (Some Cge, Int)
+  | BTwlez => (Some Cle, Int)
+  | BTwgtz => (Some Cgt, Int)
+
+  | BTdnez => (Some Cne, Long)
+  | BTdeqz => (Some Ceq, Long)
+  | BTdltz => (Some Clt, Long)
+  | BTdgez => (Some Cge, Long)
+  | BTdlez => (Some Cle, Long)
+  | BTdgtz => (Some Cgt, Long)
   end.
 
 (** Comparing integers *)
@@ -715,8 +735,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
 (** Conditional branches *)
   | Pcb bt r l =>
       match cmp_for_btest bt with
-      | Some c => eval_branch f l rs m (Val.cmp_bool c rs##r (Vint (Int.repr 0)))
-      | None => Stuck
+      | (Some c, Int)  => eval_branch f l rs m (Val.cmp_bool c rs##r (Vint (Int.repr 0)))
+      | (Some c, Long) => eval_branch f l rs m (Val.cmpl_bool c rs###r (Vlong (Int64.repr 0)))
+      | (None, _) => Stuck
       end
 (*
 (** Conditional branches, 32-bit comparisons *)
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 5ee86240..4fed544f 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -183,7 +183,11 @@ Definition transl_cbranch
       OK (transl_compl c Unsigned r1 r2 lbl k)
   | Ccomplimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
-      OK (loadimm64 RTMP n (transl_compl c Signed r1 RTMP lbl k))
+      OK (if Int64.eq n Int64.zero then
+            Pcb (btest_for_cmpsdz c) r1 lbl :: k
+          else
+            loadimm64 RTMP n (transl_compl c Signed r1 RTMP lbl k)
+         )
 (*| Ccompf c, f1 :: f2 :: nil =>
       do r1 <- freg_of f1; do r2 <- freg_of f2;
       let (insn, normal) := transl_cond_float c rd r1 r2 in
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index e10290fd..a7a41f18 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -199,7 +199,8 @@ Proof.
 (* Ccomplu *)
   - unfold transl_compl; TailNoLabel.
 (* Ccomplimm *)
-  - unfold loadimm64. destruct (make_immed64 n); TailNoLabel. unfold transl_compl; TailNoLabel.
+  - destruct (Int64.eq n Int64.zero); TailNoLabel.
+    unfold loadimm64. destruct (make_immed64 n); TailNoLabel. unfold transl_compl; TailNoLabel.
 (* Ccompluimm *)
   - unfold loadimm64. destruct (make_immed64 n); TailNoLabel. unfold transl_compl; TailNoLabel.
 Qed.
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index 27b43c17..aeee5e9e 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -601,16 +601,30 @@ Proof.
   + constructor. eexact A.
   + split; auto. apply C; auto.
 (* Ccomplimm *)
-- exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C).
-  exploit (transl_compl_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
-  exists rs'2, (Pcb BTwnez GPR31 lbl).
-  split.
-  + constructor. apply exec_straight_trans 
-       with (c2 := (transl_compl c0 Signed x GPR31 lbl k)) (rs2 := rs') (m2 := m').
-    eexact A. eexact A'.
-  + split; auto.
-    * apply C'; auto. unfold getl. rewrite B, C; eauto with asmgen.
-    * intros. rewrite B'; eauto with asmgen.
+- remember (Int64.eq n Int64.zero) as eqz.
+  destruct eqz.
+  + assert (n = (Int64.repr 0)). { 
+        destruct (Int64.eq_dec n (Int64.repr 0)) as [H|H]; auto. 
+        generalize (Int64.eq_false _ _ H).  unfold Int64.zero in Heqeqz.
+        rewrite <- Heqeqz. discriminate.
+    }
+    exists rs, (Pcb (btest_for_cmpsdz c0) x lbl).
+    split. 
+    * constructor.
+    * split; auto.
+      destruct c0; simpl; auto;
+      unfold eval_branch; rewrite <- H; unfold getl; rewrite EVAL'; auto.
+  + exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C).
+    exploit (transl_compl_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
+    exists rs'2, (Pcb BTwnez GPR31 lbl).
+    split.
+    * constructor. apply exec_straight_trans 
+         with (c2 := (transl_compl c0 Signed x GPR31 lbl k)) (rs2 := rs') (m2 := m').
+      eexact A. eexact A'.
+    * split; auto.
+      { apply C'; auto. unfold getl. rewrite B, C; eauto with asmgen. }
+      { intros. rewrite B'; eauto with asmgen. }
+
 (* Ccompluimm *)
 - exploit (loadimm64_correct GPR31 n); eauto. intros (rs' & A & B & C).
   exploit (transl_complu_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 72f6e12a..dcae5b10 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -181,6 +181,12 @@ module Target : TARGET =
       | BTwgez -> "wgez"
       | BTwlez -> "wlez"
       | BTwgtz -> "wgtz"
+      | BTdnez -> "dnez"
+      | BTdeqz -> "deqz"
+      | BTdltz -> "dltz"
+      | BTdgez -> "dgez"
+      | BTdlez -> "dlez"
+      | BTdgtz -> "dgtz"
 
     let bcond oc c = fprintf oc "%s" (bcond_name c)