From a745efa7f07a10cec625b9c302eb0196b7bfaefb Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 26 Feb 2009 14:48:59 +0000 Subject: Reserve register GPR13 for compatibility with EABI. Optimize operations 'x >= 0' and 'x < 0'. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@999 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asmgenproof.v | 29 ++++++++++++++++++++++++----- 1 file changed, 24 insertions(+), 5 deletions(-) (limited to 'powerpc/Asmgenproof.v') diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index a96125a2..40c593a3 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -432,6 +432,30 @@ Proof. apply andimm_label. apply andimm_label. Qed. Hint Rewrite transl_cond_label: labels. + +Remark transl_op_cmp_label: + forall c args r k, + find_label lbl + (match classify_condition c args with + | condition_ge0 _ a _ => + Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one + :: Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k + | condition_lt0 _ a _ => + Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one :: k + | condition_default _ _ => + transl_cond c args + (Pmfcrbit (ireg_of r) (fst (crbit_for_cond c)) + :: (if snd (crbit_for_cond c) + then k + else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k)) + end) = find_label lbl k. +Proof. + intros. destruct (classify_condition c args); auto. + autorewrite with labels. + case (snd (crbit_for_cond c)); auto. +Qed. +Hint Rewrite transl_op_cmp_label: labels. + Remark transl_op_label: forall op args r k, find_label lbl (transl_op op args r k) = find_label lbl k. Proof. @@ -441,11 +465,6 @@ Proof. case (mreg_type m); reflexivity. case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity. case (Int.eq (high_s i) Int.zero); autorewrite with labels; reflexivity. - case (snd (crbit_for_cond c)); reflexivity. - case (snd (crbit_for_cond c)); reflexivity. - case (snd (crbit_for_cond c)); reflexivity. - case (snd (crbit_for_cond c)); reflexivity. - case (snd (crbit_for_cond c)); reflexivity. Qed. Hint Rewrite transl_op_label: labels. -- cgit