[clang] cdacffe - [analyzer][z3] Use more elaborate Z3 variable names
Balazs Benics via cfe-commits
cfe-commits at lists.llvm.org
Sun Sep 13 23:44:38 PDT 2020
Author: Balazs Benics
Date: 2020-09-14T08:43:56+02:00
New Revision: cdacffe4acc083dfb1cccb6458420eed09f9d093
URL: https://github.com/llvm/llvm-project/commit/cdacffe4acc083dfb1cccb6458420eed09f9d093
DIFF: https://github.com/llvm/llvm-project/commit/cdacffe4acc083dfb1cccb6458420eed09f9d093.diff
LOG: [analyzer][z3] Use more elaborate Z3 variable names
Previously, it was a tedious task to comprehend Z3 dumps.
We will use the same name prefix just as we use in the corresponding dump method
For all `SymbolData` values:
`$###` -> `conj_$###`
`$###` -> `derived_$###`
`$###` -> `extent_$###`
`$###` -> `meta_$###`
`$###` -> `reg_$###`
Reviewed By: xazax.hun,mikhail.ramalho
Differential Revision: https://reviews.llvm.org/D86223
Added:
clang/test/Analysis/z3/pretty-dump.c
Modified:
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h
clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
clang/lib/StaticAnalyzer/Core/SymbolManager.cpp
Removed:
################################################################################
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index 6a0f5f10874e..07fc73a670f3 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -122,8 +122,7 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
// this method tries to get the interpretation (the actual value) from
// the solver, which is currently not cached.
- llvm::SMTExprRef Exp =
- SMTConv::fromData(Solver, SD->getSymbolID(), Ty, Ctx.getTypeSize(Ty));
+ llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD);
Solver->reset();
addStateConstraints(State);
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
index bdebe238829e..2d0f169260a4 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -319,11 +319,16 @@ class SMTConv {
}
/// Construct an SMTSolverRef from a SymbolData.
- static inline llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver,
- const SymbolID ID, const QualType &Ty,
- uint64_t BitWidth) {
- llvm::Twine Name = "$" + llvm::Twine(ID);
- return Solver->mkSymbol(Name.str().c_str(), mkSort(Solver, Ty, BitWidth));
+ static inline llvm::SMTExprRef
+ fromData(llvm::SMTSolverRef &Solver, ASTContext &Ctx, const SymbolData *Sym) {
+ const SymbolID ID = Sym->getSymbolID();
+ const QualType Ty = Sym->getType();
+ const uint64_t BitWidth = Ctx.getTypeSize(Ty);
+
+ llvm::SmallString<16> Str;
+ llvm::raw_svector_ostream OS(Str);
+ OS << Sym->getKindStr() << ID;
+ return Solver->mkSymbol(Str.c_str(), mkSort(Solver, Ty, BitWidth));
}
// Wrapper to generate SMTSolverRef from SymbolCast data.
@@ -422,8 +427,7 @@ class SMTConv {
if (RetTy)
*RetTy = Sym->getType();
- return fromData(Solver, SD->getSymbolID(), Sym->getType(),
- Ctx.getTypeSize(Sym->getType()));
+ return fromData(Solver, Ctx, SD);
}
if (const SymbolCast *SC = dyn_cast<SymbolCast>(Sym)) {
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h
index abfcd1d80faa..2f4ac6ba5f97 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h
@@ -126,6 +126,9 @@ class SymbolData : public SymExpr {
public:
~SymbolData() override = default;
+ /// Get a string representation of the kind of the region.
+ virtual StringRef getKindStr() const = 0;
+
SymbolID getSymbolID() const { return Sym; }
unsigned computeComplexity() const override {
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
index 390ced8c29f8..75dfbde5c151 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
+++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
@@ -59,6 +59,8 @@ class SymbolRegionValue : public SymbolData {
Profile(profile, R);
}
+ StringRef getKindStr() const override;
+
void dumpToStream(raw_ostream &os) const override;
const MemRegion *getOriginRegion() const override { return getRegion(); }
@@ -99,6 +101,8 @@ class SymbolConjured : public SymbolData {
QualType getType() const override;
+ StringRef getKindStr() const override;
+
void dumpToStream(raw_ostream &os) const override;
static void Profile(llvm::FoldingSetNodeID& profile, const Stmt *S,
@@ -141,6 +145,8 @@ class SymbolDerived : public SymbolData {
QualType getType() const override;
+ StringRef getKindStr() const override;
+
void dumpToStream(raw_ostream &os) const override;
const MemRegion *getOriginRegion() const override { return getRegion(); }
@@ -177,6 +183,8 @@ class SymbolExtent : public SymbolData {
QualType getType() const override;
+ StringRef getKindStr() const override;
+
void dumpToStream(raw_ostream &os) const override;
static void Profile(llvm::FoldingSetNodeID& profile, const SubRegion *R) {
@@ -226,6 +234,8 @@ class SymbolMetadata : public SymbolData {
QualType getType() const override;
+ StringRef getKindStr() const override;
+
void dumpToStream(raw_ostream &os) const override;
static void Profile(llvm::FoldingSetNodeID& profile, const MemRegion *R,
diff --git a/clang/lib/StaticAnalyzer/Core/SymbolManager.cpp b/clang/lib/StaticAnalyzer/Core/SymbolManager.cpp
index ae40ad910d84..700f91aed610 100644
--- a/clang/lib/StaticAnalyzer/Core/SymbolManager.cpp
+++ b/clang/lib/StaticAnalyzer/Core/SymbolManager.cpp
@@ -35,6 +35,12 @@ using namespace ento;
void SymExpr::anchor() {}
+StringRef SymbolConjured::getKindStr() const { return "conj_$"; }
+StringRef SymbolDerived::getKindStr() const { return "derived_$"; }
+StringRef SymbolExtent::getKindStr() const { return "extent_$"; }
+StringRef SymbolMetadata::getKindStr() const { return "meta_$"; }
+StringRef SymbolRegionValue::getKindStr() const { return "reg_$"; }
+
LLVM_DUMP_METHOD void SymExpr::dump() const { dumpToStream(llvm::errs()); }
void BinarySymExpr::dumpToStreamImpl(raw_ostream &OS, const SymExpr *Sym) {
@@ -65,7 +71,7 @@ void SymbolCast::dumpToStream(raw_ostream &os) const {
}
void SymbolConjured::dumpToStream(raw_ostream &os) const {
- os << "conj_$" << getSymbolID() << '{' << T.getAsString() << ", LC"
+ os << getKindStr() << getSymbolID() << '{' << T.getAsString() << ", LC"
<< LCtx->getID();
if (S)
os << ", S" << S->getID(LCtx->getDecl()->getASTContext());
@@ -75,24 +81,24 @@ void SymbolConjured::dumpToStream(raw_ostream &os) const {
}
void SymbolDerived::dumpToStream(raw_ostream &os) const {
- os << "derived_$" << getSymbolID() << '{'
- << getParentSymbol() << ',' << getRegion() << '}';
+ os << getKindStr() << getSymbolID() << '{' << getParentSymbol() << ','
+ << getRegion() << '}';
}
void SymbolExtent::dumpToStream(raw_ostream &os) const {
- os << "extent_$" << getSymbolID() << '{' << getRegion() << '}';
+ os << getKindStr() << getSymbolID() << '{' << getRegion() << '}';
}
void SymbolMetadata::dumpToStream(raw_ostream &os) const {
- os << "meta_$" << getSymbolID() << '{'
- << getRegion() << ',' << T.getAsString() << '}';
+ os << getKindStr() << getSymbolID() << '{' << getRegion() << ','
+ << T.getAsString() << '}';
}
void SymbolData::anchor() {}
void SymbolRegionValue::dumpToStream(raw_ostream &os) const {
- os << "reg_$" << getSymbolID()
- << '<' << getType().getAsString() << ' ' << R << '>';
+ os << getKindStr() << getSymbolID() << '<' << getType().getAsString() << ' '
+ << R << '>';
}
bool SymExpr::symbol_iterator::operator==(const symbol_iterator &X) const {
diff --git a/clang/test/Analysis/z3/pretty-dump.c b/clang/test/Analysis/z3/pretty-dump.c
new file mode 100644
index 000000000000..811da172e749
--- /dev/null
+++ b/clang/test/Analysis/z3/pretty-dump.c
@@ -0,0 +1,17 @@
+// RUN: %clang_cc1 -analyze -analyzer-constraints=z3 -setup-static-analyzer \
+// RUN: -analyzer-checker=core,debug.ExprInspection %s 2>&1 | FileCheck %s
+//
+// REQUIRES: z3
+//
+// Works only with the z3 constraint manager.
+
+void clang_analyzer_printState();
+
+void foo(int x) {
+ if (x == 3) {
+ clang_analyzer_printState();
+ (void)x;
+ // CHECK: "constraints": [
+ // CHECK-NEXT: { "symbol": "(reg_$[[#]]<int x>) == 3", "range": "(= reg_$[[#]] #x00000003)" }
+ }
+}
More information about the cfe-commits
mailing list