Commit 1fecf8b3 authored by Cyril SIX's avatar Cyril SIX
Browse files

MPPA - optimized branch generation for signed long compare to 0

parent e20c07dd
......@@ -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 *)
......
......@@ -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
......
......@@ -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.
......
......@@ -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').
......
......@@ -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)
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment