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
// 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);
}
/// 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.
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)) {
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 {
Profile(profile, R);
}
+ StringRef getKindStr() const override;
+
void dumpToStream(raw_ostream &os) const override;
const MemRegion *getOriginRegion() const override { return getRegion(); }
QualType getType() const override;
+ StringRef getKindStr() const override;
+
void dumpToStream(raw_ostream &os) const override;
static void Profile(llvm::FoldingSetNodeID& profile, const Stmt *S,
QualType getType() const override;
+ StringRef getKindStr() const override;
+
void dumpToStream(raw_ostream &os) const override;
const MemRegion *getOriginRegion() const override { return getRegion(); }
QualType getType() const override;
+ StringRef getKindStr() const override;
+
void dumpToStream(raw_ostream &os) const override;
static void Profile(llvm::FoldingSetNodeID& profile, const SubRegion *R) {
QualType getType() const override;
+ StringRef getKindStr() const override;
+
void dumpToStream(raw_ostream &os) const override;
static void Profile(llvm::FoldingSetNodeID& profile, const MemRegion *R,
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) {
}
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());
}
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 {
--- /dev/null
+// 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)" }
+ }
+}