diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-02-26 14:48:59 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-02-26 14:48:59 +0000 |
| commit | a745efa7f07a10cec625b9c302eb0196b7bfaefb (patch) | |
| tree | af32acc8865cf704b63bd27b8eb21da6b29d83b6 /powerpc/Asmgenproof.v | |
| parent | 26fcc4dbd92f367ecb20f4457cdf887eea0b6568 (diff) | |
| download | compcert-kvx-a745efa7f07a10cec625b9c302eb0196b7bfaefb.tar.gz compcert-kvx-a745efa7f07a10cec625b9c302eb0196b7bfaefb.zip | |
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
Diffstat (limited to 'powerpc/Asmgenproof.v')
| -rw-r--r-- | powerpc/Asmgenproof.v | 29 |
1 files changed, 24 insertions, 5 deletions
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. |