MPPA - Optimized branch generation for word compare to 0

5 files changed, 178 insertions, 30 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index d19f9340..060cffd5 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -105,11 +105,11 @@ Inductive btest: Type :=
   | BTeven                              (**r Even (LSB Clear) *)
 *)| BTwnez                              (**r Word Not Equal to Zero *)
   | BTweqz                              (**r Word Equal to Zero *)
-(*| BTwltz                              (**r Word Less Than Zero *)
+  | BTwltz                              (**r Word Less Than Zero *)
   | BTwgez                              (**r Word Greater Than or Equal to Zero *)
   | BTwlez                              (**r Word Less Than or Equal to Zero *)
   | BTwgtz                              (**r Word Greater Than Zero *)
-*).
+  .
 
 Inductive itest: Type :=
   | ITne                                (**r Not Equal *)
@@ -582,6 +582,27 @@ Definition itest_for_cmp (c: comparison) (s: signedness) :=
   | Cgt, Unsigned => ITgtu
   end.
 
+(* CoMParing Signed Words to Zero *)
+Definition btest_for_cmpswz (c: comparison) :=
+  match c with
+  | Cne => BTwnez
+  | Ceq => BTweqz
+  | Clt => BTwltz
+  | Cge => BTwgez
+  | Cle => BTwlez
+  | Cgt => BTwgtz
+  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
+  end.
+
 (** Comparing integers *)
 Definition compare_int (t: itest) (v1 v2: val) (m: mem): val :=
   match t with
@@ -693,9 +714,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
 
 (** Conditional branches *)
   | Pcb bt r l =>
