[clang] Build the Z3 mock module via CMake

clang/test/Analysis/z3-crosscheck-max-attempts.cpp

@@ -3,15 +3,10 @@
 // RUN: | FileCheck %s --match-full-lines
 // CHECK: crosscheck-with-z3-max-attempts-per-query = 3
 
-// RUN: rm -rf %t && mkdir %t
-// RUN: %host_cxx -shared -fPIC -I %z3_include_dir        \
-// RUN:   %S/z3/Inputs/MockZ3_solver_check.cpp            \
-// RUN:   -o %t/MockZ3_solver_check.so
-
-// DEFINE: %{mocked_clang} =                              \
-// DEFINE: LD_PRELOAD="%t/MockZ3_solver_check.so"         \
-// DEFINE: %clang_cc1 %s -analyze -setup-static-analyzer  \
-// DEFINE:   -analyzer-config crosscheck-with-z3=true     \
+// DEFINE: %{mocked_clang} =                                      \
+// DEFINE: LD_PRELOAD="%llvmshlibdir/MockZ3SolverCheck%pluginext" \
+// DEFINE: %clang_cc1 %s -analyze -setup-static-analyzer          \
+// DEFINE:   -analyzer-config crosscheck-with-z3=true             \
 // DEFINE:   -analyzer-checker=core
 
 // DEFINE: %{attempts} = -analyzer-config crosscheck-with-z3-max-attempts-per-query
@@ -32,7 +27,7 @@
 // RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,SAT"   %{mocked_clang} %{attempts}=3 -verify=accepted
 
 
-// REQUIRES: z3, z3-devel, asserts, shell, system-linux
+// REQUIRES: z3, z3-mock, asserts, shell, system-linux
 
 // refuted-no-diagnostics
 

clang/test/Analysis/z3/D83660.c

@@ -1,14 +1,9 @@
-// RUN: rm -rf %t && mkdir %t
-// RUN: %host_cxx -shared -fPIC -I %z3_include_dir \
-// RUN:   %S/Inputs/MockZ3_solver_check.cpp \
-// RUN:   -o %t/MockZ3_solver_check.so
-//
 // RUN: Z3_SOLVER_RESULTS="SAT,SAT,SAT,SAT,UNDEF" \
-// RUN: LD_PRELOAD="%t/MockZ3_solver_check.so" \
+// RUN: LD_PRELOAD="%llvmshlibdir/MockZ3SolverCheck%pluginext" \
 // RUN: %clang_cc1 -analyze -analyzer-constraints=z3 -setup-static-analyzer \
 // RUN:   -analyzer-checker=core %s -verify
 //
-// REQUIRES: z3, z3-devel, asserts, shell, system-linux
+// REQUIRES: z3, z3-mock, asserts, shell, system-linux
 //
 // Works only with the z3 constraint manager.
 // expected-no-diagnostics

clang/test/CMakeLists.txt

@@ -32,9 +32,21 @@ llvm_canonicalize_cmake_booleans(
 # Run tests requiring Z3 headers only if LLVM was built with Z3
 # and the headers are available while building Clang -- the latter may
 # not be the case when building standalone against installed LLVM.
-set(TEST_WITH_Z3_DEVEL 0)
-if(LLVM_WITH_Z3 AND Z3_FOUND)
-  set(TEST_WITH_Z3_DEVEL 1)
+set(TEST_WITH_Z3_MOCK 0)
+if(LLVM_WITH_Z3 AND Z3_FOUND AND CMAKE_SYSTEM_NAME MATCHES "Linux")
+  llvm_add_library(
+    MockZ3SolverCheck
+    MODULE Analysis/z3/Inputs/MockZ3_solver_check.cpp
+    DISABLE_LLVM_LINK_LLVM_DYLIB)
+
+  if(TARGET MockZ3SolverCheck)
+    list(APPEND CLANG_TEST_DEPS
+      MockZ3SolverCheck)
+    target_include_directories(
+      MockZ3SolverCheck
+      PRIVATE ${Z3_INCLUDE_DIR})
+    set(TEST_WITH_Z3_MOCK 1)
+  endif()
 endif()
 
 configure_lit_site_cfg(

clang/test/lit.cfg.py

@@ -201,11 +201,8 @@ def have_host_clang_repl_cuda():
 
     if config.clang_staticanalyzer_z3:
         config.available_features.add("z3")
-        if config.clang_staticanalyzer_z3_devel:
-            config.available_features.add("z3-devel")
-            config.substitutions.append(
-                ("%z3_include_dir", config.clang_staticanalyzer_z3_include_dir)
-            )
+        if config.clang_staticanalyzer_z3_mock:
+            config.available_features.add("z3-mock")
     else:
         config.available_features.add("no-z3")
 
@@ -251,9 +248,6 @@ def have_host_clang_repl_cuda():
     )
 )
 
-config.substitutions.append(("%host_cc", config.host_cc))
-config.substitutions.append(("%host_cxx", config.host_cxx))
-
 # Determine whether the test target is compatible with execution on the host.
 if "aarch64" in config.host_arch:
     config.available_features.add("aarch64-host")

clang/test/lit.site.cfg.py.in

@@ -17,8 +17,6 @@ config.clang_tools_dir = lit_config.substitute(path(r"@CURRENT_TOOLS_DIR@"))
 config.clang_lib_dir = path(r"@CMAKE_LIBRARY_OUTPUT_DIRECTORY@")
 config.host_triple = "@LLVM_HOST_TRIPLE@"
 config.target_triple = "@LLVM_TARGET_TRIPLE@"
-config.host_cc = "@CMAKE_C_COMPILER@"
-config.host_cxx = "@CMAKE_CXX_COMPILER@"
 config.llvm_use_sanitizer = "@LLVM_USE_SANITIZER@"
 config.have_zlib = @LLVM_ENABLE_ZLIB@
 config.have_zstd = @LLVM_ENABLE_ZSTD@
@@ -27,8 +25,7 @@ config.clang_default_pie_on_linux = @CLANG_DEFAULT_PIE_ON_LINUX@
 config.clang_default_cxx_stdlib = "@CLANG_DEFAULT_CXX_STDLIB@"
 config.clang_staticanalyzer = @CLANG_ENABLE_STATIC_ANALYZER@
 config.clang_staticanalyzer_z3 = @LLVM_WITH_Z3@
-config.clang_staticanalyzer_z3_devel = @TEST_WITH_Z3_DEVEL@
-config.clang_staticanalyzer_z3_include_dir = "@Z3_INCLUDE_DIR@"
+config.clang_staticanalyzer_z3_mock = @TEST_WITH_Z3_MOCK@
 config.clang_enable_cir = @CLANG_ENABLE_CIR@
 config.clang_examples = @CLANG_BUILD_EXAMPLES@
 config.enable_shared = @ENABLE_SHARED@