Fixup overflow on macOS Apple Silicon

[jrrk2]

During compilation of NAIF spice library on macOS Apple Silicon, linker is called via clang
and encounters a fixup overflow:
testcase.zip

% ccomp -g -Iinclude mars.c lib/cspice.a -lm
In file included from :425:
:16:9: warning: redefining builtin macro [-Wbuiltin-macro-redefined]
16 | #define STDC_NO_THREADS 1
| ^
1 warning generated.
ld: invalid use of ADRP/imm12 in '_t_getc' to '_ungetc'
final section layout:
__PAGEZERO addr=0x00000000, size=0x100000000, fileOffset=0x00000000
__TEXT addr=0x100000000, size=0x00154000, fileOffset=0x00000000
__text addr=0x1000029a0, size=0x0011b8d4, fileOffset=0x000029a0
__stubs addr=0x10011e274, size=0x000002a0, fileOffset=0x0011e274
__cstring addr=0x10011e514, size=0x000277e6, fileOffset=0x0011e514
__const addr=0x100145d00, size=0x000007c8, fileOffset=0x00145d00
__unwind_info addr=0x1001464c8, size=0x00001ff0, fileOffset=0x001464c8
__eh_frame addr=0x1001484b8, size=0x0000bb48, fileOffset=0x001484b8
__DATA_CONST addr=0x100154000, size=0x00004000, fileOffset=0x00154000
__got addr=0x100154000, size=0x000001d8, fileOffset=0x00154000
__DATA addr=0x100158000, size=0x05b34000, fileOffset=0x00158000
__data addr=0x100158000, size=0x000b018d, fileOffset=0x00158000
__bss addr=0x100208190, size=0x05a7e550, fileOffset=0x00000000
__common addr=0x105c866e0, size=0x00001a78, fileOffset=0x00000000
__LINKEDIT addr=0x105c8c000, size=0x00054000, fileOffset=0x0020c000
clang: error: linker command failed with exit code 1 (use -v to see invocation)
ccomp: error: linker command failed with exit code 1 (use -v to see invocation)

1 error detected.

[xavierleroy]

Thank you for the report and the neatly-packaged repro case.

(Note to others who'd like to reproduce: do mkdir exe before running the makeall.csh script.)

I cannot reproduce the problem on my Mac M1 using CompCert 3.14:

~/tmp/testcase$ ccomp -g -Iinclude mars.c lib/cspice.a -lm
ld: warning: can't parse dwarf compilation unit info in /var/folders/tt/d_tsrzjs5wx4kkp2gdxqglhh0000gn/T/compcert3db97e.o

Debugging support for macOS/ARM64 is broken indeed, but the command above produces an a.out that runs.

Tool versions:

~/tmp/testcase$ xcode-select --version
xcode-select version 2409.
~/tmp/testcase$ clang --version
Apple clang version 12.0.5 (clang-1205.0.22.9)
Target: arm64-apple-darwin24.0.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/bin
~/tmp/testcase$ ld -v
@(#)PROGRAM:ld  PROJECT:ld64-650.9
BUILD 00:19:34 Mar 17 2021
configured to support archs: armv6 armv7 armv7s arm64 arm64e arm64_32 i386 x86_64 x86_64h armv6m armv7k armv7m armv7em
LTO support using: LLVM version 12.0.5, (clang-1205.0.22.9) (static support for 27, runtime is 27)
TAPI support using: Apple TAPI version 12.0.5 (tapi-1205.0.7.1)

[jrrk2]

I am using the very latest O/S and versions, some version numbers are the same as you, some not. My
processor is Apple M3 which should be upward compatible.

jonathan@Jonathans-MacBook-Pro testcase % ccomp --version
The CompCert C verified compiler, version 3.14
jonathan@Jonathans-MacBook-Pro testcase % xcode-select --version
xcode-select version 2409.
jonathan@Jonathans-MacBook-Pro testcase % clang --version
Apple clang version 16.0.0 (clang-1600.0.26.4)
Target: arm64-apple-darwin24.1.0
Thread model: posix
InstalledDir: /Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/bin
jonathan@Jonathans-MacBook-Pro testcase % ld -v
@(#)PROGRAM:ld PROJECT:ld-1115.7.3
BUILD 07:38:57 Oct 4 2024
configured to support archs: armv6 armv7 armv7s arm64 arm64e arm64_32 i386 x86_64 x86_64h armv6m armv7k armv7m armv7em
will use ld-classic for: armv6 armv7 armv7s i386 armv6m armv7k armv7m armv7em
LTO support using: LLVM version 16.0.0 (static support for 29, runtime is 29)
TAPI support using: Apple TAPI version 16.0.0 (tapi-1600.0.11.8)

[jrrk2]

TKCOMPILER=ccomp
TKCOMPILEOPTIONS=-c -O1 -D_Float16=short -DNON_UNIX_STDIO
TKLINKOPTIONS=-lm

[m-schmidt]

To reproduce, one has to export the variables in the last post into the environment before calling makeall.csh. There are also a few syntax error diagnostics for some genrated (?) source files:

syntax error after ';' and before 'main'.

[jrrk2]

ccomp bombs if a function is declared without a type. other compilers default to int as the return type. i don't know if this is the correct ansi behaviour but it does prevent some dubious programs from compiling.

[m-schmidt]

And for less verbose warnings an additional -Wp,-Wno-builtin-macro-redefined in TKCOMPILEOPTIONS is recommended.

[m-schmidt]

The linker problem looks like the two functions are located too far away from each other. Therefore the 12 bit immediate offset overflows.

[jrrk2]

Absolutely, but a formally correct compiler should generate code that can cope with that situation, by generating suitable relocation information.

[xavierleroy]

Let's get two points out of the way first, so that we won't discuss them further:

• Omitting the return type of a function, expecting it defaults to int, was removed in ISO C99 (https://en.cppreference.com/w/c/language/function_definition). CompCert does not implement pre-C99 features.
• The formal verification of CompCert aims to prove that IF compiled code is produced, it runs as prescribed by the semantics of the source program. There's no proof that an executable will always be produced, and there are many cases where it is not possible.

[xavierleroy]

With the full instructions, I am able to reproduce the issue. Actually, I'm getting a more informative message for the link-time error:

ld: Absolute addressing not allowed in arm64 code but used in '_s_rsle' referencing '_ungetc'

[xavierleroy]

This message leads to the following explanation for the problem. CompCert generates adrp/adr references to symbols defined in the current compilation unit, and GOT-relative references for other symbols (which could be defined by a shared library). I think this is correct macOS code generation. However the criterion to decide which reference to produce was fragile, and the Spice code managed to fool it by declaring ungetc twice, once extern and once "common". (No way this code would include <stdio.h>, no, siree, this is 1990's cowboy C style, with nests of #ifdef masking non-conformance to C standards.) Fix coming up soon.

[xavierleroy]

Proposed fix at #538. More testing is welcome.

[jrrk2]

Have an absinthe on me! [image0.jpeg] Sent from my iPhone On 19 Nov 2024, at 14:41, Xavier Leroy ***@***.***> wrote:  Proposed fix at #538<#538>. More testing is welcome. — Reply to this email directly, view it on GitHub<#537 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AE6VVM3EZJZU6XIRV45BBH32BNEYZAVCNFSM6AAAAABR5XGURSVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDIOBVHEYDIMZRGI>. You are receiving this because you authored the thread.Message ID: ***@***.***>