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.

1 files changed, 9 insertions, 9 deletions

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.