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. --- backend/Stackingproof.v | 180 +++++++++++++++++++++++++----------------------- 1 file changed, 95 insertions(+), 85 deletions(-) (limited to 'backend/Stackingproof.v') diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 0e9c58b3..d8d916de 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -67,12 +67,14 @@ Lemma load_result_inject: forall j ty v v', Val.inject j v v' -> Val.has_type v ty -> Val.inject j v (Val.load_result (chunk_of_type ty) v'). Proof. - destruct 1; intros; auto; destruct ty; simpl; try contradiction; econstructor; eauto. + intros until v'; unfold Val.has_type, Val.load_result; destruct Archi.ptr64; + destruct 1; intros; auto; destruct ty; simpl; + try contradiction; try discriminate; econstructor; eauto. Qed. Section PRESERVATION. -Variable return_address_offset: Mach.function -> Mach.code -> int -> Prop. +Variable return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop. Hypothesis return_address_offset_exists: forall f sg ros c, @@ -100,12 +102,12 @@ Lemma unfold_transf_function: f.(Linear.fn_sig) (transl_body f fe) fe.(fe_size) - (Int.repr fe.(fe_ofs_link)) - (Int.repr fe.(fe_ofs_retaddr)). + (Ptrofs.repr fe.(fe_ofs_link)) + (Ptrofs.repr fe.(fe_ofs_retaddr)). Proof. generalize TRANSF_F. unfold transf_function. destruct (wt_function f); simpl negb. - destruct (zlt Int.max_unsigned (fe_size (make_env (function_bounds f)))). + destruct (zlt Ptrofs.max_unsigned (fe_size (make_env (function_bounds f)))). intros; discriminate. intros. unfold fe. unfold b. congruence. intros; discriminate. @@ -118,11 +120,11 @@ Proof. destruct (wt_function f); simpl negb. auto. intros; discriminate. Qed. -Lemma size_no_overflow: fe.(fe_size) <= Int.max_unsigned. +Lemma size_no_overflow: fe.(fe_size) <= Ptrofs.max_unsigned. Proof. generalize TRANSF_F. unfold transf_function. destruct (wt_function f); simpl negb. - destruct (zlt Int.max_unsigned (fe_size (make_env (function_bounds f)))). + destruct (zlt Ptrofs.max_unsigned (fe_size (make_env (function_bounds f)))). intros; discriminate. intros. unfold fe. unfold b. omega. intros; discriminate. @@ -143,18 +145,18 @@ Local Opaque Z.add Z.mul Z.divide. Lemma contains_get_stack: forall spec m ty sp ofs, m |= contains (chunk_of_type ty) sp ofs spec -> - exists v, load_stack m (Vptr sp Int.zero) ty (Int.repr ofs) = Some v /\ spec v. + exists v, load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr ofs) = Some v /\ spec v. Proof. intros. unfold load_stack. - replace (Val.add (Vptr sp Int.zero) (Vint (Int.repr ofs))) with (Vptr sp (Int.repr ofs)). + replace (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) with (Vptr sp (Ptrofs.repr ofs)). eapply loadv_rule; eauto. - simpl. rewrite Int.add_zero_l; auto. + simpl. rewrite Ptrofs.add_zero_l; auto. Qed. Lemma hasvalue_get_stack: forall ty m sp ofs v, m |= hasvalue (chunk_of_type ty) sp ofs v -> - load_stack m (Vptr sp Int.zero) ty (Int.repr ofs) = Some v. + load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr ofs) = Some v. Proof. intros. exploit contains_get_stack; eauto. intros (v' & A & B). congruence. Qed. @@ -164,13 +166,13 @@ Lemma contains_set_stack: m |= contains (chunk_of_type ty) sp ofs spec1 ** P -> spec (Val.load_result (chunk_of_type ty) v) -> exists m', - store_stack m (Vptr sp Int.zero) ty (Int.repr ofs) v = Some m' + store_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr ofs) v = Some m' /\ m' |= contains (chunk_of_type ty) sp ofs spec ** P. Proof. intros. unfold store_stack. - replace (Val.add (Vptr sp Int.zero) (Vint (Int.repr ofs))) with (Vptr sp (Int.repr ofs)). + replace (Val.offset_ptr (Vptr sp Ptrofs.zero) (Ptrofs.repr ofs)) with (Vptr sp (Ptrofs.repr ofs)). eapply storev_rule; eauto. - simpl. rewrite Int.add_zero_l; auto. + simpl. rewrite Ptrofs.add_zero_l; auto. Qed. (** [contains_locations j sp pos bound sl ls] is a separation logic assertion @@ -184,7 +186,7 @@ Qed. Program Definition contains_locations (j: meminj) (sp: block) (pos bound: Z) (sl: slot) (ls: locset) : massert := {| m_pred := fun m => - (8 | pos) /\ 0 <= pos /\ pos + 4 * bound <= Int.modulus /\ + (8 | pos) /\ 0 <= pos /\ pos + 4 * bound <= Ptrofs.modulus /\ Mem.range_perm m sp pos (pos + 4 * bound) Cur Freeable /\ forall ofs ty, 0 <= ofs -> ofs + typesize ty <= bound -> (typealign ty | ofs) -> exists v, Mem.load (chunk_of_type ty) m sp (pos + 4 * ofs) = Some v @@ -225,13 +227,13 @@ Lemma get_location: m |= contains_locations j sp pos bound sl ls -> 0 <= ofs -> ofs + typesize ty <= bound -> (typealign ty | ofs) -> exists v, - load_stack m (Vptr sp Int.zero) ty (Int.repr (pos + 4 * ofs)) = Some v + load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (pos + 4 * ofs)) = Some v /\ Val.inject j (ls (S sl ofs ty)) v. Proof. intros. destruct H as (D & E & F & G & H). exploit H; eauto. intros (v & U & V). exists v; split; auto. - unfold load_stack; simpl. rewrite Int.add_zero_l, Int.unsigned_repr; auto. - unfold Int.max_unsigned. generalize (typesize_pos ty). omega. + unfold load_stack; simpl. rewrite Ptrofs.add_zero_l, Ptrofs.unsigned_repr; auto. + unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). omega. Qed. Lemma set_location: @@ -240,7 +242,7 @@ Lemma set_location: 0 <= ofs -> ofs + typesize ty <= bound -> (typealign ty | ofs) -> Val.inject j v v' -> exists m', - store_stack m (Vptr sp Int.zero) ty (Int.repr (pos + 4 * ofs)) v' = Some m' + store_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (pos + 4 * ofs)) v' = Some m' /\ m' |= contains_locations j sp pos bound sl (Locmap.set (S sl ofs ty) v ls) ** P. Proof. intros. destruct H as (A & B & C). destruct A as (D & E & F & G & H). @@ -249,8 +251,8 @@ Proof. assert (PERM: Mem.range_perm m' sp pos (pos + 4 * bound) Cur Freeable). { red; intros; eauto with mem. } exists m'; split. -- unfold store_stack; simpl. rewrite Int.add_zero_l, Int.unsigned_repr; eauto. - unfold Int.max_unsigned. generalize (typesize_pos ty). omega. +- unfold store_stack; simpl. rewrite Ptrofs.add_zero_l, Ptrofs.unsigned_repr; eauto. + unfold Ptrofs.max_unsigned. generalize (typesize_pos ty). omega. - simpl. intuition auto. + unfold Locmap.set. destruct (Loc.eq (S sl ofs ty) (S sl ofs0 ty0)); [|destruct (Loc.diff_dec (S sl ofs ty) (S sl ofs0 ty0))]. @@ -258,7 +260,7 @@ Proof. inv e. rename ofs0 into ofs. rename ty0 into ty. exists (Val.load_result (chunk_of_type ty) v'); split. eapply Mem.load_store_similar_2; eauto. omega. - inv H3; destruct (chunk_of_type ty); simpl; econstructor; eauto. + apply Val.load_result_inject; auto. * (* different locations *) exploit H; eauto. intros (v0 & X & Y). exists v0; split; auto. rewrite <- X; eapply Mem.load_store_other; eauto. @@ -366,8 +368,8 @@ represents the Linear stack data. *) Definition frame_contents_1 (j: meminj) (sp: block) (ls ls0: locset) (parent retaddr: val) := contains_locations j sp fe.(fe_ofs_local) b.(bound_local) Local ls ** contains_locations j sp fe_ofs_arg b.(bound_outgoing) Outgoing ls - ** hasvalue Mint32 sp fe.(fe_ofs_link) parent - ** hasvalue Mint32 sp fe.(fe_ofs_retaddr) retaddr + ** hasvalue Mptr sp fe.(fe_ofs_link) parent + ** hasvalue Mptr sp fe.(fe_ofs_retaddr) retaddr ** contains_callee_saves j sp fe.(fe_ofs_callee_save) b.(used_callee_save) ls0. Definition frame_contents (j: meminj) (sp: block) (ls ls0: locset) (parent retaddr: val) := @@ -382,7 +384,7 @@ Lemma frame_get_local: m |= frame_contents j sp ls ls0 parent retaddr ** P -> slot_within_bounds b Local ofs ty -> slot_valid f Local ofs ty = true -> exists v, - load_stack m (Vptr sp Int.zero) ty (Int.repr (offset_local fe ofs)) = Some v + load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (offset_local fe ofs)) = Some v /\ Val.inject j (ls (S Local ofs ty)) v. Proof. unfold frame_contents, frame_contents_1; intros. unfold slot_valid in H1; InvBooleans. @@ -395,7 +397,7 @@ Lemma frame_get_outgoing: m |= frame_contents j sp ls ls0 parent retaddr ** P -> slot_within_bounds b Outgoing ofs ty -> slot_valid f Outgoing ofs ty = true -> exists v, - load_stack m (Vptr sp Int.zero) ty (Int.repr (offset_arg ofs)) = Some v + load_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (offset_arg ofs)) = Some v /\ Val.inject j (ls (S Outgoing ofs ty)) v. Proof. unfold frame_contents, frame_contents_1; intros. unfold slot_valid in H1; InvBooleans. @@ -406,20 +408,20 @@ Qed. Lemma frame_get_parent: forall j sp ls ls0 parent retaddr m P, m |= frame_contents j sp ls ls0 parent retaddr ** P -> - load_stack m (Vptr sp Int.zero) Tint (Int.repr fe.(fe_ofs_link)) = Some parent. + load_stack m (Vptr sp Ptrofs.zero) Tptr (Ptrofs.repr fe.(fe_ofs_link)) = Some parent. Proof. unfold frame_contents, frame_contents_1; intros. - apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_pick3 in H. + apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_pick3 in H. rewrite <- chunk_of_Tptr in H. eapply hasvalue_get_stack; eauto. Qed. Lemma frame_get_retaddr: forall j sp ls ls0 parent retaddr m P, m |= frame_contents j sp ls ls0 parent retaddr ** P -> - load_stack m (Vptr sp Int.zero) Tint (Int.repr fe.(fe_ofs_retaddr)) = Some retaddr. + load_stack m (Vptr sp Ptrofs.zero) Tptr (Ptrofs.repr fe.(fe_ofs_retaddr)) = Some retaddr. Proof. unfold frame_contents, frame_contents_1; intros. - apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_pick4 in H. + apply mconj_proj1 in H. apply sep_proj1 in H. apply sep_pick4 in H. rewrite <- chunk_of_Tptr in H. eapply hasvalue_get_stack; eauto. Qed. @@ -431,7 +433,7 @@ Lemma frame_set_local: slot_within_bounds b Local ofs ty -> slot_valid f Local ofs ty = true -> Val.inject j v v' -> exists m', - store_stack m (Vptr sp Int.zero) ty (Int.repr (offset_local fe ofs)) v' = Some m' + store_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (offset_local fe ofs)) v' = Some m' /\ m' |= frame_contents j sp (Locmap.set (S Local ofs ty) v ls) ls0 parent retaddr ** P. Proof. intros. unfold frame_contents in H. @@ -456,7 +458,7 @@ Lemma frame_set_outgoing: slot_within_bounds b Outgoing ofs ty -> slot_valid f Outgoing ofs ty = true -> Val.inject j v v' -> exists m', - store_stack m (Vptr sp Int.zero) ty (Int.repr (offset_arg ofs)) v' = Some m' + store_stack m (Vptr sp Ptrofs.zero) ty (Ptrofs.repr (offset_arg ofs)) v' = Some m' /\ m' |= frame_contents j sp (Locmap.set (S Outgoing ofs ty) v ls) ls0 parent retaddr ** P. Proof. intros. unfold frame_contents in H. @@ -855,7 +857,8 @@ Qed. Remark destroyed_by_store_caller_save: forall chunk addr, no_callee_saves (destroyed_by_store chunk addr). Proof. - unfold no_callee_saves; destruct chunk; reflexivity. +Local Transparent destroyed_by_store. + unfold no_callee_saves, destroyed_by_store; intros; destruct chunk; try reflexivity; destruct Archi.ptr64; reflexivity. Qed. Remark destroyed_by_cond_caller_save: @@ -939,12 +942,13 @@ Lemma save_callee_save_rec_correct: agree_regs j ls rs -> exists rs', exists m', star step tge - (State cs fb (Vptr sp Int.zero) (save_callee_save_rec l pos k) rs m) - E0 (State cs fb (Vptr sp Int.zero) k rs' m') + (State cs fb (Vptr sp Ptrofs.zero) (save_callee_save_rec l pos k) rs m) + E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m') /\ m' |= contains_callee_saves j sp pos l ls ** P /\ (forall ofs k p, Mem.perm m sp ofs k p -> Mem.perm m' sp ofs k p) /\ agree_regs j ls rs'. Proof. +Local Opaque mreg_type. induction l as [ | r l]; simpl; intros until P; intros CS SEP AG. - exists rs, m. split. apply star_refl. @@ -1029,8 +1033,8 @@ Lemma save_callee_save_correct: let rs1 := undef_regs destroyed_at_function_entry rs in exists rs', exists m', star step tge - (State cs fb (Vptr sp Int.zero) (save_callee_save fe k) rs1 m) - E0 (State cs fb (Vptr sp Int.zero) k rs' m') + (State cs fb (Vptr sp Ptrofs.zero) (save_callee_save fe k) rs1 m) + E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m') /\ m' |= contains_callee_saves j sp fe.(fe_ofs_callee_save) b.(used_callee_save) ls0 ** P /\ (forall ofs k p, Mem.perm m sp ofs k p -> Mem.perm m' sp ofs k p) /\ agree_regs j ls1 rs'. @@ -1071,15 +1075,15 @@ Lemma function_prologue_correct: ls1 = LTL.undef_regs destroyed_at_function_entry (LTL.call_regs ls) -> rs1 = undef_regs destroyed_at_function_entry rs -> Mem.alloc m1 0 f.(Linear.fn_stacksize) = (m2, sp) -> - Val.has_type parent Tint -> Val.has_type ra Tint -> + Val.has_type parent Tptr -> Val.has_type ra Tptr -> m1' |= minjection j m1 ** globalenv_inject ge j ** P -> exists j', exists rs', exists m2', exists sp', exists m3', exists m4', exists m5', Mem.alloc m1' 0 tf.(fn_stacksize) = (m2', sp') - /\ store_stack m2' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) parent = Some m3' - /\ store_stack m3' (Vptr sp' Int.zero) Tint tf.(fn_retaddr_ofs) ra = Some m4' + /\ store_stack m2' (Vptr sp' Ptrofs.zero) Tptr tf.(fn_link_ofs) parent = Some m3' + /\ store_stack m3' (Vptr sp' Ptrofs.zero) Tptr tf.(fn_retaddr_ofs) ra = Some m4' /\ star step tge - (State cs fb (Vptr sp' Int.zero) (save_callee_save fe k) rs1 m4') - E0 (State cs fb (Vptr sp' Int.zero) k rs' m5') + (State cs fb (Vptr sp' Ptrofs.zero) (save_callee_save fe k) rs1 m4') + E0 (State cs fb (Vptr sp' Ptrofs.zero) k rs' m5') /\ agree_regs j' ls1 rs' /\ agree_locs ls1 ls0 /\ m5' |= frame_contents j' sp' ls1 ls0 parent ra ** minjection j' m2 ** globalenv_inject ge j' ** P @@ -1113,17 +1117,17 @@ Local Opaque b fe. (* Dividing up the frame *) apply (frame_env_separated b) in SEP. replace (make_env b) with fe in SEP by auto. (* Store of parent *) - rewrite sep_swap3 in SEP. - apply (range_contains Mint32) in SEP; [|tauto]. - exploit (contains_set_stack (fun v' => v' = parent) parent (fun _ => True) m2' Tint). - eexact SEP. apply Val.load_result_same; auto. + rewrite sep_swap3 in SEP. + apply (range_contains Mptr) in SEP; [|tauto]. + exploit (contains_set_stack (fun v' => v' = parent) parent (fun _ => True) m2' Tptr). + rewrite chunk_of_Tptr; eexact SEP. apply Val.load_result_same; auto. clear SEP; intros (m3' & STORE_PARENT & SEP). rewrite sep_swap3 in SEP. (* Store of return address *) rewrite sep_swap4 in SEP. - apply (range_contains Mint32) in SEP; [|tauto]. - exploit (contains_set_stack (fun v' => v' = ra) ra (fun _ => True) m3' Tint). - eexact SEP. apply Val.load_result_same; auto. + apply (range_contains Mptr) in SEP; [|tauto]. + exploit (contains_set_stack (fun v' => v' = ra) ra (fun _ => True) m3' Tptr). + rewrite chunk_of_Tptr; eexact SEP. apply Val.load_result_same; auto. clear SEP; intros (m4' & STORE_RETADDR & SEP). rewrite sep_swap4 in SEP. (* Saving callee-save registers *) @@ -1147,7 +1151,8 @@ Local Opaque b fe. rewrite sep_swap in SEP. (* Now we frame this *) assert (SEPFINAL: m5' |= frame_contents j' sp' ls1 ls0 parent ra ** minjection j' m2 ** globalenv_inject ge j' ** P). - { eapply frame_mconj. eexact SEPCONJ. + { eapply frame_mconj. eexact SEPCONJ. + rewrite chunk_of_Tptr in SEP. unfold frame_contents_1; rewrite ! sep_assoc. exact SEP. assert (forall ofs k p, Mem.perm m2' sp' ofs k p -> Mem.perm m5' sp' ofs k p). { intros. apply PERMS. @@ -1198,12 +1203,13 @@ Lemma restore_callee_save_rec_correct: (forall r, In r l -> mreg_within_bounds b r) -> exists rs', star step tge - (State cs fb (Vptr sp Int.zero) (restore_callee_save_rec l ofs k) rs m) - E0 (State cs fb (Vptr sp Int.zero) k rs' m) + (State cs fb (Vptr sp Ptrofs.zero) (restore_callee_save_rec l ofs k) rs m) + E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m) /\ (forall r, In r l -> Val.inject j (ls0 (R r)) (rs' r)) /\ (forall r, ~(In r l) -> rs' r = rs r) /\ agree_unused ls0 rs'. Proof. +Local Opaque mreg_type. induction l as [ | r l]; simpl; intros. - (* base case *) exists rs. intuition auto. apply star_refl. @@ -1242,8 +1248,8 @@ Lemma restore_callee_save_correct: agree_unused j ls0 rs -> exists rs', star step tge - (State cs fb (Vptr sp Int.zero) (restore_callee_save fe k) rs m) - E0 (State cs fb (Vptr sp Int.zero) k rs' m) + (State cs fb (Vptr sp Ptrofs.zero) (restore_callee_save fe k) rs m) + E0 (State cs fb (Vptr sp Ptrofs.zero) k rs' m) /\ (forall r, is_callee_save r = true -> Val.inject j (ls0 (R r)) (rs' r)) /\ (forall r, @@ -1277,12 +1283,12 @@ Lemma function_epilogue_correct: j sp = Some(sp', fe.(fe_stack_data)) -> Mem.free m sp 0 f.(Linear.fn_stacksize) = Some m1 -> exists rs1, exists m1', - load_stack m' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) = Some pa - /\ load_stack m' (Vptr sp' Int.zero) Tint tf.(fn_retaddr_ofs) = Some ra + load_stack m' (Vptr sp' Ptrofs.zero) Tptr tf.(fn_link_ofs) = Some pa + /\ load_stack m' (Vptr sp' Ptrofs.zero) Tptr tf.(fn_retaddr_ofs) = Some ra /\ Mem.free m' sp' 0 tf.(fn_stacksize) = Some m1' /\ star step tge - (State cs fb (Vptr sp' Int.zero) (restore_callee_save fe k) rs m') - E0 (State cs fb (Vptr sp' Int.zero) k rs1 m') + (State cs fb (Vptr sp' Ptrofs.zero) (restore_callee_save fe k) rs m') + E0 (State cs fb (Vptr sp' Ptrofs.zero) k rs1 m') /\ agree_regs j (return_regs ls0 ls) rs1 /\ agree_callee_save (return_regs ls0 ls) ls0 /\ m1' |= minjection j m1 ** P. @@ -1304,8 +1310,8 @@ Proof. (* Reloading the back link and return address *) unfold frame_contents in SEP; apply mconj_proj1 in SEP. unfold frame_contents_1 in SEP; rewrite ! sep_assoc in SEP. - exploit (hasvalue_get_stack Tint). eapply sep_pick3; eexact SEP. intros LOAD_LINK. - exploit (hasvalue_get_stack Tint). eapply sep_pick4; eexact SEP. intros LOAD_RETADDR. + exploit (hasvalue_get_stack Tptr). rewrite chunk_of_Tptr. eapply sep_pick3; eexact SEP. intros LOAD_LINK. + exploit (hasvalue_get_stack Tptr). rewrite chunk_of_Tptr. eapply sep_pick4; eexact SEP. intros LOAD_RETADDR. clear SEP. (* Conclusions *) rewrite unfold_transf_function; simpl. @@ -1353,15 +1359,15 @@ Inductive match_stacks (j: meminj): (TRF: transf_function f = OK trf) (TRC: transl_code (make_env (function_bounds f)) c = c') (INJ: j sp = Some(sp', (fe_stack_data (make_env (function_bounds f))))) - (TY_RA: Val.has_type ra Tint) + (TY_RA: Val.has_type ra Tptr) (AGL: agree_locs f ls (parent_locset cs)) (ARGS: forall ofs ty, In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments sg)) -> slot_within_bounds (function_bounds f) Outgoing ofs ty) (STK: match_stacks j cs cs' (Linear.fn_sig f)), match_stacks j - (Linear.Stackframe f (Vptr sp Int.zero) ls c :: cs) - (Stackframe fb (Vptr sp' Int.zero) ra c' :: cs') + (Linear.Stackframe f (Vptr sp Ptrofs.zero) ls c :: cs) + (Stackframe fb (Vptr sp' Ptrofs.zero) ra c' :: cs') sg. (** Invariance with respect to change of memory injection. *) @@ -1409,17 +1415,17 @@ Qed. Lemma match_stacks_type_sp: forall j cs cs' sg, match_stacks j cs cs' sg -> - Val.has_type (parent_sp cs') Tint. + Val.has_type (parent_sp cs') Tptr. Proof. - induction 1; simpl; auto. -Qed. + induction 1; unfold parent_sp. apply Val.Vnullptr_has_type. apply Val.Vptr_has_type. +Qed. Lemma match_stacks_type_retaddr: forall j cs cs' sg, match_stacks j cs cs' sg -> - Val.has_type (parent_ra cs') Tint. + Val.has_type (parent_ra cs') Tptr. Proof. - induction 1; simpl; auto. + induction 1; unfold parent_ra. apply Val.Vnullptr_has_type. auto. Qed. (** * Syntactic properties of the translation *) @@ -1700,11 +1706,11 @@ Hypothesis SEP: m' |= frame_contents f j sp' ls ls0 parent retaddr ** minjection Lemma transl_builtin_arg_correct: forall a v, - eval_builtin_arg ge ls (Vptr sp Int.zero) m a v -> + eval_builtin_arg ge ls (Vptr sp Ptrofs.zero) m a v -> (forall l, In l (params_of_builtin_arg a) -> loc_valid f l = true) -> (forall sl ofs ty, In (S sl ofs ty) (params_of_builtin_arg a) -> slot_within_bounds b sl ofs ty) -> exists v', - eval_builtin_arg ge rs (Vptr sp' Int.zero) m' (transl_builtin_arg fe a) v' + eval_builtin_arg ge rs (Vptr sp' Ptrofs.zero) m' (transl_builtin_arg fe a) v' /\ Val.inject j v v'. Proof. assert (SYMB: forall id ofs, Val.inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address ge id ofs)). @@ -1712,7 +1718,7 @@ Proof. { eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eexact SEP. } intros; unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. destruct (Genv.find_symbol ge id) eqn:FS; auto. - destruct G. econstructor. eauto. rewrite Int.add_zero; auto. } + destruct G. econstructor. eauto. rewrite Ptrofs.add_zero; auto. } Local Opaque fe. induction 1; simpl; intros VALID BOUNDS. - assert (loc_valid f x = true) by auto. @@ -1724,13 +1730,13 @@ Local Opaque fe. - econstructor; eauto with barg. - econstructor; eauto with barg. - econstructor; eauto with barg. -- set (ofs' := Int.add ofs (Int.repr (fe_stack_data fe))). +- set (ofs' := Ptrofs.add ofs (Ptrofs.repr (fe_stack_data fe))). apply sep_proj2 in SEP. apply sep_proj1 in SEP. exploit loadv_parallel_rule; eauto. - instantiate (1 := Val.add (Vptr sp' Int.zero) (Vint ofs')). - simpl. rewrite ! Int.add_zero_l. econstructor; eauto. + instantiate (1 := Val.offset_ptr (Vptr sp' Ptrofs.zero) ofs'). + simpl. rewrite ! Ptrofs.add_zero_l. econstructor; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto. - econstructor; split; eauto with barg. - unfold Val.add. rewrite ! Int.add_zero_l. econstructor; eauto. + unfold Val.offset_ptr. rewrite ! Ptrofs.add_zero_l. econstructor; eauto. - apply sep_proj2 in SEP. apply sep_proj1 in SEP. exploit loadv_parallel_rule; eauto. intros (v' & A & B). exists v'; auto with barg. - econstructor; split; eauto with barg. @@ -1742,11 +1748,11 @@ Qed. Lemma transl_builtin_args_correct: forall al vl, - eval_builtin_args ge ls (Vptr sp Int.zero) m al vl -> + eval_builtin_args ge ls (Vptr sp Ptrofs.zero) m al vl -> (forall l, In l (params_of_builtin_args al) -> loc_valid f l = true) -> (forall sl ofs ty, In (S sl ofs ty) (params_of_builtin_args al) -> slot_within_bounds b sl ofs ty) -> exists vl', - eval_builtin_args ge rs (Vptr sp' Int.zero) m' (List.map (transl_builtin_arg fe) al) vl' + eval_builtin_args ge rs (Vptr sp' Ptrofs.zero) m' (List.map (transl_builtin_arg fe) al) vl' /\ Val.inject_list j vl vl'. Proof. induction 1; simpl; intros VALID BOUNDS. @@ -1798,8 +1804,8 @@ Inductive match_states: Linear.state -> Mach.state -> Prop := ** stack_contents j cs cs' ** minjection j m ** globalenv_inject ge j), - match_states (Linear.State cs f (Vptr sp Int.zero) c ls m) - (Mach.State cs' fb (Vptr sp' Int.zero) (transl_code (make_env (function_bounds f)) c) rs m') + match_states (Linear.State cs f (Vptr sp Ptrofs.zero) c ls m) + (Mach.State cs' fb (Vptr sp' Ptrofs.zero) (transl_code (make_env (function_bounds f)) c) rs m') | match_states_call: forall cs f ls m cs' fb rs m' j tf (STACKS: match_stacks j cs cs' (Linear.funsig f)) @@ -1882,7 +1888,7 @@ Proof. end). eapply frame_undef_regs with (rl := destroyed_by_setstack ty) in SEP. assert (A: exists m'', - store_stack m' (Vptr sp' Int.zero) ty (Int.repr ofs') (rs0 src) = Some m'' + store_stack m' (Vptr sp' Ptrofs.zero) ty (Ptrofs.repr ofs') (rs0 src) = Some m'' /\ m'' |= frame_contents f j sp' (Locmap.set (S sl ofs ty) (rs (R src)) (LTL.undef_regs (destroyed_by_setstack ty) rs)) (parent_locset s) (parent_sp cs') (parent_ra cs') @@ -1902,7 +1908,7 @@ Proof. - (* Lop *) assert (exists v', - eval_operation ge (Vptr sp' Int.zero) (transl_op (make_env (function_bounds f)) op) rs0##args m' = Some v' + eval_operation ge (Vptr sp' Ptrofs.zero) (transl_op (make_env (function_bounds f)) op) rs0##args m' = Some v' /\ Val.inject j v v'). eapply eval_operation_inject; eauto. eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP. @@ -1921,7 +1927,7 @@ Proof. - (* Lload *) assert (exists a', - eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a' + eval_addressing ge (Vptr sp' Ptrofs.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a' /\ Val.inject j a a'). eapply eval_addressing_inject; eauto. eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP. @@ -1941,7 +1947,7 @@ Proof. - (* Lstore *) assert (exists a', - eval_addressing ge (Vptr sp' Int.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a' + eval_addressing ge (Vptr sp' Ptrofs.zero) (transl_addr (make_env (function_bounds f)) addr) rs0##args = Some a' /\ Val.inject j a a'). eapply eval_addressing_inject; eauto. eapply globalenv_inject_preserves_globals. eapply sep_proj2. eapply sep_proj2. eapply sep_proj2. eexact SEP. @@ -1972,7 +1978,7 @@ Proof. apply plus_one. econstructor; eauto. econstructor; eauto. econstructor; eauto with coqlib. - simpl; auto. + apply Val.Vptr_has_type. intros; red. apply Zle_trans with (size_arguments (Linear.funsig f')); auto. apply loc_arguments_bounded; auto. @@ -2150,7 +2156,11 @@ Lemma transf_final_states: match_states st1 st2 -> Linear.final_state st1 r -> Mach.final_state st2 r. Proof. intros. inv H0. inv H. inv STACKS. - assert (R: exists r, loc_result signature_main = One r) by (econstructor; reflexivity). + assert (R: exists r, loc_result signature_main = One r). + { destruct (loc_result signature_main) as [r1 | r1 r2] eqn:LR. + - exists r1; auto. + - generalize (loc_result_type signature_main). rewrite LR. discriminate. + } destruct R as [rres EQ]. rewrite EQ in H1. simpl in H1. generalize (AGREGS rres). rewrite H1. intros A; inv A. econstructor; eauto. -- cgit