steakhal created this revision. steakhal added reviewers: NoQ, Szelethus, vsavchenko, xazax.hun, mikhail.ramalho, ddcc. Herald added subscribers: cfe-commits, ASDenysPetrov, martong, Charusso, dkrupp, donat.nagy, a.sidorin, rnkovacs, szepet, baloghadamsoftware, whisperity. Herald added a project: clang. steakhal requested review of this revision.
Previously, it was a tedious task to comprehend Z3 dumps. This prettier dumps would help during debugging, so I'm only using the longer names in debug build. For all SymbolData values: - `$###` -> `$conj_###` - `$###` -> `$derived_###` - `$###` -> `$extent_###` - `$###` -> `$meta_###` - `$###` -> `$reg_###` Repository: rG LLVM Github Monorepo https://reviews.llvm.org/D86223 Files: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h 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/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,41 @@ } /// 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); + + const auto GetPrettyPrefixFor = [](const SymbolData *Sym) -> const char * { + switch (Sym->getKind()) { + default: + llvm_unreachable("There should be no other SymbolData kind."); + case SymExpr::SymbolConjuredKind: + return "conj_"; + case SymExpr::SymbolDerivedKind: + return "derived_"; + case SymExpr::SymbolExtentKind: + return "extent_"; + case SymExpr::SymbolMetadataKind: + return "meta_"; + case SymExpr::SymbolRegionValueKind: + return "reg_"; + } + }; + // Suppress unused variable warning in release build. + static_cast<void>(GetPrettyPrefixFor); + +#if !defined(NDEBUG) || defined(LLVM_ENABLE_DUMP) +#define PRETTY_SYMBOL_KIND GetPrettyPrefixFor(Sym) +#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 +452,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);
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/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,41 @@ } /// 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); + + const auto GetPrettyPrefixFor = [](const SymbolData *Sym) -> const char * { + switch (Sym->getKind()) { + default: + llvm_unreachable("There should be no other SymbolData kind."); + case SymExpr::SymbolConjuredKind: + return "conj_"; + case SymExpr::SymbolDerivedKind: + return "derived_"; + case SymExpr::SymbolExtentKind: + return "extent_"; + case SymExpr::SymbolMetadataKind: + return "meta_"; + case SymExpr::SymbolRegionValueKind: + return "reg_"; + } + }; + // Suppress unused variable warning in release build. + static_cast<void>(GetPrettyPrefixFor); + +#if !defined(NDEBUG) || defined(LLVM_ENABLE_DUMP) +#define PRETTY_SYMBOL_KIND GetPrettyPrefixFor(Sym) +#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 +452,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