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/Inlining.v | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'backend/Inlining.v') diff --git a/backend/Inlining.v b/backend/Inlining.v index 5c8f4419..61776743 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -192,16 +192,16 @@ Definition sregs (ctx: context) (rl: list reg) := List.map (sreg ctx) rl. Definition sros (ctx: context) (ros: reg + ident) := sum_left_map (sreg ctx) ros. Definition sop (ctx: context) (op: operation) := - shift_stack_operation (Int.repr ctx.(dstk)) op. + shift_stack_operation ctx.(dstk) op. Definition saddr (ctx: context) (addr: addressing) := - shift_stack_addressing (Int.repr ctx.(dstk)) addr. + shift_stack_addressing ctx.(dstk) addr. Fixpoint sbuiltinarg (ctx: context) (a: builtin_arg reg) : builtin_arg reg := match a with | BA x => BA (sreg ctx x) - | BA_loadstack chunk ofs => BA_loadstack chunk (Int.add ofs (Int.repr ctx.(dstk))) - | BA_addrstack ofs => BA_addrstack (Int.add ofs (Int.repr ctx.(dstk))) + | BA_loadstack chunk ofs => BA_loadstack chunk (Ptrofs.add ofs (Ptrofs.repr ctx.(dstk))) + | BA_addrstack ofs => BA_addrstack (Ptrofs.add ofs (Ptrofs.repr ctx.(dstk))) | BA_splitlong hi lo => BA_splitlong (sbuiltinarg ctx hi) (sbuiltinarg ctx lo) | _ => a end. @@ -437,13 +437,13 @@ Definition expand_function (fenv: funenv) (f: function): mon context := Local Open Scope string_scope. (** Inlining can increase the size of the function's stack block. We must - make sure that the new size does not exceed [Int.max_unsigned], otherwise + make sure that the new size does not exceed [Ptrofs.max_unsigned], otherwise address computations within the stack would overflow and produce incorrect results. *) Definition transf_function (fenv: funenv) (f: function) : Errors.res function := let '(R ctx s _) := expand_function fenv f initstate in - if zlt s.(st_stksize) Int.max_unsigned then + if zlt s.(st_stksize) Ptrofs.max_unsigned then OK (mkfunction f.(fn_sig) (sregs ctx f.(fn_params)) s.(st_stksize) -- cgit