Commit e20c07dd authored by Cyril SIX's avatar Cyril SIX
Browse files

MPPA - Optimized branch generation for word compare to 0

parent a724c959
(* Replace transl_op by this wrapper to print the op *)
let thereal_transl_op op args res0 k =
match op with
| Ointconst n ->
(match args with
| [] ->
(match ireg_of res0 with
| OK x -> OK (loadimm32 x n k)
| Error msg0 -> Error msg0)
| _ :: _ ->
Error
(msg
('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('o'::('p'::[]))))))))))))))))))
| Olongconst n ->
(match args with
| [] ->
(match ireg_of res0 with
| OK x -> OK (loadimm64 x n k)
| Error msg0 -> Error msg0)
| _ :: _ ->
Error
(msg
('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('o'::('p'::[]))))))))))))))))))
| Oaddl ->
(match args with
| [] ->
Error
(msg
('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('o'::('p'::[])))))))))))))))))
| a1 :: l ->
(match l with
| [] ->
Error
(msg
('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('o'::('p'::[])))))))))))))))))
| a2 :: l0 ->
(match l0 with
| [] ->
(match ireg_of res0 with
| OK x ->
(match ireg_of a1 with
| OK x0 ->
(match ireg_of a2 with
| OK x1 -> OK ((Paddl (x, x0, x1)) :: k)
| Error msg0 -> Error msg0)
| Error msg0 -> Error msg0)
| Error msg0 -> Error msg0)
| _ :: _ ->
Error
(msg
('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('o'::('p'::[]))))))))))))))))))))
| Oaddlimm n ->
(match args with
| [] ->
Error
(msg
('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('o'::('p'::[])))))))))))))))))
| a1 :: l ->
(match l with
| [] ->
(match ireg_of res0 with
| OK x ->
(match ireg_of a1 with
| OK x0 -> OK (addimm64 x x0 n k)
| Error msg0 -> Error msg0)
| Error msg0 -> Error msg0)
| _ :: _ ->
Error
(msg
('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('o'::('p'::[])))))))))))))))))))
| _ ->
Error
(msg
('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('o'::('p'::[])))))))))))))))))
let transl_op op args res0 k =
match op with
| Omove -> (Printf.eprintf "Omove\n"; thereal_transl_op op args res0 k)
......@@ -166,19 +92,6 @@ let transl_op op args res0 k =
| Ocmp _ -> (Printf.eprintf "Ocmp _\n"; thereal_transl_op op args res0 k)
| _ -> (Printf.eprintf "_\n"; thereal_transl_op op args res0 k)
let thereal_transl_instr f i _ k =
match i with
| Mop (op, args, res0) -> transl_op op args res0 k
| Mbuiltin (ef, args, res0) ->
OK ((Pbuiltin (ef, (map (map_builtin_arg preg_of) args),
(map_builtin_res preg_of res0))) :: k)
| Mlabel lbl -> OK ((Plabel lbl) :: k)
| Mreturn -> OK (make_epilogue f (Pret :: k))
| _ ->
Error
(msg
('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('i'::('n'::('s'::('t'::('r'::[]))))))))))))))))))))
let transl_instr f i x k =
match i with
| Mgetstack _ -> (Printf.eprintf "Mgetstack\n"; thereal_transl_instr f i x k)
......
......@@ -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 *)
......
......@@ -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))
......
......@@ -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 *)
......
......@@ -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 ->
......
......@@ -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)
......
DIR=general
TESTNAMES=simple call branch for forvar forvarl
TESTNAMES=simple call branch for forvar forvarl branchz branchzu
TESTS=$(addprefix $(DIR)/,$(TESTNAMES))
ELF=$(addsuffix .bin,$(TESTS))
......
int main(void){
int a=1;
int b;
if(a==0){
b = a+4;
} else {
b = a+2;
}
return b;
}
int main(void){
int a=1;
int b;
if(!a){
b = a+4;
} else {
b = a+2;
}
return b;
}
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