diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:25:18 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-10-01 17:25:18 +0200 |
commit | e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c (patch) | |
tree | 518d558674d3e1c6ff41c46d84c784e727ed5d04 /backend/Inlining.v | |
parent | ad2a2c862abef3aee701d1bca0524fcbf2d07b30 (diff) | |
download | compcert-e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c.tar.gz compcert-e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c.zip |
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.
Diffstat (limited to 'backend/Inlining.v')
-rw-r--r-- | backend/Inlining.v | 12 |
1 files changed, 6 insertions, 6 deletions
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) |