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/Clight.v | 32 ++++++++++++++++---------------- 1 file changed, 16 insertions(+), 16 deletions(-) (limited to 'cfrontend/Clight.v') diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v index e6426fb8..7a4c49a2 100644 --- a/cfrontend/Clight.v +++ b/cfrontend/Clight.v @@ -202,7 +202,7 @@ Definition temp_env := PTree.t val. memory load is performed. If the type [ty] indicates an access by reference or by copy, the pointer [Vptr b ofs] is returned. *) -Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : val -> Prop := +Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: ptrofs) : val -> Prop := | deref_loc_value: forall chunk v, access_mode ty = By_value chunk -> Mem.loadv chunk m (Vptr b ofs) = Some v -> @@ -220,7 +220,7 @@ Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : val -> Prop := This is allowed only if [ty] indicates an access by value or by copy. [m'] is the updated memory state. *) -Inductive assign_loc (ce: composite_env) (ty: type) (m: mem) (b: block) (ofs: int): +Inductive assign_loc (ce: composite_env) (ty: type) (m: mem) (b: block) (ofs: ptrofs): val -> mem -> Prop := | assign_loc_value: forall v chunk m', access_mode ty = By_value chunk -> @@ -228,13 +228,13 @@ Inductive assign_loc (ce: composite_env) (ty: type) (m: mem) (b: block) (ofs: in assign_loc ce ty m b ofs v m' | assign_loc_copy: forall b' ofs' bytes m', access_mode ty = By_copy -> - (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Int.unsigned ofs')) -> - (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Int.unsigned ofs)) -> - b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs - \/ Int.unsigned ofs' + sizeof ce ty <= Int.unsigned ofs - \/ Int.unsigned ofs + sizeof ce ty <= Int.unsigned ofs' -> - Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ce ty) = Some bytes -> - Mem.storebytes m b (Int.unsigned ofs) bytes = Some m' -> + (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Ptrofs.unsigned ofs')) -> + (sizeof ce ty > 0 -> (alignof_blockcopy ce ty | Ptrofs.unsigned ofs)) -> + b' <> b \/ Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs + \/ Ptrofs.unsigned ofs' + sizeof ce ty <= Ptrofs.unsigned ofs + \/ Ptrofs.unsigned ofs + sizeof ce ty <= Ptrofs.unsigned ofs' -> + Mem.loadbytes m b' (Ptrofs.unsigned ofs') (sizeof ce ty) = Some bytes -> + Mem.storebytes m b (Ptrofs.unsigned ofs) bytes = Some m' -> assign_loc ce ty m b ofs (Vptr b' ofs') m'. Section SEMANTICS. @@ -274,7 +274,7 @@ Inductive bind_parameters (e: env): | bind_parameters_cons: forall m id ty params v1 vl b m1 m2, PTree.get id e = Some(b, ty) -> - assign_loc ge ty m b Int.zero v1 m1 -> + assign_loc ge ty m b Ptrofs.zero v1 m1 -> bind_parameters e m1 params vl m2 -> bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2. @@ -384,9 +384,9 @@ Inductive eval_expr: expr -> val -> Prop := sem_cast v1 (typeof a) ty m = Some v -> eval_expr (Ecast a ty) v | eval_Esizeof: forall ty1 ty, - eval_expr (Esizeof ty1 ty) (Vint (Int.repr (sizeof ge ty1))) + eval_expr (Esizeof ty1 ty) (Vptrofs (Ptrofs.repr (sizeof ge ty1))) | eval_Ealignof: forall ty1 ty, - eval_expr (Ealignof ty1 ty) (Vint (Int.repr (alignof ge ty1))) + eval_expr (Ealignof ty1 ty) (Vptrofs (Ptrofs.repr (alignof ge ty1))) | eval_Elvalue: forall a loc ofs v, eval_lvalue a loc ofs -> deref_loc (typeof a) m loc ofs v -> @@ -396,14 +396,14 @@ Inductive eval_expr: expr -> val -> Prop := in l-value position. The result is the memory location [b, ofs] that contains the value of the expression [a]. *) -with eval_lvalue: expr -> block -> int -> Prop := +with eval_lvalue: expr -> block -> ptrofs -> Prop := | eval_Evar_local: forall id l ty, e!id = Some(l, ty) -> - eval_lvalue (Evar id ty) l Int.zero + eval_lvalue (Evar id ty) l Ptrofs.zero | eval_Evar_global: forall id l ty, e!id = None -> Genv.find_symbol ge id = Some l -> - eval_lvalue (Evar id ty) l Int.zero + eval_lvalue (Evar id ty) l Ptrofs.zero | eval_Ederef: forall a ty l ofs, eval_expr a (Vptr l ofs) -> eval_lvalue (Ederef a ty) l ofs @@ -412,7 +412,7 @@ with eval_lvalue: expr -> block -> int -> Prop := typeof a = Tstruct id att -> ge.(genv_cenv)!id = Some co -> field_offset ge i (co_members co) = OK delta -> - eval_lvalue (Efield a i ty) l (Int.add ofs (Int.repr delta)) + eval_lvalue (Efield a i ty) l (Ptrofs.add ofs (Ptrofs.repr delta)) | eval_Efield_union: forall a i ty l ofs id co att, eval_expr a (Vptr l ofs) -> typeof a = Tunion id att -> -- cgit