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/SimplLocalsproof.v | 72 ++++++++++++++++++++++++++------------------ 1 file changed, 42 insertions(+), 30 deletions(-) (limited to 'cfrontend/SimplLocalsproof.v') diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v index 48a7a773..8ed924e5 100644 --- a/cfrontend/SimplLocalsproof.v +++ b/cfrontend/SimplLocalsproof.v @@ -187,21 +187,23 @@ Lemma val_casted_load_result: Val.load_result chunk v = v. Proof. intros. inversion H; clear H; subst v ty; simpl in H0. - destruct sz. +- destruct sz. destruct si; inversion H0; clear H0; subst chunk; simpl in *; congruence. destruct si; inversion H0; clear H0; subst chunk; simpl in *; congruence. clear H1. inv H0. auto. inversion H0; clear H0; subst chunk. simpl in *. destruct (Int.eq n Int.zero); subst n; reflexivity. - inv H0; auto. - inv H0; auto. - inv H0; auto. - inv H0; auto. - inv H0; auto. - inv H0; auto. - discriminate. - discriminate. - discriminate. +- inv H0; auto. +- inv H0; auto. +- inv H0; auto. +- inv H0. unfold Mptr, Val.load_result; destruct Archi.ptr64; auto. +- inv H0. unfold Mptr, Val.load_result; rewrite H1; auto. +- inv H0. unfold Val.load_result; rewrite H1; auto. +- inv H0. unfold Mptr, Val.load_result; rewrite H1; auto. +- inv H0. unfold Val.load_result; rewrite H1; auto. +- discriminate. +- discriminate. +- discriminate. Qed. Lemma val_casted_inject: @@ -209,7 +211,7 @@ Lemma val_casted_inject: Val.inject f v v' -> val_casted v ty -> val_casted v' ty. Proof. intros. inv H; auto. - inv H0; constructor. + inv H0; constructor; auto. inv H0; constructor. Qed. @@ -250,7 +252,7 @@ Proof. econstructor; eauto. unfold sem_cast, make_cast in *. destruct (classify_cast (typeof a) tto); auto. - destruct v1; inv H0; auto. + destruct v1; destruct Archi.ptr64; inv H0; auto. destruct sz2; auto. destruct v1; inv H0; auto. destruct v1; inv H0; auto. destruct v1; inv H0; auto. @@ -269,10 +271,19 @@ Lemma cast_typeconv: val_casted v ty -> sem_cast v ty (typeconv ty) m = Some v. Proof. - induction 1; simpl; auto. -- destruct sz; auto. -- unfold sem_cast. simpl. rewrite dec_eq_true; auto. + induction 1; simpl. +- unfold sem_cast, classify_cast; destruct sz, Archi.ptr64; auto. +- auto. +- auto. +- unfold sem_cast, classify_cast; destruct Archi.ptr64; auto. +- auto. +- unfold sem_cast; simpl; rewrite H; auto. +- unfold sem_cast; simpl; rewrite H; auto. +- unfold sem_cast; simpl; rewrite H; auto. +- unfold sem_cast; simpl; rewrite H; auto. +- unfold sem_cast; simpl. rewrite dec_eq_true; auto. - unfold sem_cast. simpl. rewrite dec_eq_true; auto. +- auto. Qed. Lemma step_Sdebug_temp: @@ -380,13 +391,13 @@ Lemma match_envs_assign_lifted: e!id = Some(b, ty) -> val_casted v ty -> Val.inject f v tv -> - assign_loc ge ty m b Int.zero v m' -> + assign_loc ge ty m b Ptrofs.zero v m' -> VSet.mem id cenv = true -> match_envs f cenv e le m' lo hi te (PTree.set id tv tle) tlo thi. Proof. intros. destruct H. generalize (me_vars0 id); intros MV; inv MV; try congruence. rewrite ENV in H0; inv H0. inv H3; try congruence. - unfold Mem.storev in H0. rewrite Int.unsigned_zero in H0. + unfold Mem.storev in H0. rewrite Ptrofs.unsigned_zero in H0. constructor; eauto; intros. (* vars *) destruct (peq id0 id). subst id0. @@ -746,7 +757,8 @@ Proof. unfold access_mode; intros. assert (size_chunk chunk = sizeof ge ty). { - destruct ty; try destruct i; try destruct s; try destruct f; inv H; auto. + destruct ty; try destruct i; try destruct s; try destruct f; inv H; auto; + unfold Mptr; simpl; destruct Archi.ptr64; auto. } omega. Qed. @@ -1019,10 +1031,10 @@ Proof. destruct (zeq (sizeof tge ty) 0). + (* special case size = 0 *) assert (bytes = nil). - { exploit (Mem.loadbytes_empty m bsrc (Int.unsigned osrc) (sizeof tge ty)). + { exploit (Mem.loadbytes_empty m bsrc (Ptrofs.unsigned osrc) (sizeof tge ty)). omega. congruence. } subst. - destruct (Mem.range_perm_storebytes tm bdst' (Int.unsigned (Int.add odst (Int.repr delta))) nil) + destruct (Mem.range_perm_storebytes tm bdst' (Ptrofs.unsigned (Ptrofs.add odst (Ptrofs.repr delta))) nil) as [tm' SB]. simpl. red; intros; omegaContradiction. exists tm'. @@ -1038,15 +1050,15 @@ Proof. exploit Mem.loadbytes_length; eauto. intros LEN. assert (SZPOS: sizeof tge ty > 0). { generalize (sizeof_pos tge ty); omega. } - assert (RPSRC: Mem.range_perm m bsrc (Int.unsigned osrc) (Int.unsigned osrc + sizeof tge ty) Cur Nonempty). + assert (RPSRC: Mem.range_perm m bsrc (Ptrofs.unsigned osrc) (Ptrofs.unsigned osrc + sizeof tge ty) Cur Nonempty). eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem. - assert (RPDST: Mem.range_perm m bdst (Int.unsigned odst) (Int.unsigned odst + sizeof tge ty) Cur Nonempty). + assert (RPDST: Mem.range_perm m bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sizeof tge ty) Cur Nonempty). replace (sizeof tge ty) with (Z_of_nat (length bytes)). eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem. rewrite LEN. apply nat_of_Z_eq. omega. - assert (PSRC: Mem.perm m bsrc (Int.unsigned osrc) Cur Nonempty). + assert (PSRC: Mem.perm m bsrc (Ptrofs.unsigned osrc) Cur Nonempty). apply RPSRC. omega. - assert (PDST: Mem.perm m bdst (Int.unsigned odst) Cur Nonempty). + assert (PDST: Mem.perm m bdst (Ptrofs.unsigned odst) Cur Nonempty). apply RPDST. omega. exploit Mem.address_inject. eauto. eexact PSRC. eauto. intros EQ1. exploit Mem.address_inject. eauto. eexact PDST. eauto. intros EQ2. @@ -1449,7 +1461,7 @@ Proof. rewrite ENV in H6; inv H6. inv H0; try congruence. assert (chunk0 = chunk). simpl in H. congruence. subst chunk0. - assert (v0 = v). unfold Mem.loadv in H2. rewrite Int.unsigned_zero in H2. congruence. subst v0. + assert (v0 = v). unfold Mem.loadv in H2. rewrite Ptrofs.unsigned_zero in H2. congruence. subst v0. exists tv; split; auto. constructor; auto. simpl in H; congruence. simpl in H; congruence. @@ -1464,13 +1476,13 @@ Proof. rewrite H1. exploit me_vars; eauto. instantiate (1 := id). intros MV. inv MV; try congruence. rewrite ENV in H; inv H. - exists b'; exists Int.zero; split. + exists b'; exists Ptrofs.zero; split. apply eval_Evar_local; auto. econstructor; eauto. (* global var *) rewrite H2. exploit me_vars; eauto. instantiate (1 := id). intros MV. inv MV; try congruence. - exists l; exists Int.zero; split. + exists l; exists Ptrofs.zero; split. apply eval_Evar_global. auto. rewrite <- H0. apply symbols_preserved. destruct GLOB as [bound GLOB1]. inv GLOB1. econstructor; eauto. @@ -1484,7 +1496,7 @@ Proof. inversion B. subst. econstructor; econstructor; split. eapply eval_Efield_struct; eauto. rewrite typeof_simpl_expr; eauto. - econstructor; eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + econstructor; eauto. repeat rewrite Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. (* field union *) rewrite <- comp_env_preserved in *. exploit eval_simpl_expr; eauto. intros [tv [A B]]. @@ -1721,12 +1733,12 @@ Lemma match_cont_find_funct: exists tfd, Genv.find_funct tge tvf = Some tfd /\ transf_fundef fd = OK tfd. Proof. intros. exploit match_cont_globalenv; eauto. intros [bound1 MG]. destruct MG. - inv H1; simpl in H0; try discriminate. destruct (Int.eq_dec ofs1 Int.zero); try discriminate. + inv H1; simpl in H0; try discriminate. destruct (Ptrofs.eq_dec ofs1 Ptrofs.zero); try discriminate. subst ofs1. assert (f b1 = Some(b1, 0)). apply DOMAIN. eapply FUNCTIONS; eauto. rewrite H1 in H2; inv H2. - rewrite Int.add_zero. simpl. rewrite dec_eq_true. apply function_ptr_translated; auto. + rewrite Ptrofs.add_zero. simpl. rewrite dec_eq_true. apply function_ptr_translated; auto. Qed. (** Relating execution states *) -- cgit