diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-10-11 11:14:30 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-10-11 11:14:30 +0200 |
commit | ef0f69dc1caeab169dcefca4d8b89f4d9e756bb5 (patch) | |
tree | d0ec8447f1b87b46d9dc49df81f91d80245cd396 /powerpc/SelectOpproof.v | |
parent | 659b735ed2dbefcbe8bcb2ec2123b66019ddaf14 (diff) | |
parent | 03672b4bbb2c837ea61a716d0ae67d87f68d20f8 (diff) | |
download | compcert-ef0f69dc1caeab169dcefca4d8b89f4d9e756bb5.tar.gz compcert-ef0f69dc1caeab169dcefca4d8b89f4d9e756bb5.zip |
Merge pull request #51 from AbsInt/ppc64
Take advantage of PowerPC 64-bit instructions
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. |