[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)
llvm · Sep 16, 2024 · 61da414 · 61da414
1 parent 4886403
commit 61da414
Show file tree

Hide file tree

Showing 2 changed files with 23 additions and 0 deletions.
diff --git 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 (const UnarySymExpr *USE = dyn_cast<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
@@ -0,0 +1,16 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s \
+// RUN:  -analyzer-constraints=z3 
+
+// REQUIRES: Z3
+//
+// This LIT covers a crash associated with this test.
+// The expectation is to not crash!
+//
+
+long a;
+void b() {
+  long c;
+  if (~(b && a)) // expected-warning {{address of function 'b' will always evaluate to 'true'}}
+  // expected-note@-1 {{prefix with the address-of operator to silence this warning}}
+    c ^= 0; // expected-warning {{The left expression of the compound assignment is an uninitialized value. The computed value will also be garbage}}
+}