[analyzer] Rework Z3 requirements in the CSA testsuite

[steakhal]

Summary

Summary:

• rename the USE_Z3_SOLVER llvm-lit parameter to RECHECK_WITH_Z3_SOLVER to reflect its behavior
• document the RECHECK_WITH_Z3_SOLVER parameter in the checker_dev_manual.html
• introduce the %clang_analyze_cc1_range and %clang_analyze_cc1_z3 substitutions to control the constraint manager used for the test
• FIX the REQUIRES: z3 expressions in tests (before the patch it wanted to mean something like "only run this test if we use the Z3 constraint manager"; after the patch "is clang build with z3?")
• FIX a bunch of tests, specifying the required constraint manager, and z3 requirement if needed
• DELETE z3/enabled.c test, since that no longer serves any purpose - IMO

Before the patch:

Using ./bin/llvm-lit -sv --param USE_Z3_SOLVER=0 ...../test/Analysis --show-unsupported --show-xfail:

Unsupported Tests (6):
  Clang :: Analysis/PR24184.cpp
  Clang :: Analysis/PR37855.c
  Clang :: Analysis/exploded-graph-rewriter/win_path_forbidden_chars.cpp
  Clang :: Analysis/trustnonnullchecker_test.m
  Clang :: Analysis/z3-crosscheck.c
  Clang :: Analysis/z3/enabled.c

********************
Expectedly Failed Tests (5):
  Clang :: Analysis/container-modeling-no-aggressive-binary-operation-simplification-warn.cpp
  Clang :: Analysis/iterator-modeling-no-aggressive-binary-operation-simplification-no-crash.cpp
  Clang :: Analysis/outofbound-notwork.c
  Clang :: Analysis/redecl.c
  Clang :: Analysis/string-fail.c


Testing Time: 80.68s
  Unsupported      :   6
  Passed           : 716
  Expectedly Failed:   5

---

Using ./bin/llvm-lit -sv --param USE_Z3_SOLVER=1 ...../test/Analysis --show-unsupported --show-xfail:

Unsupported Tests (3):
  Clang :: Analysis/PR24184.cpp
  Clang :: Analysis/exploded-graph-rewriter/win_path_forbidden_chars.cpp
  Clang :: Analysis/trustnonnullchecker_test.m

********************
Expectedly Failed Tests (5):
  Clang :: Analysis/container-modeling-no-aggressive-binary-operation-simplification-warn.cpp
  Clang :: Analysis/iterator-modeling-no-aggressive-binary-operation-simplification-no-crash.cpp
  Clang :: Analysis/outofbound-notwork.c
  Clang :: Analysis/redecl.c
  Clang :: Analysis/string-fail.c

********************
Failed Tests (7):
  Clang :: Analysis/constant-folding.c
  Clang :: Analysis/container-modeling.cpp
  Clang :: Analysis/dump_egraph.c
  Clang :: Analysis/expr-inspection.c
  Clang :: Analysis/iterator-modeling.cpp
  Clang :: Analysis/loop-unrolling.cpp
  Clang :: Analysis/plist-macros.cpp


Testing Time: 236.37s
  Unsupported      :   3
  Passed           : 712
  Expectedly Failed:   5
  Failed           :   7

---

After the patch:

Using ./bin/llvm-lit -sv --param RECHECK_WITH_Z3_SOLVER=0 ...../test/Analysis --show-unsupported --show-xfail:

Unsupported Tests (1):
  Clang :: Analysis/exploded-graph-rewriter/win_path_forbidden_chars.cpp

********************
Expectedly Failed Tests (5):
  Clang :: Analysis/container-modeling-no-aggressive-binary-operation-simplification-warn.cpp
  Clang :: Analysis/iterator-modeling-no-aggressive-binary-operation-simplification-no-crash.cpp
  Clang :: Analysis/outofbound-notwork.c
  Clang :: Analysis/redecl.c
  Clang :: Analysis/string-fail.c


Testing Time: 99.74s
  Unsupported      :   1
  Passed           : 720
  Expectedly Failed:   5

---

Using ./bin/llvm-lit -sv --param RECHECK_WITH_Z3_SOLVER=1 ...../test/Analysis --show-unsupported --show-xfail:

