Skip to content

Commit

Permalink
[analyzer] Indicate UnarySymExpr is not supported by Z3 (llvm#108900)
Browse files Browse the repository at this point in the history
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() llvm#8 <addr>
clang::ento::SimpleConstraintManager::assumeAux(
llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>,
clang::ento::NonLoc, bool) llvm#9 <addr>
clang::ento::SimpleConstraintManager::assume(
llvm::IntrusiveRefCntPtr<clang::ento::ProgramState const>,
clang::ento::NonLoc, bool)

Co-authored-by: einvbri <vince.a.bridgers@ericsson.com>
  • Loading branch information
vabridgers and einvbri authored Sep 19, 2024
1 parent 5fa742e commit 9ca62c5
Show file tree
Hide file tree
Showing 2 changed files with 20 additions and 0 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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()));
Expand Down
15 changes: 15 additions & 0 deletions clang/test/Analysis/z3-unarysymexpr.c
Original file line number Diff line number Diff line change
@@ -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;
}

0 comments on commit 9ca62c5

Please sign in to comment.