diff options
Diffstat (limited to 'x86/SelectOpproof.v')
-rw-r--r-- | x86/SelectOpproof.v | 16 |
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: |