https://github.com/vabridgers created
https://github.com/llvm/llvm-project/pull/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)
>From 61da41480b2067668a7f78ab436fde6d24c16c4c Mon Sep 17 00:00:00 2001
From: einvbri <vince.a.bridg...@ericsson.com>
Date: Tue, 17 Sep 2024 01:25:20 +0200
Subject: [PATCH] [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 | 16 ++++++++++++++++
2 files changed, 23 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..16a6b3a2e18112 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 (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
new file mode 100644
index 00000000000000..80625eb61eb52e
--- /dev/null
+++ 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}}
+}
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
