[analyzer] Add method to the generic SMT API to dump the SMT formula

[mikhail.ramalho]

Summary

New method dump the SMT formula and the Z3 implementation.

There is no test because I only used it for debugging.

However, if requested, I can add an option to the static analyzer to dump the formula (whole program? per path?), maybe something like the trimmed graph but for SMT formulas.

[george.karpenkov]

Can we just call it dump? Otherwise, LGTM.

[mikhail.ramalho]

Rename dumpSMTFormula() to dump().

I initially had a dumpModel, that's why this method was called dumpSMTFormula, however, the dumpModel didn't check if a model actually existed before trying to print it, which led to z3 crashing when there was no model, so I removed it.

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

public:
   /// Converts the ranged constraints of a set of symbols to SMT
   ///
   /// \param CR The set of constraints.
   virtual void addRangeConstraints(clang::ento::ConstraintRangeTy CR) = 0;
 
   /// Checks if the added constraints are satisfiable
   virtual clang::ento::ConditionTruthVal isModelFeasible() = 0;
 
+  /// Dumps SMT formula
+  LLVM_DUMP_METHOD virtual void dump() const = 0;
 }; // end class SMTConstraintManager
 
 } // namespace ento
 } // namespace clang
 
 #endif

cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

public:
   //===------------------------------------------------------------------===//
   // Implementation for Refutation.
   //===------------------------------------------------------------------===//
 
   void addRangeConstraints(clang::ento::ConstraintRangeTy CR) override;
 
   ConditionTruthVal isModelFeasible() override;
 
+  LLVM_DUMP_METHOD void dump() const override;
+
   //===------------------------------------------------------------------===//
   // Implementation for interface from ConstraintManager.
   //===------------------------------------------------------------------===//
 
   bool canReasonAbout(SVal X) const override;
 
   ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
 

 
 clang::ento::ConditionTruthVal Z3ConstraintManager::isModelFeasible() {
   if (Solver.check() == Z3_L_FALSE)
     return false;
 
   return ConditionTruthVal();
 }
 
+LLVM_DUMP_METHOD void Z3ConstraintManager::dump() const
+{
+  Solver.dump();
+}
+
 //===------------------------------------------------------------------===//
 // Internal implementation.
 //===------------------------------------------------------------------===//
 
 ProgramStateRef Z3ConstraintManager::assumeZ3Expr(ProgramStateRef State,
                                                   SymbolRef Sym,
                                                   const Z3Expr &Exp) {
   // Check the model, avoid simplifying AST to save time