Skip to content

Commit 61da414

Browse files
author
einvbri
committed
[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)
1 parent 4886403 commit 61da414

File tree

2 files changed

+23
-0
lines changed

2 files changed

+23
-0
lines changed

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

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -278,6 +278,13 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
278278
if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym))
279279
return canReasonAbout(SVB.makeSymbolVal(SC->getOperand()));
280280

281+
// If a UnarySymExpr is encountered, the Z3
282+
// wrapper does not support those. So indicate Z3 does not
283+
// support those and return.
284+
if (const UnarySymExpr *USE = dyn_cast<UnarySymExpr>(Sym)) {
285+
return false;
286+
}
287+
281288
if (const BinarySymExpr *BSE = dyn_cast<BinarySymExpr>(Sym)) {
282289
if (const SymIntExpr *SIE = dyn_cast<SymIntExpr>(BSE))
283290
return canReasonAbout(SVB.makeSymbolVal(SIE->getLHS()));

clang/test/Analysis/z3-unarysymexpr.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
// RUN: %clang_analyze_cc1 -analyzer-checker=core,debug.ExprInspection -verify %s \
2+
// RUN: -analyzer-constraints=z3
3+
4+
// REQUIRES: Z3
5+
//
6+
// This LIT covers a crash associated with this test.
7+
// The expectation is to not crash!
8+
//
9+
10+
long a;
11+
void b() {
12+
long c;
13+
if (~(b && a)) // expected-warning {{address of function 'b' will always evaluate to 'true'}}
14+
// expected-note@-1 {{prefix with the address-of operator to silence this warning}}
15+
c ^= 0; // expected-warning {{The left expression of the compound assignment is an uninitialized value. The computed value will also be garbage}}
16+
}

0 commit comments

Comments
 (0)