Unsupported Tests (1):
  Clang :: Analysis/exploded-graph-rewriter/win_path_forbidden_chars.cpp

********************
Expectedly Failed Tests (5):
  Clang :: Analysis/container-modeling-no-aggressive-binary-operation-simplification-warn.cpp
  Clang :: Analysis/iterator-modeling-no-aggressive-binary-operation-simplification-no-crash.cpp
  Clang :: Analysis/outofbound-notwork.c
  Clang :: Analysis/redecl.c
  Clang :: Analysis/string-fail.c

********************
Failed Tests (2):
  Clang :: Analysis/container-modeling.cpp
  Clang :: Analysis/iterator-modeling.cpp


Testing Time: 255.49s
  Unsupported      :   1
  Passed           : 718
  Expectedly Failed:   5
  Failed           :   2

Before and after the patch, the container-modeling.cpp and iterator-modeling.cpp were crashing using the Z3 constraint manager.
Worth to have a look at those in the future, if we think that the Z3 constraint manager worth the investment.

[steakhal]

• use the %clang_analyze_cc1_range in PR37855.c

[Szelethus]

I lack the confidence to accept this straight away, but the overall direction looks great. LGTM!

You're going to be very popular around here with these patches! :)

clang/test/Analysis/trustnonnullchecker_test.m

1–3

Why did you delete this? @NoQ, is D57062 related?

clang/www/analyzer/checker_dev_manual.html

6

This menu is still not working, right?

548–550

What is the difference in between clang_analyze_cc1 and clang_analyze_cc1_range then?

548–550

I meant to delete this inline, oops :)

[steakhal]

Thanks for the really fast feedback @Szelethus!

Should we prefer using %clang_analyze_cc1 over raw %clang_cc1 invocations with the -analyze flag? And fall back to the more specific %clang_analyze_cc1_range/%clang_analyze_cc1_z3, if the test turns out, requires a certain constraint manager?
If so, I started to update some tests according to this, and a few questions raised during that process.

• Which should we use for example the analyzer-enabled-checkers.c, which only prints the enabled checkers?

• There is also an interesting behavior about command-line parsing. [1]

---

[1]: AFAIK flags should not be position dependant.
But moving the -analyze flag around makes this test fail.

PASS:
./bin/clang -cc1 -internal-isystem ./lib/clang/11.0.0/include -nostdsysteminc -analyzer-constraints=range -setup-static-analyzer -fsyntax-only -analyze -analyzer-checker=core,debug.ExprInspection ../../clang/test/Analysis/handle_constructors_with_new_array.cpp -verify

After moving the -analyze after the -nostdsysteminc flag, it FAILs:
./bin/clang -cc1 -internal-isystem ./lib/clang/11.0.0/include -nostdsysteminc -analyze -analyzer-constraints=range -setup-static-analyzer -fsyntax-only -analyzer-checker=core,debug.ExprInspection ../../clang/test/Analysis/handle_constructors_with_new_array.cpp -verify

Could someone tell me the difference?

clang/www/analyzer/checker_dev_manual.html

6

IDK. But I don't really want to touch any css/js related things :D

[steakhal]

@Szelethus Can you vaguely remember why did we keep the invalid-analyzer-config-value.c test if the invalid-a-na-ly-zer-con-fig-value.c has the very same content?
IMO we should only keep the former with a description why has the file such a weird name :D

[NoQ]

Folks, please announce your overall plan for Z3 (unless i missed it). It looks like you are planning to actively support Z3 as a constraint manager, i.e. invoke it on every assume()? Did you consider my usual suggestion to only apply it to refuting non-buggy states in order to combat your false negatives similarly to how our current Z3 refutation refutes buggy states to combat false positives?

clang/www/analyzer/checker_dev_manual.html

534

Yeah, just delete this :)

llvm/utils/lit/lit/llvm/config.py

412–413

I'm for longer names, "range" is too vague, "z3" is already ambiguous (does it mean as constraint manager or for refutation?).

%clang_analyze_cc1_range_cm_only would probably make more sense. It also looks more like a FIXME and tells that something's wrong with the test.

[steakhal]

In D83677#2148435, @NoQ wrote:

