z3
z3 copied to clipboard
__GNUC__ isn't always defined
We're cross-compiling Z3 for Windows using MSVC Sysroot and clang-cl on Linux.
The compile steps are fine, but linking would fail due to _tzcnt_u64
symbol not defined.
I'm clueless with how MSVC works, so here are some educated assumptions:
From https://github.com/llvm/llvm-project/blob/07d2709a17860a202d91781769a88837e4fb5f2a/clang/lib/Frontend/InitPreprocessor.cpp#L868 we could see that while __clang__
and __llvm__
are always defined, but __GNUC__
is only defined when building with GNU C Version specified, which is not the case when using Clang-CL.
This results in the following Z3 code:
https://github.com/Z3Prover/z3/blob/0c16d34eb0eb9eb2627606431c631d896d547f6f/src/util/mpz.cpp#L50 and https://github.com/Z3Prover/z3/blob/0c16d34eb0eb9eb2627606431c631d896d547f6f/src/util/mpz.cpp#L65
falls back to using #define _trailing_zeros**(X) _tzcnt_u**(X)
Grepping through Windows SDK:
WinSDK/VC/Tools/MSVC/14.26.28801/include/immintrin.h:extern unsigned int _tzcnt_u32(unsigned int);
WinSDK/VC/Tools/MSVC/14.26.28801/include/ammintrin.h:unsigned int _tzcnt_u32(unsigned int);
WinSDK/VC/Tools/MSVC/14.26.28801/bin/Hostx64/x86/c1xx.dll: binary file matches
WinSDK/VC/Tools/MSVC/14.26.28801/bin/Hostx64/x86/c1.dll: binary file matches
We can see that these two builtins are listed as an external function, which makes compilation success. However without c1xx and c1.dll to lower those intrinsics calls, clang generates them to actual lib call, which fails in linking due to those functions only exists as intrinsics