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. --- driver/Driver.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'driver/Driver.ml') diff --git a/driver/Driver.ml b/driver/Driver.ml index b89d93c1..4bd08a88 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -536,9 +536,12 @@ let _ = | "arm" -> if Configuration.is_big_endian then Machine.arm_bigendian else Machine.arm_littleendian - | "ia32" -> if Configuration.abi = "macosx" - then Machine.x86_32_macosx - else Machine.x86_32 + | "ia32" -> if Configuration.model = "64" then + Machine.x86_64 + else + if Configuration.abi = "macosx" + then Machine.x86_32_macosx + else Machine.x86_32 | _ -> assert false end; Builtins.set C2C.builtins; -- cgit