aboutsummaryrefslogtreecommitdiffstats
path: root/x86/SelectOpproof.v
diff options
context:
space:
mode:
Diffstat (limited to 'x86/SelectOpproof.v')
-rw-r--r--x86/SelectOpproof.v16
1 files changed, 12 insertions, 4 deletions
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index 821a54e8..a1bb0703 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -828,7 +828,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.
- set (im := Int.repr Int.half_modulus).
+ destruct Archi.splitlong.
+- 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)).
constructor. auto.
@@ -855,6 +856,11 @@ Proof.
rewrite Int.add_neg_zero in A4.
rewrite Int.add_zero in A4.
auto.
+- apply Float.to_intu_to_long in Heqo. repeat econstructor. eauto.
+ simpl. rewrite Heqo; reflexivity.
+ simpl. unfold Int64.loword. rewrite Int64.unsigned_repr, Int.repr_unsigned; auto.
+ assert (Int.modulus < Int64.max_unsigned) by reflexivity.
+ generalize (Int.unsigned_range n); omega.
Qed.
Theorem eval_floatofintu:
@@ -864,10 +870,11 @@ Theorem eval_floatofintu:
exists v, eval_expr ge sp e m le (floatofintu a) v /\ Val.lessdef y v.
Proof.
intros until y; unfold floatofintu. case (floatofintu_match a); intros.
- InvEval. TrivialExists.
- destruct x; simpl in H0; try discriminate. inv H0.
+- InvEval. TrivialExists.
+- destruct x; simpl in H0; try discriminate. inv H0.
exists (Vfloat (Float.of_intu i)); split; auto.
- econstructor. eauto.
+ destruct Archi.splitlong.
++ econstructor. eauto.
set (fm := Float.of_intu Float.ox8000_0000).
assert (eval_expr ge sp e m (Vint i :: le) (Eletvar O) (Vint i)).
constructor. auto.
@@ -883,6 +890,7 @@ Proof.
constructor. EvalOp. simpl; eauto. constructor. simpl; eauto.
fold fm. rewrite Float.of_intu_of_int_2; auto.
rewrite Int.sub_add_opp. auto.
++ rewrite Float.of_intu_of_long. repeat econstructor. eauto. reflexivity.
Qed.
Theorem eval_intofsingle: