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, 26 insertions, 12 deletions

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 :=