Support for MacOS X's indirect symbols. (first try)

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1978 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 31 insertions, 22 deletions

diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 9b1cd89..f30bb88 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -119,9 +119,14 @@ Theorem eval_addrsymbol:
   forall le id ofs,
   exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (symbol_address ge id ofs) v.
 Proof.
-  intros. unfold addrsymbol. econstructor; split. 
-  EvalOp. simpl; eauto. 
-  auto.
+  intros. unfold addrsymbol. exists (symbol_address ge id ofs); split; auto.
+  destruct (symbol_is_external id).
+  predSpec Int.eq Int.eq_spec ofs Int.zero.
+  subst. EvalOp.
+  EvalOp. econstructor. EvalOp. simpl; eauto. econstructor. simpl. 
+  unfold symbol_address. destruct (Genv.find_symbol ge id); auto. 
+  simpl. rewrite Int.add_commut. rewrite Int.add_zero. auto. 
+  EvalOp.
 Qed.
 
 Theorem eval_addrstack:
@@ -679,32 +684,36 @@ Theorem eval_intuoffloat:
   Val.intuoffloat x = Some y ->
   exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v.
 Proof.
-  intros. destruct x; simpl in H0; try discriminate. 
+  intros. destruct x; simpl in H0; try discriminate.
   destruct (Float.intuoffloat f) as [n|]_eqn; simpl in H0; inv H0.
-  exists (Vint n); split; auto.
-  unfold intuoffloat. 
-  econstructor. eauto. 
+  exists (Vint n); split; auto. unfold intuoffloat.
   set (im := Int.repr Int.half_modulus).
   set (fm := Float.floatofintu im).
-  assert (eval_expr ge sp e m (Vfloat f :: le) (Eletvar O) (Vfloat f)).
-    constructor. auto. 
+  assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)).
+    constructor. auto.
+  assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar O) (Vfloat fm)).
+    constructor. auto.
+  econstructor. eauto.
+  econstructor. instantiate (1 := Vfloat fm). EvalOp. 
   apply eval_Econdition with (v1 := Float.cmp Clt f fm).
-  econstructor. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
-  simpl. auto.
+  econstructor. eauto with evalexpr. auto.
   destruct (Float.cmp Clt f fm) as []_eqn.
   exploit Float.intuoffloat_intoffloat_1; eauto. intro EQ.
   EvalOp. simpl. rewrite EQ; auto.
-  exploit Float.intuoffloat_intoffloat_2; eauto. intro EQ.
-  replace n with (Int.add (Int.sub n Float.ox8000_0000) Float.ox8000_0000).
-  exploit (eval_addimm Float.ox8000_0000 (Vfloat f :: le)
-     (intoffloat
-        (subf (Eletvar 0)
-           (Eop (Ofloatconst (Float.floatofintu Float.ox8000_0000)) Enil)))).
-  unfold intoffloat, subf. 
-  EvalOp. constructor. EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
-  simpl. eauto. constructor. simpl. rewrite EQ. simpl; eauto. 
-  intros [v [A B]]. simpl in B. inv B. auto.
-  rewrite Int.sub_add_opp. rewrite Int.add_assoc. apply Int.add_zero. 
+  exploit Float.intuoffloat_intoffloat_2; eauto. 
+  change Float.ox8000_0000 with im. fold fm. intro EQ.
+  set (t2 := subf (Eletvar (S O)) (Eletvar O)).
+  set (t3 := intoffloat t2).
+  exploit (eval_subf (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f) (Eletvar O)); eauto.
+  fold t2. intros [v2 [A2 B2]]. simpl in B2. inv B2. 
+  exploit (eval_addimm Float.ox8000_0000 (Vfloat fm :: Vfloat f :: le) t3).
+    unfold t3. unfold intoffloat. EvalOp. simpl. rewrite EQ. simpl. eauto. 
+  intros [v4 [A4 B4]]. simpl in B4. inv B4. 
+  rewrite Int.sub_add_opp in A4. rewrite Int.add_assoc in A4. 
+  rewrite (Int.add_commut (Int.neg im)) in A4. 
+  rewrite Int.add_neg_zero in A4. 
+  rewrite Int.add_zero in A4.
+  auto.
 Qed.
 
 Theorem eval_floatofintu: