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. --- common/AST.v | 38 ++++++++++++++++++++++++++------------ 1 file changed, 26 insertions(+), 12 deletions(-) (limited to 'common/AST.v') 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 := -- cgit