-      match bt with
-      | BTwnez => eval_branch f l rs m (Val.cmp_bool Cne rs##r (Vint (Int.repr 0)))
-      | _ => Stuck
+      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
       end
 (*
 (** Conditional branches, 32-bit comparisons *)
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 710bb32c..5ee86240 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -132,12 +132,33 @@ Definition transl_compl
     (c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction :=
   Pcompd (itest_for_cmp c s) RTMP r1 r2 :: Pcb BTwnez RTMP lbl :: k.
 
+Definition select_comp (n: int) (c: comparison) : option comparison :=
+  if Int.eq n Int.zero then
+    match c with
+    | Ceq => Some Ceq
+    | Cne => Some Cne
+    | _   => None
+    end
+  else
+    None
+  .
+
+Definition transl_opt_compuimm
+    (n: int) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction :=
+  match select_comp n c with
+  | Some Ceq => Pcb BTweqz r1 lbl :: k
+  | Some Cne => Pcb BTwnez r1 lbl :: k
+  | Some _   => nil (* Never happens *)
+  | None     => loadimm32 RTMP n (transl_comp c Unsigned r1 RTMP lbl k)
+  end
+  .
+
 Definition transl_cbranch
     (cond: condition) (args: list mreg) (lbl: label) (k: code) : res (list instruction ) :=
   match cond, args with
   | Ccompuimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
-      OK (loadimm32 RTMP n (transl_comp c Unsigned r1 RTMP lbl k))
+      OK (transl_opt_compuimm n c r1 lbl k)
   | Ccomp c, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2;
       OK (transl_comp c Signed r1 r2 lbl k)
@@ -146,7 +167,11 @@ Definition transl_cbranch
       OK (transl_comp c Unsigned r1 r2 lbl k)
   | Ccompimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
-      OK (loadimm32 RTMP n (transl_comp c Signed r1 RTMP lbl k))
+      OK (if Int.eq n Int.zero then
+            Pcb (btest_for_cmpswz c) r1 lbl :: k
+          else
+            loadimm32 RTMP n (transl_comp c Signed r1 RTMP lbl k)
+         )
   | Ccompluimm c n, a1 :: nil =>
       do r1 <- ireg_of a1;
       OK (loadimm64 RTMP n (transl_compl c Unsigned r1 RTMP lbl k))
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 3dce24cf..e10290fd 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -185,9 +185,15 @@ Proof.
 (* Ccompu *)
   - unfold transl_comp; TailNoLabel.
 (* Ccompimm *)
-  - unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel.
+  - destruct (Int.eq n Int.zero); TailNoLabel.
+    unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel.
 (* Ccompuimm *)
-  - unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel.
+  - unfold transl_opt_compuimm.
+    remember (select_comp n c0) as selcomp; destruct selcomp.
+    + destruct c; TailNoLabel; contradict Heqselcomp; unfold select_comp;
+      destruct (Int.eq n Int.zero); destruct c0; discriminate.
+    + unfold loadimm32;
+      destruct (make_immed32 n); TailNoLabel; unfold transl_comp; TailNoLabel.
 (* Ccompl *)
   - unfold transl_compl; TailNoLabel.
 (* Ccomplu *)
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index fe037994..27b43c17 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -444,6 +444,77 @@ Proof.
     rewrite H0. simpl; auto.
 Qed.
 
+Lemma transl_opt_compuimm_correct:
+  forall n cmp r1 lbl k rs m b c,
+  select_comp n cmp = Some c ->
+  exists rs', exists insn,
+     exec_straight_opt (transl_opt_compuimm n cmp r1 lbl k) rs m (insn :: k) rs' m
+  /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)  
+  /\ ( Val.cmpu_bool (Mem.valid_pointer m) cmp rs##r1 (Vint n) = Some b ->
+       exec_instr ge fn insn rs' m = eval_branch fn lbl rs' m (Some b))
+  .
+Proof.
+  intros.
+  unfold transl_opt_compuimm; rewrite H; simpl.
+  remember c as c'.
+  destruct c'.
+  - (* c = Ceq *)
+    assert (Int.eq n Int.zero = true) as H'. 
+    { remember (Int.eq n Int.zero) as termz. destruct termz; auto.
+      generalize H. unfold select_comp; rewrite <- Heqtermz; simpl.
+      discriminate. }
+    assert (n = (Int.repr 0)) as H0. { 
+      destruct (Int.eq_dec n (Int.repr 0)) as [Ha|Ha]; auto. 
+      generalize (Int.eq_false _ _ Ha).  unfold Int.zero in H'.
+      rewrite H'. discriminate.
+    }
+    assert (Ceq = cmp). { 
+      remember cmp as c0'. destruct c0'; auto; generalize H; unfold select_comp;
+      rewrite H'; simpl; auto;
+      intros; contradict H; discriminate.
+    }
+
+    exists rs, (Pcb BTweqz r1 lbl).
+    split.
+    * constructor.
+    * split; auto. simpl. intros.
+      assert (Val.cmp_bool Ceq (rs r1) (Vint (Int.repr 0)) = Some b) as EVAL'S.
+      { rewrite <- H2. rewrite <- H0. rewrite <- H1. auto. }
+      auto;
+      unfold eval_branch. unfold getw. rewrite EVAL'S; auto.
+  - (* c = Cne *)
+    assert (Int.eq n Int.zero = true) as H'. 
+    { remember (Int.eq n Int.zero) as termz. destruct termz; auto.
+      generalize H. unfold select_comp; rewrite <- Heqtermz; simpl.
+      discriminate. }
+    assert (n = (Int.repr 0)) as H0. { 
+      destruct (Int.eq_dec n (Int.repr 0)) as [Ha|Ha]; auto. 
+      generalize (Int.eq_false _ _ Ha).  unfold Int.zero in H'.
+      rewrite H'. discriminate.
+    }
+    assert (Cne = cmp). { 
+      remember cmp as c0'. destruct c0'; auto; generalize H; unfold select_comp;
+      rewrite H'; simpl; auto;
+      intros; contradict H; discriminate.
+    }
+    exists rs, (Pcb BTwnez r1 lbl).
+    split.
+    * constructor.
+    * split; auto. simpl. intros.
+      assert (Val.cmp_bool Cne (rs r1) (Vint (Int.repr 0)) = Some b) as EVAL'S.
+      { rewrite <- H2. rewrite <- H0. rewrite <- H1. auto. }
+      auto;
+      unfold eval_branch. unfold getw. rewrite EVAL'S; auto.
+  - (* c = Clt *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero);
+    destruct cmp; discriminate.
+  - (* c = Cle *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero);
+    destruct cmp; discriminate.
+  - (* c = Cgt *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero);
+    destruct cmp; discriminate.
+  - (* c = Cge *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero);
+    destruct cmp; discriminate.
+Qed.
+
 Lemma transl_cbranch_correct_1:
   forall cond args lbl k c m ms b sp rs m',
   transl_cbranch cond args lbl k = OK c ->
@@ -474,27 +545,49 @@ Proof.
   + constructor. eexact A.
   + split; auto. apply C; auto.
 (* Ccompimm *)
-- exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C).
-  exploit (transl_comp_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_comp c0 Signed x GPR31 lbl k)) (rs2 := rs') (m2 := m').
-    eexact A. eexact A'.
-  + split; auto.
-    * apply C'; auto. unfold getw. rewrite B, C; eauto with asmgen.
-    * intros. rewrite B'; eauto with asmgen.
+- remember (Int.eq n Int.zero) as eqz.
+  destruct eqz.
+  + assert (n = (Int.repr 0)). { 
+        destruct (Int.eq_dec n (Int.repr 0)) as [H|H]; auto. 
+        generalize (Int.eq_false _ _ H).  unfold Int.zero in Heqeqz.
+        rewrite <- Heqeqz. discriminate.
+    }
+    exists rs, (Pcb (btest_for_cmpswz c0) x lbl).
+    split. 
+    * constructor.
+    * split; auto.
+      destruct c0; simpl; auto;
+      unfold eval_branch; rewrite <- H; unfold getw; rewrite EVAL'; auto.
+  + exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C).
+    exploit (transl_comp_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_comp c0 Signed x GPR31 lbl k)) (rs2 := rs') (m2 := m').
+      eexact A. eexact A'.
+    * split; auto.
+      { apply C'; auto. unfold getw. rewrite B, C; eauto with asmgen. }
+      { intros. rewrite B'; eauto with asmgen. }
 (* Ccompuimm *)
-- exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C).
-  exploit (transl_compu_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_comp c0 Unsigned x GPR31 lbl k)) (rs2 := rs') (m2 := m').
-    eexact A. eexact A'.
-  + split; auto.
-    * apply C'; auto. unfold getw. rewrite B, C; eauto with asmgen.
-    * intros. rewrite B'; eauto with asmgen.
+- remember (select_comp n c0) as selcomp.
+  destruct selcomp.
+  + exploit (transl_opt_compuimm_correct n c0 x lbl k). apply eq_sym. apply Heqselcomp.
+    intros (rs' & i & A & B & C).
+    exists rs', i.
+    split.
+    * apply A.
+    * split; auto. apply C. apply EVAL'.
+  + unfold transl_opt_compuimm. rewrite <- Heqselcomp; simpl.
+    exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C).
+    exploit (transl_compu_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_comp c0 Unsigned x GPR31 lbl k)) (rs2 := rs') (m2 := m').
+      eexact A. eexact A'.
+    * split; auto.
+      { apply C'; auto. unfold getw. rewrite B, C; eauto with asmgen. }
+      { intros. rewrite B'; eauto with asmgen. }
 (* Ccompl *)
 - exploit (transl_compl_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
   exists rs', (Pcb BTwnez GPR31 lbl).
@@ -531,7 +624,6 @@ Proof.
     * intros. rewrite B'; eauto with asmgen.
 Qed.
 
-
 Lemma transl_cbranch_correct_true:
   forall cond args lbl k c m ms sp rs m',
   transl_cbranch cond args lbl k = OK c ->
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index ac6f8f1b..72f6e12a 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -177,6 +177,10 @@ module Target : TARGET =
     let bcond_name = function
       | BTwnez -> "wnez"
       | BTweqz -> "weqz"
+      | BTwltz -> "wltz"
+      | BTwgez -> "wgez"
+      | BTwlez -> "wlez"
+      | BTwgtz -> "wgtz"
 
     let bcond oc c = fprintf oc "%s" (bcond_name c)