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)" } + } +} _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits