Fix FindZ3.cmake's version detection mechanism

[Naville]

Summary

• Fix the issue that when the test program is not executed (Ex: Can't run due to missing dependency library), on Windows the error message of missing DLLs is used to parse version info
• Z3 has bumped its versioning to two digits (4.11.0) which old regex can't recognize. (4.11.0 got identified as 4.1.0, which is an error)

[Naville]

Obviously {1,2} is not supported in CMake, updated to use +

[steakhal]

LGTM, but prior approval I'll get a second pair of eyes.
I'm not using windows.

[Naville]

In D132441#3769497, @steakhal wrote:

LGTM, but prior approval I'll get a second pair of eyes.
I'm not using windows.

It's not strictly Windows, the output is obviously meaningless if the test program failed to execute, which we detect with Z3_RETURNCODE

CMake Reference

[steakhal]

Let's land this. Thanks for your patience. Also thanks for fixing this.

[steakhal]

Oh, @Godin called my attention to a detail. Now, I'm no longer comfortable approving this unless I get some clarification.

llvm/cmake/modules/FindZ3.cmake

85

Why did you remove the CMAKE_CROSSCOMPILING?

[Naville]

i>>! In D132441#3772196, @steakhal wrote:

Oh, @Godin called my attention to a detail. Now, I'm no longer comfortable approving this unless I get some clarification.

Hi:

In the Windows example (similar reasoning elsewhere):

• The linked test program failed to execute because it's missing a specific version of CRT (I remember it was Debug version of CRT vs. Release version of CRT)
• In this case the program still failed to execute, but it's definitely not cross-compiling since we are still targeting x64 Windows

EDIT 01:
In my understanding, cross-compiling -> failed to execute -> catched by the Z3_RETURNCODE patch -> fallback to header regex path.

Though, I don't cross-compile LLVM myself so I can't personally confirm the implementation is correct w.r.t. cross-compiling. But the logic seems to be right? I think?

EDIT02:
While we are at it, it'll be even better if LLVM's builtbot could test this patch for cross-compiling

[Naville]

Ping @steakhal is there any issue with my clarification?

[Godin]

Hi @Naville ,

Please excuse for the delay with the response, I think @steakhal wanted to see the response from me, but it was a day off for me yesterday.

The linked test program failed to execute because it's missing a specific version of CRT (I remember it was Debug version of CRT vs. Release version of CRT)

Isn't it the root of the problem that should be fixed instead? To my taste, it sounds a bit weird for the non-cross-compiling mode to let the build process continue after the failure to run the test program due to such a mismatch - isn't this opening a door for a failure to link Z3 with Clang later?
I'm also not on Windows, but we have a CI at work that builds Clang with Z3, and I saw such a mismatch only in cases when z3 will fail to link with Clang, so I'm curious if can reproduce your case in order to better understand it - could you please share how do you build Z3 and Clang?

[Naville]

In D132441#3779344, @Godin wrote:

Hi @Naville ,

Please excuse for the delay with the response, I think @steakhal wanted to see the response from me, but it was a day off for me yesterday.

The linked test program failed to execute because it's missing a specific version of CRT (I remember it was Debug version of CRT vs. Release version of CRT)

Isn't it the root of the problem that should be fixed instead? To my taste, it sounds a bit weird for the non-cross-compiling mode to let the build process continue after the failure to run the test program due to such a mismatch - isn't this opening a door for a failure to link Z3 with Clang later?
I'm also not on Windows, but we have a CI at work that builds Clang with Z3, and I saw such a mismatch only in cases when z3 will fail to link with Clang, so I'm curious if can reproduce your case in order to better understand it - could you please share how do you build Z3 and Clang?

Hi:
I think Z3 was built with VCPKG with triplet `x64-windows`, unfortunately can't reproduce the exact environment since it's been a while and we have switch to static built z3 since.
But I do remember at one time I need to add `%Path%=.....` to add Z3.dll and its dependencies to the DLL search path for the test program to work, even without CRT version mismatch

[Naville]

Browsed through my catalog and found one.
Basically, vcpkg put libZ3.dll in its own "exported toolchain folder", and then you use it with `-DCMAKE_TOOLCHAIN_FILE=vcpkg/...../vcpkg.cmake XXXXX`.
In this case, libZ3.dll is not copied into the same directory with the built test program, nor is it in system DLL path, hence broke current FindZ3.cmake in another completely different way

EDIT01:
Plus, I see no reason why we can't always use the regex path as the final fallback plan

EDIT02:

for a failure to link Z3 with Clang later?

This will not broke in the case mentioned above, because CMake guides the linker to link the "stub library" instead, and only requires the .dll when actually running

[Godin]

Sorry, but I'm not familiar with vcpkg

why we can't always use the regex path as the final fallback plan

and I don't feel that I'm the right person to answer this question and take a decision about this, so have to resign from the reviewer here.

But to me personally this doesn't sound right, because if I understood you correctly it didn't result in link failure in this case, but might result in a runtime failure.

All other changes look good to me. So maybe will be better to leave them only and revert vcpkg-related changes here, especially since you also don't rely on it anymore.

[mikhail.ramalho]

Sorry, I just saw this patch...

Part of it was just merged in D134261.

May I ask you to rebase?

@stilriv is this related to what you plan next?

[stilriv]

Not really. I want to split try_run into try_compile (both cross and native) and try_run (native or when CROSSCOMPILING_EMULATOR is specified) or fallback to header parsing in cross build (when there is no CROSSCOMPILING_EMULATOR). The reasoning is that try_run without emulator always causes a configuration error unless explicit Z3RETURNCODE (or something) and Z3TRYRUN_OUTPUT (or something) are passed through command line which is very inconvenient keepind in mind this machinery is meant to detect version without user input.

[stilriv]

In D132441#3779356, @Naville wrote:

Browsed through my catalog and found one.
Basically, vcpkg put libZ3.dll in its own "exported toolchain folder", and then you use it with `-DCMAKE_TOOLCHAIN_FILE=vcpkg/...../vcpkg.cmake XXXXX`.
In this case, libZ3.dll is not copied into the same directory with the built test program, nor is it in system DLL path, hence broke current FindZ3.cmake in another completely different way

EDIT01:
Plus, I see no reason why we can't always use the regex path as the final fallback plan

EDIT02:

for a failure to link Z3 with Clang later?

This will not broke in the case mentioned above, because CMake guides the linker to link the "stub library" instead, and only requires the .dll when actually running

You are describing problem with the toolchain here, not with LLVM's cmakes. And, IMO, this should be fixed on the toolchain side (in your case by adding directory with libZ3.dll to the PATH variable). The advantage of try_run path is that it is clearly diagnose problems with [broken] toolchain during configuration phase, so instead of getting broken LLVM libs after compilation you get early configuration error.

[mikhail.ramalho]

You are describing problem with the toolchain here, not with LLVM's cmakes. And, IMO, this should be fixed on the toolchain side (in your case by adding directory with libZ3.dll to the PATH variable). The advantage of try_run path is that it is clearly diagnose problems with [broken] toolchain during configuration phase, so instead of getting broken LLVM libs after compilation you get early configuration error.

I wouldn't describe it as a problem, since relying on cmake to download the dependencies is becoming common.

If it also works for cross-compilation, it could simplify the findz3.cmake considerably.

Also, I think it should only download the static z3 lib, right? Otherwise, we could have problems when running clang.

llvm/cmake/modules/FindZ3.cmake

     RUN_OUTPUT_VARIABLE SRC_OUTPUT
   )
 
