Introduce and use the platform-specific Archi module giving:

- endianness
- alignment constraints for 8-byte types
    (which is 4 for x86 ABI and 8 for other ABIs)
- NaN handling options (superceding the Nan module, removed).


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

2 files changed, 26 insertions, 26 deletions

diff --git a/common/Memdata.v b/common/Memdata.v
index 47f8471..d8d347e 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -17,6 +17,7 @@
 (** In-memory representation of values. *)
 
 Require Import Coqlib.
+Require Archi.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -146,10 +147,8 @@ Fixpoint int_of_bytes (l: list byte): Z :=
   | b :: l' => Byte.unsigned b + int_of_bytes l' * 256
   end.
 
-Parameter big_endian: bool.
-
 Definition rev_if_be (l: list byte) : list byte :=
-  if big_endian then List.rev l else l.
+  if Archi.big_endian then List.rev l else l.
 
 Definition encode_int (sz: nat) (x: Z) : list byte :=
   rev_if_be (bytes_of_int sz x).
@@ -168,7 +167,7 @@ Qed.
 Lemma rev_if_be_length:
   forall l, length (rev_if_be l) = length l.
 Proof.
-  intros; unfold rev_if_be; destruct big_endian.
+  intros; unfold rev_if_be; destruct Archi.big_endian.
   apply List.rev_length.
   auto.
 Qed.
@@ -200,7 +199,7 @@ Qed.
 Lemma rev_if_be_involutive:
   forall l, rev_if_be (rev_if_be l) = l.
 Proof.
-  intros; unfold rev_if_be; destruct big_endian. 
+  intros; unfold rev_if_be; destruct Archi.big_endian. 
   apply List.rev_involutive. 
   auto.
 Qed.
@@ -914,8 +913,8 @@ Lemma decode_val_int64:
   forall l1 l2,
   length l1 = 4%nat -> length l2 = 4%nat ->
   decode_val Mint64 (l1 ++ l2) =
-  Val.longofwords (decode_val Mint32 (if big_endian then l1 else l2))
-                  (decode_val Mint32 (if big_endian then l2 else l1)).
+  Val.longofwords (decode_val Mint32 (if Archi.big_endian then l1 else l2))
+                  (decode_val Mint32 (if Archi.big_endian then l2 else l1)).
 Proof.
   intros. unfold decode_val.
   assert (PP: forall vl, match proj_pointer vl with Vundef => True | Vptr _ _ => True | _ => False end).
@@ -935,7 +934,7 @@ Proof.
     generalize (int_of_bytes_range l). rewrite H1. 
     change (two_p (Z.of_nat 4 * 8)) with (Int.max_unsigned + 1). 
     omega.
-  unfold decode_int, rev_if_be. destruct big_endian; rewrite B1; rewrite B2.
+  unfold decode_int, rev_if_be. destruct Archi.big_endian; rewrite B1; rewrite B2.
   + rewrite <- (rev_length b1) in L1. 
     rewrite <- (rev_length b2) in L2.
     rewrite rev_app_distr.
@@ -946,9 +945,9 @@ Proof.
   + unfold Val.longofwords. f_equal. rewrite Int64.ofwords_add. f_equal.
     rewrite !UR by auto. rewrite int_of_bytes_append. 
     rewrite L1. change (Z.of_nat 4 * 8) with 32. ring.
-- destruct big_endian; rewrite B1; rewrite B2; auto.
-- destruct big_endian; rewrite B1; rewrite B2; auto.
-- destruct big_endian; rewrite B1; rewrite B2; auto.
+- destruct Archi.big_endian; rewrite B1; rewrite B2; auto.
+- destruct Archi.big_endian; rewrite B1; rewrite B2; auto.
+- destruct Archi.big_endian; rewrite B1; rewrite B2; auto.
 Qed.
 
 Lemma bytes_of_int_append:
@@ -987,10 +986,10 @@ Qed.
 Lemma encode_val_int64:
   forall v,
   encode_val Mint64 v =
-     encode_val Mint32 (if big_endian then Val.hiword v else Val.loword v)
-  ++ encode_val Mint32 (if big_endian then Val.loword v else Val.hiword v).
+     encode_val Mint32 (if Archi.big_endian then Val.hiword v else Val.loword v)
+  ++ encode_val Mint32 (if Archi.big_endian then Val.loword v else Val.hiword v).
 Proof.
