steakhal updated this revision to Diff 287197.
steakhal marked 2 inline comments as done.
steakhal edited the summary of this revision.
steakhal added a comment.
In D86223#2231959 <https://reviews.llvm.org/D86223#2231959>, @mikhail.ramalho
wrote:
> I don't mind having it for release builds as well, why are you applying it
> only for debug builds?
It might introduce a slight overhead since Z3 will parse longer the symbol
names.
---
Diff update:
- Simplify macro usage.
- Introduce the `llvm_enable_dump` lit test requires clause.
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
clang/test/lit.cfg.py
clang/test/lit.site.cfg.py.in
Index: clang/test/lit.site.cfg.py.in
===================================================================
--- clang/test/lit.site.cfg.py.in
+++ clang/test/lit.site.cfg.py.in
@@ -12,6 +12,7 @@
config.clang_obj_root = path(r"@CLANG_BINARY_DIR@")
config.clang_src_dir = path(r"@CLANG_SOURCE_DIR@")
config.clang_tools_dir = path(r"@CLANG_TOOLS_DIR@")
+config.llvm_enable_dump = "@LLVM_ENABLE_DUMP@"
config.host_triple = "@LLVM_HOST_TRIPLE@"
config.target_triple = "@TARGET_TRIPLE@"
config.host_cxx = "@CMAKE_CXX_COMPILER@"
Index: clang/test/lit.cfg.py
===================================================================
--- clang/test/lit.cfg.py
+++ clang/test/lit.cfg.py
@@ -68,6 +68,10 @@
'clang-extdef-mapping'), unresolved='ignore'),
]
+llvm_enable_dump = getattr(config, 'llvm_enable_dump', None)
+if llvm_enable_dump:
+ config.available_features.add('llvm_enable_dump')
+
if config.clang_examples:
config.available_features.add('examples')
tools.append('clang-interpreter')
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: llvm_enable_dump, 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,20 @@
}
/// 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);
+#ifdef LLVM_ENABLE_DUMP
+ OS << Sym->getKindStr() << ID;
+#else
+ OS << '$' << ID;
+#endif
+ return Solver->mkSymbol(Str.c_str(), mkSort(Solver, Ty, BitWidth));
}
// Wrapper to generate SMTSolverRef from SymbolCast data.
@@ -422,8 +431,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
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
