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. --- backend/CminorSel.v | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) (limited to 'backend/CminorSel.v') diff --git a/backend/CminorSel.v b/backend/CminorSel.v index d654502b..9439c269 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -246,7 +246,7 @@ Inductive eval_expr_or_symbol: letenv -> expr + ident -> val -> Prop := eval_expr_or_symbol le (inl _ e) v | eval_eos_s: forall le id b, Genv.find_symbol ge id = Some b -> - eval_expr_or_symbol le (inr _ id) (Vptr b Int.zero). + eval_expr_or_symbol le (inr _ id) (Vptr b Ptrofs.zero). Inductive eval_builtin_arg: builtin_arg expr -> val -> Prop := | eval_BA: forall a v, @@ -261,10 +261,10 @@ Inductive eval_builtin_arg: builtin_arg expr -> val -> Prop := | eval_BA_single: forall n, eval_builtin_arg (BA_single n) (Vsingle n) | eval_BA_loadstack: forall chunk ofs v, - Mem.loadv chunk m (Val.add sp (Vint ofs)) = Some v -> + Mem.loadv chunk m (Val.offset_ptr sp ofs) = Some v -> eval_builtin_arg (BA_loadstack chunk ofs) v | eval_BA_addrstack: forall ofs, - eval_builtin_arg (BA_addrstack ofs) (Val.add sp (Vint ofs)) + eval_builtin_arg (BA_addrstack ofs) (Val.offset_ptr sp ofs) | eval_BA_loadglobal: forall chunk id ofs v, Mem.loadv chunk m (Genv.symbol_address ge id ofs) = Some v -> eval_builtin_arg (BA_loadglobal chunk id ofs) v @@ -338,7 +338,7 @@ Inductive step: state -> trace -> state -> Prop := | step_skip_call: forall f k sp e m m', is_call_cont k -> Mem.free m sp 0 f.(fn_stackspace) = Some m' -> - step (State f Sskip k (Vptr sp Int.zero) e m) + step (State f Sskip k (Vptr sp Ptrofs.zero) e m) E0 (Returnstate Vundef k m') | step_assign: forall f id a k sp e m v, @@ -363,12 +363,12 @@ Inductive step: state -> trace -> state -> Prop := E0 (Callstate fd vargs (Kcall optid f sp e k) m) | step_tailcall: forall f sig a bl k sp e m vf vargs fd m', - eval_expr_or_symbol (Vptr sp Int.zero) e m nil a vf -> - eval_exprlist (Vptr sp Int.zero) e m nil bl vargs -> + eval_expr_or_symbol (Vptr sp Ptrofs.zero) e m nil a vf -> + eval_exprlist (Vptr sp Ptrofs.zero) e m nil bl vargs -> Genv.find_funct ge vf = Some fd -> funsig fd = sig -> Mem.free m sp 0 f.(fn_stackspace) = Some m' -> - step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m) + step (State f (Stailcall sig a bl) k (Vptr sp Ptrofs.zero) e m) E0 (Callstate fd vargs (call_cont k) m') | step_builtin: forall f res ef al k sp e m vl t v m', @@ -411,12 +411,12 @@ Inductive step: state -> trace -> state -> Prop := | step_return_0: forall f k sp e m m', Mem.free m sp 0 f.(fn_stackspace) = Some m' -> - step (State f (Sreturn None) k (Vptr sp Int.zero) e m) + step (State f (Sreturn None) k (Vptr sp Ptrofs.zero) e m) E0 (Returnstate Vundef (call_cont k) m') | step_return_1: forall f a k sp e m v m', - eval_expr (Vptr sp Int.zero) e m nil a v -> + eval_expr (Vptr sp Ptrofs.zero) e m nil a v -> Mem.free m sp 0 f.(fn_stackspace) = Some m' -> - step (State f (Sreturn (Some a)) k (Vptr sp Int.zero) e m) + step (State f (Sreturn (Some a)) k (Vptr sp Ptrofs.zero) e m) E0 (Returnstate v (call_cont k) m') | step_label: forall f lbl s k sp e m, @@ -432,7 +432,7 @@ Inductive step: state -> trace -> state -> Prop := Mem.alloc m 0 f.(fn_stackspace) = (m', sp) -> set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e -> step (Callstate (Internal f) vargs k m) - E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m') + E0 (State f f.(fn_body) k (Vptr sp Ptrofs.zero) e m') | step_external_function: forall ef vargs k m t vres m', external_call ef ge vargs m t vres m' -> step (Callstate (External ef) vargs k m) -- cgit