-  intros. destruct v; destruct big_endian eqn:BI; try reflexivity;
+  intros. destruct v; destruct Archi.big_endian eqn:BI; try reflexivity;
   unfold Val.loword, Val.hiword, encode_val.
   unfold inj_bytes. rewrite <- map_app. f_equal. 
   unfold encode_int, rev_if_be. rewrite BI. rewrite <- rev_app_distr. f_equal.
diff --git a/common/Memory.v b/common/Memory.v
index 79fc8a0..0260a89 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -31,6 +31,7 @@ Require Import Axioms.
 Require Import Coqlib.
 Require Intv.
 Require Import Maps.
+Require Archi.
 Require Import AST.
 Require Import Integers.
 Require Import Floats.
@@ -891,8 +892,8 @@ Theorem load_int64_split:
   forall m b ofs v,
   load Mint64 m b ofs = Some v ->
   exists v1 v2,
-     load Mint32 m b ofs = Some (if big_endian then v1 else v2)
-  /\ load Mint32 m b (ofs + 4) = Some (if big_endian then v2 else v1)
+     load Mint32 m b ofs = Some (if Archi.big_endian then v1 else v2)
+  /\ load Mint32 m b (ofs + 4) = Some (if Archi.big_endian then v2 else v1)
   /\ v = Val.longofwords v1 v2.
 Proof.
   intros. 
@@ -909,10 +910,10 @@ Proof.
   exploit loadbytes_load. eexact LB2.
   simpl. apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto.
   intros L2.
-  exists (decode_val Mint32 (if big_endian then bytes1 else bytes2));
-  exists (decode_val Mint32 (if big_endian then bytes2 else bytes1)).
-  split. destruct big_endian; auto.
-  split. destruct big_endian; auto.
+  exists (decode_val Mint32 (if Archi.big_endian then bytes1 else bytes2));
+  exists (decode_val Mint32 (if Archi.big_endian then bytes2 else bytes1)).
+  split. destruct Archi.big_endian; auto.
+  split. destruct Archi.big_endian; auto.
   rewrite EQ. rewrite APP. apply decode_val_int64.
   erewrite loadbytes_length; eauto. reflexivity. 
   erewrite loadbytes_length; eauto. reflexivity. 
@@ -922,8 +923,8 @@ Theorem loadv_int64_split:
   forall m a v,
   loadv Mint64 m a = Some v ->
   exists v1 v2,
-     loadv Mint32 m a = Some (if big_endian then v1 else v2)
-  /\ loadv  Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if big_endian then v2 else v1)
+     loadv Mint32 m a = Some (if Archi.big_endian then v1 else v2)
+  /\ loadv  Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if Archi.big_endian then v2 else v1)
   /\ v = Val.longofwords v1 v2.
 Proof.
   intros. destruct a; simpl in H; try discriminate.
@@ -1674,8 +1675,8 @@ Theorem store_int64_split:
   forall m b ofs v m',
   store Mint64 m b ofs v = Some m' ->
   exists m1,
-     store Mint32 m b ofs (if big_endian then Val.hiword v else Val.loword v) = Some m1
-  /\ store Mint32 m1 b (ofs + 4) (if big_endian then Val.loword v else Val.hiword v) = Some m'.
+     store Mint32 m b ofs (if Archi.big_endian then Val.hiword v else Val.loword v) = Some m1
+  /\ store Mint32 m1 b (ofs + 4) (if Archi.big_endian then Val.loword v else Val.hiword v) = Some m'.
 Proof.
   intros. 
   exploit store_valid_access_3; eauto. intros [A B]. simpl in *.
@@ -1694,8 +1695,8 @@ Theorem storev_int64_split:
   forall m a v m',
   storev Mint64 m a v = Some m' ->
   exists m1,
-     storev Mint32 m a (if big_endian then Val.hiword v else Val.loword v) = Some m1
-  /\ storev Mint32 m1 (Val.add a (Vint (Int.repr 4))) (if big_endian then Val.loword v else Val.hiword v) = Some m'.
+     storev Mint32 m a (if Archi.big_endian then Val.hiword v else Val.loword v) = Some m1
+  /\ storev Mint32 m1 (Val.add a (Vint (Int.repr 4))) (if Archi.big_endian then Val.loword v else Val.hiword v) = Some m'.
 Proof.
   intros. destruct a; simpl in H; try discriminate.
   exploit store_int64_split; eauto. intros [m1 [A B]].