[...] It looks like you are planning to actively support Z3 as a constraint manager. [...] Did you consider my usual suggestion to only apply it to refuting non-buggy states in order to combat your false negatives similarly to how our current Z3 refutation refutes buggy states to combat false positives?

I don't plan to invest time to support Z3-CM.

Although, I highly value the refutation infrastructure. TBH this patch focused fixing the test-infra to be able to have tests explicitly testing refutation related warnings.
Please note that previously you could not require z3 and only run the test using the range-CM. Using also the Z3-CM would not emit warning for that case, making the test fail.
Besides fixing this (which was my primary object), adds new ToolSubsts in a backward-compatible manner to let the test author specify explicitly the CM of their choice.

clang/www/analyzer/checker_dev_manual.html

534

Is the ninja check-clang-analysis the prefered way running the test?
I will reword the doc then.

llvm/utils/lit/lit/llvm/config.py

412–413

I'm for longer names, "range" is too vague, "z3" is already ambiguous (does it mean as constraint manager or for refutation?).

If we don't expect the clangSA dev to be able to differentiate, why should we expect them to know what 'cm' means there?
I'm not against longer names, but kinda hard to strike the balance for finding short but descriptive names.

A lengthy ToolSubst would consume most of the available space in the line, rendering most of the RUN commands to span across multiple lines.

[...] It also looks more like a FIXME and tells that something's wrong with the test.

I don't think that should be suspicious.
I wouldn't assume that test is wrong, simply that test works only with the range-CM.

clang/test/Analysis/PR24184.cpp

-// UNSUPPORTED: z3
-// RUN: %clang_analyze_cc1 -w -fcxx-exceptions -analyzer-checker=core -analyzer-checker=alpha.core.PointerArithm,alpha.core.CastToStruct -analyzer-max-loop 64 -verify %s
-// RUN: %clang_analyze_cc1 -w -analyzer-checker=core -analyzer-checker=cplusplus -fcxx-exceptions -analyzer-checker alpha.core.PointerArithm,alpha.core.CastToStruct -analyzer-max-loop 63 -verify %s
+// RUN: %clang_analyze_cc1_range -w -fcxx-exceptions -analyzer-max-loop 64 -verify %s \
+// RUN:   -analyzer-checker=core,alpha.core.PointerArithm,alpha.core.CastToStruct
+//
+// RUN: %clang_analyze_cc1_range -w -fcxx-exceptions -analyzer-max-loop 63 -verify %s \
+// RUN:   -analyzer-checker=core,alpha.core.PointerArithm,alpha.core.CastToStruct,cplusplus
 
 // These tests used to hit an assertion in the bug report. Test case from http://llvm.org/PR24184.
 typedef struct {
   int cbData;
   unsigned pbData;
 } CRYPT_DATA_BLOB;
 
 typedef enum { DT_NONCE_FIXED } DATA_TYPE;

clang/test/Analysis/PR37855.c

-// RUN: %clang_cc1 -analyze -analyzer-checker=core -w -DNO_CROSSCHECK -verify %s
-// RUN: %clang_cc1 -analyze -analyzer-checker=core -w -analyzer-config crosscheck-with-z3=true -verify %s
+// RUN: %clang_analyze_cc1_range -analyzer-checker=core -w -verify %s
+// RUN: %clang_analyze_cc1_range -analyzer-checker=core -w -verify %s -analyzer-config crosscheck-with-z3=true
 // REQUIRES: z3
 
 typedef struct o p;
 struct o {
   struct {
   } s;
 };
 

clang/test/Analysis/analyzer_test.py

 import lit.formats
 import lit.TestRunner
 
 # Custom format class for static analyzer tests
 class AnalyzerTest(lit.formats.ShTest):
 
-    def __init__(self, execute_external, use_z3_solver=False):
+    def __init__(self, execute_external, recheck_with_z3_solver=False):
         super(AnalyzerTest, self).__init__(execute_external)
-        self.use_z3_solver = use_z3_solver
+        self.recheck_with_z3_solver = recheck_with_z3_solver
 
     def execute(self, test, litConfig):
         results = []
 
         # Parse any test requirements ('REQUIRES: ')
         saved_test = test
         lit.TestRunner.parseIntegratedTestScript(test)
 
