[llvm-bugs] [Bug 43464] New: Z3 prover not recognized when cmake configures LLVM 9 on Windows

[via llvm-bugs]

https://bugs.llvm.org/show_bug.cgi?id=43464

            Bug ID: 43464
           Summary: Z3 prover not recognized when cmake configures LLVM 9
                    on Windows
           Product: Build scripts
           Version: 9.0
          Hardware: PC
                OS: Windows NT
            Status: NEW
          Severity: enhancement
          Priority: P
         Component: cmake
          Assignee: unassignedbugs at nondot.org
          Reporter: man130117 at outlook.com
                CC: llvm-bugs at lists.llvm.org

Created attachment 22578
  --> https://bugs.llvm.org/attachment.cgi?id=22578&action=edit
New/modified FindZ3.cmake module

When cmake configures building LLVM 9, under Windows (10 Pro), with "x64 Native
Tools Command Prompt for VS 2019", it complains (among others) like this:

-- Could NOT find Z3: Found unsuitable version "0.0.0", but required is at
least "4.7.1" (found
C:/Users/Marek/AppData/Local/Programs/z3-4.8.6-x64/bin/libz3.lib)

and then Z3 is not used for building (though it is available as can be seen
above). 

I've found the reason of this in llvm/cmake/modules/FindZ3.cmake. Function 
"check_z3_version" in command "try_run" makes use of parameter: 

  "LINK_LIBRARIES -L${z3_lib_path} -lz3"

that finally creates a command line not understood by MSVC linker; the linker
fails to link and the function returns "0.0.0" as the Z3 version string.

I've changed the module a little (see attachment) to provide LINK_LIBRARIES in
a way suitable for MSVC, and now cmake finds Z3 correctly:

-- Found Z3: C:/Users/Marek/AppData/Local/Programs/z3-4.8.6-x64/bin/libz3.lib
(found suitable version "4.8.6", minimum required is "4.7.1")

Marek Anioła

PS. Here is the diff between the original and the new module:

---
C:\Users\Marek\AppData\Local\Temp\smartgit-2473644940642043647tmp\compare\FindZ3-index--6400871964085648525.cmake
  2019-09-26 15:15:07.188000000 +0200
+++ C:\Users\Marek\Develop\llvm-project\llvm\cmake\modules\FindZ3.cmake
2019-09-26 15:15:08.110000000 +0200
@@ -13,16 +13,21 @@
           return 0;
        }")

-  # Get lib path
-  get_filename_component(z3_lib_path ${z3_lib} PATH)
-
+  if (MSVC)
+    set(z3_test_libs "${z3_lib}")
+  else()
+    # Get lib path
+    get_filename_component(z3_lib_path ${z3_lib} PATH)
+    set(z3_test_libs "-L${z3_lib_path} -lz3")
+  endif()
+  
   try_run(
     Z3_RETURNCODE
     Z3_COMPILED
     ${CMAKE_BINARY_DIR}
     ${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/CMakeTmp/testz3.c
     COMPILE_DEFINITIONS -I"${z3_include}"
-    LINK_LIBRARIES -L${z3_lib_path} -lz3
+    LINK_LIBRARIES ${z3_test_libs}
     RUN_OUTPUT_VARIABLE SRC_OUTPUT
   )

-- 
You are receiving this mail because:
You are on the CC list for the bug.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-bugs/attachments/20190926/d0e0129f/attachment.html>