[analyzer] Don't crash if the analyzer-constraint is set to Z3, but llvm is not built with it

[Szelethus]

Summary

Exactly what it says on the tin! We had a nasty crash with the following incovation:

$ clang --analyze -Xclang -analyzer-constraints=z3 test.c
fatal error: error in backend: LLVM was not compiled with Z3 support, rebuild with -DLLVM_ENABLE_Z3_SOLVER=ON
... <stack trace> ...

[steakhal]

Thanks. LGTM.

Besides abusing the -analyzer-constraints=z3 option we should really have some way displaying whether or not this clang was built w/o Z3.

I'm accepting this, given that you fix the conditional code segment.

clang/lib/Frontend/CompilerInvocation.cpp

918–922

This define is produced by the llvm/include/llvm/Config/llvm-config.h.cmake cmake configuration file.

/* Define if we have z3 and want to build it */
#cmakedefine LLVM_WITH_Z3 ${LLVM_WITH_Z3}

And according to the cmake configure_file
#cmakedefine VAR ... will be either defined or not defined.

clang/include/clang/Basic/DiagnosticDriverKinds.td

def err_analyzer_config_invalid_input : Error<
   "invalid input for analyzer-config option '%0', that expects %1 value">;
 def err_analyzer_config_unknown : Error<"unknown analyzer-config '%0'">;
 def err_analyzer_checker_option_unknown : Error<
   "checker '%0' has no option called '%1'">;
 def err_analyzer_checker_option_invalid_input : Error<
   "invalid input for checker option '%0', that expects %1">;
 def err_analyzer_checker_incompatible_analyzer_option : Error<
   "checker cannot be enabled with analyzer option '%0' == %1">;
+def err_analyzer_not_built_with_z3 : Error<
+  "analyzer constraint manager 'z3' is only available if LLVM was built with "
+  "-DLLVM_ENABLE_Z3_SOLVER=ON">;
 
 def warn_drv_needs_hvx : Warning<
   "%0 requires HVX, use -mhvx/-mhvx= to enable it">,
   InGroup<OptionIgnored>;
 def err_drv_needs_hvx : Error<
   "%0 requires HVX, use -mhvx/-mhvx= to enable it">;
 def err_drv_needs_hvx_version : Error<
   "%0 is not supported on HVX %1">;

clang/lib/Frontend/CompilerInvocation.cpp

 #define ANALYSIS_CONSTRAINTS(NAME, CMDFLAG, DESC, CREATFN) \
       .Case(CMDFLAG, NAME##Model)
 #include "clang/StaticAnalyzer/Core/Analyses.def"
       .Default(NumConstraints);
     if (Value == NumConstraints) {
       Diags.Report(diag::err_drv_invalid_value)
         << A->getAsString(Args) << Name;
     } else {
+#ifndef LLVM_WITH_Z3
+      if (Value == AnalysisConstraints::Z3ConstraintsModel) {
+        Diags.Report(diag::err_analyzer_not_built_with_z3);
+      }
+#endif // LLVM_WITH_Z3
       Opts.AnalysisConstraintsOpt = Value;
     }
   }
 
   if (Arg *A = Args.getLastArg(OPT_analyzer_output)) {
     StringRef Name = A->getValue();
     AnalysisDiagClients Value = llvm::StringSwitch<AnalysisDiagClients>(Name)
 #define ANALYSIS_DIAGNOSTICS(NAME, CMDFLAG, DESC, CREATFN) \

clang/test/Analysis/missing-z3-nocrash.c

+// RUN: not %clang_analyze_cc1 -analyzer-constraints=z3 %s 2>&1 | FileCheck %s
+// REQUIRES: no-z3
+
+// CHECK: error: analyzer constraint manager 'z3' is only available if LLVM
+// CHECK: was built with -DLLVM_ENABLE_Z3_SOLVER=ON

clang/test/lit.cfg.py

if have_host_jit_support():
     config.available_features.add('host-supports-jit')
 
 if config.clang_staticanalyzer:
     config.available_features.add('staticanalyzer')
     tools.append('clang-check')
 
     if config.clang_staticanalyzer_z3:
         config.available_features.add('z3')
+    else:
+        config.available_features.add('no-z3')
 
     check_analyzer_fixit_path = os.path.join(
         config.test_source_root, "Analysis", "check-analyzer-fixit.py")
     config.substitutions.append(
         ('%check_analyzer_fixit',
          '"%s" %s' % (config.python_executable, check_analyzer_fixit_path)))
 
 llvm_config.add_tool_substitutions(tools, tool_dirs)