[clang] Build the Z3 mock module via CMake

Build the Z3 mock module via CMake rather than compiling it directly
in tests.  This ensures that the toolchain file is exported,
and therefore fixes testing for Gentoo multilib.  Also, it ensures
that the module is compiled only once for the two tests using it.

While at it, remove the related Z3 include directory and host compiler
substitutions -- they are not used anymore, and the latter can't be
reliably used in tests.

The code is based on the existing bits for CTTestTidyModule.

See llvm#145731 (comment)

Author: mgorny

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@