From 265fa07b34a813ba9d8249ddad82d71e6002c10d Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 2 Sep 2010 12:42:19 +0000
Subject: Merge of the reuse-temps branch: - Reload temporaries are marked as
 destroyed (set to Vundef) across   operations in the semantics of LTL, LTLin,
 Linear and Mach,   allowing Asmgen to reuse them. - Added IA32 port. -
 Cleaned up float conversions and axiomatization of floats.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 common/Errors.v      | 40 ++++++++++++++++++++++++++++++++++++++--
 common/Memdataaux.ml |  1 +
 common/Values.v      |  6 ++++++
 3 files changed, 45 insertions(+), 2 deletions(-)

(limited to 'common')

diff --git a/common/Errors.v b/common/Errors.v
index 2165db3..36e70c5 100644
--- a/common/Errors.v
+++ b/common/Errors.v
@@ -93,10 +93,37 @@ Proof.
   intros; discriminate.
 Qed.
 
-Open Local Scope error_monad_scope.
+(** Assertions *)
+
+Definition assertion (b: bool) : res unit :=
+  if b then OK tt else Error(msg "Assertion failed").
+
+Remark assertion_inversion:
+  forall b x, assertion b = OK x -> b = true.
+Proof.
+  unfold assertion; intros. destruct b; inv H; auto.
+Qed.
+
+Remark assertion_inversion_1:
+  forall (P Q: Prop) (a: {P}+{Q}) x,
+  assertion (proj_sumbool a) = OK x -> P.
+Proof.
+  intros. exploit assertion_inversion; eauto. 
+  unfold proj_sumbool. destruct a. auto. congruence.
+Qed.
+
+Remark assertion_inversion_2:
+  forall (P Q: Prop) (a: {P}+{Q}) x,
+  assertion (negb(proj_sumbool a)) = OK x -> Q.
+Proof.
+  intros. exploit assertion_inversion; eauto. 
+  unfold proj_sumbool. destruct a; simpl. congruence. auto.
+Qed.
 
 (** This is the familiar monadic map iterator. *)
 
+Open Local Scope error_monad_scope.
+
 Fixpoint mmap (A B: Type) (f: A -> res B) (l: list A) {struct l} : res (list B) :=
   match l with
   | nil => OK nil
@@ -152,6 +179,15 @@ Ltac monadInv1 H :=
       destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]];
       clear H;
       try (monadInv1 EQ2)))))
+  | (assertion (negb (proj_sumbool ?a)) = OK ?X) =>
+      let A := fresh "A" in (generalize (assertion_inversion_2 _ H); intro A);
+      clear H
+  | (assertion (proj_sumbool ?a) = OK ?X) =>
+      let A := fresh "A" in (generalize (assertion_inversion_1 _ H); intro A);
+      clear H
+  | (assertion ?b = OK ?X) =>
+      let A := fresh "A" in (generalize (assertion_inversion _ H); intro A);
+      clear H
   | (mmap ?F ?L = OK ?M) =>
       generalize (mmap_inversion F L H); intro
   end.
@@ -162,6 +198,7 @@ Ltac monadInv H :=
   | (Error _ = OK _) => monadInv1 H
   | (bind ?F ?G = OK ?X) => monadInv1 H
   | (bind2 ?F ?G = OK ?X) => monadInv1 H
+  | (assertion _ = OK _) => monadInv1 H
   | (?F _ _ _ _ _ _ _ _ = OK _) => 
       ((progress simpl in H) || unfold F in H); monadInv1 H
   | (?F _ _ _ _ _ _ _ = OK _) => 
@@ -179,4 +216,3 @@ Ltac monadInv H :=
   | (?F _ = OK _) => 
       ((progress simpl in H) || unfold F in H); monadInv1 H
   end.
-
diff --git a/common/Memdataaux.ml b/common/Memdataaux.ml
index 0ec7523..8bfd434 100644
--- a/common/Memdataaux.ml
+++ b/common/Memdataaux.ml
@@ -14,4 +14,5 @@ let big_endian =
   match Configuration.arch with
   | "powerpc" -> true
   | "arm" -> false
+  | "ia32" -> false
   | _ -> assert false
diff --git a/common/Values.v b/common/Values.v
index 236a5ae..af242c9 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -139,6 +139,12 @@ Definition floatofintu (v: val) : val :=
   | _ => Vundef
   end.
 
+Definition floatofwords (v1 v2: val) : val :=
+  match v1, v2 with
+  | Vint n1, Vint n2 => Vfloat (Float.from_words n1 n2)
+  | _, _ => Vundef
+  end.
+
 Definition notint (v: val) : val :=
   match v with
   | Vint n => Vint (Int.xor n Int.mone)
-- 
cgit v1.2.3