shylie/llvm-project
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

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

Browse Source 
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
https://github.com/llvm/llvm-project/pull/145731#issuecomment-3015197983
This commit is contained in:
Michał Górny 2025-06-30 10:57:35 +02:00 committed by GitHub
parent af82e14c4a
commit b42c8831d5
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
5 changed files with 25 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
clang/test/Analysis/z3-crosscheck-max-attempts.cpp
View File

@ -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

9
clang/test/Analysis/z3/D83660.c
View File

@ -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

18
clang/test/CMakeLists.txt
View File

@ -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(

10
clang/test/lit.cfg.py
View File

@ -201,11 +201,8 @@ if config.clang_staticanalyzer:
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 @@ config.substitutions.append(
)
)
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")

5
clang/test/lit.site.cfg.py.in
View File

@ -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@