Automerge: [clang] Build the Z3 mock module via CMake (#146284)

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/llvm-project#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@