[analyzer][z3] Use more elaborate Z3 variable names

[steakhal]

Summary

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_$###

[xazax.hun]

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.

[steakhal]

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?

[xazax.hun]

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

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

[steakhal]

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.

[xazax.hun]

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?

[steakhal]

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.

[xazax.hun]

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.

[steakhal]

Use virtual getKindStr method for acquiring the kind name.

[xazax.hun]

This is what I had in mind, thanks!

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h

335

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

[xazax.hun]

clang/test/Analysis/z3/pretty-dump.c

16

Will this test case work with non-debug builds?

[mikhail.ramalho]

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

[steakhal]

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.

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h

335

Thanks.

clang/test/Analysis/z3/pretty-dump.c

16

Fixed.

[mikhail.ramalho]

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.

[steakhal]

In D86223#2232681, @mikhail.ramalho wrote:

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.

Fixed.

---

Revision updated:

• Use the prettier symbol names unconditionally
• Revert changes to the test infra

[mikhail.ramalho]

LGTM!

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
       assert(!Ty->isRealFloatingType());
       llvm::APSInt Value(Ctx.getTypeSize(Ty),
                          !Ty->isSignedIntegerOrEnumerationType());
 
       // TODO: this should call checkModel so we can use the cache, however,
       // 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);
 
       // Constraints are unsatisfiable
       Optional<bool> isSat = Solver->check();
       if (!isSat.hasValue() || !isSat.getValue())
         return nullptr;

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h

static inline llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver,
                                         const llvm::APSInt &V, QualType ToTy,
                                         uint64_t ToWidth, QualType FromTy,
                                         uint64_t FromWidth) {
     APSIntType TargetType(ToWidth, !ToTy->isSignedIntegerOrEnumerationType());
     return TargetType.convert(V);
   }
 
   /// 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.
   static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver,
                                              ASTContext &Ctx,
                                              const llvm::SMTExprRef &Exp,
                                              QualType FromTy, QualType ToTy) {
     return fromCast(Solver, Exp, ToTy, Ctx.getTypeSize(ToTy), FromTy,
                     Ctx.getTypeSize(FromTy));
   }
 
   // Wrapper to generate SMTSolverRef from unpacked binary symbolic
public:
   static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver,
                                             ASTContext &Ctx, SymbolRef Sym,
                                             QualType *RetTy,
                                             bool *hasComparison) {
     if (const SymbolData *SD = dyn_cast<SymbolData>(Sym)) {
       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)) {
       if (RetTy)
         *RetTy = Sym->getType();
 
       QualType FromTy;
       llvm::SMTExprRef Exp =

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h

 protected:
   SymbolData(Kind k, SymbolID sym) : SymExpr(k), Sym(sym) {
     assert(classof(this));
   }
 
 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 {
     return 1;
   };
 
   // Implement isa<T> support.
   static inline bool classof(const SymExpr *SE) {

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h

static void Profile(llvm::FoldingSetNodeID& profile, const TypedValueRegion* R) {
     profile.AddInteger((unsigned) SymbolRegionValueKind);
     profile.AddPointer(R);
   }
 
   void Profile(llvm::FoldingSetNodeID& profile) override {
     Profile(profile, R);
   }
 
+  StringRef getKindStr() const override;
+
   void dumpToStream(raw_ostream &os) const override;
   const MemRegion *getOriginRegion() const override { return getRegion(); }
 
   QualType getType() const override;
 
   // Implement isa<T> support.
   static bool classof(const SymExpr *SE) {
     return SE->getKind() == SymbolRegionValueKind;
public:
   }
 
   const Stmt *getStmt() const { return S; }
   unsigned getCount() const { return Count; }
   const void *getTag() const { return SymbolTag; }
 
   QualType getType() const override;
 
+  StringRef getKindStr() const override;
+
   void dumpToStream(raw_ostream &os) const override;
 
   static void Profile(llvm::FoldingSetNodeID& profile, const Stmt *S,
                       QualType T, unsigned Count, const LocationContext *LCtx,
                       const void *SymbolTag) {
     profile.AddInteger((unsigned) SymbolConjuredKind);
     profile.AddPointer(S);
     profile.AddPointer(LCtx);
SymbolDerived(SymbolID sym, SymbolRef parent, const TypedValueRegion *r)
     assert(isValidTypeForSymbol(r->getValueType()));
   }
 
   SymbolRef getParentSymbol() const { return parentSymbol; }
   const TypedValueRegion *getRegion() const { return R; }
 
   QualType getType() const override;
 
+  StringRef getKindStr() const override;
+
   void dumpToStream(raw_ostream &os) const override;
   const MemRegion *getOriginRegion() const override { return getRegion(); }
 
   static void Profile(llvm::FoldingSetNodeID& profile, SymbolRef parent,
                       const TypedValueRegion *r) {
     profile.AddInteger((unsigned) SymbolDerivedKind);
     profile.AddPointer(r);
     profile.AddPointer(parent);
SymbolExtent(SymbolID sym, const SubRegion *r)
       : SymbolData(SymbolExtentKind, sym), R(r) {
     assert(r);
   }
 
   const SubRegion *getRegion() const { return R; }
 
   QualType getType() const override;
 
+  StringRef getKindStr() const override;
+
   void dumpToStream(raw_ostream &os) const override;
 
   static void Profile(llvm::FoldingSetNodeID& profile, const SubRegion *R) {
     profile.AddInteger((unsigned) SymbolExtentKind);
     profile.AddPointer(R);
   }
 
   void Profile(llvm::FoldingSetNodeID& profile) override {
public:
   const MemRegion *getRegion() const { return R; }
   const Stmt *getStmt() const { return S; }
   const LocationContext *getLocationContext() const { return LCtx; }
   unsigned getCount() const { return Count; }
   const void *getTag() const { return Tag; }
 
   QualType getType() const override;
 
+  StringRef getKindStr() const override;
+
   void dumpToStream(raw_ostream &os) const override;
 
   static void Profile(llvm::FoldingSetNodeID& profile, const MemRegion *R,
                       const Stmt *S, QualType T, const LocationContext *LCtx,
                       unsigned Count, const void *Tag) {
     profile.AddInteger((unsigned) SymbolMetadataKind);
     profile.AddPointer(R);
     profile.AddPointer(S);

clang/lib/StaticAnalyzer/Core/SymbolManager.cpp

 #include "llvm/Support/raw_ostream.h"
 #include <cassert>
 
 using namespace clang;
 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) {
   OS << '(';
   Sym->dumpToStream(OS);
   OS << ')';
 }
 

 
 void SymbolCast::dumpToStream(raw_ostream &os) const {
   os << '(' << ToTy.getAsString() << ") (";
   Operand->dumpToStream(os);
   os << ')';
 }
 
 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());
   else
     os << ", no stmt";
   os << ", #" << Count << '}';
 }
 
 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 {
   return itr == X.itr;
 }
 
 bool SymExpr::symbol_iterator::operator!=(const symbol_iterator &X) const {
   return itr != X.itr;

clang/test/Analysis/z3/pretty-dump.c

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