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/RTLtyping.v | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) (limited to 'backend/RTLtyping.v') diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index dec1b988..f9f01d49 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -73,9 +73,9 @@ Definition type_of_builtin_arg (a: builtin_arg reg) : typ := | BA_float _ => Tfloat | BA_single _ => Tsingle | BA_loadstack chunk ofs => type_of_chunk chunk - | BA_addrstack ofs => Tint + | BA_addrstack ofs => Tptr | BA_loadglobal chunk id ofs => type_of_chunk chunk - | BA_addrglobal id ofs => Tint + | BA_addrglobal id ofs => Tptr | BA_splitlong hi lo => Tlong end. @@ -116,14 +116,14 @@ Inductive wt_instr : instruction -> Prop := wt_instr (Istore chunk addr args src s) | wt_Icall: forall sig ros args res s, - match ros with inl r => env r = Tint | inr s => True end -> + match ros with inl r => env r = Tptr | inr s => True end -> map env args = sig.(sig_args) -> env res = proj_sig_res sig -> valid_successor s -> wt_instr (Icall sig ros args res s) | wt_Itailcall: forall sig ros args, - match ros with inl r => env r = Tint | inr s => True end -> + match ros with inl r => env r = Tptr | inr s => True end -> map env args = sig.(sig_args) -> sig.(sig_res) = funct.(fn_sig).(sig_res) -> tailcall_possible sig -> @@ -227,7 +227,7 @@ Fixpoint check_successors (sl: list node): res unit := Definition type_ros (e: S.typenv) (ros: reg + ident) : res S.typenv := match ros with - | inl r => S.set e r Tint + | inl r => S.set e r Tptr | inr s => OK e end. @@ -245,9 +245,9 @@ Definition type_builtin_arg (e: S.typenv) (a: builtin_arg reg) (ty: typ) : res S | BA_float _ => type_expect e ty Tfloat | BA_single _ => type_expect e ty Tsingle | BA_loadstack chunk ofs => type_expect e ty (type_of_chunk chunk) - | BA_addrstack ofs => type_expect e ty Tint + | BA_addrstack ofs => type_expect e ty Tptr | BA_loadglobal chunk id ofs => type_expect e ty (type_of_chunk chunk) - | BA_addrglobal id ofs => type_expect e ty Tint + | BA_addrglobal id ofs => type_expect e ty Tptr | BA_splitlong hi lo => type_expect e ty Tlong end. @@ -367,7 +367,7 @@ Hint Resolve type_ros_incr: ty. Lemma type_ros_sound: forall e ros e' te, type_ros e ros = OK e' -> S.satisf te e' -> - match ros with inl r => te r = Tint | inr s => True end. + match ros with inl r => te r = Tptr | inr s => True end. Proof. unfold type_ros; intros. destruct ros. eapply S.set_sound; eauto. @@ -594,7 +594,7 @@ Qed. Lemma type_ros_complete: forall te ros e, S.satisf te e -> - match ros with inl r => te r = Tint | inr s => True end -> + match ros with inl r => te r = Tptr | inr s => True end -> exists e', type_ros e ros = OK e' /\ S.satisf te e'. Proof. intros; destruct ros; simpl. -- cgit