[clang] Fix tests requiring Z3 headers in standalone builds (#146200)

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)

Signed-off-by: Michał Górny <[email protected]>

Author: mgorny

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
 

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
 

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

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

clang/test/lit.cfg.py

@@ -201,9 +201,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")
 

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@