[analyzer] Fix tests broken by empty %z3_include_dir

[NagyDonat]

This commit should fix the build failure caused by my recent commit 40cc437

[llvmbot]

@llvm/pr-subscribers-clang

@llvm/pr-subscribers-clang-static-analyzer-1

Author: Donát Nagy (NagyDonat)

Changes

This commit should fix the build failure caused by my recent commit 40cc437

---

Full diff: https://github.com/llvm/llvm-project/pull/146042.diff

3 Files Affected:

• (modified) clang/test/Analysis/z3-crosscheck-max-attempts.cpp (+1-1)
• (modified) clang/test/Analysis/z3/D83660.c (+1-1)
• (modified) clang/test/lit.cfg.py (+6-3)

diff --git a/clang/test/Analysis/z3-crosscheck-max-attempts.cpp b/clang/test/Analysis/z3-crosscheck-max-attempts.cpp
index 572e452fdcac2..1c93f32fc21f5 100644
--- a/clang/test/Analysis/z3-crosscheck-max-attempts.cpp
+++ b/clang/test/Analysis/z3-crosscheck-max-attempts.cpp
@@ -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
 
diff --git a/clang/test/Analysis/z3/D83660.c b/clang/test/Analysis/z3/D83660.c
index 0a7c8bab8e345..a24566adbc7d1 100644
--- a/clang/test/Analysis/z3/D83660.c
+++ b/clang/test/Analysis/z3/D83660.c
@@ -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
 //
diff --git a/clang/test/lit.cfg.py b/clang/test/lit.cfg.py
index 24bcdb5b668fc..3d79f44ff8967 100644
--- a/clang/test/lit.cfg.py
+++ b/clang/test/lit.cfg.py
@@ -173,13 +173,16 @@ 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:
+            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"

[github-actions]

✅ With the latest revision this PR passed the Python code formatter.

[steakhal]

I'm not convinced about this change.

[steakhal]

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.

[NagyDonat]

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.

[steakhal]

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.

[NagyDonat]

Thanks for researching this!

[mgorny]

That's not the correct solution. You either need to export these variables from LLVM (implying renaming them to prefix with LLVM namespace), or issue another find_package() in clang standalone block.

[NagyDonat]

Apparently this does not work: #145731 (comment)