[clang] Build the Z3 mock module via CMake #146284
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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)
mgorny
requested review from
tstellar,
MaskRay,
steakhal,
thesamesam and
NagyDonat
llvmbot
added
clang
|
@llvm/pr-subscribers-clang Author: Michał Górny (mgorny) ChangesBuild 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. Full diff: https://github.com/llvm/llvm-project/pull/146284.diff 5 Files Affected:
diff --git a/clang/test/Analysis/z3-crosscheck-max-attempts.cpp b/clang/test/Analysis/z3-crosscheck-max-attempts.cpp
index 312e442f23f4f..eb5d0ae0cca19 100644
--- a/clang/test/Analysis/z3-crosscheck-max-attempts.cpp
+++ b/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
diff --git a/clang/test/Analysis/z3/D83660.c b/clang/test/Analysis/z3/D83660.c
index 2ca4a4d0b53e9..58022659e14a2 100644
--- a/clang/test/Analysis/z3/D83660.c
+++ b/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
diff --git a/clang/test/CMakeLists.txt b/clang/test/CMakeLists.txt
index 8baea5b0ca937..483deb0c1b51d 100644
--- a/clang/test/CMakeLists.txt
+++ b/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(
diff --git a/clang/test/lit.cfg.py b/clang/test/lit.cfg.py
index 6375e73f5df82..1957bb1715eb6 100644
--- a/clang/test/lit.cfg.py
+++ b/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")
diff --git a/clang/test/lit.site.cfg.py.in b/clang/test/lit.site.cfg.py.in
index ec0e4aa10ed79..176cf644badcc 100644
--- a/clang/test/lit.site.cfg.py.in
+++ b/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@
|
|
@llvm/pr-subscribers-clang-static-analyzer-1 Author: Michał Górny (mgorny) ChangesBuild 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. Full diff: https://github.com/llvm/llvm-project/pull/146284.diff 5 Files Affected:
diff --git a/clang/test/Analysis/z3-crosscheck-max-attempts.cpp b/clang/test/Analysis/z3-crosscheck-max-attempts.cpp
index 312e442f23f4f..eb5d0ae0cca19 100644
--- a/clang/test/Analysis/z3-crosscheck-max-attempts.cpp
+++ b/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
diff --git a/clang/test/Analysis/z3/D83660.c b/clang/test/Analysis/z3/D83660.c
index 2ca4a4d0b53e9..58022659e14a2 100644
--- a/clang/test/Analysis/z3/D83660.c
+++ b/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
diff --git a/clang/test/CMakeLists.txt b/clang/test/CMakeLists.txt
index 8baea5b0ca937..483deb0c1b51d 100644
--- a/clang/test/CMakeLists.txt
+++ b/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(
diff --git a/clang/test/lit.cfg.py b/clang/test/lit.cfg.py
index 6375e73f5df82..1957bb1715eb6 100644
--- a/clang/test/lit.cfg.py
+++ b/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")
diff --git a/clang/test/lit.site.cfg.py.in b/clang/test/lit.site.cfg.py.in
index ec0e4aa10ed79..176cf644badcc 100644
--- a/clang/test/lit.site.cfg.py.in
+++ b/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@
|
steakhal
approved these changes
Jun 29, 2025
There was a problem hiding this comment.
Looks really good. Sweet!
Thank you for this patch. If it works then it works.
There is only one thing though.
We have a couple uses of %clang_cc1 and we could substitute when we are at it.
See an example here #145895
I hope you don't mind this nitpicking.
Thank you for your time for fixing this. I couldn't have done it. I'm sure @NagyDonat would say the same.
|
Hmm, but I see it's already part of #145895 — and I think that PR will apply cleanly once this change is made, so I think it's better to keep them separately and focused on a single aspect. |
steakhal
approved these changes
Jun 30, 2025
gentoo-bot
pushed a commit
to gentoo/gentoo
that referenced
this pull request
Jun 30, 2025
Remove the Z3 test hack, as the relevant tests are now fixed upstream. See-also: llvm/llvm-project#146284 Signed-off-by: Michał Górny <[email protected]>
|
@mgorny Thank you very much for developing this more elegant build solution for this mock module! |
flint2
pushed a commit
to flint2/gentoo
that referenced
this pull request
Jun 30, 2025
Remove the Z3 test hack, as the relevant tests are now fixed upstream. See-also: llvm/llvm-project#146284 Signed-off-by: Michał Górny <[email protected]>
|
LLVM Buildbot has detected a new failure on builder Full details are available at: https://lab.llvm.org/buildbot/#/builders/186/builds/10302 Here is the relevant piece of the build log for the reference |
|
No problem. I'm sorry to have caused a merge failure on yours. |
rlavaee
pushed a commit
to rlavaee/llvm-project
that referenced
this pull request
Jul 1, 2025
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)
rlavaee
pushed a commit
to rlavaee/llvm-project
that referenced
this pull request
Jul 1, 2025
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)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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 #145731 (comment)