diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-09-13 11:44:32 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-09-13 11:44:32 +0200 |
| commit | 378ac3925503e6efd24cc34796e85d95c031e72d (patch) | |
| tree | 98005d8fc2dfdd4b0e48aebbd3aaaa1c3b8adc0e /powerpc/SelectOpproof.v | |
| parent | 470f6402ea49a81a5c861fcce66cb05ebff977c1 (diff) | |
| download | compcert-kvx-378ac3925503e6efd24cc34796e85d95c031e72d.tar.gz compcert-kvx-378ac3925503e6efd24cc34796e85d95c031e72d.zip | |
Use PowerPC 64 bits instructions (when available) for int<->FP conversions.
Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence.
Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-".
Diffstat (limited to 'powerpc/SelectOpproof.v')
| -rw-r--r-- | powerpc/SelectOpproof.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 147132dd..ad1adc47 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -838,6 +838,8 @@ Proof. intros. destruct x; simpl in H0; try discriminate. destruct (Float.to_intu f) as [n|] eqn:?; simpl in H0; inv H0. exists (Vint n); split; auto. unfold intuoffloat. + destruct Archi.ppc64. + econstructor. constructor; eauto. constructor. simpl; rewrite Heqo; auto. set (im := Int.repr Int.half_modulus). set (fm := Float.of_intu im). assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)). @@ -875,6 +877,8 @@ Theorem eval_floatofint: Proof. intros until y. unfold floatofint. destruct (floatofint_match a); intros. InvEval. TrivialExists. + destruct Archi.ppc64. + TrivialExists. rename e0 into a. destruct x; simpl in H0; inv H0. exists (Vfloat (Float.of_int i)); split; auto. set (t1 := addimm Float.ox8000_0000 a). @@ -897,6 +901,8 @@ Theorem eval_floatofintu: Proof. intros until y. unfold floatofintu. destruct (floatofintu_match a); intros. InvEval. TrivialExists. + destruct Archi.ppc64. + TrivialExists. rename e0 into a. destruct x; simpl in H0; inv H0. exists (Vfloat (Float.of_intu i)); split; auto. unfold floatofintu. |