[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_$[[#]]<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);


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D86223.286576.patch
Type: text/x-patch
Size: 3736 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20200819/ea82082f/attachment.bin>