[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

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);

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<SymbolCast>(Sym)) {

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 {

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,

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 {

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)" }
+  }
+}