Z3Prover / z3

The Z3 Theorem Prover
Other
10.22k stars 1.47k forks source link

__GNUC__ isn't always defined #7318

Closed Naville closed 1 month ago

Naville commented 2 months ago

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

Naville commented 2 months ago

I marked those two checks to check for __clang__ too and it worked. which confirmed my guesses

Naville commented 2 months ago

For this specific case, another even better alternative would be using [__has_builtin]()

#if defined __has_builtin
#  if __has_builtin (__builtin_ctz)
#    define _trailing_zeros32(X) __builtin_ctz(X)
# endif
#  if __has_builtin (__builtin_ctzll)
#    define _trailing_zeros64(X) __builtin_ctzll(X)
#  endif
#endif
Naville commented 1 month ago

ping