-        if 'z3' not in test.requires:
-            results.append(self.executeWithAnalyzeSubstitution(
-                saved_test, litConfig, '-analyzer-constraints=range'))
+        results.append(self.executeWithConstraintManagerSubstitution(
 
-            if results[-1].code == lit.Test.FAIL:
-                return results[-1]
 
-        # If z3 backend available, add an additional run line for it
-        if self.use_z3_solver == '1':
+        # If we want to rerun the test with the Z3 solver, add an additional run line for it
+        if self.recheck_with_z3_solver == '1':
             assert(test.config.clang_staticanalyzer_z3 == '1')
-            results.append(self.executeWithAnalyzeSubstitution(
+            results.append(self.executeWithConstraintManagerSubstitution(
                 saved_test, litConfig, '-analyzer-constraints=z3 -DANALYZER_CM_Z3'))
 
         # Combine all result outputs into the last element
         for x in results:
             if x != results[-1]:
                 results[-1].output = x.output + results[-1].output
 
         if results:
             return results[-1]
         return lit.Test.Result(lit.Test.UNSUPPORTED,
             "Test requires the following unavailable features: z3")
 
-    def executeWithAnalyzeSubstitution(self, test, litConfig, substitution):
+    def executeWithConstraintManagerSubstitution(self, test, litConfig, substitution):
         saved_substitutions = list(test.config.substitutions)
-        test.config.substitutions.append(('%analyze', substitution))
+        test.config.substitutions.append(('%constraint_manager', substitution))
         result = lit.TestRunner.executeShTest(test, litConfig,
             self.execute_external)
         test.config.substitutions = saved_substitutions
 
         return result

clang/test/Analysis/constant-folding.c

-// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify -analyzer-config eagerly-assume=false %s
+// RUN: %clang_analyze_cc1_range -analyzer-config eagerly-assume=false -verify %s \
+// RUN:   -analyzer-checker=core,debug.ExprInspection
 
 #define UINT_MAX (~0U)
 #define INT_MAX (int)(UINT_MAX & (UINT_MAX >> 1))
 #define INT_MIN (int)(UINT_MAX & ~(UINT_MAX >> 1))
 
 void clang_analyzer_eval(int);
 
 // There should be no warnings unless otherwise indicated.

clang/test/Analysis/dump_egraph.c

-// RUN: %clang_analyze_cc1 -analyzer-checker=core \
-// RUN:  -analyzer-dump-egraph=%t.dot %s
+// RUN: %clang_analyze_cc1_range -analyzer-checker=core \
+// RUN:   -analyzer-dump-egraph=%t.dot %s
 // RUN: cat %t.dot | FileCheck %s
-
-// RUN: %clang_analyze_cc1 -analyzer-checker=core \
-// RUN:  -analyzer-dump-egraph=%t.dot \
-// RUN:  -trim-egraph %s
+//
+// RUN: %clang_analyze_cc1_range -analyzer-checker=core \
+// RUN:   -analyzer-dump-egraph=%t.dot \
+// RUN:   -trim-egraph %s
 // RUN: cat %t.dot | FileCheck %s
-
+//
 // REQUIRES: asserts
 
 int getJ();
 
 int foo() {
   int *x = 0, *y = 0;
   char c = '\x13';
 

clang/test/Analysis/expr-inspection.c

-// RUN: %clang_analyze_cc1 \
-// RUN:  -analyzer-checker=debug.ExprInspection \
-// RUN:  -verify %s 2>&1 | FileCheck %s
-
+// RUN: %clang_analyze_cc1_range -analyzer-checker=debug.ExprInspection -verify %s 2>&1 | FileCheck %s
+//
 // Self-tests for the debug.ExprInspection checker.
 
 void clang_analyzer_dump(int x);
 void clang_analyzer_dump_pointer(int *p);
 void clang_analyzer_printState();
 void clang_analyzer_numTimesReached();
 
 void foo(int x) {

clang/test/Analysis/lit.local.cfg

 # -*- Python -*- vim: set ft=python ts=4 sw=4 expandtab tw=79:
 
 import site
 
 # Load the custom analyzer test format, which runs the test again with Z3 if it
 # is available.
 site.addsitedir(os.path.dirname(__file__))
 import analyzer_test
 config.test_format = analyzer_test.AnalyzerTest(
-        config.test_format.execute_external, config.use_z3_solver)
+        config.test_format.execute_external, config.recheck_with_z3_solver)
 
 # Filtering command used by Clang Analyzer tests (when comparing .plist files
 # with reference output)
 config.substitutions.append(('%normalize_plist',
     "grep -Ev '%s|%s|%s'" %
         ('^[[:space:]]*<string>.* version .*</string>[[:space:]]*$',
          '^[[:space:]]*<string>/.*</string>[[:space:]]*$',
          '^[[:space:]]*<string>.:.*</string>[[:space:]]*$')))

clang/test/Analysis/loop-unrolling.cpp

-// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -analyzer-config unroll-loops=true,cfg-loopexit=true -verify -std=c++11 -analyzer-config exploration_strategy=unexplored_first_queue %s
-// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -analyzer-config unroll-loops=true,cfg-loopexit=true,exploration_strategy=dfs -verify -std=c++11 -DDFS=1 %s
+// RUN: %clang_analyze_cc1_range -verify=expected,ufq -std=c++11 %s \
+// RUN:   -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config unroll-loops=true,cfg-loopexit=true,exploration_strategy=unexplored_first_queue
+//
+// RUN: %clang_analyze_cc1_range -verify=expected,dfs -std=c++11 %s \
+// RUN:   -analyzer-checker=core,debug.ExprInspection \
+// RUN:   -analyzer-config unroll-loops=true,cfg-loopexit=true,exploration_strategy=dfs
 
 void clang_analyzer_numTimesReached();
 void clang_analyzer_warnIfReached();
 
 int getNum();
 void foo(int &);
 
 int simple_unroll1() {
for (int i = 2; i < 12; i++) {
     // This function is inlined in nested_inlined_unroll1()
     clang_analyzer_numTimesReached(); // expected-warning {{90}}
   }
   return 0;
 }
 
 int simple_unknown_bound_loop() {
   for (int i = 2; i < getNum(); i++) {
-#ifdef DFS
-    clang_analyzer_numTimesReached(); // expected-warning {{16}}
-#else
-    clang_analyzer_numTimesReached(); // expected-warning {{8}}
-#endif
+    clang_analyzer_numTimesReached();
+    // dfs-warning@-1 {{16}}
+    // ufq-warning@-2 {{8}}
   }
   return 0;
 }
 
 int nested_inlined_unroll1() {
   int k;
   for (int i = 0; i < 9; i++) {
     clang_analyzer_numTimesReached(); // expected-warning {{9}}
     k = simple_known_bound_loop();    // no reevaluation without inlining
   }
   int a = 22 / k; // expected-warning {{Division by zero}}
   return 0;
 }
 
 int nested_inlined_no_unroll1() {
   int k;
   for (int i = 0; i < 9; i++) {
-#ifdef DFS
-    clang_analyzer_numTimesReached(); // expected-warning {{18}}
-#else
-    clang_analyzer_numTimesReached(); // expected-warning {{14}}
-#endif
+    clang_analyzer_numTimesReached();
+    // dfs-warning@-1 {{18}}
+    // ufq-warning@-2 {{14}}
     k = simple_unknown_bound_loop();  // reevaluation without inlining, splits the state as well
   }
   int a = 22 / k; // no-warning
   return 0;
 }
 
 int recursion_unroll1(bool b) {
   int k = 2;

clang/test/Analysis/plist-macros.cpp

-// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -verify %s
-// RUN: %clang_analyze_cc1 -analyzer-checker=core,unix -analyzer-output=plist-multi-file %s -o %t.plist
+// RUN: %clang_analyze_cc1_range -analyzer-checker=core,unix -verify %s
+// RUN: %clang_analyze_cc1_range -analyzer-checker=core,unix -analyzer-output=plist-multi-file %s -o %t.plist
 // RUN: %normalize_plist <%t.plist | diff -ub %S/Inputs/expected-plists/plist-macros.cpp.plist -
 
 
 typedef __typeof(sizeof(int)) size_t;
 void *malloc(size_t);
 
 #define mallocmemory int *x = (int*)malloc(12);
 void noteOnMacro(int y) {

clang/test/Analysis/trustnonnullchecker_test.m

-// Temporarily disabling the test, it failes the "system is over-constrained"
-// assertion in *non* optimized builds.
-// REQUIRES: rdar44992170
-// RUN: %clang_analyze_cc1 -fblocks -analyze -analyzer-checker=core,nullability,apiModeling,debug.ExprInspection  -verify %s
+// RUN: %clang_analyze_cc1 -fblocks -analyze -analyzer-checker=core,nullability,apiModeling,debug.ExprInspection -verify %s
 
 #include "Inputs/system-header-simulator-for-nullability.h"
 
 void clang_analyzer_warnIfReached();
 
 NSString* _Nonnull trust_nonnull_framework_annotation() {
   NSString* out = [NSString generateString];
   if (out) {}

clang/test/Analysis/z3/enabled.c

-// REQUIRES: z3
-// RUN: echo %clang_analyze_cc1 | FileCheck %s
-// CHECK: -analyzer-constraints=z3

clang/test/CMakeLists.txt

list(APPEND CLANG_TEST_DEPS
     Attribute
     AnnotateFunctions
     clang-interpreter
     PrintFunctionNames
     )
 endif ()
 
 set(CLANG_TEST_PARAMS
-  USE_Z3_SOLVER=0
+  RECHECK_WITH_Z3_SOLVER=0
   )
 
 if( NOT CLANG_BUILT_STANDALONE )
   list(APPEND CLANG_TEST_DEPS
     llvm-config
     FileCheck count not
     llc
     llvm-as

clang/test/lit.site.cfg.py.in

 config.clang_staticanalyzer_z3 = "@LLVM_WITH_Z3@"
 config.clang_examples = @CLANG_BUILD_EXAMPLES@
 config.enable_shared = @ENABLE_SHARED@
 config.enable_backtrace = @ENABLE_BACKTRACES@
 config.enable_experimental_new_pass_manager = @ENABLE_EXPERIMENTAL_NEW_PASS_MANAGER@
 config.enable_threads = @LLVM_ENABLE_THREADS@
 config.host_arch = "@HOST_ARCH@"
 config.python_executable = "@Python3_EXECUTABLE@"
-config.use_z3_solver = lit_config.params.get('USE_Z3_SOLVER', "@USE_Z3_SOLVER@")
+config.recheck_with_z3_solver = lit_config.params.get('RECHECK_WITH_Z3_SOLVER', "@RECHECK_WITH_Z3_SOLVER@")
 config.has_plugins = @LLVM_ENABLE_PLUGINS@
 config.clang_vendor_uti = "@CLANG_VENDOR_UTI@"
 
 # Support substitution of the tools and libs dirs with user parameters. This is
 # used when we can't determine the tool dir at configuration time.
 try:
     config.clang_tools_dir = config.clang_tools_dir % lit_config.params
     config.llvm_tools_dir = config.llvm_tools_dir % lit_config.params

clang/www/analyzer/checker_dev_manual.html

 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN"
           "http://www.w3.org/TR/html4/strict.dtd">
 <html>
 <head>
   <title>Checker Developer Manual</title>
   <link type="text/css" rel="stylesheet" href="menu.css">
   <link type="text/css" rel="stylesheet" href="content.css">
   <script type="text/javascript" src="scripts/menu.js"></script>
 </head>
 <body>
 
 <div id="page">
 <!--#include virtual="menu.html.incl"-->
 
<h2 id=ast>AST Visitors</h2>
   situation, AST callbacks <tt><b>checkASTDecl</b></tt> and
   <tt><b>checkASTCodeBody</b></tt> are your best friends.
 
 <h2 id=testing>Testing</h2>
   Every patch should be well tested with Clang regression tests. The checker tests
   live in <tt>clang/test/Analysis</tt> folder. To run all of the analyzer tests,
   execute the following from the <tt>clang</tt> build directory:
     <pre class="code">
     $ <b>bin/llvm-lit -sv ../llvm/tools/clang/test/Analysis</b>
     </pre>
+  Or you can simply use the corresponding ninja target to achieve this:
+    <pre class="code">
+    $ <b>ninja check-clang-analysis</b>
+    </pre>
+
+  Tests that require the Z3 constraint manager won't run since those would require too much time.
+  It will require clang to be built with the Z3 though.
+  You can enable these tests by an explicit llvm-lit parameter:
+    <pre class="code">
+    $ <b>bin/llvm-lit -sv ../llvm/tools/clang/test/Analysis --param RECHECK_WITH_Z3_SOLVER=1</b>
+    </pre>
+
+  The <tt>RECHECK_WITH_Z3_SOLVER</tt> parameter lets the testsuite to use both
+  constraint managers, which are substituted by the <tt>%clang_analyze_cc1</tt>
+  in each <tt>RUN</tt> line.
+  Your test can explicitly require a specific constraint manager using either
+  <tt>%clang_analyze_cc1_range</tt> or <tt>%clang_analyze_cc1_z3</tt> if that won't
+  work with both of them.
 
 <h2 id=commands>Useful Commands/Debugging Hints</h2>
 
 <h3 id=attaching>Attaching the Debugger</h3>
 
 <p>When your command contains the <tt><b>-cc1</b></tt> flag, you can attach the
 debugger to it directly:</p>
 

llvm/utils/gn/secondary/clang/test/BUILD.gn

extra_values = [
     # builds exist, to make sure it's a toolchain var.
     "CMAKE_CXX_COMPILER=c++",
     "ENABLE_BACKTRACES=1",
     "ENABLE_EXPERIMENTAL_NEW_PASS_MANAGER=0",
     "LLVM_HOST_TRIPLE=$llvm_current_triple",
     "LLVM_LIT_TOOLS_DIR=",  # Intentionally empty, matches cmake build.
     "LLVM_USE_SANITIZER=",
     "Python3_EXECUTABLE=$python_path",
-    "USE_Z3_SOLVER=",
+    "RECHECK_WITH_Z3_SOLVER=",
   ]
 
   if (clang_enable_arcmt) {
     extra_values += [ "CLANG_ENABLE_ARCMT=1" ]
   } else {
     extra_values += [ "CLANG_ENABLE_ARCMT=0" ]
   }
 

llvm/utils/lit/lit/llvm/config.py

def use_clang(self, additional_tool_dirs=[], additional_flags=[], required=True):
         if shl:
             self.config.substitutions.append(('%llvmshlibdir', shl))
         if pext:
             self.config.substitutions.append(('%pluginext', pext))
 
         builtin_include_dir = self.get_clang_builtin_include_dir(self.config.clang)
         tool_substitutions = [
             ToolSubst('%clang', command=self.config.clang, extra_args=additional_flags),
-            ToolSubst('%clang_analyze_cc1', command='%clang_cc1', extra_args=['-analyze', '%analyze', '-setup-static-analyzer']+additional_flags),
+            ToolSubst('%clang_analyze_cc1_range', command='%clang_cc1', extra_args=['-analyze', '-analyzer-constraints=range', '-setup-static-analyzer']+additional_flags),
+            ToolSubst('%clang_analyze_cc1_z3', command='%clang_cc1', extra_args=['-analyze', '-analyzer-constraints=z3', '-setup-static-analyzer']+additional_flags),
+            ToolSubst('%clang_analyze_cc1', command='%clang_cc1', extra_args=['-analyze', '%constraint_manager', '-setup-static-analyzer']+additional_flags),
             ToolSubst('%clang_cc1', command=self.config.clang, extra_args=['-cc1', '-internal-isystem', builtin_include_dir, '-nostdsysteminc']+additional_flags),
             ToolSubst('%clang_cpp', command=self.config.clang, extra_args=['--driver-mode=cpp']+additional_flags),
             ToolSubst('%clang_cl', command=self.config.clang, extra_args=['--driver-mode=cl']+additional_flags),
             ToolSubst('%clangxx', command=self.config.clang, extra_args=['--driver-mode=g++']+additional_flags),
             ]
         self.add_tool_substitutions(tool_substitutions)
 
         self.config.substitutions.append(('%itanium_abi_triple',