From 362f2f36a44fa6ab4fe28264ed572d721adece70 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 3 Jan 2014 17:09:54 +0000 Subject: 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 --- common/Memdata.v | 27 +++++++++++++-------------- common/Memory.v | 25 +++++++++++++------------ 2 files changed, 26 insertions(+), 26 deletions(-) (limited to 'common') 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]]. -- cgit v1.2.3