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. --- cfrontend/Ctypes.v | 50 ++++++++++++++++++++++++++++---------------------- 1 file changed, 28 insertions(+), 22 deletions(-) (limited to 'cfrontend/Ctypes.v') diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 9faa6d40..0794743d 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -78,15 +78,19 @@ with typelist : Type := | Tnil: typelist | Tcons: type -> typelist -> typelist. +Lemma intsize_eq: forall (s1 s2: intsize), {s1=s2} + {s1<>s2}. +Proof. + decide equality. +Defined. + Lemma type_eq: forall (ty1 ty2: type), {ty1=ty2} + {ty1<>ty2} with typelist_eq: forall (tyl1 tyl2: typelist), {tyl1=tyl2} + {tyl1<>tyl2}. Proof. - assert (forall (x y: intsize), {x=y} + {x<>y}) by decide equality. assert (forall (x y: signedness), {x=y} + {x<>y}) by decide equality. assert (forall (x y: floatsize), {x=y} + {x<>y}) by decide equality. assert (forall (x y: attr), {x=y} + {x<>y}). { decide equality. decide equality. apply N.eq_dec. apply bool_dec. } - generalize ident_eq zeq bool_dec ident_eq; intros. + generalize ident_eq zeq bool_dec ident_eq intsize_eq; intros. decide equality. decide equality. decide equality. @@ -272,7 +276,7 @@ Fixpoint alignof (env: composite_env) (t: type) : Z := | Tlong _ _ => Archi.align_int64 | Tfloat F32 _ => 4 | Tfloat F64 _ => Archi.align_float64 - | Tpointer _ _ => 4 + | Tpointer _ _ => if Archi.ptr64 then 8 else 4 | Tarray t' _ _ => alignof env t' | Tfunction _ _ _ => 1 | Tstruct id _ | Tunion id _ => @@ -299,11 +303,11 @@ Proof. exists 1%nat; auto. exists 2%nat; auto. exists 0%nat; auto. - (exists 2%nat; reflexivity) || (exists 3%nat; reflexivity). + unfold Archi.align_int64. destruct Archi.ptr64; ((exists 2%nat; reflexivity) || (exists 3%nat; reflexivity)). destruct f. exists 2%nat; auto. - (exists 2%nat; reflexivity) || (exists 3%nat; reflexivity). - exists 2%nat; auto. + unfold Archi.align_float64. destruct Archi.ptr64; ((exists 2%nat; reflexivity) || (exists 3%nat; reflexivity)). + exists (if Archi.ptr64 then 3%nat else 2%nat); destruct Archi.ptr64; auto. apply IHt. exists 0%nat; auto. destruct (env!i). apply co_alignof_two_p. exists 0%nat; auto. @@ -335,7 +339,7 @@ Fixpoint sizeof (env: composite_env) (t: type) : Z := | Tlong _ _ => 8 | Tfloat F32 _ => 4 | Tfloat F64 _ => 8 - | Tpointer _ _ => 4 + | Tpointer _ _ => if Archi.ptr64 then 8 else 4 | Tarray t' n _ => sizeof env t' * Z.max 0 n | Tfunction _ _ _ => 1 | Tstruct id _ | Tunion id _ => @@ -348,6 +352,7 @@ Proof. induction t; simpl; try omega. destruct i; omega. destruct f; omega. + destruct Archi.ptr64; omega. change 0 with (0 * Z.max 0 z) at 2. apply Zmult_ge_compat_r. auto. xomega. destruct (env!i). apply co_sizeof_pos. omega. destruct (env!i). apply co_sizeof_pos. omega. @@ -370,8 +375,8 @@ Proof. induction t; intros [A B]; unfold alignof, align_attr; rewrite A; simpl. - apply Zdivide_refl. - destruct i; apply Zdivide_refl. -- exists (8 / Archi.align_int64); reflexivity. -- destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64); reflexivity. +- exists (8 / Archi.align_int64). unfold Archi.align_int64; destruct Archi.ptr64; reflexivity. +- destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64). unfold Archi.align_float64; destruct Archi.ptr64; reflexivity. - apply Zdivide_refl. - apply Z.divide_mul_l; auto. - apply Zdivide_refl. @@ -576,7 +581,7 @@ Definition access_mode (ty: type) : mode := | Tfloat F32 _ => By_value Mfloat32 | Tfloat F64 _ => By_value Mfloat64 | Tvoid => By_nothing - | Tpointer _ _ => By_value Mint32 + | Tpointer _ _ => By_value Mptr | Tarray _ _ _ => By_reference | Tfunction _ _ _ => By_reference | Tstruct _ _ => By_copy @@ -609,7 +614,7 @@ Fixpoint alignof_blockcopy (env: composite_env) (t: type) : Z := | Tlong _ _ => 8 | Tfloat F32 _ => 4 | Tfloat F64 _ => 8 - | Tpointer _ _ => 4 + | Tpointer _ _ => if Archi.ptr64 then 8 else 4 | Tarray t' _ _ => alignof_blockcopy env t' | Tfunction _ _ _ => 1 | Tstruct id _ | Tunion id _ => @@ -633,9 +638,14 @@ Proof. rewrite two_power_nat_two_p. rewrite ! inj_S. change 8 with (two_p 3). apply two_p_monotone. omega. } - induction ty; simpl; auto. + induction ty; simpl. + auto. destruct i; auto. + auto. destruct f; auto. + destruct Archi.ptr64; auto. + apply IHty. + auto. destruct (env!i); auto. destruct (env!i); auto. Qed. @@ -714,20 +724,16 @@ Fixpoint type_of_params (params: list (ident * type)) : typelist := Definition typ_of_type (t: type) : AST.typ := match t with - | Tfloat F32 _ => AST.Tsingle - | Tfloat _ _ => AST.Tfloat + | Tvoid => AST.Tint + | Tint _ _ _ => AST.Tint | Tlong _ _ => AST.Tlong - | _ => AST.Tint + | Tfloat F32 _ => AST.Tsingle + | Tfloat F64 _ => AST.Tfloat + | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tptr end. Definition opttyp_of_type (t: type) : option AST.typ := - match t with - | Tvoid => None - | Tfloat F32 _ => Some AST.Tsingle - | Tfloat _ _ => Some AST.Tfloat - | Tlong _ _ => Some AST.Tlong - | _ => Some AST.Tint - end. + if type_eq t Tvoid then None else Some (typ_of_type t). Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ := match tl with -- cgit