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. --- cfrontend/Initializersproof.v | 84 +++++++++++++++++++++---------------------- 1 file changed, 42 insertions(+), 42 deletions(-) (limited to 'cfrontend/Initializersproof.v') diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index d5f39d7d..49ac858e 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -12,21 +12,9 @@ (** Compile-time evaluation of initializers for global C variables. *) -Require Import Coqlib. -Require Import Errors. -Require Import Maps. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import AST. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Smallstep. -Require Import Ctypes. -Require Import Cop. -Require Import Csyntax. -Require Import Csem. +Require Import Coqlib Maps. +Require Import Errors Integers Floats Values AST Memory Globalenvs Events Smallstep. +Require Import Ctypes Cop Csyntax Csem. Require Import Initializers. Open Scope error_monad_scope. @@ -77,23 +65,23 @@ Section SIMPLE_EXPRS. Variable e: env. Variable m: mem. -Inductive eval_simple_lvalue: expr -> block -> int -> Prop := +Inductive eval_simple_lvalue: expr -> block -> ptrofs -> Prop := | esl_loc: forall b ofs ty, eval_simple_lvalue (Eloc b ofs ty) b ofs | esl_var_local: forall x ty b, e!x = Some(b, ty) -> - eval_simple_lvalue (Evar x ty) b Int.zero + eval_simple_lvalue (Evar x ty) b Ptrofs.zero | esl_var_global: forall x ty b, e!x = None -> Genv.find_symbol ge x = Some b -> - eval_simple_lvalue (Evar x ty) b Int.zero + eval_simple_lvalue (Evar x ty) b Ptrofs.zero | esl_deref: forall r ty b ofs, eval_simple_rvalue r (Vptr b ofs) -> eval_simple_lvalue (Ederef r ty) b ofs | esl_field_struct: forall r f ty b ofs id co a delta, eval_simple_rvalue r (Vptr b ofs) -> typeof r = Tstruct id a -> ge.(genv_cenv)!id = Some co -> field_offset ge f (co_members co) = OK delta -> - eval_simple_lvalue (Efield r f ty) b (Int.add ofs (Int.repr delta)) + eval_simple_lvalue (Efield r f ty) b (Ptrofs.add ofs (Ptrofs.repr delta)) | esl_field_union: forall r f ty b ofs id a, eval_simple_rvalue r (Vptr b ofs) -> typeof r = Tunion id a -> @@ -123,9 +111,9 @@ with eval_simple_rvalue: expr -> val -> Prop := sem_cast v1 (typeof r1) ty m = Some v -> eval_simple_rvalue (Ecast r1 ty) v | esr_sizeof: forall ty1 ty, - eval_simple_rvalue (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1))) + eval_simple_rvalue (Esizeof ty1 ty) (Vptrofs (Ptrofs.repr (sizeof ge ty1))) | esr_alignof: forall ty1 ty, - eval_simple_rvalue (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1))) + eval_simple_rvalue (Ealignof ty1 ty) (Vptrofs (Ptrofs.repr (alignof ge ty1))) | esr_seqand_true: forall r1 r2 ty v1 v2 v3, eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true -> eval_simple_rvalue r2 v2 -> @@ -418,9 +406,9 @@ Proof. (* cast *) eapply sem_cast_match; eauto. (* sizeof *) - constructor. + auto. (* alignof *) - constructor. + auto. (* seqand *) destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. @@ -459,7 +447,7 @@ Proof. rewrite H0 in CV. monadInv CV. unfold lookup_composite in EQ; rewrite H1 in EQ; monadInv EQ. exploit constval_rvalue; eauto. intro MV. inv MV. simpl. replace x0 with delta by congruence. econstructor; eauto. - rewrite ! Int.add_assoc. f_equal. apply Int.add_commut. + rewrite ! Ptrofs.add_assoc. f_equal. apply Ptrofs.add_commut. simpl. auto. (* field union *) rewrite H0 in CV. eauto. @@ -617,30 +605,36 @@ Proof. exploit sem_cast_match; eauto. intros D. unfold Genv.store_init_data. inv D. - (* int *) - destruct ty; try discriminate. - destruct i0; inv EQ2. +- (* int *) + remember Archi.ptr64 as ptr64. destruct ty; try discriminate EQ2. ++ destruct i0; inv EQ2. destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto. destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto. simpl in H2; inv H2. assumption. simpl in H2; inv H2. assumption. - inv EQ2. simpl in H2; inv H2. assumption. - (* long *) - destruct ty; inv EQ2. simpl in H2; inv H2. assumption. - (* float *) ++ destruct ptr64; inv EQ2. simpl in H2; unfold Mptr in H2; rewrite <- Heqptr64 in H2; inv H2. assumption. +- (* Long *) + remember Archi.ptr64 as ptr64. destruct ty; inv EQ2. ++ simpl in H2; inv H2. assumption. ++ simpl in H2; unfold Mptr in H2; destruct Archi.ptr64; inv H4. + inv H2; assumption. +- (* float *) destruct ty; try discriminate. destruct f1; inv EQ2; simpl in H2; inv H2; assumption. - (* single *) +- (* single *) destruct ty; try discriminate. destruct f1; inv EQ2; simpl in H2; inv H2; assumption. - (* pointer *) +- (* pointer *) unfold inj in H. - assert (data = Init_addrof b1 ofs1 /\ chunk = Mint32). - destruct ty; inv EQ2; inv H2. - destruct i; inv H5. intuition congruence. auto. + assert (data = Init_addrof b1 ofs1 /\ chunk = Mptr). + { remember Archi.ptr64 as ptr64. + destruct ty; inversion EQ2. + destruct i; inv H5. unfold Mptr. destruct Archi.ptr64; inv H6; inv H2; auto. + subst ptr64. unfold Mptr. destruct Archi.ptr64; inv H5; inv H2; auto. + inv H2. auto. } destruct H4; subst. destruct (Genv.find_symbol ge b1); inv H. - rewrite Int.add_zero in H3. auto. - (* undef *) + rewrite Ptrofs.add_zero in H3. auto. +- (* undef *) discriminate. Qed. @@ -651,19 +645,24 @@ Lemma transl_init_single_size: transl_init_single ge ty a = OK data -> init_data_size data = sizeof ge ty. Proof. - intros. monadInv H. destruct x0. + intros. monadInv H. remember Archi.ptr64 as ptr64. destruct x0. - monadInv EQ2. - destruct ty; try discriminate. destruct i0; inv EQ2; auto. - inv EQ2; auto. -- destruct ty; inv EQ2; auto. + destruct ptr64; inv EQ2. +Local Transparent sizeof. + unfold sizeof. rewrite <- Heqptr64; auto. +- destruct ty; inv EQ2; auto. + unfold sizeof. destruct Archi.ptr64; inv H0; auto. - destruct ty; try discriminate. destruct f0; inv EQ2; auto. - destruct ty; try discriminate. destruct f0; inv EQ2; auto. - destruct ty; try discriminate. destruct i0; inv EQ2; auto. - inv EQ2; auto. + destruct Archi.ptr64 eqn:SF; inv H0. simpl. rewrite SF; auto. + destruct ptr64; inv EQ2. simpl. rewrite <- Heqptr64; auto. + inv EQ2. unfold init_data_size, sizeof. auto. Qed. Notation idlsize := init_data_list_size. @@ -710,6 +709,7 @@ with tr_init_struct_size: sizeof_struct ge pos fl <= sizeof ge ty -> idlsize data + pos = sizeof ge ty. Proof. +Local Opaque sizeof. - destruct 1; simpl. + erewrite transl_init_single_size by eauto. omega. + Local Transparent sizeof. simpl. eapply tr_init_array_size; eauto. -- cgit