[clang] 9ca62c5 - [analyzer] Indicate UnarySymExpr is not supported by Z3 (#108900)

[via cfe-commits]

Author: vabridgers
Date: 2024-09-19T09:57:25-05:00
New Revision: 9ca62c5302633d0220de30f2b2a21d87dee64ac0

URL: https://github.com/llvm/llvm-project/commit/9ca62c5302633d0220de30f2b2a21d87dee64ac0
DIFF: https://github.com/llvm/llvm-project/commit/9ca62c5302633d0220de30f2b2a21d87dee64ac0.diff

LOG: [analyzer] Indicate UnarySymExpr is not supported by Z3 (#108900)

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)

Co-authored-by: einvbri <vince.a.bridgers at ericsson.com>

Added: 
    clang/test/Analysis/z3-unarysymexpr.c

Modified: 
    clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

Removed: 
    


################################################################################
diff  --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index bf18c353b85083..5766af1fc78a4f 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -278,6 +278,11 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
     if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
       return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
 
+    // UnarySymExpr support is not yet implemented in the Z3 wrapper.
+    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;
+}