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/Asmgenproof0.v | 75 +++++++++++++++++++++++++++----------------------- 1 file changed, 41 insertions(+), 34 deletions(-) (limited to 'backend/Asmgenproof0.v') diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 30d6990e..2c7994e9 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -81,7 +81,7 @@ Qed. Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen. Lemma nextinstr_pc: - forall rs, (nextinstr rs)#PC = Val.add rs#PC Vone. + forall rs, (nextinstr rs)#PC = Val.offset_ptr rs#PC Ptrofs.one. Proof. intros. apply Pregmap.gss. Qed. @@ -100,7 +100,7 @@ Qed. Lemma nextinstr_set_preg: forall rs m v, - (nextinstr (rs#(preg_of m) <- v))#PC = Val.add rs#PC Vone. + (nextinstr (rs#(preg_of m) <- v))#PC = Val.offset_ptr rs#PC Ptrofs.one. Proof. intros. unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_PC. @@ -491,13 +491,12 @@ Qed. Lemma code_tail_next_int: forall fn ofs i c, - list_length_z fn <= Int.max_unsigned -> - code_tail (Int.unsigned ofs) fn (i :: c) -> - code_tail (Int.unsigned (Int.add ofs Int.one)) fn c. + list_length_z fn <= Ptrofs.max_unsigned -> + code_tail (Ptrofs.unsigned ofs) fn (i :: c) -> + code_tail (Ptrofs.unsigned (Ptrofs.add ofs Ptrofs.one)) fn c. Proof. - intros. rewrite Int.add_unsigned. - change (Int.unsigned Int.one) with 1. - rewrite Int.unsigned_repr. apply code_tail_next with i; auto. + intros. rewrite Ptrofs.add_unsigned, Ptrofs.unsigned_one. + rewrite Ptrofs.unsigned_repr. apply code_tail_next with i; auto. generalize (code_tail_bounds_2 _ _ _ _ H0). omega. Qed. @@ -513,7 +512,7 @@ Inductive transl_code_at_pc (ge: Mach.genv): Genv.find_funct_ptr ge b = Some(Internal f) -> transf_function f = Errors.OK tf -> transl_code f c ep = OK tc -> - code_tail (Int.unsigned ofs) (fn_code tf) tc -> + code_tail (Ptrofs.unsigned ofs) (fn_code tf) tc -> transl_code_at_pc ge (Vptr b ofs) b f c ep tf tc. (** Equivalence between [transl_code] and [transl_code']. *) @@ -563,11 +562,11 @@ Qed. >> *) -Definition return_address_offset (f: Mach.function) (c: Mach.code) (ofs: int) : Prop := +Definition return_address_offset (f: Mach.function) (c: Mach.code) (ofs: ptrofs) : Prop := forall tf tc, transf_function f = OK tf -> transl_code f c false = OK tc -> - code_tail (Int.unsigned ofs) (fn_code tf) tc. + code_tail (Ptrofs.unsigned ofs) (fn_code tf) tc. (** We now show that such an offset always exists if the Mach code [c] is a suffix of [f.(fn_code)]. This holds because the translation @@ -590,7 +589,7 @@ Hypothesis transf_function_inv: forall f tf, transf_function f = OK tf -> exists tc, exists ep, transl_code f (Mach.fn_code f) ep = OK tc /\ is_tail tc (fn_code tf). Hypothesis transf_function_len: - forall f tf, transf_function f = OK tf -> list_length_z (fn_code tf) <= Int.max_unsigned. + forall f tf, transf_function f = OK tf -> list_length_z (fn_code tf) <= Ptrofs.max_unsigned. Lemma transl_code_tail: forall f c1 c2, is_tail c1 c2 -> @@ -618,11 +617,11 @@ Opaque transl_instr. apply is_tail_trans with tc2; auto. eapply transl_instr_tail; eauto. } exploit is_tail_code_tail. eexact TL3. intros [ofs CT]. - exists (Int.repr ofs). red; intros. - rewrite Int.unsigned_repr. congruence. + exists (Ptrofs.repr ofs). red; intros. + rewrite Ptrofs.unsigned_repr. congruence. exploit code_tail_bounds_1; eauto. apply transf_function_len in TF. omega. -+ exists Int.zero; red; intros. congruence. ++ exists Ptrofs.zero; red; intros. congruence. Qed. End RETADDR_EXISTS. @@ -651,8 +650,8 @@ Lemma return_address_offset_correct: Proof. intros. inv H. red in H0. exploit code_tail_unique. eexact H12. eapply H0; eauto. intro. - rewrite <- (Int.repr_unsigned ofs). - rewrite <- (Int.repr_unsigned ofs'). + rewrite <- (Ptrofs.repr_unsigned ofs). + rewrite <- (Ptrofs.repr_unsigned ofs'). congruence. Qed. @@ -758,12 +757,12 @@ Inductive exec_straight: code -> regset -> mem -> | exec_straight_one: forall i1 c rs1 m1 rs2 m2, exec_instr ge fn i1 rs1 m1 = Next rs2 m2 -> - rs2#PC = Val.add rs1#PC Vone -> + rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one -> exec_straight (i1 :: c) rs1 m1 c rs2 m2 | exec_straight_step: forall i c rs1 m1 rs2 m2 c' rs3 m3, exec_instr ge fn i rs1 m1 = Next rs2 m2 -> - rs2#PC = Val.add rs1#PC Vone -> + rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one -> exec_straight c rs2 m2 c' rs3 m3 -> exec_straight (i :: c) rs1 m1 c' rs3 m3. @@ -782,8 +781,8 @@ Lemma exec_straight_two: forall i1 i2 c rs1 m1 rs2 m2 rs3 m3, exec_instr ge fn i1 rs1 m1 = Next rs2 m2 -> exec_instr ge fn i2 rs2 m2 = Next rs3 m3 -> - rs2#PC = Val.add rs1#PC Vone -> - rs3#PC = Val.add rs2#PC Vone -> + rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one -> + rs3#PC = Val.offset_ptr rs2#PC Ptrofs.one -> exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3. Proof. intros. apply exec_straight_step with rs2 m2; auto. @@ -795,9 +794,9 @@ Lemma exec_straight_three: exec_instr ge fn i1 rs1 m1 = Next rs2 m2 -> exec_instr ge fn i2 rs2 m2 = Next rs3 m3 -> exec_instr ge fn i3 rs3 m3 = Next rs4 m4 -> - rs2#PC = Val.add rs1#PC Vone -> - rs3#PC = Val.add rs2#PC Vone -> - rs4#PC = Val.add rs3#PC Vone -> + rs2#PC = Val.offset_ptr rs1#PC Ptrofs.one -> + rs3#PC = Val.offset_ptr rs2#PC Ptrofs.one -> + rs4#PC = Val.offset_ptr rs3#PC Ptrofs.one -> exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4. Proof. intros. apply exec_straight_step with rs2 m2; auto. @@ -810,11 +809,11 @@ Qed. Lemma exec_straight_steps_1: forall c rs m c' rs' m', exec_straight c rs m c' rs' m' -> - list_length_z (fn_code fn) <= Int.max_unsigned -> + list_length_z (fn_code fn) <= Ptrofs.max_unsigned -> forall b ofs, rs#PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal fn) -> - code_tail (Int.unsigned ofs) (fn_code fn) c -> + code_tail (Ptrofs.unsigned ofs) (fn_code fn) c -> plus step ge (State rs m) E0 (State rs' m'). Proof. induction 1; intros. @@ -824,7 +823,7 @@ Proof. eapply plus_left'. econstructor; eauto. eapply find_instr_tail. eauto. - apply IHexec_straight with b (Int.add ofs Int.one). + apply IHexec_straight with b (Ptrofs.add ofs Ptrofs.one). auto. rewrite H0. rewrite H3. reflexivity. auto. apply code_tail_next_int with i; auto. @@ -834,20 +833,20 @@ Qed. Lemma exec_straight_steps_2: forall c rs m c' rs' m', exec_straight c rs m c' rs' m' -> - list_length_z (fn_code fn) <= Int.max_unsigned -> + list_length_z (fn_code fn) <= Ptrofs.max_unsigned -> forall b ofs, rs#PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal fn) -> - code_tail (Int.unsigned ofs) (fn_code fn) c -> + code_tail (Ptrofs.unsigned ofs) (fn_code fn) c -> exists ofs', rs'#PC = Vptr b ofs' - /\ code_tail (Int.unsigned ofs') (fn_code fn) c'. + /\ code_tail (Ptrofs.unsigned ofs') (fn_code fn) c'. Proof. induction 1; intros. - exists (Int.add ofs Int.one). split. + exists (Ptrofs.add ofs Ptrofs.one). split. rewrite H0. rewrite H2. auto. apply code_tail_next_int with i1; auto. - apply IHexec_straight with (Int.add ofs Int.one). + apply IHexec_straight with (Ptrofs.add ofs Ptrofs.one). auto. rewrite H0. rewrite H3. reflexivity. auto. apply code_tail_next_int with i; auto. Qed. @@ -871,10 +870,18 @@ Inductive match_stack: list Mach.stackframe -> Prop := match_stack (Stackframe fb sp ra c :: s). Lemma parent_sp_def: forall s, match_stack s -> parent_sp s <> Vundef. -Proof. induction 1; simpl. unfold Vzero; congruence. auto. Qed. +Proof. + induction 1; simpl. + unfold Vnullptr; destruct Archi.ptr64; congruence. + auto. +Qed. Lemma parent_ra_def: forall s, match_stack s -> parent_ra s <> Vundef. -Proof. induction 1; simpl. unfold Vzero; congruence. inv H0. congruence. Qed. +Proof. + induction 1; simpl. + unfold Vnullptr; destruct Archi.ptr64; congruence. + inv H0. congruence. +Qed. Lemma lessdef_parent_sp: forall s v, -- cgit