steakhal updated this revision to Diff 287192.
steakhal edited the summary of this revision.
steakhal added a comment.
Use virtual getKindStr method for acquiring the kind name.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D86223/new/
https://reviews.llvm.org/D86223
Files:
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
clang/test/Analysis/z3/pretty-dump.c
Index: clang/test/Analysis/z3/pretty-dump.c
===================================================================
--- /dev/null
+++ 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)" }
+ }
+}
Index: clang/lib/StaticAnalyzer/Core/SymbolManager.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/SymbolManager.cpp
+++ clang/lib/StaticAnalyzer/Core/SymbolManager.cpp
@@ -34,6 +34,12 @@
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) {
@@ -64,7 +70,7 @@
}
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());
@@ -74,24 +80,24 @@
}
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 {
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h
@@ -59,6 +59,8 @@
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 @@
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 @@
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 @@
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 @@
QualType getType() const override;
+ StringRef getKindStr() const override;
+
void dumpToStream(raw_ostream &os) const override;
static void Profile(llvm::FoldingSetNodeID& profile, const MemRegion *R,
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h
@@ -126,6 +126,9 @@
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 {
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h
@@ -319,11 +319,22 @@
}
/// 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);
+
+#if !defined(NDEBUG) || defined(LLVM_ENABLE_DUMP)
+#define PRETTY_SYMBOL_KIND Sym->getKindStr()
+#else
+#define PRETTY_SYMBOL_KIND "$"
+#endif
+ llvm::SmallString<16> Str;
+ llvm::raw_svector_ostream OS(Str);
+ OS << PRETTY_SYMBOL_KIND << ID;
+#undef PRETTY_SYMBOL_KIND
+ return Solver->mkSymbol(Str.c_str(), mkSort(Solver, Ty, BitWidth));
}
// Wrapper to generate SMTSolverRef from SymbolCast data.
@@ -422,8 +433,7 @@
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)) {
Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -122,8 +122,7 @@
// 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);
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
