[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Balázs Benics via Phabricator via cfe-commits]

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_$[[#]]) == 3", "range": "(= 
$reg_[[#]] #x0003)" }
+  }
+}
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(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(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
+//
+// R

[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun accepted this revision.
xazax.hun added a comment.
This revision is now accepted and ready to land.

LGTM!

I wonder whether having a virtual method for symbols to get the prefix would be 
cleaner (something like getKindCStr), but I do not insist.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D86223/new/

https://reviews.llvm.org/D86223

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Balázs Benics via Phabricator via cfe-commits]

steakhal added a comment.

In D86223#2226630 , @xazax.hun wrote:

> I wonder whether having a virtual method for symbols to get the prefix would 
> be cleaner (something like getKindCStr), but I do not insist.

Are you implying to have something like:

  virtual SmallString<8> clang::ento::SymbolData::getKindStr() const;

BTW probably we could make use of this in the `SymbolData` dump method family.

Or do you want to lift this function to the `SymExpr` class?


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D86223/new/

https://reviews.llvm.org/D86223

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added a comment.

Exactly, but you could return a StringRef to static storage.

I am fine with both approach. Whichever you find cleaner.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D86223/new/

https://reviews.llvm.org/D86223

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Balázs Benics via Phabricator via cfe-commits]

steakhal added a comment.

In D86223#2226876 , @xazax.hun wrote:

> Exactly, but you could return a StringRef to static storage.
>
> I am fine with both approach. Whichever you find cleaner.

Eh, I'm not sure if it worth it to put these into virtual functions - as 
conditionally overriding functions is not really a good idea.
So we would not win much.

I still think that this way is the cleanest AFAIK.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D86223/new/

https://reviews.llvm.org/D86223

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added a comment.

In D86223#2227353 , @steakhal wrote:

> Eh, I'm not sure if it worth it to put these into virtual functions - as 
> conditionally overriding functions is not really a good idea.

I am not sure I follow. What do you mean by conditionally overriding? What is 
the condition?


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D86223/new/

https://reviews.llvm.org/D86223

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Balázs Benics via Phabricator via cfe-commits]

steakhal added a comment.

In D86223#2228731 , @xazax.hun wrote:

> In D86223#2227353 , @steakhal wrote:
>
>> Eh, I'm not sure if it worth it to put these into virtual functions - as 
>> conditionally overriding functions is not really a good idea.
>
> I am not sure I follow. What do you mean by conditionally overriding? What is 
> the condition?

I wanted to conditionally, aka. in debug configuration override the base 
implementation of the SymbolData::getKindStr to print return the specific kind 
string. In any other configuration I wanted to indef out the overriding 
functions to let the SymbolData implementation to be triggered.
In that way less macro expansion would have been necessary, resulting in 
cleaner code.

Unfortunately I would have needed even more macros to make the subtype override 
function declarations disappear.

This was the reason that I suggested to leave the current implementation as-is.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D86223/new/

https://reviews.llvm.org/D86223

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added a comment.

In D86223#2228855 , @steakhal wrote:

> I wanted to conditionally, aka. in debug configuration override the base 
> implementation of the SymbolData::getKindStr

I see. Yeah, that does not make much sense. I was thinking about always 
overriding the methods but call them conditionally.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D86223/new/

https://reviews.llvm.org/D86223

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Balázs Benics via Phabricator via cfe-commits]

steakhal updated this revision to Diff 287192.
steakhal edited the summary of this revision.
steakhal added a comment.

Use virtual getKindStr method for acquiring the kind name.


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

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_$[[#]]) == 3", "range": "(= reg_$[[#]] #x0003)" }
+  }
+}
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 v

[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun accepted this revision.
xazax.hun added a comment.

This is what I had in mind, thanks!




Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:335
+llvm::raw_svector_ostream OS(Str);
+OS << PRETTY_SYMBOL_KIND << ID;
+#undef PRETTY_SYMBOL_KIND

Maybe, in this case, it is cleaner to duplicate the line rather than introduce 
`PRETTY_SYMBOL_KIND`?


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D86223/new/

https://reviews.llvm.org/D86223

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Gábor Horváth via Phabricator via cfe-commits]

xazax.hun added inline comments.



Comment at: clang/test/Analysis/z3/pretty-dump.c:15
+// CHECK: "constraints": [
+// CHECK-NEXT: { "symbol": "(reg_$[[#]]) == 3", "range": "(= 
reg_$[[#]] #x0003)" }
+  }

Will this test case work with non-debug builds? 


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D86223/new/

https://reviews.llvm.org/D86223

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho added a comment.

I don't mind having it for release builds as well, why are you applying it only 
for debug builds?


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D86223/new/

https://reviews.llvm.org/D86223

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Balázs Benics via Phabricator via cfe-commits]

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 , @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_$[[#]]) == 3", "range": "(= reg_$[[#]] #x0003)" }
+  }
+}
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::operat

[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Balázs Benics via Phabricator via cfe-commits]

steakhal added inline comments.



Comment at: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h:335
+llvm::raw_svector_ostream OS(Str);
+OS << PRETTY_SYMBOL_KIND << ID;
+#undef PRETTY_SYMBOL_KIND

xazax.hun wrote:
> Maybe, in this case, it is cleaner to duplicate the line rather than 
> introduce `PRETTY_SYMBOL_KIND`?
Thanks.



Comment at: clang/test/Analysis/z3/pretty-dump.c:15
+// CHECK: "constraints": [
+// CHECK-NEXT: { "symbol": "(reg_$[[#]]) == 3", "range": "(= 
reg_$[[#]] #x0003)" }
+  }

xazax.hun wrote:
> Will this test case work with non-debug builds? 
Fixed.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D86223/new/

https://reviews.llvm.org/D86223

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

[PATCH] D86223: [analyzer][z3] Use more elaborate z3 variable names in debug build

[Mikhail Ramalho via Phabricator via cfe-commits]

mikhail.ramalho requested changes to this revision.
mikhail.ramalho added a comment.
This revision now requires changes to proceed.

In D86223#2231991 , @steakhal wrote:

> In 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.

That overhead should be negligible, in the worst case you are adding just a few 
extra characters to the variable's name.

I rather have it for release builds as well so we don't introduce different 
outputs depending on the build options, and we can improve debugging for 
release builds as well.

Also as a bonus, we don't have to change the test scripts for a single test.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D86223/new/

https://reviews.llvm.org/D86223

___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits