From c50680bb86564fe61db61e6140a418ccc7d36677 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Wed, 23 Dec 2020 15:54:51 +0100 Subject: AArch64: macOS port This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors. --- aarch64/CBuiltins.ml | 26 +++++++++++++++++++------- 1 file changed, 19 insertions(+), 7 deletions(-) (limited to 'aarch64/CBuiltins.ml') diff --git a/aarch64/CBuiltins.ml b/aarch64/CBuiltins.ml index e2a9c87a..4ba7e5ae 100644 --- a/aarch64/CBuiltins.ml +++ b/aarch64/CBuiltins.ml @@ -17,16 +17,28 @@ open C -(* va_list is a struct of size 32 and alignment 8, passed by reference *) +(* AAPCS64: + va_list is a struct of size 32 and alignment 8, passed by reference + Apple: + va_list is a pointer (size 8, alignment 8), passed by reference *) -let va_list_type = TArray(TInt(IULong, []), Some 4L, []) -let size_va_list = 32 -let va_list_scalar = false +let (va_list_type, size_va_list, va_list_scalar) = + match Archi.abi with + | Archi.AAPCS64 -> (TArray(TInt(IULong, []), Some 4L, []), 32, false) + | Archi.Apple -> (TPtr(TVoid [], []), 8, true) + +(* Some macOS headers use the GCC built-in types "__int128_t" and + "__uint128_t" unconditionally. Provide a dummy definition. *) + +let int128_type = TArray(TInt(IULong, []), Some 2L, []) let builtins = { - builtin_typedefs = [ - "__builtin_va_list", va_list_type - ]; + builtin_typedefs = + [ "__builtin_va_list", va_list_type ] @ + (if Configuration.system = "macosx" then + [ "__int128_t", int128_type; + "__uint128_t", int128_type ] + else []); builtin_functions = [ (* Synchronization *) "__builtin_fence", -- cgit From ab62e1bed37d2efe4d2a9e0139839bae21b1cdd9 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 18 Jan 2021 19:56:44 +0100 Subject: "macosx" is now called "macos" The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos". --- aarch64/CBuiltins.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'aarch64/CBuiltins.ml') diff --git a/aarch64/CBuiltins.ml b/aarch64/CBuiltins.ml index 4ba7e5ae..4cfb7edf 100644 --- a/aarch64/CBuiltins.ml +++ b/aarch64/CBuiltins.ml @@ -35,7 +35,7 @@ let int128_type = TArray(TInt(IULong, []), Some 2L, []) let builtins = { builtin_typedefs = [ "__builtin_va_list", va_list_type ] @ - (if Configuration.system = "macosx" then + (if Configuration.system = "macos" then [ "__int128_t", int128_type; "__uint128_t", int128_type ] else []); -- cgit From 04f499c632a76e460560fc9ec4e14d8216e7fc18 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 4 May 2021 10:46:17 +0200 Subject: Use the LGPL instead of the GPL for dual-licensed files The GPL makes sense for whole applications, but the dual-licensed Coq and OCaml files are more like libraries to be combined with other code, so the LGPL is more appropriate. --- aarch64/CBuiltins.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'aarch64/CBuiltins.ml') diff --git a/aarch64/CBuiltins.ml b/aarch64/CBuiltins.ml index 4cfb7edf..80d66310 100644 --- a/aarch64/CBuiltins.ml +++ b/aarch64/CBuiltins.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* under the terms of the GNU Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 of *) +(* the License, or (at your option) any later version. *) +(* This file is also distributed under the terms of the *) +(* INRIA Non-Commercial License Agreement. *) (* *) (* *********************************************************************) -- cgit