-  if(Z3_COMPILED)
+  if(Z3_COMPILED AND NOT (Z3_RETURNCODE STREQUAL FAILED_TO_RUN))
     string(REGEX REPLACE "([0-9]*\\.[0-9]*\\.[0-9]*)" "\\1"
            z3_version "${SRC_OUTPUT}")
     set(Z3_VERSION_STRING ${z3_version} PARENT_SCOPE)

 
 # If the dynamic check fails, we might be cross compiling: if that's the case,
 # check the version in the headers, otherwise, fail with a message
-if(NOT Z3_VERSION_STRING AND (CMAKE_CROSSCOMPILING AND
-                              Z3_INCLUDE_DIR AND
-                              EXISTS "${Z3_INCLUDE_DIR}/z3_version.h"))
+if(NOT Z3_VERSION_STRING AND (Z3_INCLUDE_DIR AND EXISTS "${Z3_INCLUDE_DIR}/z3_version.h"))
   # TODO: print message warning that we couldn't find a compatible lib?
 
   # Z3 4.8.1+ has the version is in a public header.
   file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
        z3_version_str REGEX "^#define[\t ]+Z3_MAJOR_VERSION[\t ]+.*")
-  string(REGEX REPLACE "^.*Z3_MAJOR_VERSION[\t ]+([0-9]).*$" "\\1"
+  string(REGEX REPLACE "^.*Z3_MAJOR_VERSION[\t ]+([0-9]+).*$" "\\1"
          Z3_MAJOR "${z3_version_str}")
 
   file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
        z3_version_str REGEX "^#define[\t ]+Z3_MINOR_VERSION[\t ]+.*")
-  string(REGEX REPLACE "^.*Z3_MINOR_VERSION[\t ]+([0-9]).*$" "\\1"
+  string(REGEX REPLACE "^.*Z3_MINOR_VERSION[\t ]+([0-9]+).*$" "\\1"
          Z3_MINOR "${z3_version_str}")
 
   file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h"
        z3_version_str REGEX "^#define[\t ]+Z3_BUILD_NUMBER[\t ]+.*")
-  string(REGEX REPLACE "^.*Z3_BUILD_NUMBER[\t ]+([0-9]).*$" "\\1"
+  string(REGEX REPLACE "^.*Z3_BUILD_NUMBER[\t ]+([0-9]+).*$" "\\1"
          Z3_BUILD "${z3_version_str}")
 
   set(Z3_VERSION_STRING ${Z3_MAJOR}.${Z3_MINOR}.${Z3_BUILD})

                                   REQUIRED_VARS Z3_LIBRARIES Z3_INCLUDE_DIR
                                   VERSION_VAR Z3_VERSION_STRING)
 
-mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES)
+mark_as_advanced(Z3_INCLUDE_DIR Z3_LIBRARIES)
 No newline at end of file