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

[Kristóf Umann via cfe-commits]

Author: Kristóf Umann
Date: 2022-02-25T17:51:37+01:00
New Revision: 5048a58a6792ee7432b749a48c937cc9b6a9dc93

URL: https://github.com/llvm/llvm-project/commit/5048a58a6792ee7432b749a48c937cc9b6a9dc93
DIFF: https://github.com/llvm/llvm-project/commit/5048a58a6792ee7432b749a48c937cc9b6a9dc93.diff

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

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> ...

Differential Revision: https://reviews.llvm.org/D120325

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

Modified: 
    clang/include/clang/Basic/DiagnosticDriverKinds.td
    clang/lib/Frontend/CompilerInvocation.cpp
    clang/test/lit.cfg.py

Removed: 
    


################################################################################
diff  --git a/clang/include/clang/Basic/DiagnosticDriverKinds.td b/clang/include/clang/Basic/DiagnosticDriverKinds.td
index b608b8ec50682..1ac5bf844efe6 100644
--- a/clang/include/clang/Basic/DiagnosticDriverKinds.td
+++ b/clang/include/clang/Basic/DiagnosticDriverKinds.td
@@ -438,6 +438,9 @@ 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">,

diff  --git a/clang/lib/Frontend/CompilerInvocation.cpp b/clang/lib/Frontend/CompilerInvocation.cpp
index 1014147451091..5d7c999b0143a 100644
--- a/clang/lib/Frontend/CompilerInvocation.cpp
+++ b/clang/lib/Frontend/CompilerInvocation.cpp
@@ -915,6 +915,11 @@ static bool ParseAnalyzerArgs(AnalyzerOptions &Opts, ArgList &Args,
       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;
     }
   }

diff  --git a/clang/test/Analysis/missing-z3-nocrash.c b/clang/test/Analysis/missing-z3-nocrash.c
new file mode 100644
index 0000000000000..698430fffe1a1
--- /dev/null
+++ b/clang/test/Analysis/missing-z3-nocrash.c
@@ -0,0 +1,5 @@
+// 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

diff  --git a/clang/test/lit.cfg.py b/clang/test/lit.cfg.py
index a8efe6c593e98..31425e4009fe2 100644
--- a/clang/test/lit.cfg.py
+++ b/clang/test/lit.cfg.py
@@ -100,6 +100,8 @@ def have_host_jit_support():
 
     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")