From e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 1 Oct 2016 17:25:18 +0200 Subject: Support for 64-bit architectures: generic support - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly. --- common/Memdata.v | 120 ++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 75 insertions(+), 45 deletions(-) (limited to 'common/Memdata.v') diff --git a/common/Memdata.v b/common/Memdata.v index 4ef7836b..87547e1e 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -68,6 +68,11 @@ Proof. intros; exists n; auto. Qed. +Lemma size_chunk_Mptr: size_chunk Mptr = if Archi.ptr64 then 8 else 4. +Proof. + unfold Mptr; destruct Archi.ptr64; auto. +Qed. + (** Memory reads and writes must respect alignment constraints: the byte offset of the location being addressed should be an exact multiple of the natural alignment for the chunk being addressed. @@ -98,6 +103,11 @@ Proof. intro. destruct chunk; simpl; omega. Qed. +Lemma align_chunk_Mptr: align_chunk Mptr = if Archi.ptr64 then 8 else 4. +Proof. + unfold Mptr; destruct Archi.ptr64; auto. +Qed. + Lemma align_size_chunk_divides: forall chunk, (align_chunk chunk | size_chunk chunk). Proof. @@ -360,8 +370,9 @@ Definition encode_val (chunk: memory_chunk) (v: val) : list memval := | Vint n, (Mint8signed | Mint8unsigned) => inj_bytes (encode_int 1%nat (Int.unsigned n)) | Vint n, (Mint16signed | Mint16unsigned) => inj_bytes (encode_int 2%nat (Int.unsigned n)) | Vint n, Mint32 => inj_bytes (encode_int 4%nat (Int.unsigned n)) - | Vptr b ofs, Mint32 => inj_value Q32 v + | Vptr b ofs, Mint32 => if Archi.ptr64 then list_repeat 4%nat Undef else inj_value Q32 v | Vlong n, Mint64 => inj_bytes (encode_int 8%nat (Int64.unsigned n)) + | Vptr b ofs, Mint64 => if Archi.ptr64 then inj_value Q64 v else list_repeat 8%nat Undef | Vsingle n, Mfloat32 => inj_bytes (encode_int 4%nat (Int.unsigned (Float32.to_bits n))) | Vfloat n, Mfloat64 => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.to_bits n))) | _, Many32 => inj_value Q32 v @@ -386,19 +397,26 @@ Definition decode_val (chunk: memory_chunk) (vl: list memval) : val := end | None => match chunk with - | Mint32 | Many32 => Val.load_result chunk (proj_value Q32 vl) + | Mint32 => if Archi.ptr64 then Vundef else Val.load_result chunk (proj_value Q32 vl) + | Many32 => Val.load_result chunk (proj_value Q32 vl) + | Mint64 => if Archi.ptr64 then Val.load_result chunk (proj_value Q64 vl) else Vundef | Many64 => Val.load_result chunk (proj_value Q64 vl) | _ => Vundef end end. +Ltac solve_encode_val_length := + match goal with + | [ |- length (inj_bytes _) = _ ] => rewrite length_inj_bytes; solve_encode_val_length + | [ |- length (encode_int _ _) = _ ] => apply encode_int_length + | [ |- length (if ?x then _ else _) = _ ] => destruct x eqn:?; solve_encode_val_length + | _ => reflexivity + end. + Lemma encode_val_length: forall chunk v, length(encode_val chunk v) = size_chunk_nat chunk. Proof. - intros. destruct v; simpl; destruct chunk; - solve [ reflexivity - | apply length_list_repeat - | rewrite length_inj_bytes; apply encode_int_length ]. + intros. destruct v; simpl; destruct chunk; solve_encode_val_length. Qed. Lemma check_inj_value: @@ -447,13 +465,15 @@ Definition decode_encode_val (v1: val) (chunk1 chunk2: memory_chunk) (v2: val) : | Vint n, Mint16signed, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n) | Vint n, Mint16unsigned, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n) | Vint n, Mint32, Mint32 => v2 = Vint n - | Vint n, Many32, (Mint32 | Many32) => v2 = Vint n + | Vint n, Many32, Many32 => v2 = Vint n | Vint n, Mint32, Mfloat32 => v2 = Vsingle(Float32.of_bits n) | Vint n, Many64, Many64 => v2 = Vint n | Vint n, (Mint64 | Mfloat32 | Mfloat64 | Many64), _ => v2 = Vundef | Vint n, _, _ => True (**r nothing meaningful to say about v2 *) - | Vptr b ofs, (Mint32 | Many32), (Mint32 | Many32) => v2 = Vptr b ofs + | Vptr b ofs, (Mint32 | Many32), (Mint32 | Many32) => v2 = if Archi.ptr64 then Vundef else Vptr b ofs + | Vptr b ofs, Mint64, (Mint64 | Many64) => v2 = if Archi.ptr64 then Vptr b ofs else Vundef | Vptr b ofs, Many64, Many64 => v2 = Vptr b ofs + | Vptr b ofs, Many64, Mint64 => v2 = if Archi.ptr64 then Vptr b ofs else Vundef | Vptr b ofs, _, _ => v2 = Vundef | Vlong n, Mint64, Mint64 => v2 = Vlong n | Vlong n, Mint64, Mfloat64 => v2 = Vfloat(Float.of_bits n) @@ -476,7 +496,7 @@ Definition decode_encode_val (v1: val) (chunk1 chunk2: memory_chunk) (v2: val) : Remark decode_val_undef: forall bl chunk, decode_val chunk (Undef :: bl) = Vundef. Proof. - intros. unfold decode_val. simpl. destruct chunk; auto. + intros. unfold decode_val. simpl. destruct chunk, Archi.ptr64; auto. Qed. Remark proj_bytes_inj_value: @@ -485,33 +505,33 @@ Proof. intros. destruct q; reflexivity. Qed. +Ltac solve_decode_encode_val_general := + exact I || reflexivity || + match goal with + | |- context [ if Archi.ptr64 then _ else _ ] => destruct Archi.ptr64 eqn:? + | |- context [ proj_bytes (inj_bytes _) ] => rewrite proj_inj_bytes + | |- context [ proj_bytes (inj_value _ _) ] => rewrite proj_bytes_inj_value + | |- context [ proj_value _ (inj_value _ _) ] => rewrite ?proj_inj_value, ?proj_inj_value_mismatch by congruence + | |- context [ Int.repr(decode_int (encode_int 1 (Int.unsigned _))) ] => rewrite decode_encode_int_1 + | |- context [ Int.repr(decode_int (encode_int 2 (Int.unsigned _))) ] => rewrite decode_encode_int_2 + | |- context [ Int.repr(decode_int (encode_int 4 (Int.unsigned _))) ] => rewrite decode_encode_int_4 + | |- context [ Int64.repr(decode_int (encode_int 8 (Int64.unsigned _))) ] => rewrite decode_encode_int_8 + | |- Vint (Int.sign_ext _ (Int.sign_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_idem; omega + | |- Vint (Int.zero_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.zero_ext_idem; omega + | |- Vint (Int.sign_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_zero_ext; omega + end. + Lemma decode_encode_val_general: forall v chunk1 chunk2, decode_encode_val v chunk1 chunk2 (decode_val chunk2 (encode_val chunk1 v)). Proof. Opaque inj_value. intros. - destruct v; destruct chunk1 eqn:C1; simpl; try (apply decode_val_undef); - destruct chunk2 eqn:C2; unfold decode_val; auto; - try (rewrite proj_inj_bytes); try (rewrite proj_bytes_inj_value); - try (rewrite proj_inj_value); try (rewrite proj_inj_value_mismatch by congruence); - auto. - rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. omega. - rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. omega. - rewrite decode_encode_int_1. decEq. apply Int.sign_ext_zero_ext. omega. - rewrite decode_encode_int_1. decEq. apply Int.zero_ext_idem. omega. - rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. omega. - rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. omega. - rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. omega. - rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. omega. - rewrite decode_encode_int_4. auto. - rewrite decode_encode_int_4. auto. - rewrite decode_encode_int_8. auto. - rewrite decode_encode_int_8. auto. - rewrite decode_encode_int_8. auto. - rewrite decode_encode_int_8. decEq. apply Float.of_to_bits. - rewrite decode_encode_int_4. auto. - rewrite decode_encode_int_4. decEq. apply Float32.of_to_bits. + destruct v; destruct chunk1 eqn:C1; try (apply decode_val_undef); + destruct chunk2 eqn:C2; unfold decode_encode_val, decode_val, encode_val, Val.load_result; + repeat solve_decode_encode_val_general. +- rewrite Float.of_to_bits; auto. +- rewrite Float32.of_to_bits; auto. Qed. Lemma decode_encode_val_similar: @@ -533,7 +553,9 @@ Proof. intros. unfold decode_val. destruct (proj_bytes cl). destruct chunk; simpl; auto. - destruct chunk; exact I || apply Val.load_result_type. +Local Opaque Val.load_result. + destruct chunk; simpl; + (exact I || apply Val.load_result_type || destruct Archi.ptr64; (exact I || apply Val.load_result_type)). Qed. Lemma encode_val_int8_signed_unsigned: @@ -601,7 +623,7 @@ Definition quantity_chunk (chunk: memory_chunk) := Inductive shape_encoding (chunk: memory_chunk) (v: val): list memval -> Prop := | shape_encoding_f: forall q i mvl, - (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) -> + (chunk = Mint32 \/ chunk = Many32 \/ chunk = Mint64 \/ chunk = Many64) -> q = quantity_chunk chunk -> S i = size_quantity_nat q -> (forall mv, In mv mvl -> exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q) -> @@ -628,7 +650,7 @@ Proof. } assert (B: forall q, q = quantity_chunk chunk -> - (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) -> + (chunk = Mint32 \/ chunk = Many32 \/ chunk = Mint64 \/ chunk = Many64) -> shape_encoding chunk v (inj_value q v)). { Local Transparent inj_value. @@ -651,12 +673,15 @@ Local Transparent inj_value. intros. eapply in_list_repeat; eauto. } generalize (encode_val_length chunk v). intros LEN. - unfold encode_val; unfold encode_val in LEN; destruct v; destruct chunk; (apply B || apply C || apply D); auto; red; auto. + unfold encode_val; unfold encode_val in LEN; + destruct v; destruct chunk; + (apply B || apply C || apply D || (destruct Archi.ptr64; (apply B || apply D))); + auto. Qed. Inductive shape_decoding (chunk: memory_chunk): list memval -> val -> Prop := | shape_decoding_f: forall v q i mvl, - (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) -> + (chunk = Mint32 \/ chunk = Many32 \/ chunk = Mint64 \/ chunk = Many64) -> q = quantity_chunk chunk -> S i = size_quantity_nat q -> (forall mv, In mv mvl -> exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q) -> @@ -696,7 +721,7 @@ Proof. destruct chunk; auto. } assert (C: forall q, size_quantity_nat q = size_chunk_nat chunk -> - (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) -> + (chunk = Mint32 \/ chunk = Many32 \/ chunk = Mint64 \/ chunk = Many64) -> shape_decoding chunk (mv1 :: mvl) (Val.load_result chunk (proj_value q (mv1 :: mvl)))). { intros. unfold proj_value. destruct mv1; auto. @@ -706,7 +731,7 @@ Proof. destruct (beq_nat sz n) eqn:EQN; auto. destruct (check_value sz v q mvl) eqn:CHECK; auto. simpl. apply beq_nat_true in EQN. subst n q0. constructor. auto. - destruct H0 as [E|[E|E]]; subst chunk; destruct q; auto || discriminate. + destruct H0 as [E|[E|[E|E]]]; subst chunk; destruct q; auto || discriminate. congruence. intros. eapply B; eauto. omega. } @@ -714,7 +739,7 @@ Proof. destruct (proj_bytes (mv1 :: mvl)) as [bl|] eqn:PB. exploit (A mv1); eauto with coqlib. intros [b1 EQ1]; subst mv1. destruct chunk; (apply shape_decoding_u || apply shape_decoding_b); eauto with coqlib. - destruct chunk; (apply shape_decoding_u || apply C); auto. + destruct chunk, Archi.ptr64; (apply shape_decoding_u || apply C); auto. Qed. (** * Compatibility with memory injections *) @@ -835,7 +860,7 @@ Proof. rewrite proj_value_undef. destruct chunk; auto. eapply proj_bytes_not_inject; eauto. congruence. apply Val.load_result_inject. apply proj_value_inject; auto. } - destruct chunk; auto. + destruct chunk; destruct Archi.ptr64; auto. Qed. (** Symmetrically, [encode_val], applied to values related by [Val.inject], @@ -883,10 +908,13 @@ Theorem encode_val_inject: Val.inject f v1 v2 -> list_forall2 (memval_inject f) (encode_val chunk v1) (encode_val chunk v2). Proof. +Local Opaque list_repeat. intros. inversion H; subst; simpl; destruct chunk; auto using inj_bytes_inject, inj_value_inject, repeat_Undef_inject_self, repeat_Undef_inject_encode_val. - unfold encode_val. destruct v2; apply inj_value_inject; auto. - unfold encode_val. destruct v2; apply inj_value_inject; auto. +- destruct Archi.ptr64; auto using inj_value_inject, repeat_Undef_inject_self. +- destruct Archi.ptr64; auto using inj_value_inject, repeat_Undef_inject_self. +- unfold encode_val. destruct v2; apply inj_value_inject; auto. +- unfold encode_val. destruct v2; apply inj_value_inject; auto. Qed. Definition memval_lessdef: memval -> memval -> Prop := memval_inject inject_id. @@ -964,20 +992,20 @@ Qed. Lemma decode_val_int64: forall l1 l2, - length l1 = 4%nat -> length l2 = 4%nat -> + length l1 = 4%nat -> length l2 = 4%nat -> Archi.ptr64 = false -> Val.lessdef (decode_val Mint64 (l1 ++ l2)) (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. + intros. unfold decode_val. rewrite H1. rewrite proj_bytes_append. destruct (proj_bytes l1) as [b1|] eqn:B1; destruct (proj_bytes l2) as [b2|] eqn:B2; auto. exploit length_proj_bytes. eexact B1. rewrite H; intro L1. exploit length_proj_bytes. eexact B2. rewrite H0; intro L2. assert (UR: forall l, length l = 4%nat -> Int.unsigned (Int.repr (int_of_bytes l)) = int_of_bytes l). intros. apply Int.unsigned_repr. - generalize (int_of_bytes_range l). rewrite H1. + generalize (int_of_bytes_range l). rewrite H2. change (two_p (Z.of_nat 4 * 8)) with (Int.max_unsigned + 1). omega. apply Val.lessdef_same. @@ -1029,11 +1057,13 @@ Qed. Lemma encode_val_int64: forall v, + Archi.ptr64 = false -> encode_val Mint64 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 Archi.big_endian eqn:BI; try reflexivity; + intros. unfold encode_val. rewrite H. + 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. -- cgit