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/Globalenvs.v | 124 ++++++++++++++++++++++++++++++++++++++-------------- 1 file changed, 91 insertions(+), 33 deletions(-) (limited to 'common/Globalenvs.v') diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 2a8d6d97..9affd634 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -93,17 +93,37 @@ Record t: Type := mksenv { forall b, block_is_volatile b = true -> Plt b nextblock }. -Definition symbol_address (ge: t) (id: ident) (ofs: int) : val := +Definition symbol_address (ge: t) (id: ident) (ofs: ptrofs) : val := match find_symbol ge id with | Some b => Vptr b ofs | None => Vundef end. Theorem shift_symbol_address: + forall ge id ofs delta, + symbol_address ge id (Ptrofs.add ofs delta) = Val.offset_ptr (symbol_address ge id ofs) delta. +Proof. + intros. unfold symbol_address, Val.offset_ptr. destruct (find_symbol ge id); auto. +Qed. + +Theorem shift_symbol_address_32: + forall ge id ofs n, + Archi.ptr64 = false -> + symbol_address ge id (Ptrofs.add ofs (Ptrofs.of_int n)) = Val.add (symbol_address ge id ofs) (Vint n). +Proof. + intros. unfold symbol_address. destruct (find_symbol ge id). +- unfold Val.add. rewrite H. auto. +- auto. +Qed. + +Theorem shift_symbol_address_64: forall ge id ofs n, - symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n). + Archi.ptr64 = true -> + symbol_address ge id (Ptrofs.add ofs (Ptrofs.of_int64 n)) = Val.addl (symbol_address ge id ofs) (Vlong n). Proof. - intros. unfold symbol_address. destruct (find_symbol ge id); auto. + intros. unfold symbol_address. destruct (find_symbol ge id). +- unfold Val.addl. rewrite H. auto. +- auto. Qed. Definition equiv (se1 se2: t) : Prop := @@ -146,7 +166,7 @@ Definition find_symbol (ge: t) (id: ident) : option block := with [id], at byte offset [ofs]. [Vundef] is returned if no block is associated to [id]. *) -Definition symbol_address (ge: t) (id: ident) (ofs: int) : val := +Definition symbol_address (ge: t) (id: ident) (ofs: ptrofs) : val := match find_symbol ge id with | Some b => Vptr b ofs | None => Vundef @@ -176,7 +196,7 @@ Definition find_funct_ptr (ge: t) (b: block) : option F := Definition find_funct (ge: t) (v: val) : option F := match v with - | Vptr b ofs => if Int.eq_dec ofs Int.zero then find_funct_ptr ge b else None + | Vptr b ofs => if Ptrofs.eq_dec ofs Ptrofs.zero then find_funct_ptr ge b else None | _ => None end. @@ -341,25 +361,45 @@ Proof. Qed. Theorem shift_symbol_address: + forall ge id ofs delta, + symbol_address ge id (Ptrofs.add ofs delta) = Val.offset_ptr (symbol_address ge id ofs) delta. +Proof. + intros. unfold symbol_address, Val.offset_ptr. destruct (find_symbol ge id); auto. +Qed. + +Theorem shift_symbol_address_32: forall ge id ofs n, - symbol_address ge id (Int.add ofs n) = Val.add (symbol_address ge id ofs) (Vint n). + Archi.ptr64 = false -> + symbol_address ge id (Ptrofs.add ofs (Ptrofs.of_int n)) = Val.add (symbol_address ge id ofs) (Vint n). Proof. - intros. unfold symbol_address. destruct (find_symbol ge id); auto. + intros. unfold symbol_address. destruct (find_symbol ge id). +- unfold Val.add. rewrite H. auto. +- auto. +Qed. + +Theorem shift_symbol_address_64: + forall ge id ofs n, + Archi.ptr64 = true -> + symbol_address ge id (Ptrofs.add ofs (Ptrofs.of_int64 n)) = Val.addl (symbol_address ge id ofs) (Vlong n). +Proof. + intros. unfold symbol_address. destruct (find_symbol ge id). +- unfold Val.addl. rewrite H. auto. +- auto. Qed. Theorem find_funct_inv: forall ge v f, - find_funct ge v = Some f -> exists b, v = Vptr b Int.zero. + find_funct ge v = Some f -> exists b, v = Vptr b Ptrofs.zero. Proof. intros until f; unfold find_funct. destruct v; try congruence. - destruct (Int.eq_dec i Int.zero); try congruence. + destruct (Ptrofs.eq_dec i Ptrofs.zero); try congruence. intros. exists b; congruence. Qed. Theorem find_funct_find_funct_ptr: forall ge b, - find_funct ge (Vptr b Int.zero) = find_funct_ptr ge b. + find_funct ge (Vptr b Ptrofs.zero) = find_funct_ptr ge b. Proof. intros; simpl. apply dec_eq_true. Qed. @@ -594,7 +634,7 @@ Definition store_init_data (m: mem) (b: block) (p: Z) (id: init_data) : option m | Init_addrof symb ofs => match find_symbol ge symb with | None => None - | Some b' => Mem.store Mint32 m b p (Vptr b' ofs) + | Some b' => Mem.store Mptr m b p (Vptr b' ofs) end | Init_space n => Some m end. @@ -824,7 +864,8 @@ Proof. try (eapply Mem.store_unchanged_on; eauto; fail). inv H; apply Mem.unchanged_on_refl. destruct (find_symbol ge i); try congruence. - eapply Mem.store_unchanged_on; eauto. + eapply Mem.store_unchanged_on; eauto; + unfold Mptr; destruct Archi.ptr64; eauto. Qed. Remark store_init_data_list_unchanged: @@ -886,11 +927,17 @@ Definition bytes_of_init_data (i: init_data): list memval := | Init_space n => list_repeat (Z.to_nat n) (Byte Byte.zero) | Init_addrof id ofs => match find_symbol ge id with - | Some b => inj_value Q32 (Vptr b ofs) - | None => list_repeat 4%nat Undef + | Some b => inj_value (if Archi.ptr64 then Q64 else Q32) (Vptr b ofs) + | None => list_repeat (if Archi.ptr64 then 8%nat else 4%nat) Undef end end. +Remark init_data_size_addrof: + forall id ofs, init_data_size (Init_addrof id ofs) = size_chunk Mptr. +Proof. + intros. unfold Mptr. simpl. destruct Archi.ptr64; auto. +Qed. + Lemma store_init_data_loadbytes: forall m b p i m', store_init_data m b p i = Some m' -> @@ -902,8 +949,10 @@ Proof. assert (EQ: Z.of_nat (Z.to_nat z) = Z.max z 0). { destruct (zle 0 z). rewrite Z2Nat.id; xomega. destruct z; try discriminate. simpl. xomega. } rewrite <- EQ. apply H0. omega. simpl. omega. -- simpl; destruct (find_symbol ge i) as [b'|]; try discriminate. - apply (Mem.loadbytes_store_same _ _ _ _ _ _ H). +- rewrite init_data_size_addrof. simpl. + destruct (find_symbol ge i) as [b'|]; try discriminate. + rewrite (Mem.loadbytes_store_same _ _ _ _ _ _ H). + unfold encode_val, Mptr; destruct Archi.ptr64; reflexivity. Qed. Fixpoint bytes_of_init_data_list (il: list init_data): list memval := @@ -999,8 +1048,8 @@ Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {s Mem.load Mfloat64 m b p = Some(Vfloat n) /\ load_store_init_data m b (p + 8) il' | Init_addrof symb ofs :: il' => - (exists b', find_symbol ge symb = Some b' /\ Mem.load Mint32 m b p = Some(Vptr b' ofs)) - /\ load_store_init_data m b (p + 4) il' + (exists b', find_symbol ge symb = Some b' /\ Mem.load Mptr m b p = Some(Vptr b' ofs)) + /\ load_store_init_data m b (p + size_chunk Mptr) il' | Init_space n :: il' => read_as_zero m b p n /\ load_store_init_data m b (p + Zmax n 0) il' @@ -1024,8 +1073,8 @@ Proof. eapply Mem.load_store_same; eauto. } induction il; simpl. - auto. - intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence. +- auto. +- intros. destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence. exploit IHil; eauto. set (P := fun (b': block) ofs' => p + init_data_size a <= ofs'). apply read_as_zero_unchanged with (m := m) (P := P). @@ -1034,21 +1083,27 @@ Proof. intros; unfold P. omega. intros; unfold P. omega. intro D. - destruct a; simpl in Heqo; intuition. - eapply (A Mint8unsigned (Vint i)); eauto. - eapply (A Mint16unsigned (Vint i)); eauto. - eapply (A Mint32 (Vint i)); eauto. - eapply (A Mint64 (Vlong i)); eauto. - eapply (A Mfloat32 (Vsingle f)); eauto. - eapply (A Mfloat64 (Vfloat f)); eauto. + destruct a; simpl in Heqo. ++ split; auto. eapply (A Mint8unsigned (Vint i)); eauto. ++ split; auto. eapply (A Mint16unsigned (Vint i)); eauto. ++ split; auto. eapply (A Mint32 (Vint i)); eauto. ++ split; auto. eapply (A Mint64 (Vlong i)); eauto. ++ split; auto. eapply (A Mfloat32 (Vsingle f)); eauto. ++ split; auto. eapply (A Mfloat64 (Vfloat f)); eauto. ++ split; auto. set (P := fun (b': block) ofs' => ofs' < p + init_data_size (Init_space z)). inv Heqo. apply read_as_zero_unchanged with (m := m1) (P := P). red; intros. apply H0; auto. simpl. generalize (init_data_list_size_pos il); xomega. eapply store_init_data_list_unchanged; eauto. intros; unfold P. omega. intros; unfold P. simpl; xomega. - destruct (find_symbol ge i); try congruence. exists b0; split; auto. - eapply (A Mint32 (Vptr b0 i0)); eauto. ++ rewrite init_data_size_addrof in *. + split; auto. + destruct (find_symbol ge i); try congruence. + exists b0; split; auto. + transitivity (Some (Val.load_result Mptr (Vptr b0 i0))). + eapply (A Mptr (Vptr b0 i0)); eauto. + unfold Val.load_result, Mptr; destruct Archi.ptr64; auto. Qed. Remark alloc_global_unchanged: @@ -1324,7 +1379,7 @@ Proof. destruct (find_symbol ge i) as [b'|] eqn:E; try discriminate. eapply Mem.store_inject_neutral; eauto. econstructor. unfold Mem.flat_inj. apply pred_dec_true; auto. eauto. - rewrite Int.add_zero. auto. + rewrite Ptrofs.add_zero. auto. Qed. Lemma store_init_data_list_neutral: @@ -1417,7 +1472,7 @@ Definition init_data_alignment (i: init_data) : Z := | Init_int64 n => 8 | Init_float32 n => 4 | Init_float64 n => 4 - | Init_addrof symb ofs => 4 + | Init_addrof symb ofs => if Archi.ptr64 then 8 else 4 | Init_space n => 1 end. @@ -1444,7 +1499,8 @@ Proof. { intros. apply Mem.store_valid_access_3 in H0. destruct H0. congruence. } destruct i; simpl in H; eauto. simpl. apply Z.divide_1_l. - destruct (find_symbol ge i); try discriminate. eauto. + destruct (find_symbol ge i); try discriminate. eapply DFL. eassumption. + unfold Mptr, init_data_alignment; destruct Archi.ptr64; auto. Qed. Lemma store_init_data_list_aligned: @@ -1531,7 +1587,9 @@ Proof. exists m'; auto. } destruct i; eauto. simpl. exists m; auto. - simpl. exploit H1; eauto. intros (b1 & FS). rewrite FS. eauto. + simpl. exploit H1; eauto. intros (b1 & FS). rewrite FS. eapply DFL. + unfold init_data_size, Mptr. destruct Archi.ptr64; auto. + unfold init_data_alignment, Mptr. destruct Archi.ptr64; auto. Qed. Lemma store_init_data_list_exists: -- cgit