From: Balazs Benics Date: Mon, 14 Sep 2020 06:43:56 +0000 (+0200) Subject: [analyzer][z3] Use more elaborate Z3 variable names X-Git-Tag: llvmorg-13-init~12219 X-Git-Url: http://review.tizen.org/git/?a=commitdiff_plain;h=cdacffe4acc083dfb1cccb6458420eed09f9d093;p=platform%2Fupstream%2Fllvm.git [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 --- diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h index 6a0f5f1..07fc73a 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -122,8 +122,7 @@ public: // 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 bdebe23..2d0f169 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h @@ -319,11 +319,16 @@ public: } /// 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 @@ public: 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(Sym)) { diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h index abfcd1d..2f4ac6b 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h @@ -126,6 +126,9 @@ protected: 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 390ced8..75dfbde 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h @@ -59,6 +59,8 @@ public: 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 @@ public: 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 @@ public: 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 @@ public: 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 @@ public: 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 ae40ad9..700f91a 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 0000000..811da17 --- /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_$[[#]]) == 3", "range": "(= reg_$[[#]] #x00000003)" } + } +}