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/Csem.v | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) (limited to 'cfrontend/Csem.v') diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 30e6200d..0c3e00de 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -63,7 +63,7 @@ Variable ge: genv. returned, and [t] the trace of observables (nonempty if this is a volatile access). *) -Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : trace -> val -> Prop := +Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: ptrofs) : trace -> val -> Prop := | deref_loc_value: forall chunk v, access_mode ty = By_value chunk -> type_is_volatile ty = false -> @@ -87,7 +87,7 @@ Inductive deref_loc (ty: type) (m: mem) (b: block) (ofs: int) : trace -> val -> [m'] is the updated memory state and [t] the trace of observables (nonempty if this is a volatile store). *) -Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: int): +Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: ptrofs): val -> trace -> mem -> Prop := | assign_loc_value: forall v chunk m', access_mode ty = By_value chunk -> @@ -100,13 +100,13 @@ Inductive assign_loc (ty: type) (m: mem) (b: block) (ofs: int): assign_loc ty m b ofs v t m' | assign_loc_copy: forall b' ofs' bytes m', access_mode ty = By_copy -> - (alignof_blockcopy ge ty | Int.unsigned ofs') -> - (alignof_blockcopy ge ty | Int.unsigned ofs) -> - b' <> b \/ Int.unsigned ofs' = Int.unsigned ofs - \/ Int.unsigned ofs' + sizeof ge ty <= Int.unsigned ofs - \/ Int.unsigned ofs + sizeof ge ty <= Int.unsigned ofs' -> - Mem.loadbytes m b' (Int.unsigned ofs') (sizeof ge ty) = Some bytes -> - Mem.storebytes m b (Int.unsigned ofs) bytes = Some m' -> + (alignof_blockcopy ge ty | Ptrofs.unsigned ofs') -> + (alignof_blockcopy ge ty | Ptrofs.unsigned ofs) -> + b' <> b \/ Ptrofs.unsigned ofs' = Ptrofs.unsigned ofs + \/ Ptrofs.unsigned ofs' + sizeof ge ty <= Ptrofs.unsigned ofs + \/ Ptrofs.unsigned ofs + sizeof ge ty <= Ptrofs.unsigned ofs' -> + Mem.loadbytes m b' (Ptrofs.unsigned ofs') (sizeof ge ty) = Some bytes -> + Mem.storebytes m b (Ptrofs.unsigned ofs) bytes = Some m' -> assign_loc ty m b ofs (Vptr b' ofs') E0 m'. (** Allocation of function-local variables. @@ -142,7 +142,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 ty m b Int.zero v1 E0 m1 -> + assign_loc ty m b Ptrofs.zero v1 E0 m1 -> bind_parameters e m1 params vl m2 -> bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2. @@ -211,12 +211,12 @@ Inductive lred: expr -> mem -> expr -> mem -> Prop := | red_var_local: forall x ty m b, e!x = Some(b, ty) -> lred (Evar x ty) m - (Eloc b Int.zero ty) m + (Eloc b Ptrofs.zero ty) m | red_var_global: forall x ty m b, e!x = None -> Genv.find_symbol ge x = Some b -> lred (Evar x ty) m - (Eloc b Int.zero ty) m + (Eloc b Ptrofs.zero ty) m | red_deref: forall b ofs ty1 ty m, lred (Ederef (Eval (Vptr b ofs) ty1) ty) m (Eloc b ofs ty) m @@ -224,7 +224,7 @@ Inductive lred: expr -> mem -> expr -> mem -> Prop := ge.(genv_cenv)!id = Some co -> field_offset ge f (co_members co) = OK delta -> lred (Efield (Eval (Vptr b ofs) (Tstruct id a)) f ty) m - (Eloc b (Int.add ofs (Int.repr delta)) ty) m + (Eloc b (Ptrofs.add ofs (Ptrofs.repr delta)) ty) m | red_field_union: forall b ofs id co a f ty m, ge.(genv_cenv)!id = Some co -> lred (Efield (Eval (Vptr b ofs) (Tunion id a)) f ty) m @@ -274,10 +274,10 @@ Inductive rred: expr -> mem -> trace -> expr -> mem -> Prop := E0 (Eparen (if b then r1 else r2) ty ty) m | red_sizeof: forall ty1 ty m, rred (Esizeof ty1 ty) m - E0 (Eval (Vint (Int.repr (sizeof ge ty1))) ty) m + E0 (Eval (Vptrofs (Ptrofs.repr (sizeof ge ty1))) ty) m | red_alignof: forall ty1 ty m, rred (Ealignof ty1 ty) m - E0 (Eval (Vint (Int.repr (alignof ge ty1))) ty) m + E0 (Eval (Vptrofs (Ptrofs.repr (alignof ge ty1))) ty) m | red_assign: forall b ofs ty1 v2 ty2 m v t m', sem_cast v2 ty2 ty1 m = Some v -> assign_loc ty1 m b ofs v t m' -> -- cgit