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

3 files changed, 45 insertions, 2 deletions

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)