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/AST.v | 38 ++- common/Determinism.v | 8 +- common/Events.v | 169 +++++++----- common/Globalenvs.v | 124 ++++++--- common/Memdata.v | 120 +++++---- common/Memory.v | 166 ++++++------ common/Memtype.v | 38 +-- common/Separation.v | 30 +-- common/Values.v | 712 +++++++++++++++++++++++++++++++++++++++++---------- 9 files changed, 1004 insertions(+), 401 deletions(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index ae7178f4..e6fdec3c 100644 --- a/common/AST.v +++ b/common/AST.v @@ -18,6 +18,7 @@ Require Import String. Require Import Coqlib Maps Errors Integers Floats. +Require Archi. Set Implicit Arguments. @@ -50,6 +51,8 @@ Definition opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2} Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2} := list_eq_dec typ_eq. +Definition Tptr : typ := if Archi.ptr64 then Tlong else Tint. + Definition typesize (ty: typ) : Z := match ty with | Tint => 4 @@ -63,6 +66,9 @@ Definition typesize (ty: typ) : Z := Lemma typesize_pos: forall ty, typesize ty > 0. Proof. destruct ty; simpl; omega. Qed. +Lemma typesize_Tptr: typesize Tptr = if Archi.ptr64 then 8 else 4. +Proof. unfold Tptr; destruct Archi.ptr64; auto. Qed. + (** All values of size 32 bits are also of type [Tany32]. All values are of type [Tany64]. This corresponds to the following subtyping relation over types. *) @@ -150,6 +156,8 @@ Definition chunk_eq: forall (c1 c2: memory_chunk), {c1=c2} + {c1<>c2}. Proof. decide equality. Defined. Global Opaque chunk_eq. +Definition Mptr : memory_chunk := if Archi.ptr64 then Mint64 else Mint32. + (** The type (integer/pointer or float) of a chunk. *) Definition type_of_chunk (c: memory_chunk) : typ := @@ -166,6 +174,9 @@ Definition type_of_chunk (c: memory_chunk) : typ := | Many64 => Tany64 end. +Lemma type_of_Mptr: type_of_chunk Mptr = Tptr. +Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed. + (** The chunk that is appropriate to store and reload a value of the given type, without losing information. *) @@ -179,6 +190,9 @@ Definition chunk_of_type (ty: typ) := | Tany64 => Many64 end. +Lemma chunk_of_Tptr: chunk_of_type Tptr = Mptr. +Proof. unfold Mptr, Tptr; destruct Archi.ptr64; auto. Qed. + (** Initialization data for global variables. *) Inductive init_data: Type := @@ -189,7 +203,7 @@ Inductive init_data: Type := | Init_float32: float32 -> init_data | Init_float64: float -> init_data | Init_space: Z -> init_data - | Init_addrof: ident -> int -> init_data. (**r address of symbol + offset *) + | Init_addrof: ident -> ptrofs -> init_data. (**r address of symbol + offset *) Definition init_data_size (i: init_data) : Z := match i with @@ -199,7 +213,7 @@ Definition init_data_size (i: init_data) : Z := | Init_int64 _ => 8 | Init_float32 _ => 4 | Init_float64 _ => 8 - | Init_addrof _ _ => 4 + | Init_addrof _ _ => if Archi.ptr64 then 8 else 4 | Init_space n => Zmax n 0 end. @@ -212,7 +226,7 @@ Fixpoint init_data_list_size (il: list init_data) {struct il} : Z := Lemma init_data_size_pos: forall i, init_data_size i >= 0. Proof. - destruct i; simpl; xomega. + destruct i; simpl; try xomega. destruct Archi.ptr64; omega. Qed. Lemma init_data_list_size_pos: @@ -463,11 +477,11 @@ Definition ef_sig (ef: external_function): signature := | EF_external name sg => sg | EF_builtin name sg => sg | EF_runtime name sg => sg - | EF_vload chunk => mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default - | EF_vstore chunk => mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default - | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default - | EF_free => mksignature (Tint :: nil) None cc_default - | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default + | EF_vload chunk => mksignature (Tptr :: nil) (Some (type_of_chunk chunk)) cc_default + | EF_vstore chunk => mksignature (Tptr :: type_of_chunk chunk :: nil) None cc_default + | EF_malloc => mksignature (Tptr :: nil) (Some Tptr) cc_default + | EF_free => mksignature (Tptr :: nil) None cc_default + | EF_memcpy sz al => mksignature (Tptr :: Tptr :: nil) None cc_default | EF_annot text targs => mksignature targs None cc_default | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default | EF_inline_asm text sg clob => sg @@ -609,10 +623,10 @@ Inductive builtin_arg (A: Type) : Type := | BA_long (n: int64) | BA_float (f: float) | BA_single (f: float32) - | BA_loadstack (chunk: memory_chunk) (ofs: int) - | BA_addrstack (ofs: int) - | BA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: int) - | BA_addrglobal (id: ident) (ofs: int) + | BA_loadstack (chunk: memory_chunk) (ofs: ptrofs) + | BA_addrstack (ofs: ptrofs) + | BA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: ptrofs) + | BA_addrglobal (id: ident) (ofs: ptrofs) | BA_splitlong (hi lo: builtin_arg A). Inductive builtin_res (A: Type) : Type := diff --git a/common/Determinism.v b/common/Determinism.v index a813dd92..7fa01c2d 100644 --- a/common/Determinism.v +++ b/common/Determinism.v @@ -42,18 +42,18 @@ Require Import Behaviors. CoInductive world: Type := World (io: string -> list eventval -> option (eventval * world)) - (vload: memory_chunk -> ident -> int -> option (eventval * world)) - (vstore: memory_chunk -> ident -> int -> eventval -> option world). + (vload: memory_chunk -> ident -> ptrofs -> option (eventval * world)) + (vstore: memory_chunk -> ident -> ptrofs -> eventval -> option world). Definition nextworld_io (w: world) (evname: string) (evargs: list eventval) : option (eventval * world) := match w with World io vl vs => io evname evargs end. -Definition nextworld_vload (w: world) (chunk: memory_chunk) (id: ident) (ofs: int) : +Definition nextworld_vload (w: world) (chunk: memory_chunk) (id: ident) (ofs: ptrofs) : option (eventval * world) := match w with World io vl vs => vl chunk id ofs end. -Definition nextworld_vstore (w: world) (chunk: memory_chunk) (id: ident) (ofs: int) (v: eventval): +Definition nextworld_vstore (w: world) (chunk: memory_chunk) (id: ident) (ofs: ptrofs) (v: eventval): option world := match w with World io vl vs => vs chunk id ofs v end. diff --git a/common/Events.v b/common/Events.v index c94d6d35..97d4f072 100644 --- a/common/Events.v +++ b/common/Events.v @@ -59,12 +59,12 @@ Inductive eventval: Type := | EVlong: int64 -> eventval | EVfloat: float -> eventval | EVsingle: float32 -> eventval - | EVptr_global: ident -> int -> eventval. + | EVptr_global: ident -> ptrofs -> eventval. Inductive event: Type := | Event_syscall: string -> list eventval -> eventval -> event - | Event_vload: memory_chunk -> ident -> int -> eventval -> event - | Event_vstore: memory_chunk -> ident -> int -> eventval -> event + | Event_vload: memory_chunk -> ident -> ptrofs -> eventval -> event + | Event_vstore: memory_chunk -> ident -> ptrofs -> eventval -> event | Event_annot: string -> list eventval -> event. (** The dynamic semantics for programs collect traces of events. @@ -278,7 +278,7 @@ Inductive eventval_match: eventval -> typ -> val -> Prop := | ev_match_ptr: forall id b ofs, Senv.public_symbol ge id = true -> Senv.find_symbol ge id = Some b -> - eventval_match (EVptr_global id ofs) Tint (Vptr b ofs). + eventval_match (EVptr_global id ofs) Tptr (Vptr b ofs). Inductive eventval_list_match: list eventval -> list typ -> list val -> Prop := | evl_match_nil: @@ -295,7 +295,7 @@ Lemma eventval_match_type: forall ev ty v, eventval_match ev ty v -> Val.has_type v ty. Proof. - intros. inv H; simpl; auto. + intros. inv H; simpl; auto. unfold Tptr; destruct Archi.ptr64; auto. Qed. Lemma eventval_list_match_length: @@ -359,7 +359,7 @@ Definition eventval_type (ev: eventval) : typ := | EVlong _ => Tlong | EVfloat _ => Tfloat | EVsingle _ => Tsingle - | EVptr_global id ofs => Tint + | EVptr_global id ofs => Tptr end. Lemma eventval_match_receptive: @@ -368,15 +368,23 @@ Lemma eventval_match_receptive: eventval_valid ev1 -> eventval_valid ev2 -> eventval_type ev1 = eventval_type ev2 -> exists v2, eventval_match ev2 ty v2. Proof. - intros. inv H; destruct ev2; simpl in H2; try discriminate. + intros. unfold eventval_type, Tptr in H2. remember Archi.ptr64 as ptr64. + inversion H; subst ev1 ty v1; clear H; destruct ev2; simpl in H2; inv H2. - exists (Vint i0); constructor. - simpl in H1; exploit Senv.public_symbol_exists; eauto. intros [b FS]. - exists (Vptr b i1); constructor; auto. + exists (Vptr b i1); rewrite H3. constructor; auto. - exists (Vlong i0); constructor. +- simpl in H1; exploit Senv.public_symbol_exists; eauto. intros [b FS]. + exists (Vptr b i1); rewrite H3; constructor; auto. - exists (Vfloat f0); constructor. +- destruct Archi.ptr64; discriminate. - exists (Vsingle f0); constructor; auto. -- exists (Vint i); constructor. -- simpl in H1. exploit Senv.public_symbol_exists. eexact H1. intros [b' FS]. +- destruct Archi.ptr64; discriminate. +- exists (Vint i); unfold Tptr; rewrite H5; constructor. +- exists (Vlong i); unfold Tptr; rewrite H5; constructor. +- destruct Archi.ptr64; discriminate. +- destruct Archi.ptr64; discriminate. +- exploit Senv.public_symbol_exists. eexact H1. intros [b' FS]. exists (Vptr b' i0); constructor; auto. Qed. @@ -458,7 +466,7 @@ Lemma eventval_match_inject: Proof. intros. inv H; inv H0; try constructor; auto. destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b3 [EQ FS]]. rewrite H4 in EQ; inv EQ. - rewrite Int.add_zero. constructor; auto. rewrite A; auto. + rewrite Ptrofs.add_zero. constructor; auto. rewrite A; auto. Qed. Lemma eventval_match_inject_2: @@ -469,7 +477,7 @@ Proof. intros. inv H; try (econstructor; split; eauto; constructor; fail). destruct symb_inj as (A & B & C & D). exploit C; eauto. intros [b2 [EQ FS]]. exists (Vptr b2 ofs); split. econstructor; eauto. - econstructor; eauto. rewrite Int.add_zero; auto. + econstructor; eauto. rewrite Ptrofs.add_zero; auto. Qed. Lemma eventval_list_match_inject: @@ -546,7 +554,7 @@ Fixpoint output_trace (t: trace) : Prop := (** * Semantics of volatile memory accesses *) Inductive volatile_load (ge: Senv.t): - memory_chunk -> mem -> block -> int -> trace -> val -> Prop := + memory_chunk -> mem -> block -> ptrofs -> trace -> val -> Prop := | volatile_load_vol: forall chunk m b ofs id ev v, Senv.block_is_volatile ge b = true -> Senv.find_symbol ge id = Some b -> @@ -556,11 +564,11 @@ Inductive volatile_load (ge: Senv.t): (Val.load_result chunk v) | volatile_load_nonvol: forall chunk m b ofs v, Senv.block_is_volatile ge b = false -> - Mem.load chunk m b (Int.unsigned ofs) = Some v -> + Mem.load chunk m b (Ptrofs.unsigned ofs) = Some v -> volatile_load ge chunk m b ofs E0 v. Inductive volatile_store (ge: Senv.t): - memory_chunk -> mem -> block -> int -> val -> trace -> mem -> Prop := + memory_chunk -> mem -> block -> ptrofs -> val -> trace -> mem -> Prop := | volatile_store_vol: forall chunk m b ofs id ev v, Senv.block_is_volatile ge b = true -> Senv.find_symbol ge id = Some b -> @@ -570,7 +578,7 @@ Inductive volatile_store (ge: Senv.t): m | volatile_store_nonvol: forall chunk m b ofs v m', Senv.block_is_volatile ge b = false -> - Mem.store chunk m b (Int.unsigned ofs) v = Some m' -> + Mem.store chunk m b (Ptrofs.unsigned ofs) v = Some m' -> volatile_store ge chunk m b ofs v E0 m'. (** * Semantics of external functions *) @@ -737,7 +745,7 @@ Proof. - (* volatile load *) inv VI. exploit B; eauto. intros [U V]. subst delta. exploit eventval_match_inject_2; eauto. intros (v2 & X & Y). - rewrite Int.add_zero. exists (Val.load_result chunk v2); split. + rewrite Ptrofs.add_zero. exists (Val.load_result chunk v2); split. constructor; auto. erewrite D; eauto. apply Val.load_result_inject. auto. @@ -762,7 +770,7 @@ Qed. Lemma volatile_load_ok: forall chunk, extcall_properties (volatile_load_sem chunk) - (mksignature (Tint :: nil) (Some (type_of_chunk chunk)) cc_default). + (mksignature (Tptr :: nil) (Some (type_of_chunk chunk)) cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -880,7 +888,7 @@ Proof. inv VS. - (* volatile store *) inv AI. exploit Q; eauto. intros [A B]. subst delta. - rewrite Int.add_zero. exists m1'; split. + rewrite Ptrofs.add_zero. exists m1'; split. constructor; auto. erewrite S; eauto. eapply eventval_match_inject; eauto. apply Val.load_result_inject. auto. intuition auto with mem. @@ -894,7 +902,7 @@ Proof. unfold loc_unmapped; intros. inv AI; congruence. + eapply Mem.store_unchanged_on; eauto. unfold loc_out_of_reach; intros. red; intros. simpl in A. - assert (EQ: Int.unsigned (Int.add ofs (Int.repr delta)) = Int.unsigned ofs + delta) + assert (EQ: Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta)) = Ptrofs.unsigned ofs + delta) by (eapply Mem.address_inject; eauto with mem). rewrite EQ in *. eelim H3; eauto. @@ -913,7 +921,7 @@ Qed. Lemma volatile_store_ok: forall chunk, extcall_properties (volatile_store_sem chunk) - (mksignature (Tint :: type_of_chunk chunk :: nil) None cc_default). + (mksignature (Tptr :: type_of_chunk chunk :: nil) None cc_default). Proof. intros; constructor; intros. (* well typed *) @@ -951,19 +959,19 @@ Qed. Inductive extcall_malloc_sem (ge: Senv.t): list val -> mem -> trace -> val -> mem -> Prop := - | extcall_malloc_sem_intro: forall n m m' b m'', - Mem.alloc m (-4) (Int.unsigned n) = (m', b) -> - Mem.store Mint32 m' b (-4) (Vint n) = Some m'' -> - extcall_malloc_sem ge (Vint n :: nil) m E0 (Vptr b Int.zero) m''. + | extcall_malloc_sem_intro: forall sz m m' b m'', + Mem.alloc m (- size_chunk Mptr) (Ptrofs.unsigned sz) = (m', b) -> + Mem.store Mptr m' b (- size_chunk Mptr) (Vptrofs sz) = Some m'' -> + extcall_malloc_sem ge (Vptrofs sz :: nil) m E0 (Vptr b Ptrofs.zero) m''. Lemma extcall_malloc_ok: extcall_properties extcall_malloc_sem - (mksignature (Tint :: nil) (Some Tint) cc_default). + (mksignature (Tptr :: nil) (Some Tptr) cc_default). Proof. assert (UNCHANGED: - forall (P: block -> Z -> Prop) m n m' b m'', - Mem.alloc m (-4) (Int.unsigned n) = (m', b) -> - Mem.store Mint32 m' b (-4) (Vint n) = Some m'' -> + forall (P: block -> Z -> Prop) m lo hi v m' b m'', + Mem.alloc m lo hi = (m', b) -> + Mem.store Mptr m' b lo v = Some m'' -> Mem.unchanged_on P m m''). { intros. @@ -975,7 +983,7 @@ Proof. } constructor; intros. (* well typed *) -- inv H. unfold proj_sig_res; simpl. auto. +- inv H. unfold proj_sig_res, Tptr; simpl. destruct Archi.ptr64; auto. (* symbols preserved *) - inv H0; econstructor; eauto. (* valid block *) @@ -987,23 +995,28 @@ Proof. (* readonly *) - inv H. eapply UNCHANGED; eauto. (* mem extends *) -- inv H. inv H1. inv H5. inv H7. +- inv H. inv H1. inv H7. + assert (SZ: v2 = Vptrofs sz). + { unfold Vptrofs in *. destruct Archi.ptr64; inv H5; auto. } + subst v2. exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. intros [m3' [A B]]. - exploit Mem.store_within_extends. eexact B. eauto. - instantiate (1 := Vint n). auto. + exploit Mem.store_within_extends. eexact B. eauto. eauto. intros [m2' [C D]]. - exists (Vptr b Int.zero); exists m2'; intuition. + exists (Vptr b Ptrofs.zero); exists m2'; intuition. econstructor; eauto. eapply UNCHANGED; eauto. (* mem injects *) -- inv H0. inv H2. inv H6. inv H8. +- inv H0. inv H2. inv H8. + assert (SZ: v' = Vptrofs sz). + { unfold Vptrofs in *. destruct Archi.ptr64; inv H6; auto. } + subst v'. exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl. intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]]. exploit Mem.store_mapped_inject. eexact A. eauto. eauto. - instantiate (1 := Vint n). auto. - intros [m2' [E G]]. - exists f'; exists (Vptr b' Int.zero); exists m2'; intuition. + instantiate (1 := Vptrofs sz). unfold Vptrofs; destruct Archi.ptr64; constructor. + rewrite Zplus_0_r. intros [m2' [E G]]. + exists f'; exists (Vptr b' Ptrofs.zero); exists m2'; intuition auto. econstructor; eauto. econstructor. eauto. auto. eapply UNCHANGED; eauto. @@ -1017,7 +1030,14 @@ Proof. - assert (t1 = t2). inv H; inv H0; auto. subst t2. exists vres1; exists m1; auto. (* determ *) -- inv H; inv H0. split. constructor. intuition congruence. +- inv H. simple inversion H0. + assert (EQ2: sz0 = sz). + { unfold Vptrofs in H4; destruct Archi.ptr64 eqn:SF. + rewrite <- (Ptrofs.of_int64_to_int64 SF sz0), <- (Ptrofs.of_int64_to_int64 SF sz). congruence. + rewrite <- (Ptrofs.of_int_to_int SF sz0), <- (Ptrofs.of_int_to_int SF sz). congruence. + } + subst. + split. constructor. intuition congruence. Qed. (** ** Semantics of dynamic memory deallocation (free) *) @@ -1025,14 +1045,14 @@ Qed. Inductive extcall_free_sem (ge: Senv.t): list val -> mem -> trace -> val -> mem -> Prop := | extcall_free_sem_intro: forall b lo sz m m', - Mem.load Mint32 m b (Int.unsigned lo - 4) = Some (Vint sz) -> - Int.unsigned sz > 0 -> - Mem.free m b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) = Some m' -> + Mem.load Mptr m b (Ptrofs.unsigned lo - size_chunk Mptr) = Some (Vptrofs sz) -> + Ptrofs.unsigned sz > 0 -> + Mem.free m b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz) = Some m' -> extcall_free_sem ge (Vptr b lo :: nil) m E0 Vundef m'. Lemma extcall_free_ok: extcall_properties extcall_free_sem - (mksignature (Tint :: nil) None cc_default). + (mksignature (Tptr :: nil) None cc_default). Proof. constructor; intros. (* well typed *) @@ -1050,7 +1070,10 @@ Proof. eapply Mem.free_range_perm; eauto. (* mem extends *) - inv H. inv H1. inv H8. inv H6. - exploit Mem.load_extends; eauto. intros [vsz [A B]]. inv B. + exploit Mem.load_extends; eauto. intros [v' [A B]]. + assert (v' = Vptrofs sz). + { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. } + subst v'. exploit Mem.free_parallel_extends; eauto. intros [m2' [C D]]. exists Vundef; exists m2'; intuition. econstructor; eauto. @@ -1062,26 +1085,30 @@ Proof. tauto. (* mem inject *) - inv H0. inv H2. inv H7. inv H9. - exploit Mem.load_inject; eauto. intros [vsz [A B]]. inv B. - assert (Mem.range_perm m1 b (Int.unsigned lo - 4) (Int.unsigned lo + Int.unsigned sz) Cur Freeable). + exploit Mem.load_inject; eauto. intros [v' [A B]]. + assert (v' = Vptrofs sz). + { unfold Vptrofs in *; destruct Archi.ptr64; inv B; auto. } + subst v'. + assert (P: Mem.range_perm m1 b (Ptrofs.unsigned lo - size_chunk Mptr) (Ptrofs.unsigned lo + Ptrofs.unsigned sz) Cur Freeable). eapply Mem.free_range_perm; eauto. exploit Mem.address_inject; eauto. apply Mem.perm_implies with Freeable; auto with mem. - apply H0. instantiate (1 := lo). omega. + apply P. instantiate (1 := lo). + generalize (size_chunk_pos Mptr); omega. intro EQ. exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D). exists f, Vundef, m2'; split. apply extcall_free_sem_intro with (sz := sz) (m' := m2'). rewrite EQ. rewrite <- A. f_equal. omega. - auto. + auto. auto. rewrite ! EQ. rewrite <- C. f_equal; omega. split. auto. split. auto. split. eapply Mem.free_unchanged_on; eauto. unfold loc_unmapped. intros; congruence. split. eapply Mem.free_unchanged_on; eauto. unfold loc_out_of_reach. - intros. red; intros. eelim H7; eauto. + intros. red; intros. eelim H2; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. - apply H0. omega. + apply P. omega. split. auto. red; intros. congruence. (* trace length *) @@ -1090,7 +1117,15 @@ Proof. - assert (t1 = t2). inv H; inv H0; auto. subst t2. exists vres1; exists m1; auto. (* determ *) -- inv H; inv H0. split. constructor. intuition congruence. +- inv H; inv H0. + assert (EQ1: Vptrofs sz0 = Vptrofs sz) by congruence. + assert (EQ2: sz0 = sz). + { unfold Vptrofs in EQ1; destruct Archi.ptr64 eqn:SF. + rewrite <- (Ptrofs.of_int64_to_int64 SF sz0), <- (Ptrofs.of_int64_to_int64 SF sz). congruence. + rewrite <- (Ptrofs.of_int_to_int SF sz0), <- (Ptrofs.of_int_to_int SF sz). congruence. + } + subst sz0. + split. constructor. intuition congruence. Qed. (** ** Semantics of [memcpy] operations. *) @@ -1099,19 +1134,19 @@ Inductive extcall_memcpy_sem (sz al: Z) (ge: Senv.t): list val -> mem -> trace -> val -> mem -> Prop := | extcall_memcpy_sem_intro: forall bdst odst bsrc osrc m bytes m', al = 1 \/ al = 2 \/ al = 4 \/ al = 8 -> sz >= 0 -> (al | sz) -> - (sz > 0 -> (al | Int.unsigned osrc)) -> - (sz > 0 -> (al | Int.unsigned odst)) -> - bsrc <> bdst \/ Int.unsigned osrc = Int.unsigned odst - \/ Int.unsigned osrc + sz <= Int.unsigned odst - \/ Int.unsigned odst + sz <= Int.unsigned osrc -> - Mem.loadbytes m bsrc (Int.unsigned osrc) sz = Some bytes -> - Mem.storebytes m bdst (Int.unsigned odst) bytes = Some m' -> + (sz > 0 -> (al | Ptrofs.unsigned osrc)) -> + (sz > 0 -> (al | Ptrofs.unsigned odst)) -> + bsrc <> bdst \/ Ptrofs.unsigned osrc = Ptrofs.unsigned odst + \/ Ptrofs.unsigned osrc + sz <= Ptrofs.unsigned odst + \/ Ptrofs.unsigned odst + sz <= Ptrofs.unsigned osrc -> + Mem.loadbytes m bsrc (Ptrofs.unsigned osrc) sz = Some bytes -> + Mem.storebytes m bdst (Ptrofs.unsigned odst) bytes = Some m' -> extcall_memcpy_sem sz al ge (Vptr bdst odst :: Vptr bsrc osrc :: nil) m E0 Vundef m'. Lemma extcall_memcpy_ok: forall sz al, extcall_properties (extcall_memcpy_sem sz al) - (mksignature (Tint :: Tint :: nil) None cc_default). + (mksignature (Tptr :: Tptr :: nil) None cc_default). Proof. intros. constructor. - (* return type *) @@ -1147,9 +1182,9 @@ Proof. destruct (zeq sz 0). + (* special case sz = 0 *) assert (bytes = nil). - { exploit (Mem.loadbytes_empty m1 bsrc (Int.unsigned osrc) sz). omega. congruence. } + { exploit (Mem.loadbytes_empty m1 bsrc (Ptrofs.unsigned osrc) sz). omega. congruence. } subst. - destruct (Mem.range_perm_storebytes m1' b0 (Int.unsigned (Int.add odst (Int.repr delta0))) nil) + destruct (Mem.range_perm_storebytes m1' b0 (Ptrofs.unsigned (Ptrofs.add odst (Ptrofs.repr delta0))) nil) as [m2' SB]. simpl. red; intros; omegaContradiction. exists f, Vundef, m2'. @@ -1168,15 +1203,15 @@ Proof. red; intros; congruence. + (* general case sz > 0 *) exploit Mem.loadbytes_length; eauto. intros LEN. - assert (RPSRC: Mem.range_perm m1 bsrc (Int.unsigned osrc) (Int.unsigned osrc + sz) Cur Nonempty). + assert (RPSRC: Mem.range_perm m1 bsrc (Ptrofs.unsigned osrc) (Ptrofs.unsigned osrc + sz) Cur Nonempty). eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem. - assert (RPDST: Mem.range_perm m1 bdst (Int.unsigned odst) (Int.unsigned odst + sz) Cur Nonempty). + assert (RPDST: Mem.range_perm m1 bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sz) Cur Nonempty). replace sz 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 m1 bsrc (Int.unsigned osrc) Cur Nonempty). + assert (PSRC: Mem.perm m1 bsrc (Ptrofs.unsigned osrc) Cur Nonempty). apply RPSRC. omega. - assert (PDST: Mem.perm m1 bdst (Int.unsigned odst) Cur Nonempty). + assert (PDST: Mem.perm m1 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. @@ -1509,10 +1544,10 @@ Inductive eval_builtin_arg: builtin_arg A -> val -> Prop := | eval_BA_single: forall n, eval_builtin_arg (BA_single n) (Vsingle n) | eval_BA_loadstack: forall chunk ofs v, - Mem.loadv chunk m (Val.add sp (Vint ofs)) = Some v -> + Mem.loadv chunk m (Val.offset_ptr sp ofs) = Some v -> eval_builtin_arg (BA_loadstack chunk ofs) v | eval_BA_addrstack: forall ofs, - eval_builtin_arg (BA_addrstack ofs) (Val.add sp (Vint ofs)) + eval_builtin_arg (BA_addrstack ofs) (Val.offset_ptr sp ofs) | eval_BA_loadglobal: forall chunk id ofs v, Mem.loadv chunk m (Senv.symbol_address ge id ofs) = Some v -> eval_builtin_arg (BA_loadglobal chunk id ofs) 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: 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. diff --git a/common/Memory.v b/common/Memory.v index 672012be..d0cbe8a0 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -450,7 +450,7 @@ Definition load (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z): option val : Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val := match addr with - | Vptr b ofs => load chunk m b (Int.unsigned ofs) + | Vptr b ofs => load chunk m b (Ptrofs.unsigned ofs) | _ => None end. @@ -566,7 +566,7 @@ Qed. Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem := match addr with - | Vptr b ofs => store chunk m b (Int.unsigned ofs) v + | Vptr b ofs => store chunk m b (Ptrofs.unsigned ofs) v | _ => None end. @@ -873,7 +873,7 @@ Qed. Theorem load_int64_split: forall m b ofs v, - load Mint64 m b ofs = Some v -> + load Mint64 m b ofs = Some v -> Archi.ptr64 = false -> exists v1 v2, 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) @@ -897,29 +897,47 @@ Proof. 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. + rewrite EQ. rewrite APP. apply decode_val_int64; auto. erewrite loadbytes_length; eauto. reflexivity. erewrite loadbytes_length; eauto. reflexivity. Qed. +Lemma addressing_int64_split: + forall i, + Archi.ptr64 = false -> + (8 | Ptrofs.unsigned i) -> + Ptrofs.unsigned (Ptrofs.add i (Ptrofs.of_int (Int.repr 4))) = Ptrofs.unsigned i + 4. +Proof. + intros. + rewrite Ptrofs.add_unsigned. + replace (Ptrofs.unsigned (Ptrofs.of_int (Int.repr 4))) with (Int.unsigned (Int.repr 4)) + by (symmetry; apply Ptrofs.agree32_of_int; auto). + change (Int.unsigned (Int.repr 4)) with 4. + apply Ptrofs.unsigned_repr. + exploit (Zdivide_interval (Ptrofs.unsigned i) Ptrofs.modulus 8). + omega. apply Ptrofs.unsigned_range. auto. + exists (two_p (Ptrofs.zwordsize - 3)). + unfold Ptrofs.modulus, Ptrofs.zwordsize, Ptrofs.wordsize. + unfold Wordsize_Ptrofs.wordsize. destruct Archi.ptr64; reflexivity. + unfold Ptrofs.max_unsigned. omega. +Qed. + Theorem loadv_int64_split: forall m a v, - loadv Mint64 m a = Some v -> + loadv Mint64 m a = Some v -> Archi.ptr64 = false -> exists v1 v2, 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) + /\ loadv Mint32 m (Val.add a (Vint (Int.repr 4))) = Some (if Archi.big_endian then v2 else v1) /\ Val.lessdef v (Val.longofwords v1 v2). Proof. - intros. destruct a; simpl in H; try discriminate. + intros. destruct a; simpl in H; inv H. exploit load_int64_split; eauto. intros (v1 & v2 & L1 & L2 & EQ). - assert (NV: Int.unsigned (Int.add i (Int.repr 4)) = Int.unsigned i + 4). - rewrite Int.add_unsigned. apply Int.unsigned_repr. - exploit load_valid_access. eexact H. intros [P Q]. simpl in Q. - exploit (Zdivide_interval (Int.unsigned i) Int.modulus 8). - omega. apply Int.unsigned_range. auto. exists (two_p (32-3)); reflexivity. - unfold Int.max_unsigned. omega. - exists v1; exists v2. -Opaque Int.repr. + unfold Val.add; rewrite H0. + assert (NV: Ptrofs.unsigned (Ptrofs.add i (Ptrofs.of_int (Int.repr 4))) = Ptrofs.unsigned i + 4). + { apply addressing_int64_split; auto. + exploit load_valid_access. eexact H2. intros [P Q]. auto. } + exists v1, v2. +Opaque Ptrofs.repr. split. auto. split. simpl. rewrite NV. auto. auto. @@ -1205,18 +1223,18 @@ Qed. Definition compat_pointer_chunks (chunk1 chunk2: memory_chunk) : Prop := match chunk1, chunk2 with | (Mint32 | Many32), (Mint32 | Many32) => True - | Many64, Many64 => True + | (Mint64 | Many64), (Mint64 | Many64) => True | _, _ => False end. Lemma compat_pointer_chunks_true: forall chunk1 chunk2, - (chunk1 = Mint32 \/ chunk1 = Many32 \/ chunk1 = Many64) -> - (chunk2 = Mint32 \/ chunk2 = Many32 \/ chunk2 = Many64) -> + (chunk1 = Mint32 \/ chunk1 = Many32 \/ chunk1 = Mint64 \/ chunk1 = Many64) -> + (chunk2 = Mint32 \/ chunk2 = Many32 \/ chunk2 = Mint64 \/ chunk2 = Many64) -> quantity_chunk chunk1 = quantity_chunk chunk2 -> compat_pointer_chunks chunk1 chunk2. Proof. - intros. destruct H as [P|[P|P]]; destruct H0 as [Q|[Q|Q]]; + intros. destruct H as [P|[P|[P|P]]]; destruct H0 as [Q|[Q|[Q|Q]]]; subst; red; auto; discriminate. Qed. @@ -1237,10 +1255,11 @@ Proof. destruct CASES as [(A & B) | [(A & B) | (A & B)]]. - (* Same offset *) subst. inv ENC. - assert (chunk = Mint32 \/ chunk = Many32 \/ chunk = Many64) + assert (chunk = Mint32 \/ chunk = Many32 \/ chunk = Mint64 \/ chunk = Many64) by (destruct chunk; auto || contradiction). left; split. rewrite H3. - destruct H4 as [P|[P|P]]; subst chunk'; destruct v0; simpl in H3; congruence. + destruct H4 as [P|[P|[P|P]]]; subst chunk'; destruct v0; simpl in H3; + try congruence; destruct Archi.ptr64; congruence. split. apply compat_pointer_chunks_true; auto. auto. - (* ofs' > ofs *) @@ -1612,7 +1631,7 @@ Qed. Theorem store_int64_split: forall m b ofs v m', - store Mint64 m b ofs v = Some m' -> + store Mint64 m b ofs v = Some m' -> Archi.ptr64 = false -> exists m1, 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'. @@ -1620,7 +1639,7 @@ Proof. intros. exploit store_valid_access_3; eauto. intros [A B]. simpl in *. exploit store_storebytes. eexact H. intros SB. - rewrite encode_val_int64 in SB. + rewrite encode_val_int64 in SB by auto. exploit storebytes_split. eexact SB. intros [m1 [SB1 SB2]]. rewrite encode_val_length in SB2. simpl in SB2. exists m1; split. @@ -1632,20 +1651,18 @@ Qed. Theorem storev_int64_split: forall m a v m', - storev Mint64 m a v = Some m' -> + storev Mint64 m a v = Some m' -> Archi.ptr64 = false -> exists m1, 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. + intros. destruct a; simpl in H; inv H. rewrite H2. exploit store_int64_split; eauto. intros [m1 [A B]]. exists m1; split. exact A. - unfold storev, Val.add. rewrite Int.add_unsigned. rewrite Int.unsigned_repr. exact B. - exploit store_valid_access_3. eexact H. intros [P Q]. simpl in Q. - exploit (Zdivide_interval (Int.unsigned i) Int.modulus 8). - omega. apply Int.unsigned_range. auto. exists (two_p (32-3)); reflexivity. - change (Int.unsigned (Int.repr 4)) with 4. unfold Int.max_unsigned. omega. + unfold storev, Val.add. rewrite H0. + rewrite addressing_int64_split; auto. + exploit store_valid_access_3. eexact H2. intros [P Q]. exact Q. Qed. (** ** Properties related to [alloc]. *) @@ -1811,7 +1828,8 @@ Theorem load_alloc_same: Proof. intros. exploit load_result; eauto. intro. rewrite H0. injection ALLOC; intros. rewrite <- H2; simpl. rewrite <- H1. - rewrite PMap.gss. destruct chunk; simpl; repeat rewrite ZMap.gi; reflexivity. + rewrite PMap.gss. destruct (size_chunk_nat_pos chunk) as [n E]. rewrite E. simpl. + rewrite ZMap.gi. apply decode_val_undef. Qed. Theorem load_alloc_same': @@ -3142,8 +3160,8 @@ Record inject' (f: meminj) (m1 m2: mem) : Prop := mi_representable: forall b b' delta ofs, f b = Some(b', delta) -> - perm m1 b (Int.unsigned ofs) Max Nonempty \/ perm m1 b (Int.unsigned ofs - 1) Max Nonempty -> - delta >= 0 /\ 0 <= Int.unsigned ofs + delta <= Int.max_unsigned; + perm m1 b (Ptrofs.unsigned ofs) Max Nonempty \/ perm m1 b (Ptrofs.unsigned ofs - 1) Max Nonempty -> + delta >= 0 /\ 0 <= Ptrofs.unsigned ofs + delta <= Ptrofs.max_unsigned; mi_perm_inv: forall b1 ofs b2 delta k p, f b1 = Some(b2, delta) -> @@ -3246,24 +3264,24 @@ Qed. Lemma address_inject: forall f m1 m2 b1 ofs1 b2 delta p, inject f m1 m2 -> - perm m1 b1 (Int.unsigned ofs1) Cur p -> + perm m1 b1 (Ptrofs.unsigned ofs1) Cur p -> f b1 = Some (b2, delta) -> - Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta. + Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta. Proof. intros. - assert (perm m1 b1 (Int.unsigned ofs1) Max Nonempty) by eauto with mem. + assert (perm m1 b1 (Ptrofs.unsigned ofs1) Max Nonempty) by eauto with mem. exploit mi_representable; eauto. intros [A B]. - assert (0 <= delta <= Int.max_unsigned). - generalize (Int.unsigned_range ofs1). omega. - unfold Int.add. repeat rewrite Int.unsigned_repr; omega. + assert (0 <= delta <= Ptrofs.max_unsigned). + generalize (Ptrofs.unsigned_range ofs1). omega. + unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; omega. Qed. Lemma address_inject': forall f m1 m2 chunk b1 ofs1 b2 delta, inject f m1 m2 -> - valid_access m1 chunk b1 (Int.unsigned ofs1) Nonempty -> + valid_access m1 chunk b1 (Ptrofs.unsigned ofs1) Nonempty -> f b1 = Some (b2, delta) -> - Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta. + Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta. Proof. intros. destruct H0. eapply address_inject; eauto. apply H0. generalize (size_chunk_pos chunk). omega. @@ -3272,24 +3290,24 @@ Qed. Theorem weak_valid_pointer_inject_no_overflow: forall f m1 m2 b ofs b' delta, inject f m1 m2 -> - weak_valid_pointer m1 b (Int.unsigned ofs) = true -> + weak_valid_pointer m1 b (Ptrofs.unsigned ofs) = true -> f b = Some(b', delta) -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. intros. rewrite weak_valid_pointer_spec in H0. rewrite ! valid_pointer_nonempty_perm in H0. exploit mi_representable; eauto. destruct H0; eauto with mem. intros [A B]. - pose proof (Int.unsigned_range ofs). - rewrite Int.unsigned_repr; omega. + pose proof (Ptrofs.unsigned_range ofs). + rewrite Ptrofs.unsigned_repr; omega. Qed. Theorem valid_pointer_inject_no_overflow: forall f m1 m2 b ofs b' delta, inject f m1 m2 -> - valid_pointer m1 b (Int.unsigned ofs) = true -> + valid_pointer m1 b (Ptrofs.unsigned ofs) = true -> f b = Some(b', delta) -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. eauto using weak_valid_pointer_inject_no_overflow, valid_pointer_implies. Qed. @@ -3297,9 +3315,9 @@ Qed. Theorem valid_pointer_inject_val: forall f m1 m2 b ofs b' ofs', inject f m1 m2 -> - valid_pointer m1 b (Int.unsigned ofs) = true -> + valid_pointer m1 b (Ptrofs.unsigned ofs) = true -> Val.inject f (Vptr b ofs) (Vptr b' ofs') -> - valid_pointer m2 b' (Int.unsigned ofs') = true. + valid_pointer m2 b' (Ptrofs.unsigned ofs') = true. Proof. intros. inv H1. erewrite address_inject'; eauto. @@ -3310,9 +3328,9 @@ Qed. Theorem weak_valid_pointer_inject_val: forall f m1 m2 b ofs b' ofs', inject f m1 m2 -> - weak_valid_pointer m1 b (Int.unsigned ofs) = true -> + weak_valid_pointer m1 b (Ptrofs.unsigned ofs) = true -> Val.inject f (Vptr b ofs) (Vptr b' ofs') -> - weak_valid_pointer m2 b' (Int.unsigned ofs') = true. + weak_valid_pointer m2 b' (Ptrofs.unsigned ofs') = true. Proof. intros. inv H1. exploit weak_valid_pointer_inject; eauto. intros W. @@ -3320,8 +3338,8 @@ Proof. rewrite ! valid_pointer_nonempty_perm in H0. exploit mi_representable; eauto. destruct H0; eauto with mem. intros [A B]. - pose proof (Int.unsigned_range ofs). - unfold Int.add. repeat rewrite Int.unsigned_repr; auto; omega. + pose proof (Ptrofs.unsigned_range ofs). + unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; auto; omega. Qed. Theorem inject_no_overlap: @@ -3341,13 +3359,13 @@ Theorem different_pointers_inject: forall f m m' b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, inject f m m' -> b1 <> b2 -> - valid_pointer m b1 (Int.unsigned ofs1) = true -> - valid_pointer m b2 (Int.unsigned ofs2) = true -> + valid_pointer m b1 (Ptrofs.unsigned ofs1) = true -> + valid_pointer m b2 (Ptrofs.unsigned ofs2) = true -> f b1 = Some (b1', delta1) -> f b2 = Some (b2', delta2) -> b1' <> b2' \/ - Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> - Int.unsigned (Int.add ofs2 (Int.repr delta2)). + Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> + Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)). Proof. intros. rewrite valid_pointer_valid_access in H1. @@ -3356,8 +3374,8 @@ Proof. rewrite (address_inject' _ _ _ _ _ _ _ _ H H2 H4). inv H1. simpl in H5. inv H2. simpl in H1. eapply mi_no_overlap; eauto. - apply perm_cur_max. apply (H5 (Int.unsigned ofs1)). omega. - apply perm_cur_max. apply (H1 (Int.unsigned ofs2)). omega. + apply perm_cur_max. apply (H5 (Ptrofs.unsigned ofs1)). omega. + apply perm_cur_max. apply (H1 (Ptrofs.unsigned ofs2)). omega. Qed. Require Intv. @@ -3439,8 +3457,8 @@ Proof. intros. inv H1; simpl in H0; try discriminate. exploit load_inject; eauto. intros [v2 [LOAD INJ]]. exists v2; split; auto. unfold loadv. - replace (Int.unsigned (Int.add ofs1 (Int.repr delta))) - with (Int.unsigned ofs1 + delta). + replace (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta))) + with (Ptrofs.unsigned ofs1 + delta). auto. symmetry. eapply address_inject'; eauto with mem. Qed. @@ -3547,8 +3565,8 @@ Theorem storev_mapped_inject: Proof. intros. inv H1; simpl in H0; try discriminate. unfold storev. - replace (Int.unsigned (Int.add ofs1 (Int.repr delta))) - with (Int.unsigned ofs1 + delta). + replace (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta))) + with (Ptrofs.unsigned ofs1 + delta). eapply store_mapped_inject; eauto. symmetry. eapply address_inject'; eauto with mem. Qed. @@ -3740,8 +3758,8 @@ Theorem alloc_left_mapped_inject: inject f m1 m2 -> alloc m1 lo hi = (m1', b1) -> valid_block m2 b2 -> - 0 <= delta <= Int.max_unsigned -> - (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Int.max_unsigned) -> + 0 <= delta <= Ptrofs.max_unsigned -> + (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Ptrofs.max_unsigned) -> (forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) -> inj_offset_aligned delta (hi-lo) -> (forall b delta' ofs k p, @@ -3803,10 +3821,10 @@ Proof. subst. injection H9; intros; subst b' delta0. destruct H10. exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro. exploit H3. apply H4 with (k := Max) (p := Nonempty); eauto. - generalize (Int.unsigned_range_2 ofs). omega. + generalize (Ptrofs.unsigned_range_2 ofs). omega. exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro. exploit H3. apply H4 with (k := Max) (p := Nonempty); eauto. - generalize (Int.unsigned_range_2 ofs). omega. + generalize (Ptrofs.unsigned_range_2 ofs). omega. eapply mi_representable0; try eassumption. destruct H10; eauto using perm_alloc_4. (* perm inv *) @@ -3843,7 +3861,7 @@ Proof. eapply alloc_right_inject; eauto. eauto. instantiate (1 := b2). eauto with mem. - instantiate (1 := 0). unfold Int.max_unsigned. generalize Int.modulus_pos; omega. + instantiate (1 := 0). unfold Ptrofs.max_unsigned. generalize Ptrofs.modulus_pos; omega. auto. intros. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. omega. @@ -4054,13 +4072,13 @@ Proof. destruct (f b) as [[b1 delta1] |] eqn:?; try discriminate. destruct (f' b1) as [[b2 delta2] |] eqn:?; inv H. exploit mi_representable0; eauto. intros [A B]. - set (ofs' := Int.repr (Int.unsigned ofs + delta1)). - assert (Int.unsigned ofs' = Int.unsigned ofs + delta1). - unfold ofs'; apply Int.unsigned_repr. auto. + set (ofs' := Ptrofs.repr (Ptrofs.unsigned ofs + delta1)). + assert (Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs + delta1). + unfold ofs'; apply Ptrofs.unsigned_repr. auto. exploit mi_representable1. eauto. instantiate (1 := ofs'). rewrite H. - replace (Int.unsigned ofs + delta1 - 1) with - ((Int.unsigned ofs - 1) + delta1) by omega. + replace (Ptrofs.unsigned ofs + delta1 - 1) with + ((Ptrofs.unsigned ofs - 1) + delta1) by omega. destruct H0; eauto using perm_inj. rewrite H. omega. (* perm inv *) @@ -4185,7 +4203,7 @@ Proof. apply flat_inj_no_overlap. (* range *) unfold flat_inj; intros. - destruct (plt b (nextblock m)); inv H0. generalize (Int.unsigned_range_2 ofs); omega. + destruct (plt b (nextblock m)); inv H0. generalize (Ptrofs.unsigned_range_2 ofs); omega. (* perm inv *) unfold flat_inj; intros. destruct (plt b1 (nextblock m)); inv H0. diff --git a/common/Memtype.v b/common/Memtype.v index 5dbb66dc..b055668c 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -124,13 +124,13 @@ Parameter store: forall (chunk: memory_chunk) (m: mem) (b: block) (ofs: Z) (v: v Definition loadv (chunk: memory_chunk) (m: mem) (addr: val) : option val := match addr with - | Vptr b ofs => load chunk m b (Int.unsigned ofs) + | Vptr b ofs => load chunk m b (Ptrofs.unsigned ofs) | _ => None end. Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem := match addr with - | Vptr b ofs => store chunk m b (Int.unsigned ofs) v + | Vptr b ofs => store chunk m b (Ptrofs.unsigned ofs) v | _ => None end. @@ -445,7 +445,7 @@ Axiom load_store_other: Definition compat_pointer_chunks (chunk1 chunk2: memory_chunk) : Prop := match chunk1, chunk2 with | (Mint32 | Many32), (Mint32 | Many32) => True - | Many64, Many64 => True + | (Mint64 | Many64), (Mint64 | Many64) => True | _, _ => False end. @@ -978,37 +978,37 @@ Axiom weak_valid_pointer_inject: Axiom address_inject: forall f m1 m2 b1 ofs1 b2 delta p, inject f m1 m2 -> - perm m1 b1 (Int.unsigned ofs1) Cur p -> + perm m1 b1 (Ptrofs.unsigned ofs1) Cur p -> f b1 = Some (b2, delta) -> - Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta. + Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta. Axiom valid_pointer_inject_no_overflow: forall f m1 m2 b ofs b' delta, inject f m1 m2 -> - valid_pointer m1 b (Int.unsigned ofs) = true -> + valid_pointer m1 b (Ptrofs.unsigned ofs) = true -> f b = Some(b', delta) -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Axiom weak_valid_pointer_inject_no_overflow: forall f m1 m2 b ofs b' delta, inject f m1 m2 -> - weak_valid_pointer m1 b (Int.unsigned ofs) = true -> + weak_valid_pointer m1 b (Ptrofs.unsigned ofs) = true -> f b = Some(b', delta) -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Axiom valid_pointer_inject_val: forall f m1 m2 b ofs b' ofs', inject f m1 m2 -> - valid_pointer m1 b (Int.unsigned ofs) = true -> + valid_pointer m1 b (Ptrofs.unsigned ofs) = true -> Val.inject f (Vptr b ofs) (Vptr b' ofs') -> - valid_pointer m2 b' (Int.unsigned ofs') = true. + valid_pointer m2 b' (Ptrofs.unsigned ofs') = true. Axiom weak_valid_pointer_inject_val: forall f m1 m2 b ofs b' ofs', inject f m1 m2 -> - weak_valid_pointer m1 b (Int.unsigned ofs) = true -> + weak_valid_pointer m1 b (Ptrofs.unsigned ofs) = true -> Val.inject f (Vptr b ofs) (Vptr b' ofs') -> - weak_valid_pointer m2 b' (Int.unsigned ofs') = true. + weak_valid_pointer m2 b' (Ptrofs.unsigned ofs') = true. Axiom inject_no_overlap: forall f m1 m2 b1 b2 b1' b2' delta1 delta2 ofs1 ofs2, @@ -1024,13 +1024,13 @@ Axiom different_pointers_inject: forall f m m' b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, inject f m m' -> b1 <> b2 -> - valid_pointer m b1 (Int.unsigned ofs1) = true -> - valid_pointer m b2 (Int.unsigned ofs2) = true -> + valid_pointer m b1 (Ptrofs.unsigned ofs1) = true -> + valid_pointer m b2 (Ptrofs.unsigned ofs2) = true -> f b1 = Some (b1', delta1) -> f b2 = Some (b2', delta2) -> b1' <> b2' \/ - Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> - Int.unsigned (Int.add ofs2 (Int.repr delta2)). + Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> + Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)). Axiom load_inject: forall f m1 m2 chunk b1 ofs b2 delta v1, @@ -1141,8 +1141,8 @@ Axiom alloc_left_mapped_inject: inject f m1 m2 -> alloc m1 lo hi = (m1', b1) -> valid_block m2 b2 -> - 0 <= delta <= Int.max_unsigned -> - (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Int.max_unsigned) -> + 0 <= delta <= Ptrofs.max_unsigned -> + (forall ofs k p, perm m2 b2 ofs k p -> delta = 0 \/ 0 <= ofs < Ptrofs.max_unsigned) -> (forall ofs k p, lo <= ofs < hi -> perm m2 b2 (ofs + delta) k p) -> inj_offset_aligned delta (hi-lo) -> (forall b delta' ofs k p, diff --git a/common/Separation.v b/common/Separation.v index efcd3281..c0a3c9cf 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -319,7 +319,7 @@ Qed. Program Definition range (b: block) (lo hi: Z) : massert := {| m_pred := fun m => - 0 <= lo /\ hi <= Int.modulus + 0 <= lo /\ hi <= Ptrofs.modulus /\ (forall i k p, lo <= i < hi -> Mem.perm m b i k p); m_footprint := fun b' ofs' => b' = b /\ lo <= ofs' < hi |}. @@ -333,7 +333,7 @@ Qed. Lemma alloc_rule: forall m lo hi b m' P, Mem.alloc m lo hi = (m', b) -> - 0 <= lo -> hi <= Int.modulus -> + 0 <= lo -> hi <= Ptrofs.modulus -> m |= P -> m' |= range b lo hi ** P. Proof. @@ -413,7 +413,7 @@ Qed. Program Definition contains (chunk: memory_chunk) (b: block) (ofs: Z) (spec: val -> Prop) : massert := {| m_pred := fun m => - 0 <= ofs <= Int.max_unsigned + 0 <= ofs <= Ptrofs.max_unsigned /\ Mem.valid_access m chunk b ofs Freeable /\ exists v, Mem.load chunk m b ofs = Some v /\ spec v; m_footprint := fun b' ofs' => b' = b /\ ofs <= ofs' < ofs + size_chunk chunk @@ -431,7 +431,7 @@ Qed. Lemma contains_no_overflow: forall spec m chunk b ofs, m |= contains chunk b ofs spec -> - 0 <= ofs <= Int.max_unsigned. + 0 <= ofs <= Ptrofs.max_unsigned. Proof. intros. simpl in H. tauto. Qed. @@ -448,10 +448,10 @@ Qed. Lemma loadv_rule: forall spec m chunk b ofs, m |= contains chunk b ofs spec -> - exists v, Mem.loadv chunk m (Vptr b (Int.repr ofs)) = Some v /\ spec v. + exists v, Mem.loadv chunk m (Vptr b (Ptrofs.repr ofs)) = Some v /\ spec v. Proof. intros. exploit load_rule; eauto. intros (v & A & B). exists v; split; auto. - simpl. rewrite Int.unsigned_repr; auto. eapply contains_no_overflow; eauto. + simpl. rewrite Ptrofs.unsigned_repr; auto. eapply contains_no_overflow; eauto. Qed. Lemma store_rule: @@ -477,10 +477,10 @@ Lemma storev_rule: m |= contains chunk b ofs spec1 ** P -> spec (Val.load_result chunk v) -> exists m', - Mem.storev chunk m (Vptr b (Int.repr ofs)) v = Some m' /\ m' |= contains chunk b ofs spec ** P. + Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= contains chunk b ofs spec ** P. Proof. intros. exploit store_rule; eauto. intros (m' & A & B). exists m'; split; auto. - simpl. rewrite Int.unsigned_repr; auto. eapply contains_no_overflow. eapply sep_pick1; eauto. + simpl. rewrite Ptrofs.unsigned_repr; auto. eapply contains_no_overflow. eapply sep_pick1; eauto. Qed. Lemma range_contains: @@ -493,7 +493,7 @@ Proof. split; [|split]. - assert (Mem.valid_access m chunk b ofs Freeable). { split; auto. red; auto. } - split. generalize (size_chunk_pos chunk). unfold Int.max_unsigned. omega. + split. generalize (size_chunk_pos chunk). unfold Ptrofs.max_unsigned. omega. split. auto. + destruct (Mem.valid_access_load m chunk b ofs) as [v LOAD]. eauto with mem. @@ -530,7 +530,7 @@ Lemma storev_rule': forall chunk m b ofs v (spec1: val -> Prop) P, m |= contains chunk b ofs spec1 ** P -> exists m', - Mem.storev chunk m (Vptr b (Int.repr ofs)) v = Some m' /\ m' |= hasvalue chunk b ofs (Val.load_result chunk v) ** P. + Mem.storev chunk m (Vptr b (Ptrofs.repr ofs)) v = Some m' /\ m' |= hasvalue chunk b ofs (Val.load_result chunk v) ** P. Proof. intros. eapply storev_rule; eauto. Qed. @@ -656,9 +656,9 @@ Proof. intros. destruct H as (A & B & C). simpl in A. exploit Mem.storev_mapped_inject; eauto. intros (m2' & STORE & INJ). inv H1; simpl in STORE; try discriminate. - assert (VALID: Mem.valid_access m1 chunk b1 (Int.unsigned ofs1) Writable) + assert (VALID: Mem.valid_access m1 chunk b1 (Ptrofs.unsigned ofs1) Writable) by eauto with mem. - assert (EQ: Int.unsigned (Int.add ofs1 (Int.repr delta)) = Int.unsigned ofs1 + delta). + assert (EQ: Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta). { eapply Mem.address_inject'; eauto with mem. } exists m2'; split; auto. split; [|split]. @@ -681,7 +681,7 @@ Lemma alloc_parallel_rule: (8 | delta) -> lo = delta -> hi = delta + Zmax 0 sz1 -> - 0 <= sz2 <= Int.max_unsigned -> + 0 <= sz2 <= Ptrofs.max_unsigned -> 0 <= delta -> hi <= sz2 -> exists j', m2' |= range b2 0 lo ** range b2 hi sz2 ** minjection j' m1' ** P @@ -709,7 +709,7 @@ Proof. exists j'; split; auto. rewrite <- ! sep_assoc. split; [|split]. -+ simpl. intuition auto; try (unfold Int.max_unsigned in *; omega). ++ simpl. intuition auto; try (unfold Ptrofs.max_unsigned in *; omega). * apply Mem.perm_implies with Freeable; auto with mem. eapply Mem.perm_alloc_2; eauto. omega. * apply Mem.perm_implies with Freeable; auto with mem. @@ -891,7 +891,7 @@ Lemma alloc_parallel_rule_2: (8 | delta) -> lo = delta -> hi = delta + Zmax 0 sz1 -> - 0 <= sz2 <= Int.max_unsigned -> + 0 <= sz2 <= Ptrofs.max_unsigned -> 0 <= delta -> hi <= sz2 -> exists j', m2' |= range b2 0 lo ** range b2 hi sz2 ** minjection j' m1' ** globalenv_inject ge j' ** P diff --git a/common/Values.v b/common/Values.v index 663bddf6..d1058fe8 100644 --- a/common/Values.v +++ b/common/Values.v @@ -16,6 +16,7 @@ (** This module defines the type of values that is used in the dynamic semantics of all our intermediate languages. *) +Require Archi. Require Import Coqlib. Require Import AST. Require Import Integers. @@ -39,7 +40,7 @@ Inductive val: Type := | Vlong: int64 -> val | Vfloat: float -> val | Vsingle: float32 -> val - | Vptr: block -> int -> val. + | Vptr: block -> ptrofs -> val. Definition Vzero: val := Vint Int.zero. Definition Vone: val := Vint Int.one. @@ -48,6 +49,12 @@ Definition Vmone: val := Vint Int.mone. Definition Vtrue: val := Vint Int.one. Definition Vfalse: val := Vint Int.zero. +Definition Vnullptr := + if Archi.ptr64 then Vlong Int64.zero else Vint Int.zero. + +Definition Vptrofs (n: ptrofs) := + if Archi.ptr64 then Vlong (Ptrofs.to_int64 n) else Vint (Ptrofs.to_int n). + (** * Operations over values *) (** The module [Val] defines a number of arithmetic and logical operations @@ -63,7 +70,7 @@ Proof. apply Int64.eq_dec. apply Float.eq_dec. apply Float32.eq_dec. - apply Int.eq_dec. + apply Ptrofs.eq_dec. apply eq_block. Defined. Global Opaque eq. @@ -75,8 +82,10 @@ Definition has_type (v: val) (t: typ) : Prop := | Vlong _, Tlong => True | Vfloat _, Tfloat => True | Vsingle _, Tsingle => True - | Vptr _ _, Tint => True - | (Vint _ | Vptr _ _ | Vsingle _), Tany32 => True + | Vptr _ _, Tint => Archi.ptr64 = false + | Vptr _ _, Tlong => Archi.ptr64 = true + | (Vint _ | Vsingle _), Tany32 => True + | Vptr _ _, Tany32 => Archi.ptr64 = false | _, Tany64 => True | _, _ => False end. @@ -94,12 +103,25 @@ Definition has_opttype (v: val) (ot: option typ) : Prop := | Some t => has_type v t end. +Lemma Vptr_has_type: + forall b ofs, has_type (Vptr b ofs) Tptr. +Proof. + intros. unfold Tptr, has_type; destruct Archi.ptr64; reflexivity. +Qed. + +Lemma Vnullptr_has_type: + has_type Vnullptr Tptr. +Proof. + unfold has_type, Vnullptr, Tptr; destruct Archi.ptr64; reflexivity. +Qed. + Lemma has_subtype: forall ty1 ty2 v, subtype ty1 ty2 = true -> has_type v ty1 -> has_type v ty2. Proof. - intros. destruct ty1; destruct ty2; simpl in H; discriminate || assumption || idtac; - unfold has_type in *; destruct v; auto. + intros. destruct ty1; destruct ty2; simpl in H; + (contradiction || discriminate || assumption || idtac); + unfold has_type in *; destruct v; auto; contradiction. Qed. Lemma has_subtype_list: @@ -257,17 +279,18 @@ Definition floatofsingle (v: val) : val := Definition add (v1 v2: val): val := match v1, v2 with | Vint n1, Vint n2 => Vint(Int.add n1 n2) - | Vptr b1 ofs1, Vint n2 => Vptr b1 (Int.add ofs1 n2) - | Vint n1, Vptr b2 ofs2 => Vptr b2 (Int.add ofs2 n1) + | Vptr b1 ofs1, Vint n2 => if Archi.ptr64 then Vundef else Vptr b1 (Ptrofs.add ofs1 (Ptrofs.of_int n2)) + | Vint n1, Vptr b2 ofs2 => if Archi.ptr64 then Vundef else Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int n1)) | _, _ => Vundef end. Definition sub (v1 v2: val): val := match v1, v2 with | Vint n1, Vint n2 => Vint(Int.sub n1 n2) - | Vptr b1 ofs1, Vint n2 => Vptr b1 (Int.sub ofs1 n2) + | Vptr b1 ofs1, Vint n2 => if Archi.ptr64 then Vundef else Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.of_int n2)) | Vptr b1 ofs1, Vptr b2 ofs2 => - if eq_block b1 b2 then Vint(Int.sub ofs1 ofs2) else Vundef + if Archi.ptr64 then Vundef else + if eq_block b1 b2 then Vint(Ptrofs.to_int (Ptrofs.sub ofs1 ofs2)) else Vundef | _, _ => Vundef end. @@ -571,12 +594,19 @@ Definition singleoflongu (v: val) : option val := Definition addl (v1 v2: val): val := match v1, v2 with | Vlong n1, Vlong n2 => Vlong(Int64.add n1 n2) + | Vptr b1 ofs1, Vlong n2 => if Archi.ptr64 then Vptr b1 (Ptrofs.add ofs1 (Ptrofs.of_int64 n2)) else Vundef + | Vlong n1, Vptr b2 ofs2 => if Archi.ptr64 then Vptr b2 (Ptrofs.add ofs2 (Ptrofs.of_int64 n1)) else Vundef | _, _ => Vundef end. Definition subl (v1 v2: val): val := match v1, v2 with | Vlong n1, Vlong n2 => Vlong(Int64.sub n1 n2) + | Vptr b1 ofs1, Vlong n2 => + if Archi.ptr64 then Vptr b1 (Ptrofs.sub ofs1 (Ptrofs.of_int64 n2)) else Vundef + | Vptr b1 ofs1, Vptr b2 ofs2 => + if negb Archi.ptr64 then Vundef else + if eq_block b1 b2 then Vlong(Ptrofs.to_int64 (Ptrofs.sub ofs1 ofs2)) else Vundef | _, _ => Vundef end. @@ -626,6 +656,18 @@ Definition modlu (v1 v2: val): option val := | _, _ => None end. +Definition subl_overflow (v1 v2: val) : val := + match v1, v2 with + | Vlong n1, Vlong n2 => Vint (Int.repr (Int64.unsigned (Int64.sub_overflow n1 n2 Int64.zero))) + | _, _ => Vundef + end. + +Definition negativel (v: val) : val := + match v with + | Vlong n => Vint (Int.repr (Int64.unsigned (Int64.negative n))) + | _ => Vundef + end. + Definition andl (v1 v2: val): val := match v1, v2 with | Vlong n1, Vlong n2 => Vlong(Int64.and n1 n2) @@ -671,6 +713,24 @@ Definition shrlu (v1 v2: val): val := | _, _ => Vundef end. +Definition roll (v1 v2: val): val := + match v1, v2 with + | Vlong n1, Vint n2 => Vlong(Int64.rol n1 (Int64.repr (Int.unsigned n2))) + | _, _ => Vundef + end. + +Definition rorl (v1 v2: val): val := + match v1, v2 with + | Vlong n1, Vint n2 => Vlong(Int64.ror n1 (Int64.repr (Int.unsigned n2))) + | _, _ => Vundef + end. + +Definition rolml (v: val) (amount mask: int64): val := + match v with + | Vlong n => Vlong(Int64.rolm n amount mask) + | _ => Vundef + end. + (** Comparisons *) Section COMPARISONS. @@ -696,22 +756,25 @@ Definition cmpu_bool (c: comparison) (v1 v2: val): option bool := | Vint n1, Vint n2 => Some (Int.cmpu c n1 n2) | Vint n1, Vptr b2 ofs2 => - if Int.eq n1 Int.zero && weak_valid_ptr b2 (Int.unsigned ofs2) + if Archi.ptr64 then None else + if Int.eq n1 Int.zero && weak_valid_ptr b2 (Ptrofs.unsigned ofs2) then cmp_different_blocks c else None | Vptr b1 ofs1, Vptr b2 ofs2 => + if Archi.ptr64 then None else if eq_block b1 b2 then - if weak_valid_ptr b1 (Int.unsigned ofs1) - && weak_valid_ptr b2 (Int.unsigned ofs2) - then Some (Int.cmpu c ofs1 ofs2) + if weak_valid_ptr b1 (Ptrofs.unsigned ofs1) + && weak_valid_ptr b2 (Ptrofs.unsigned ofs2) + then Some (Ptrofs.cmpu c ofs1 ofs2) else None else - if valid_ptr b1 (Int.unsigned ofs1) - && valid_ptr b2 (Int.unsigned ofs2) + if valid_ptr b1 (Ptrofs.unsigned ofs1) + && valid_ptr b2 (Ptrofs.unsigned ofs2) then cmp_different_blocks c else None | Vptr b1 ofs1, Vint n2 => - if Int.eq n2 Int.zero && weak_valid_ptr b1 (Int.unsigned ofs1) + if Archi.ptr64 then None else + if Int.eq n2 Int.zero && weak_valid_ptr b1 (Ptrofs.unsigned ofs1) then cmp_different_blocks c else None | _, _ => None @@ -738,6 +801,28 @@ Definition cmpl_bool (c: comparison) (v1 v2: val): option bool := Definition cmplu_bool (c: comparison) (v1 v2: val): option bool := match v1, v2 with | Vlong n1, Vlong n2 => Some (Int64.cmpu c n1 n2) + | Vlong n1, Vptr b2 ofs2 => + if negb Archi.ptr64 then None else + if Int64.eq n1 Int64.zero && weak_valid_ptr b2 (Ptrofs.unsigned ofs2) + then cmp_different_blocks c + else None + | Vptr b1 ofs1, Vptr b2 ofs2 => + if negb Archi.ptr64 then None else + if eq_block b1 b2 then + if weak_valid_ptr b1 (Ptrofs.unsigned ofs1) + && weak_valid_ptr b2 (Ptrofs.unsigned ofs2) + then Some (Ptrofs.cmpu c ofs1 ofs2) + else None + else + if valid_ptr b1 (Ptrofs.unsigned ofs1) + && valid_ptr b2 (Ptrofs.unsigned ofs2) + then cmp_different_blocks c + else None + | Vptr b1 ofs1, Vlong n2 => + if negb Archi.ptr64 then None else + if Int64.eq n2 Int64.zero && weak_valid_ptr b1 (Ptrofs.unsigned ofs1) + then cmp_different_blocks c + else None | _, _ => None end. @@ -770,6 +855,14 @@ Definition maskzero_bool (v: val) (mask: int): option bool := End COMPARISONS. +(** Add the given offset to the given pointer. *) + +Definition offset_ptr (v: val) (delta: ptrofs) : val := + match v with + | Vptr b ofs => Vptr b (Ptrofs.add ofs delta) + | _ => Vundef + end. + (** [load_result] reflects the effect of storing a value with a given memory chunk, then reading it back with the same chunk. Depending on the chunk and the type of the value, some normalization occurs. @@ -786,11 +879,13 @@ Definition load_result (chunk: memory_chunk) (v: val) := | Mint16signed, Vint n => Vint (Int.sign_ext 16 n) | Mint16unsigned, Vint n => Vint (Int.zero_ext 16 n) | Mint32, Vint n => Vint n - | Mint32, Vptr b ofs => Vptr b ofs + | Mint32, Vptr b ofs => if Archi.ptr64 then Vundef else Vptr b ofs | Mint64, Vlong n => Vlong n + | Mint64, Vptr b ofs => if Archi.ptr64 then Vptr b ofs else Vundef | Mfloat32, Vsingle f => Vsingle f | Mfloat64, Vfloat f => Vfloat f - | Many32, (Vint _ | Vptr _ _ | Vsingle _) => v + | Many32, (Vint _ | Vsingle _) => v + | Many32, Vptr _ _ => if Archi.ptr64 then Vundef else v | Many64, _ => v | _, _ => Vundef end. @@ -798,13 +893,14 @@ Definition load_result (chunk: memory_chunk) (v: val) := Lemma load_result_type: forall chunk v, has_type (load_result chunk v) (type_of_chunk chunk). Proof. - intros. destruct chunk; destruct v; simpl; auto. + intros. unfold has_type; destruct chunk; destruct v; simpl; auto; destruct Archi.ptr64 eqn:SF; simpl; auto. Qed. Lemma load_result_same: forall v ty, has_type v ty -> load_result (chunk_of_type ty) v = v. Proof. - unfold has_type; intros. destruct v; destruct ty; try contradiction; auto. + unfold has_type, load_result; intros. + destruct v; destruct ty; destruct Archi.ptr64; try contradiction; try discriminate; auto. Qed. (** Theorems on arithmetic operations. *) @@ -882,13 +978,15 @@ Qed. Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z). Proof. - destruct x; destruct y; destruct z; simpl; auto. - rewrite Int.add_assoc; auto. - rewrite Int.add_assoc; auto. - decEq. decEq. apply Int.add_commut. - decEq. rewrite Int.add_commut. rewrite <- Int.add_assoc. - decEq. apply Int.add_commut. - decEq. rewrite Int.add_assoc. auto. + unfold add; intros; destruct Archi.ptr64 eqn:SF, x, y, z; simpl; auto. +- rewrite Int.add_assoc; auto. +- rewrite Int.add_assoc; auto. +- rewrite ! Ptrofs.add_assoc. f_equal. f_equal. + rewrite Ptrofs.add_commut. auto with ptrofs. +- rewrite ! Ptrofs.add_assoc. f_equal. f_equal. + apply Ptrofs.add_commut. +- rewrite ! Ptrofs.add_assoc. f_equal. f_equal. + symmetry. auto with ptrofs. Qed. Theorem add_permut: forall x y z, add x (add y z) = add y (add x z). @@ -910,7 +1008,8 @@ Qed. Theorem neg_add_distr: forall x y, neg(add x y) = add (neg x) (neg y). Proof. - destruct x; destruct y; simpl; auto. decEq. apply Int.neg_add_distr. + unfold neg, add; intros; destruct Archi.ptr64 eqn:SF, x, y; simpl; auto; + rewrite Int.neg_add_distr; auto. Qed. Theorem sub_zero_r: forall x, sub Vzero x = neg x. @@ -920,37 +1019,40 @@ Qed. Theorem sub_add_opp: forall x y, sub x (Vint y) = add x (Vint (Int.neg y)). Proof. - destruct x; intro y; simpl; auto; rewrite Int.sub_add_opp; auto. + unfold sub, add; intros; destruct Archi.ptr64 eqn:SF, x; auto. +- rewrite Int.sub_add_opp; auto. +- rewrite Int.sub_add_opp; auto. +- rewrite Ptrofs.sub_add_opp. f_equal. f_equal. symmetry. auto with ptrofs. Qed. Theorem sub_opp_add: forall x y, sub x (Vint (Int.neg y)) = add x (Vint y). Proof. - intros. unfold sub, add. - destruct x; auto; rewrite Int.sub_add_opp; rewrite Int.neg_involutive; auto. + intros. rewrite sub_add_opp. rewrite Int.neg_involutive. auto. Qed. Theorem sub_add_l: forall v1 v2 i, sub (add v1 (Vint i)) v2 = add (sub v1 v2) (Vint i). Proof. - destruct v1; destruct v2; intros; simpl; auto. - rewrite Int.sub_add_l. auto. - rewrite Int.sub_add_l. auto. - case (eq_block b b0); intro. rewrite Int.sub_add_l. auto. reflexivity. + unfold sub, add; intros; destruct Archi.ptr64 eqn:SF, v1, v2; auto. +- rewrite Int.sub_add_l; auto. +- rewrite Int.sub_add_l; auto. +- rewrite Ptrofs.sub_add_l; auto. +- destruct (eq_block b b0); auto. + f_equal. rewrite Ptrofs.sub_add_l. auto with ptrofs. Qed. Theorem sub_add_r: forall v1 v2 i, sub v1 (add v2 (Vint i)) = add (sub v1 v2) (Vint (Int.neg i)). Proof. - destruct v1; destruct v2; intros; simpl; auto. - rewrite Int.sub_add_r. auto. - repeat rewrite Int.sub_add_opp. decEq. - repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - decEq. repeat rewrite Int.sub_add_opp. - rewrite Int.add_assoc. decEq. apply Int.neg_add_distr. - case (eq_block b b0); intro. simpl. decEq. - repeat rewrite Int.sub_add_opp. rewrite Int.add_assoc. decEq. - apply Int.neg_add_distr. - reflexivity. + unfold sub, add; intros; destruct Archi.ptr64 eqn:SF, v1, v2; auto. +- rewrite Int.add_commut. rewrite Int.sub_add_r. auto. +- rewrite Int.add_commut. rewrite Int.sub_add_r. auto. +- f_equal. replace (Ptrofs.of_int (Int.add i1 i)) with (Ptrofs.add (Ptrofs.of_int i) (Ptrofs.of_int i1)). + rewrite Ptrofs.sub_add_r. f_equal. + symmetry. auto with ptrofs. + symmetry. rewrite Int.add_commut. auto with ptrofs. +- destruct (eq_block b b0); auto. + f_equal. rewrite Ptrofs.add_commut. rewrite Ptrofs.sub_add_r. auto with ptrofs. Qed. Theorem mul_commut: forall x y, mul x y = mul y x. @@ -967,16 +1069,15 @@ Qed. Theorem mul_add_distr_l: forall x y z, mul (add x y) z = add (mul x z) (mul y z). Proof. - destruct x; destruct y; destruct z; simpl; auto. - decEq. apply Int.mul_add_distr_l. + unfold mul, add; intros; destruct Archi.ptr64 eqn:SF, x, y, z; simpl; auto; + rewrite Int.mul_add_distr_l; auto. Qed. - Theorem mul_add_distr_r: forall x y z, mul x (add y z) = add (mul x y) (mul x z). Proof. - destruct x; destruct y; destruct z; simpl; auto. - decEq. apply Int.mul_add_distr_r. + unfold mul, add; intros; destruct Archi.ptr64 eqn:SF, x, y, z; simpl; auto; + rewrite Int.mul_add_distr_r; auto. Qed. Theorem mul_pow2: @@ -1165,6 +1266,144 @@ Proof. intros; destruct x; simpl; auto. decEq. apply Int.rolm_zero. Qed. +Theorem addl_commut: forall x y, addl x y = addl y x. +Proof. + destruct x; destruct y; simpl; auto. + decEq. apply Int64.add_commut. +Qed. + +Theorem addl_assoc: forall x y z, addl (addl x y) z = addl x (addl y z). +Proof. + unfold addl; intros; destruct Archi.ptr64 eqn:SF, x, y, z; simpl; auto. +- rewrite Int64.add_assoc; auto. +- rewrite ! Ptrofs.add_assoc. f_equal. f_equal. + rewrite Ptrofs.add_commut. auto with ptrofs. +- rewrite ! Ptrofs.add_assoc. f_equal. f_equal. + apply Ptrofs.add_commut. +- rewrite ! Ptrofs.add_assoc. f_equal. f_equal. + symmetry. auto with ptrofs. +- rewrite Int64.add_assoc; auto. +Qed. + +Theorem addl_permut: forall x y z, addl x (addl y z) = addl y (addl x z). +Proof. + intros. rewrite (addl_commut y z). rewrite <- addl_assoc. apply addl_commut. +Qed. + +Theorem addl_permut_4: + forall x y z t, addl (addl x y) (addl z t) = addl (addl x z) (addl y t). +Proof. + intros. rewrite addl_permut. rewrite addl_assoc. + rewrite addl_permut. symmetry. apply addl_assoc. +Qed. + +Theorem negl_addl_distr: forall x y, negl(addl x y) = addl (negl x) (negl y). +Proof. + unfold negl, addl; intros; destruct Archi.ptr64 eqn:SF; destruct x; destruct y; simpl; auto; + decEq; apply Int64.neg_add_distr. +Qed. + +Theorem subl_addl_opp: forall x y, subl x (Vlong y) = addl x (Vlong (Int64.neg y)). +Proof. + unfold subl, addl; intros; destruct Archi.ptr64 eqn:SF, x; auto. +- rewrite Int64.sub_add_opp; auto. +- rewrite Ptrofs.sub_add_opp. f_equal. f_equal. symmetry. auto with ptrofs. +- rewrite Int64.sub_add_opp; auto. +Qed. + +Theorem subl_opp_addl: forall x y, subl x (Vlong (Int64.neg y)) = addl x (Vlong y). +Proof. + intros. rewrite subl_addl_opp. rewrite Int64.neg_involutive. auto. +Qed. + +Theorem subl_addl_l: + forall v1 v2 i, subl (addl v1 (Vlong i)) v2 = addl (subl v1 v2) (Vlong i). +Proof. + unfold subl, addl; intros; destruct Archi.ptr64 eqn:SF, v1, v2; auto. +- rewrite Int64.sub_add_l; auto. +- rewrite Ptrofs.sub_add_l; auto. +- destruct (eq_block b b0); auto. + simpl. f_equal. rewrite Ptrofs.sub_add_l. auto with ptrofs. +- rewrite Int64.sub_add_l; auto. +Qed. + +Theorem subl_addl_r: + forall v1 v2 i, subl v1 (addl v2 (Vlong i)) = addl (subl v1 v2) (Vlong (Int64.neg i)). +Proof. + unfold subl, addl; intros; destruct Archi.ptr64 eqn:SF, v1, v2; auto. +- rewrite Int64.add_commut. rewrite Int64.sub_add_r. auto. +- f_equal. replace (Ptrofs.of_int64 (Int64.add i1 i)) with (Ptrofs.add (Ptrofs.of_int64 i) (Ptrofs.of_int64 i1)). + rewrite Ptrofs.sub_add_r. f_equal. + symmetry. auto with ptrofs. + symmetry. rewrite Int64.add_commut. auto with ptrofs. +- destruct (eq_block b b0); auto. + simpl; f_equal. rewrite Ptrofs.add_commut. rewrite Ptrofs.sub_add_r. auto with ptrofs. +- rewrite Int64.add_commut. rewrite Int64.sub_add_r. auto. +Qed. + +Theorem mull_commut: forall x y, mull x y = mull y x. +Proof. + destruct x; destruct y; simpl; auto. decEq. apply Int64.mul_commut. +Qed. + +Theorem mull_assoc: forall x y z, mull (mull x y) z = mull x (mull y z). +Proof. + destruct x; destruct y; destruct z; simpl; auto. + decEq. apply Int64.mul_assoc. +Qed. + +Theorem mull_addl_distr_l: + forall x y z, mull (addl x y) z = addl (mull x z) (mull y z). +Proof. + unfold mull, addl; intros; destruct Archi.ptr64 eqn:SF; destruct x; destruct y; destruct z; simpl; auto; + decEq; apply Int64.mul_add_distr_l. +Qed. + +Theorem mull_addl_distr_r: + forall x y z, mull x (addl y z) = addl (mull x y) (mull x z). +Proof. + unfold mull, addl; intros; destruct Archi.ptr64 eqn:SF; destruct x; destruct y; destruct z; simpl; auto; + decEq; apply Int64.mul_add_distr_r. +Qed. + +Theorem andl_commut: forall x y, andl x y = andl y x. +Proof. + destruct x; destruct y; simpl; auto. decEq. apply Int64.and_commut. +Qed. + +Theorem andl_assoc: forall x y z, andl (andl x y) z = andl x (andl y z). +Proof. + destruct x; destruct y; destruct z; simpl; auto. + decEq. apply Int64.and_assoc. +Qed. + +Theorem orl_commut: forall x y, orl x y = orl y x. +Proof. + destruct x; destruct y; simpl; auto. decEq. apply Int64.or_commut. +Qed. + +Theorem orl_assoc: forall x y z, orl (orl x y) z = orl x (orl y z). +Proof. + destruct x; destruct y; destruct z; simpl; auto. + decEq. apply Int64.or_assoc. +Qed. + +Theorem xorl_commut: forall x y, xorl x y = xorl y x. +Proof. + destruct x; destruct y; simpl; auto. decEq. apply Int64.xor_commut. +Qed. + +Theorem xorl_assoc: forall x y z, xorl (xorl x y) z = xorl x (xorl y z). +Proof. + destruct x; destruct y; destruct z; simpl; auto. + decEq. apply Int64.xor_assoc. +Qed. + +Theorem notl_xorl: forall x, notl x = xorl x (Vlong Int64.mone). +Proof. + destruct x; simpl; auto. +Qed. + Theorem negate_cmp_bool: forall c x y, cmp_bool (negate_comparison c) x y = option_map negb (cmp_bool c x y). Proof. @@ -1177,17 +1416,44 @@ Theorem negate_cmpu_bool: Proof. assert (forall c, cmp_different_blocks (negate_comparison c) = option_map negb (cmp_different_blocks c)). - destruct c; auto. - destruct x; destruct y; simpl; auto. - rewrite Int.negate_cmpu. auto. - destruct (Int.eq i Int.zero && (valid_ptr b (Int.unsigned i0) || valid_ptr b (Int.unsigned i0 - 1))); auto. - destruct (Int.eq i0 Int.zero && (valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1))); auto. - destruct (eq_block b b0). - destruct ((valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1)) && - (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))). - rewrite Int.negate_cmpu. auto. + { destruct c; auto. } + unfold cmpu_bool; intros; destruct Archi.ptr64 eqn:SF, x, y; auto. +- rewrite Int.negate_cmpu. auto. +- rewrite Int.negate_cmpu. auto. +- destruct (Int.eq i Int.zero && (valid_ptr b (Ptrofs.unsigned i0) || valid_ptr b (Ptrofs.unsigned i0 - 1))); auto. +- destruct (Int.eq i0 Int.zero && (valid_ptr b (Ptrofs.unsigned i) || valid_ptr b (Ptrofs.unsigned i - 1))); auto. +- destruct (eq_block b b0). + destruct ((valid_ptr b (Ptrofs.unsigned i) || valid_ptr b (Ptrofs.unsigned i - 1)) && + (valid_ptr b0 (Ptrofs.unsigned i0) || valid_ptr b0 (Ptrofs.unsigned i0 - 1))). + rewrite Ptrofs.negate_cmpu. auto. auto. - destruct (valid_ptr b (Int.unsigned i) && valid_ptr b0 (Int.unsigned i0)); auto. + destruct (valid_ptr b (Ptrofs.unsigned i) && valid_ptr b0 (Ptrofs.unsigned i0)); auto. +Qed. + +Theorem negate_cmpl_bool: + forall c x y, cmpl_bool (negate_comparison c) x y = option_map negb (cmpl_bool c x y). +Proof. + destruct x; destruct y; simpl; auto. rewrite Int64.negate_cmp. auto. +Qed. + +Theorem negate_cmplu_bool: + forall valid_ptr c x y, + cmplu_bool valid_ptr (negate_comparison c) x y = option_map negb (cmplu_bool valid_ptr c x y). +Proof. + assert (forall c, + cmp_different_blocks (negate_comparison c) = option_map negb (cmp_different_blocks c)). + { destruct c; auto. } + unfold cmplu_bool; intros; destruct Archi.ptr64 eqn:SF, x, y; auto. +- rewrite Int64.negate_cmpu. auto. +- simpl. destruct (Int64.eq i Int64.zero && (valid_ptr b (Ptrofs.unsigned i0) || valid_ptr b (Ptrofs.unsigned i0 - 1))); auto. +- simpl. destruct (Int64.eq i0 Int64.zero && (valid_ptr b (Ptrofs.unsigned i) || valid_ptr b (Ptrofs.unsigned i - 1))); auto. +- simpl. destruct (eq_block b b0). + destruct ((valid_ptr b (Ptrofs.unsigned i) || valid_ptr b (Ptrofs.unsigned i - 1)) && + (valid_ptr b0 (Ptrofs.unsigned i0) || valid_ptr b0 (Ptrofs.unsigned i0 - 1))). + rewrite Ptrofs.negate_cmpu. auto. + auto. + destruct (valid_ptr b (Ptrofs.unsigned i) && valid_ptr b0 (Ptrofs.unsigned i0)); auto. +- rewrite Int64.negate_cmpu. auto. Qed. Lemma not_of_optbool: @@ -1223,21 +1489,47 @@ Theorem swap_cmpu_bool: cmpu_bool valid_ptr (swap_comparison c) x y = cmpu_bool valid_ptr c y x. Proof. - assert (forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c). - destruct c; auto. - destruct x; destruct y; simpl; auto. - rewrite Int.swap_cmpu. auto. - destruct (Int.eq i Int.zero && (valid_ptr b (Int.unsigned i0) || valid_ptr b (Int.unsigned i0 - 1))); auto. - destruct (Int.eq i0 Int.zero && (valid_ptr b (Int.unsigned i) || valid_ptr b (Int.unsigned i - 1))); auto. - destruct (eq_block b b0); subst. + assert (E: forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c). + { destruct c; auto. } + intros; unfold cmpu_bool. rewrite ! E. destruct Archi.ptr64 eqn:SF, x, y; auto. +- rewrite Int.swap_cmpu. auto. +- rewrite Int.swap_cmpu. auto. +- destruct (eq_block b b0); subst. + rewrite dec_eq_true. + destruct (valid_ptr b0 (Ptrofs.unsigned i) || valid_ptr b0 (Ptrofs.unsigned i - 1)); + destruct (valid_ptr b0 (Ptrofs.unsigned i0) || valid_ptr b0 (Ptrofs.unsigned i0 - 1)); + simpl; auto. + rewrite Ptrofs.swap_cmpu. auto. + rewrite dec_eq_false by auto. + destruct (valid_ptr b (Ptrofs.unsigned i)); + destruct (valid_ptr b0 (Ptrofs.unsigned i0)); simpl; auto. +Qed. + +Theorem swap_cmpl_bool: + forall c x y, + cmpl_bool (swap_comparison c) x y = cmpl_bool c y x. +Proof. + destruct x; destruct y; simpl; auto. rewrite Int64.swap_cmp. auto. +Qed. + +Theorem swap_cmplu_bool: + forall valid_ptr c x y, + cmplu_bool valid_ptr (swap_comparison c) x y = cmplu_bool valid_ptr c y x. +Proof. + assert (E: forall c, cmp_different_blocks (swap_comparison c) = cmp_different_blocks c). + { destruct c; auto. } + intros; unfold cmplu_bool. rewrite ! E. destruct Archi.ptr64 eqn:SF, x, y; auto. +- rewrite Int64.swap_cmpu. auto. +- destruct (eq_block b b0); subst. rewrite dec_eq_true. - destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1)); - destruct (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1)); + destruct (valid_ptr b0 (Ptrofs.unsigned i) || valid_ptr b0 (Ptrofs.unsigned i - 1)); + destruct (valid_ptr b0 (Ptrofs.unsigned i0) || valid_ptr b0 (Ptrofs.unsigned i0 - 1)); simpl; auto. - rewrite Int.swap_cmpu. auto. + rewrite Ptrofs.swap_cmpu. auto. rewrite dec_eq_false by auto. - destruct (valid_ptr b (Int.unsigned i)); - destruct (valid_ptr b0 (Int.unsigned i0)); simpl; auto. + destruct (valid_ptr b (Ptrofs.unsigned i)); + destruct (valid_ptr b0 (Ptrofs.unsigned i0)); simpl; auto. +- rewrite Int64.swap_cmpu. auto. Qed. Theorem negate_cmpf_eq: @@ -1426,6 +1718,13 @@ Proof. intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto. Qed. +Lemma addl_lessdef: + forall v1 v1' v2 v2', + lessdef v1 v1' -> lessdef v2 v2' -> lessdef (addl v1 v2) (addl v1' v2'). +Proof. + intros. inv H. inv H0. auto. destruct v1'; simpl; auto. simpl; auto. +Qed. + Lemma cmpu_bool_lessdef: forall valid_ptr valid_ptr' c v1 v1' v2 v2' b, (forall b ofs, valid_ptr b ofs = true -> valid_ptr' b ofs = true) -> @@ -1434,23 +1733,60 @@ Lemma cmpu_bool_lessdef: cmpu_bool valid_ptr' c v1' v2' = Some b. Proof. intros. - assert (A: forall b ofs, valid_ptr b ofs || valid_ptr b (ofs - 1) = true -> - valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true). - { intros until ofs. rewrite ! orb_true_iff. intuition. } - destruct v1; simpl in H2; try discriminate; - destruct v2; simpl in H2; try discriminate; - inv H0; inv H1; simpl; auto. - destruct (Int.eq i Int.zero && (valid_ptr b0 (Int.unsigned i0) || valid_ptr b0 (Int.unsigned i0 - 1))) eqn:E; try discriminate. - InvBooleans. rewrite H0, A by auto. auto. - destruct (Int.eq i0 Int.zero && (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1))) eqn:E; try discriminate. - InvBooleans. rewrite H0, A by auto. auto. - destruct (eq_block b0 b1). - destruct (valid_ptr b0 (Int.unsigned i) || valid_ptr b0 (Int.unsigned i - 1)) eqn:?; try discriminate. - destruct (valid_ptr b1 (Int.unsigned i0) || valid_ptr b1 (Int.unsigned i0 - 1)) eqn:?; try discriminate. - erewrite ! A by eauto. auto. - destruct (valid_ptr b0 (Int.unsigned i)) eqn:?; try discriminate. - destruct (valid_ptr b1 (Int.unsigned i0)) eqn:?; try discriminate. - erewrite ! H by eauto. auto. + assert (X: forall b ofs, + valid_ptr b ofs || valid_ptr b (ofs - 1) = true -> + valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true). + { intros. apply orb_true_intro. destruct (orb_prop _ _ H3). + rewrite (H b0 ofs); auto. + rewrite (H b0 (ofs - 1)); auto. } + inv H0; [ | discriminate]. + inv H1; [ | destruct v1'; discriminate ]. + unfold cmpu_bool in *. remember Archi.ptr64 as ptr64. + destruct v1'; auto; destruct v2'; auto; destruct ptr64; auto. +- destruct (Int.eq i Int.zero); auto. + destruct (valid_ptr b0 (Ptrofs.unsigned i0) || valid_ptr b0 (Ptrofs.unsigned i0 - 1)) eqn:A; inv H2. + rewrite X; auto. +- destruct (Int.eq i0 Int.zero); auto. + destruct (valid_ptr b0 (Ptrofs.unsigned i) || valid_ptr b0 (Ptrofs.unsigned i - 1)) eqn:A; inv H2. + rewrite X; auto. +- destruct (eq_block b0 b1). ++ destruct (valid_ptr b0 (Ptrofs.unsigned i) || valid_ptr b0 (Ptrofs.unsigned i - 1)) eqn:A; inv H2. + destruct (valid_ptr b1 (Ptrofs.unsigned i0) || valid_ptr b1 (Ptrofs.unsigned i0 - 1)) eqn:B; inv H1. + rewrite ! X; auto. ++ destruct (valid_ptr b0 (Ptrofs.unsigned i) && valid_ptr b1 (Ptrofs.unsigned i0)) eqn:A; inv H2. + InvBooleans. rewrite ! H; auto. +Qed. + +Lemma cmplu_bool_lessdef: + forall valid_ptr valid_ptr' c v1 v1' v2 v2' b, + (forall b ofs, valid_ptr b ofs = true -> valid_ptr' b ofs = true) -> + lessdef v1 v1' -> lessdef v2 v2' -> + cmplu_bool valid_ptr c v1 v2 = Some b -> + cmplu_bool valid_ptr' c v1' v2' = Some b. +Proof. + intros. + assert (X: forall b ofs, + valid_ptr b ofs || valid_ptr b (ofs - 1) = true -> + valid_ptr' b ofs || valid_ptr' b (ofs - 1) = true). + { intros. apply orb_true_intro. destruct (orb_prop _ _ H3). + rewrite (H b0 ofs); auto. + rewrite (H b0 (ofs - 1)); auto. } + inv H0; [ | discriminate]. + inv H1; [ | destruct v1'; discriminate ]. + unfold cmplu_bool in *. remember Archi.ptr64 as ptr64. + destruct v1'; auto; destruct v2'; auto; destruct ptr64; auto. +- destruct (Int64.eq i Int64.zero); auto. + destruct (valid_ptr b0 (Ptrofs.unsigned i0) || valid_ptr b0 (Ptrofs.unsigned i0 - 1)) eqn:A; inv H2. + rewrite X; auto. +- destruct (Int64.eq i0 Int64.zero); auto. + destruct (valid_ptr b0 (Ptrofs.unsigned i) || valid_ptr b0 (Ptrofs.unsigned i - 1)) eqn:A; inv H2. + rewrite X; auto. +- destruct (eq_block b0 b1). ++ destruct (valid_ptr b0 (Ptrofs.unsigned i) || valid_ptr b0 (Ptrofs.unsigned i - 1)) eqn:A; inv H2. + destruct (valid_ptr b1 (Ptrofs.unsigned i0) || valid_ptr b1 (Ptrofs.unsigned i0 - 1)) eqn:B; inv H1. + rewrite ! X; auto. ++ destruct (valid_ptr b0 (Ptrofs.unsigned i) && valid_ptr b1 (Ptrofs.unsigned i0)) eqn:A; inv H2. + InvBooleans. rewrite ! H; auto. Qed. Lemma of_optbool_lessdef: @@ -1480,6 +1816,18 @@ Proof. intros. inv H; auto. Qed. +Lemma offset_ptr_zero: + forall v, lessdef (offset_ptr v Ptrofs.zero) v. +Proof. + intros. destruct v; simpl; auto. rewrite Ptrofs.add_zero; auto. +Qed. + +Lemma offset_ptr_assoc: + forall v d1 d2, offset_ptr (offset_ptr v d1) d2 = offset_ptr v (Ptrofs.add d1 d2). +Proof. + intros. destruct v; simpl; auto. f_equal. apply Ptrofs.add_assoc. +Qed. + (** * Values and memory injections *) (** A memory injection [f] is a function from addresses to either [None] @@ -1509,7 +1857,7 @@ Inductive inject (mi: meminj): val -> val -> Prop := | inject_ptr: forall b1 ofs1 b2 ofs2 delta, mi b1 = Some (b2, delta) -> - ofs2 = Int.add ofs1 (Int.repr delta) -> + ofs2 = Ptrofs.add ofs1 (Ptrofs.repr delta) -> inject mi (Vptr b1 ofs1) (Vptr b2 ofs2) | val_inject_undef: forall v, inject mi Vundef v. @@ -1525,6 +1873,14 @@ Inductive inject_list (mi: meminj): list val -> list val-> Prop:= Hint Resolve inject_list_nil inject_list_cons. +Lemma inject_ptrofs: + forall mi i, inject mi (Vptrofs i) (Vptrofs i). +Proof. + unfold Vptrofs; intros. destruct Archi.ptr64; auto. +Qed. + +Hint Resolve inject_ptrofs. + Section VAL_INJ_OPS. Variable f: meminj. @@ -1534,7 +1890,7 @@ Lemma load_result_inject: inject f v1 v2 -> inject f (Val.load_result chunk v1) (Val.load_result chunk v2). Proof. - intros. inv H; destruct chunk; simpl; econstructor; eauto. + intros. inv H; destruct chunk; simpl; try constructor; destruct Archi.ptr64; econstructor; eauto. Qed. Remark add_inject: @@ -1543,9 +1899,13 @@ Remark add_inject: inject f v2 v2' -> inject f (Val.add v1 v2) (Val.add v1' v2'). Proof. - intros. inv H; inv H0; simpl; econstructor; eauto. - repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + intros. unfold Val.add. destruct Archi.ptr64 eqn:SF. +- inv H; inv H0; constructor. +- inv H; inv H0; simpl; auto. ++ econstructor; eauto. + rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. ++ econstructor; eauto. + rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. Qed. Remark sub_inject: @@ -1554,10 +1914,52 @@ Remark sub_inject: inject f v2 v2' -> inject f (Val.sub v1 v2) (Val.sub v1' v2'). Proof. - intros. inv H; inv H0; simpl; auto. - econstructor; eauto. rewrite Int.sub_add_l. auto. - destruct (eq_block b1 b0); auto. subst. rewrite H1 in H. inv H. rewrite dec_eq_true. - rewrite Int.sub_shifted. auto. + intros. unfold Val.sub. destruct Archi.ptr64 eqn:SF. +- inv H; inv H0; constructor. +- inv H; inv H0; simpl; auto. ++ econstructor; eauto. + rewrite Ptrofs.sub_add_l. auto. ++ destruct (eq_block b1 b0); auto. + subst. rewrite H1 in H. inv H. rewrite dec_eq_true. + rewrite Ptrofs.sub_shifted. auto. +Qed. + +Remark addl_inject: + forall v1 v1' v2 v2', + inject f v1 v1' -> + inject f v2 v2' -> + inject f (Val.addl v1 v2) (Val.addl v1' v2'). +Proof. + intros. unfold Val.addl. destruct Archi.ptr64 eqn:SF. +- inv H; inv H0; simpl; auto. ++ econstructor; eauto. + rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. ++ econstructor; eauto. + rewrite ! Ptrofs.add_assoc. decEq. apply Ptrofs.add_commut. +- inv H; inv H0; constructor. +Qed. + +Remark subl_inject: + forall v1 v1' v2 v2', + inject f v1 v1' -> + inject f v2 v2' -> + inject f (Val.subl v1 v2) (Val.subl v1' v2'). +Proof. + intros. unfold Val.subl. destruct Archi.ptr64 eqn:SF. +- inv H; inv H0; simpl; auto. ++ econstructor; eauto. + rewrite Ptrofs.sub_add_l. auto. ++ destruct (eq_block b1 b0); auto. + subst. rewrite H1 in H. inv H. rewrite dec_eq_true. + rewrite Ptrofs.sub_shifted. auto. +- inv H; inv H0; constructor. +Qed. + +Lemma offset_ptr_inject: + forall v v' ofs, inject f v v' -> inject f (offset_ptr v ofs) (offset_ptr v' ofs). +Proof. + intros. inv H; simpl; econstructor; eauto. + rewrite ! Ptrofs.add_assoc. f_equal. apply Ptrofs.add_commut. Qed. Lemma cmp_bool_inject: @@ -1578,30 +1980,30 @@ Let weak_valid_ptr2 b ofs := valid_ptr2 b ofs || valid_ptr2 b (ofs - 1). Hypothesis valid_ptr_inj: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - valid_ptr1 b1 (Int.unsigned ofs) = true -> - valid_ptr2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + valid_ptr1 b1 (Ptrofs.unsigned ofs) = true -> + valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Hypothesis weak_valid_ptr_inj: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - weak_valid_ptr1 b1 (Int.unsigned ofs) = true -> - weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + weak_valid_ptr1 b1 (Ptrofs.unsigned ofs) = true -> + weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Hypothesis weak_valid_ptr_no_overflow: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - weak_valid_ptr1 b1 (Int.unsigned ofs) = true -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + weak_valid_ptr1 b1 (Ptrofs.unsigned ofs) = true -> + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Hypothesis valid_different_ptrs_inj: forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, b1 <> b2 -> - valid_ptr1 b1 (Int.unsigned ofs1) = true -> - valid_ptr1 b2 (Int.unsigned ofs2) = true -> + valid_ptr1 b1 (Ptrofs.unsigned ofs1) = true -> + valid_ptr1 b2 (Ptrofs.unsigned ofs2) = true -> f b1 = Some (b1', delta1) -> f b2 = Some (b2', delta2) -> b1' <> b2' \/ - Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)). + Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)). Lemma cmpu_bool_inject: forall c v1 v2 v1' v2' b, @@ -1610,38 +2012,84 @@ Lemma cmpu_bool_inject: Val.cmpu_bool valid_ptr1 c v1 v2 = Some b -> Val.cmpu_bool valid_ptr2 c v1' v2' = Some b. Proof. - Local Opaque Int.add. - intros. inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto. -- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1. - fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))). + Local Opaque Int.add Ptrofs.add. + intros. + unfold cmpu_bool in *; destruct Archi.ptr64; + inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto. +- fold (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) in H1. + fold (weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))). destruct (Int.eq i Int.zero); auto. - destruct (weak_valid_ptr1 b1 (Int.unsigned ofs1)) eqn:E; try discriminate. + destruct (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) eqn:E; try discriminate. erewrite weak_valid_ptr_inj by eauto. auto. -- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1. - fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))). +- fold (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) in H1. + fold (weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))). destruct (Int.eq i Int.zero); auto. - destruct (weak_valid_ptr1 b1 (Int.unsigned ofs1)) eqn:E; try discriminate. + destruct (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) eqn:E; try discriminate. + erewrite weak_valid_ptr_inj by eauto. auto. +- fold (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) in H1. + fold (weak_valid_ptr1 b0 (Ptrofs.unsigned ofs0)) in H1. + fold (weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))). + fold (weak_valid_ptr2 b3 (Ptrofs.unsigned (Ptrofs.add ofs0 (Ptrofs.repr delta0)))). + destruct (eq_block b1 b0); subst. + rewrite H in H2. inv H2. rewrite dec_eq_true. + destruct (weak_valid_ptr1 b0 (Ptrofs.unsigned ofs1)) eqn:?; try discriminate. + destruct (weak_valid_ptr1 b0 (Ptrofs.unsigned ofs0)) eqn:?; try discriminate. + erewrite !weak_valid_ptr_inj by eauto. simpl. + rewrite <-H1. simpl. decEq. apply Ptrofs.translate_cmpu; eauto. + destruct (valid_ptr1 b1 (Ptrofs.unsigned ofs1)) eqn:?; try discriminate. + destruct (valid_ptr1 b0 (Ptrofs.unsigned ofs0)) eqn:?; try discriminate. + destruct (eq_block b2 b3); subst. + assert (valid_ptr_implies: forall b ofs, valid_ptr1 b ofs = true -> weak_valid_ptr1 b ofs = true). + intros. unfold weak_valid_ptr1. rewrite H0; auto. + erewrite !weak_valid_ptr_inj by eauto using valid_ptr_implies. simpl. + exploit valid_different_ptrs_inj; eauto. intros [?|?]; [congruence |]. + destruct c; simpl in H1; inv H1. + simpl; decEq. rewrite Ptrofs.eq_false; auto. congruence. + simpl; decEq. rewrite Ptrofs.eq_false; auto. congruence. + now erewrite !valid_ptr_inj by eauto. +Qed. + +Lemma cmplu_bool_inject: + forall c v1 v2 v1' v2' b, + inject f v1 v1' -> + inject f v2 v2' -> + Val.cmplu_bool valid_ptr1 c v1 v2 = Some b -> + Val.cmplu_bool valid_ptr2 c v1' v2' = Some b. +Proof. + Local Opaque Int64.add Ptrofs.add. + intros. + unfold cmplu_bool in *; destruct Archi.ptr64; + inv H; simpl in H1; try discriminate; inv H0; simpl in H1; try discriminate; simpl; auto. +- fold (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) in H1. + fold (weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))). + destruct (Int64.eq i Int64.zero); auto. + destruct (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) eqn:E; try discriminate. + erewrite weak_valid_ptr_inj by eauto. auto. +- fold (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) in H1. + fold (weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))). + destruct (Int64.eq i Int64.zero); auto. + destruct (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) eqn:E; try discriminate. erewrite weak_valid_ptr_inj by eauto. auto. -- fold (weak_valid_ptr1 b1 (Int.unsigned ofs1)) in H1. - fold (weak_valid_ptr1 b0 (Int.unsigned ofs0)) in H1. - fold (weak_valid_ptr2 b2 (Int.unsigned (Int.add ofs1 (Int.repr delta)))). - fold (weak_valid_ptr2 b3 (Int.unsigned (Int.add ofs0 (Int.repr delta0)))). +- fold (weak_valid_ptr1 b1 (Ptrofs.unsigned ofs1)) in H1. + fold (weak_valid_ptr1 b0 (Ptrofs.unsigned ofs0)) in H1. + fold (weak_valid_ptr2 b2 (Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)))). + fold (weak_valid_ptr2 b3 (Ptrofs.unsigned (Ptrofs.add ofs0 (Ptrofs.repr delta0)))). destruct (eq_block b1 b0); subst. rewrite H in H2. inv H2. rewrite dec_eq_true. - destruct (weak_valid_ptr1 b0 (Int.unsigned ofs1)) eqn:?; try discriminate. - destruct (weak_valid_ptr1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate. + destruct (weak_valid_ptr1 b0 (Ptrofs.unsigned ofs1)) eqn:?; try discriminate. + destruct (weak_valid_ptr1 b0 (Ptrofs.unsigned ofs0)) eqn:?; try discriminate. erewrite !weak_valid_ptr_inj by eauto. simpl. - rewrite <-H1. simpl. decEq. apply Int.translate_cmpu; eauto. - destruct (valid_ptr1 b1 (Int.unsigned ofs1)) eqn:?; try discriminate. - destruct (valid_ptr1 b0 (Int.unsigned ofs0)) eqn:?; try discriminate. + rewrite <-H1. simpl. decEq. apply Ptrofs.translate_cmpu; eauto. + destruct (valid_ptr1 b1 (Ptrofs.unsigned ofs1)) eqn:?; try discriminate. + destruct (valid_ptr1 b0 (Ptrofs.unsigned ofs0)) eqn:?; try discriminate. destruct (eq_block b2 b3); subst. assert (valid_ptr_implies: forall b ofs, valid_ptr1 b ofs = true -> weak_valid_ptr1 b ofs = true). intros. unfold weak_valid_ptr1. rewrite H0; auto. erewrite !weak_valid_ptr_inj by eauto using valid_ptr_implies. simpl. exploit valid_different_ptrs_inj; eauto. intros [?|?]; [congruence |]. destruct c; simpl in H1; inv H1. - simpl; decEq. rewrite Int.eq_false; auto. congruence. - simpl; decEq. rewrite Int.eq_false; auto. congruence. + simpl; decEq. rewrite Ptrofs.eq_false; auto. congruence. + simpl; decEq. rewrite Ptrofs.eq_false; auto. congruence. now erewrite !valid_ptr_inj by eauto. Qed. @@ -1710,8 +2158,8 @@ Lemma val_inject_lessdef: forall v1 v2, Val.lessdef v1 v2 <-> Val.inject (fun b => Some(b, 0)) v1 v2. Proof. intros; split; intros. - inv H; auto. destruct v2; econstructor; eauto. rewrite Int.add_zero; auto. - inv H; auto. inv H0. rewrite Int.add_zero; auto. + inv H; auto. destruct v2; econstructor; eauto. rewrite Ptrofs.add_zero; auto. + inv H; auto. inv H0. rewrite Ptrofs.add_zero; auto. Qed. Lemma val_inject_list_lessdef: @@ -1732,8 +2180,8 @@ Lemma val_inject_id: Proof. intros; split; intros. inv H; auto. - unfold inject_id in H0. inv H0. rewrite Int.add_zero. constructor. - inv H. destruct v2; econstructor. unfold inject_id; reflexivity. rewrite Int.add_zero; auto. + unfold inject_id in H0. inv H0. rewrite Ptrofs.add_zero. constructor. + inv H. destruct v2; econstructor. unfold inject_id; reflexivity. rewrite Ptrofs.add_zero; auto. constructor. Qed. @@ -1757,5 +2205,5 @@ Lemma val_inject_compose: Proof. intros. inv H; auto; inv H0; auto. econstructor. unfold compose_meminj; rewrite H1; rewrite H3; eauto. - rewrite Int.add_assoc. decEq. unfold Int.add. apply Int.eqm_samerepr. auto with ints. + rewrite Ptrofs.add_assoc. decEq. unfold Ptrofs.add. apply Ptrofs.eqm_samerepr. auto with ints. Qed. -- cgit