[clang] Fix tests requiring Z3 headers in standalone builds

[mgorny]

Fix running tests that require Z3 headers in standalone build. They were wrongly relying on Z3_INCLUDE_DIR being passed through from LLVM, which is not the case for a standalone build. Instead, perform find_package(Z3) again to find Z3 development files and set Z3_INCLUDE_DIR. While at it, handle the possibility that Z3 development package is no longer installed -- run the tests only if both LLVM has been built against Z3, and the headers are still available.

#145731 (comment)

[llvmbot]

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

@llvm/pr-subscribers-clang

Author: Michał Górny (mgorny)

Changes

Fix running tests that require Z3 headers in standalone build. They were wrongly relying on Z3_INCLUDE_DIR being passed through from LLVM, which is not the case for a standalone build. Instead, perform find_package(Z3) again to find Z3 development files and set Z3_INCLUDE_DIR. While at it, handle the possibility that Z3 development package is no longer installed -- run the tests only if both LLVM has been built against Z3, and the headers are still available.

#145731 (comment)

---

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

6 Files Affected:

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

diff --git a/clang/CMakeLists.txt b/clang/CMakeLists.txt
index 94607a8e8473c..1bb73599970c1 100644
--- a/clang/CMakeLists.txt
+++ b/clang/CMakeLists.txt
@@ -150,6 +150,12 @@ if(CLANG_BUILT_STANDALONE)
     endif()
 
     umbrella_lit_testsuite_begin(check-all)
+
+    # If LLVM was built with Z3, check if we still have the headers around.
+    # They are used by a few tests.
+    if (LLVM_WITH_Z3)
+      find_package(Z3 4.8.9)
+    endif()
   endif() # LLVM_INCLUDE_TESTS
 endif() # standalone
 
diff --git a/clang/test/Analysis/z3-crosscheck-max-attempts.cpp b/clang/test/Analysis/z3-crosscheck-max-attempts.cpp
index 572e452fdcac2..312e442f23f4f 100644
--- a/clang/test/Analysis/z3-crosscheck-max-attempts.cpp
+++ b/clang/test/Analysis/z3-crosscheck-max-attempts.cpp
@@ -32,7 +32,7 @@
 // RUN: Z3_SOLVER_RESULTS="UNDEF,UNDEF,SAT"   %{mocked_clang} %{attempts}=3 -verify=accepted
 
 
-// REQUIRES: z3, asserts, shell, system-linux
+// REQUIRES: z3, z3-devel, asserts, shell, system-linux
 
 // refuted-no-diagnostics
 
diff --git a/clang/test/Analysis/z3/D83660.c b/clang/test/Analysis/z3/D83660.c
index 0a7c8bab8e345..2ca4a4d0b53e9 100644
--- a/clang/test/Analysis/z3/D83660.c
+++ b/clang/test/Analysis/z3/D83660.c
@@ -8,7 +8,7 @@
 // RUN: %clang_cc1 -analyze -analyzer-constraints=z3 -setup-static-analyzer \
 // RUN:   -analyzer-checker=core %s -verify
 //
-// REQUIRES: z3, asserts, shell, system-linux
+// REQUIRES: z3, z3-devel, 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 e5b4a3bb84645..8baea5b0ca937 100644
--- a/clang/test/CMakeLists.txt
+++ b/clang/test/CMakeLists.txt
@@ -29,6 +29,14 @@ llvm_canonicalize_cmake_booleans(
   LLVM_EXPERIMENTAL_KEY_INSTRUCTIONS
   )
 
+# 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)
+endif()
+
 configure_lit_site_cfg(
   ${CMAKE_CURRENT_SOURCE_DIR}/lit.site.cfg.py.in
   ${CMAKE_CURRENT_BINARY_DIR}/lit.site.cfg.py
diff --git a/clang/test/lit.cfg.py b/clang/test/lit.cfg.py
index 24bcdb5b668fc..7730e45b9686e 100644
--- a/clang/test/lit.cfg.py
+++ b/clang/test/lit.cfg.py
@@ -175,9 +175,11 @@ def have_host_clang_repl_cuda():
 
     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_devel:
+            config.available_features.add("z3-devel")
+            config.substitutions.append(
+                ("%z3_include_dir", config.clang_staticanalyzer_z3_include_dir)
+            )
     else:
         config.available_features.add("no-z3")
 
diff --git a/clang/test/lit.site.cfg.py.in b/clang/test/lit.site.cfg.py.in
index 00480d34852da..ec0e4aa10ed79 100644
--- a/clang/test/lit.site.cfg.py.in
+++ b/clang/test/lit.site.cfg.py.in
@@ -27,6 +27,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_enable_cir = @CLANG_ENABLE_CIR@
 config.clang_examples = @CLANG_BUILD_EXAMPLES@

[steakhal]

Thank you for doing this extra mile. I really appreciate it.

I had a look at the patch and it makes sense. Looks good.

[mgorny]

Thanks for the prompt review!