Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge

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.