Skip to content

[analyzer] Fix tests broken by empty %z3_include_dir #146042

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 2 commits into from
Closed

[analyzer] Fix tests broken by empty %z3_include_dir #146042

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
b7bfc54
[analyzer] Fix tests broken by empty %z3_include_dir
NagyDonat Jun 27, 2025
e4e8428
Satisfy darker code formatting
NagyDonat Jun 27, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion clang/test/Analysis/z3-crosscheck-max-attempts.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
// 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: %host_cxx -shared -fPIC %I_z3_include_dir \
// RUN: %S/z3/Inputs/MockZ3_solver_check.cpp \
// RUN: -o %t/MockZ3_solver_check.so

Expand Down
2 changes: 1 addition & 1 deletion clang/test/Analysis/z3/D83660.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// RUN: rm -rf %t && mkdir %t
// RUN: %host_cxx -shared -fPIC -I %z3_include_dir \
// RUN: %host_cxx -shared -fPIC %I_z3_include_dir \
// RUN: %S/Inputs/MockZ3_solver_check.cpp \
// RUN: -o %t/MockZ3_solver_check.so
//
Expand Down
7 changes: 4 additions & 3 deletions clang/test/lit.cfg.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -173,13 +173,14 @@ def have_host_clang_repl_cuda():
config.available_features.add("staticanalyzer")
tools.append("clang-check")

I_z3_include_dir = ""
if config.clang_staticanalyzer_z3:
config.available_features.add("z3")
config.substitutions.append(
("%z3_include_dir", config.clang_staticanalyzer_z3_include_dir)
)
if config.clang_staticanalyzer_z3_include_dir:
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't the presence of config.clang_staticanalyzer_z3 imply the presence of config.clang_staticanalyzer_z3_include_dir?

The problem I see here is that the clang/test/Analysis/z3-crosscheck-max-attempts.cpp test case would not compile without the necessary Z3 include dir. So config.clang_staticanalyzer_z3 should imply config.clang_staticanalyzer_z3_include_dir. Otherwise the REQUIRES: z3 filter would not cover the test case and still fail. In conclusion, substituting I_z3_include_dir to an empty string is not the right solution. It can't be.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't the presence of config.clang_staticanalyzer_z3 imply the presence of config.clang_staticanalyzer_z3_include_dir?

This is what I would've assumed, but the build failure reported by @mgorny strongly suggests that this is not always true. My current suspicion is that if Z3 is installed in some standard include directory, then the clang build system autodetects that Z3 is available (it tries to compile a simple C source file, and that experiment succeeds if Z3 is available in the default include path), but somehow doesn't determine Z3_INCLUDE_DIR.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you check llvm/cmake/modules/FindZ3.cmake, then you can see that Z3_INCLUDE_DIR and Z3_LIBRARIES cmake variables must be defined if Z3 is detected.

By judging this section of code from llvm/CMakeLists.txt:

option(LLVM_ENABLE_Z3_SOLVER
  "Enable Support for the Z3 constraint solver in LLVM."
  ${LLVM_ENABLE_Z3_SOLVER_DEFAULT}
)

if (LLVM_ENABLE_Z3_SOLVER)
  find_package(Z3 4.8.9)

  if (LLVM_Z3_INSTALL_DIR)
    if (NOT Z3_FOUND)
      message(FATAL_ERROR "Z3 >= 4.8.9 has not been found in LLVM_Z3_INSTALL_DIR: ${LLVM_Z3_INSTALL_DIR}.")
    endif()
  endif()

  if (NOT Z3_FOUND)
    message(FATAL_ERROR "LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available.")
  endif()

  set(LLVM_WITH_Z3 1)
endif()

set(LLVM_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}")

I think LLVM_WITH_Z3 can only be true if Z3_FOUND is true, which is only the case if find_package(Z3 4.8.9) find Z3 when executing llvm/cmake/modules/FindZ3.cmake, which defines the Z3_INCLUDE_DIR and Z3_LIBRARIES variables.
It has checks that Z3_INCLUDE_DIR must exist and contain a file called z3_version.h.

So in sight of this, I don't think there is anything to be fixed here.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for researching this!

I_z3_include_dir = '-I "%s"' % config.clang_staticanalyzer_z3_include_dir
else:
config.available_features.add("no-z3")
config.substitutions.append(("%I_z3_include_dir", I_z3_include_dir))

check_analyzer_fixit_path = os.path.join(
config.test_source_root, "Analysis", "check-analyzer-fixit.py"
Expand Down
Loading