diff options
Diffstat (limited to 'x86/SelectOpproof.v')
-rw-r--r-- | x86/SelectOpproof.v | 43 |
1 files changed, 30 insertions, 13 deletions
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v index 5e0f84e3..b59f4a87 100644 --- a/x86/SelectOpproof.v +++ b/x86/SelectOpproof.v @@ -13,15 +13,9 @@ (** Correctness of instruction selection for operators *) Require Import Coqlib. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Cminor. -Require Import Op. -Require Import CminorSel. +Require Import AST Integers Floats. +Require Import Values Memory Builtins Globalenvs. +Require Import Cminor Op CminorSel. Require Import SelectOp. Require Import OpHelpers. Require Import OpHelpersproof. @@ -838,7 +832,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. @@ -865,6 +860,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: @@ -874,10 +874,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. @@ -893,6 +894,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: @@ -1014,6 +1016,7 @@ Proof. - constructor; auto. Qed. +<<<<<<< HEAD (* floating-point division without HELPERS *) Theorem eval_divf_base: @@ -1035,4 +1038,18 @@ Proof. intros; unfold divfs_base. TrivialExists. Qed. +======= +(** Platform-specific known builtins *) + +Theorem eval_platform_builtin: + forall bf al a vl v le, + platform_builtin bf al = Some a -> + eval_exprlist ge sp e m le al vl -> + platform_builtin_sem bf vl = Some v -> + exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'. +Proof. + intros. discriminate. +Qed. + +>>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf End CMCONSTR. |