z3 icon indicating copy to clipboard operation
z3 copied to clipboard

__GNUC__ isn't always defined

Open Naville opened this issue 6 months ago • 3 comments

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 avatar Jul 31 '24 07:07 Naville