[clang] [analyzer] Indicate UnarySymExpr is not supported by Z3 (PR #108900)

[via cfe-commits]

https://github.com/vabridgers updated https://github.com/llvm/llvm-project/pull/108900

>From 1790ebab722f53b5dba3ef7cd2afb7cf2549f245 Mon Sep 17 00:00:00 2001
From: einvbri <vince.a.bridgers at ericsson.com>
Date: Tue, 17 Sep 2024 01:25:20 +0200
Subject: [PATCH 1/2] [analyzer] Indicate UnarySymExpr is not supported by Z3

Random testing found that the Z3 wrapper does not support UnarySymExpr,
which was added recently and not included in the original Z3 wrapper.
For now, just avoid submitting expressions to Z3 to avoid compiler crashes.

Some crash context ...

clang -cc1 -analyze -analyzer-checker=core z3-unarysymexpr.c -analyzer-constraints=z3

Unsupported expression to reason about!
UNREACHABLE executed at clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h:297!

Stack dump:
3.	<root>/clang/test/Analysis/z3-unarysymexpr.c:13:7: Error evaluating branch
 #0 <addr> llvm::sys::PrintStackTrace(llvm::raw_ostream&, int)
 #1 <addr> llvm::sys::RunSignalHandlers()
 #8 <addr> clang::ento::SimpleConstraintManager::assumeAux(
            llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>, clang::ento::NonLoc, bool)
 #9 <addr> clang::ento::SimpleConstraintManager::assume(
            llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>, clang::ento::NonLoc, bool)
---
 .../Core/PathSensitive/SMTConstraintManager.h     |  7 +++++++
 clang/test/Analysis/z3-unarysymexpr.c             | 15 +++++++++++++++
 2 files changed, 22 insertions(+)
 create mode 100644 clang/test/Analysis/z3-unarysymexpr.c

diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index bf18c353b85083..86342a4080375f 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -278,6 +278,13 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
     if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
       return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
 
+    // If a UnarySymExpr is encountered, the Z3
+    // wrapper does not support those. So indicate Z3 does not
+    // support those and return.
+    if (isa<UnarySymExpr>(Sym)) {
+      return false;
+    }
+
     if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
       if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
         return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));
diff --git a/clang/test/Analysis/z3-unarysymexpr.c b/clang/test/Analysis/z3-unarysymexpr.c
new file mode 100644
index 00000000000000..ed9ba72468422e
--- /dev/null
+++ b/clang/test/Analysis/z3-unarysymexpr.c
@@ -0,0 +1,15 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s \
+// RUN:  -analyzer-constraints=z3 
+
+// REQUIRES: Z3
+//
+// Previously Z3 analysis crashed when it encountered an UnarySymExpr, validate
+// that this no longer happens.
+//
+
+// expected-no-diagnostics
+int negate(int x, int y) {
+  if ( ~(x && y))
+    return 0;
+  return 1;
+}

>From cad3cd6ededd0df2aeee59fe0eb75bee2db705eb Mon Sep 17 00:00:00 2001
From: einvbri <vince.a.bridgers at ericsson.com>
Date: Thu, 19 Sep 2024 15:40:31 +0200
Subject: [PATCH 2/2] update

---
 .../StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h  | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index 86342a4080375f..5766af1fc78a4f 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -278,9 +278,7 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
     if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
       return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
 
-    // If a UnarySymExpr is encountered, the Z3
-    // wrapper does not support those. So indicate Z3 does not
-    // support those and return.
+    // UnarySymExpr support is not yet implemented in the Z3 wrapper.
     if (isa<UnarySymExpr>(Sym)) {
       return false;
     }