[WIP] [analyzer] Dump counterexample traces as C programs

[george.karpenkov]

Summary

This patch is work in progress, but has already shown itself to be useful.

For large traces understanding the analyzer output can be painful, especially when arrows indicating the flow start to loop around.
This patch provides an alternative output method: simply iterate over all program points in a bug report, and dump them to the associated C statements (with program-line-based granularity).
In the ideal case (which we currently don't aim to get) the resulting program is a refinement of an input which goes through the indicated error path.
In the current case, it is a C-like visualization (as some statements are unexpectedly dropped, and some context is missing) of what the error path is.

Sample output is:

gram.c:18444|int yychar;
gram.c:18447|YYSTYPE yylval;
gram.c:18450|int yynerrs;
gram.c:18452|YYLTYPE yylloc;
gram.c:18454|  register int yystate;
gram.c:18455|  register int yyn;
gram.c:18456|  int yyresult;
gram.c:18458|  int yyerrstatus;
gram.c:18460|  int yytoken = 0;
gram.c:18471|  short	yyssa[YYINITDEPTH];
gram.c:18472|  short *yyss = yyssa;
gram.c:18473|  register short *yyssp;
gram.c:18476|  YYSTYPE yyvsa[YYINITDEPTH];
gram.c:18477|  YYSTYPE *yyvs = yyvsa;
gram.c:18478|  register YYSTYPE *yyvsp;
gram.c:18481|  YYLTYPE yylsa[YYINITDEPTH];
gram.c:18482|  YYLTYPE *yyls = yylsa;
gram.c:18483|  YYLTYPE *yylsp;
gram.c:18484|  YYLTYPE *yylerrsp;
gram.c:18488|  YYSIZE_T yystacksize = YYINITDEPTH;
gram.c:18492|  YYSTYPE yyval;
gram.c:18493|  YYLTYPE yyloc;
gram.c:18497|  int yylen;
gram.c:18501|  yystate = 0;
gram.c:18502|  yyerrstatus = 0;
gram.c:18503|  yynerrs = 0;
gram.c:18504|  yychar = YYEMPTY;		/* Cause a token to be read.  */
gram.c:18511|  yyssp = yyss;
gram.c:18512|  yyvsp = yyvs;
gram.c:18513|  yylsp = yyls;
gram.c:18646|  if (yyn == YYFINAL)
gram.c:18653|  if (yychar != YYEOF)
gram.c:18654|    yychar = YYEMPTY;
gram.c:18656|  *++yyvsp = yylval;
gram.c:18657|  *++yylsp = yylloc;
gram.c:18661|  if (yyerrstatus)
gram.c:18664|  yystate = yyn;
gram.c:18523|  yyssp++;
gram.c:18526|  *yyssp = yystate;
gram.c:18528|  if (yyss + yystacksize - 1 <= yyssp)
gram.c:18608|  yyn = yypact[yystate];
gram.c:18609|  if (yyn == YYPACT_NINF)
gram.c:18615|  if (yychar == YYEMPTY)
gram.c:18618|      yychar = YYLEX;
gram.c:18621|  if (yychar <= YYEOF)
gram.c:18628|      yytoken = YYTRANSLATE (yychar);
gram.c:18634|  yyn += yytoken;
gram.c:18635|  if (yyn < 0 || YYLAST < yyn || yycheck[yyn] != yytoken)
gram.c:18637|  yyn = yytable[yyn];
gram.c:18638|  if (yyn <= 0)
gram.c:18640|      if (yyn == 0 || yyn == YYTABLE_NINF)
gram.c:18642|      yyn = -yyn;
gram.c:18683|  yylen = yyr2[yyn];
gram.c:18693|  yyval = yyvsp[1-yylen];
gram.c:18696|  YYLLOC_DEFAULT (yyloc, (yylsp - yylen), yylen);
gram.c:18698|  switch (yyn)
gram.y:11696|					TypeName *t = makeTypeNameFromNameList(yyvsp[-4].list);
gram.y:11697|					ListCell *lc;
gram.y:11704|					foreach(lc, yyvsp[-2].list)
gram.y:11714|					t->typmods = yyvsp[-2].list;
gram.y:11715|					t->location = yylsp[-4];

[NoQ]

This looks great for understanding what exactly is going on in a large real-world report.

If you want to turn this into a form of user-facing analyzer output variant, you may want to implement it as a PathDiagnosticConsumer rather than a visitor. If we only want a neat debugging mechanism, then you might want to stick it directly into BugReporter::emitReport() or maybe BugReporter::FlushReport() (not sure how both of these interact with report deduplication).

[NoQ]

In D40809#945551, @NoQ wrote:

If you want to turn this into a form of user-facing analyzer output variant, you may want to implement it as a PathDiagnosticConsumer rather than a visitor.

Or maybe no, actually it's totally wrong, never mind. PathDiagnosticConsumer only operates on diagnostics, and it no longer knows anything about nodes, so the info is lost by that time. We could probably still go this way by making a visitor emit special per-line path diagnostics that are all ignored by all consumers except yours. This may actually be the best way to go, but such patch would be very intrusive because there are many switches by diagnostic kinds all over the place and they all would need to be updated.

[NoQ]

So we have an ExplodedGraph, in that there's an ExplodedNode against which the report is being thrown, we have a bunch of BugReporterVisitors that walk from that node to the root of the graph and mark places they find interesting with PathDiagnosticPieces of different kinds, and PathDiagnosticConsumers (such as Plist or Html) that look at the vector of pieces and display it to the user.

It sounds solid (even if a bit over-engineered) to implement your counterexample generator as a set of:

1. new class of PathDiagnosticPieces that holds information that you need about a single line of code. Like, a while ago i was adding blue bubbles to scan-build (D24278), you might use this as an example on how to add a new class of diagnostic pieces.
2. a new BugReporterVisitor attached to all reports that puts such piece on every line of code. You already have it, but now it'd return the piece instead of printing stuff to console. Now that i think of it, the best place to add a visitor to all reports would be GRBugReporter::generatePathDiagnostic() - this is where other non-checker-specific visitors are added.
3. a new PathDiagnosticConsumer that would transform your new pieces into report files or however you want to present the results. I guess you could follow the examples of the existing consumers here; i didn't hack much on those, but there doesn't seem to be much boilerplate here. Most of the complicated processing, if any, goes here, the visitor can at best provide a set of pieces in chronological order, he cannot rearrange them anyhow but the consumer can.

[dcoughlin]

This is seems like a very useful visualization, *especially* for loops. Can we this patch get it into a state where it can be committed and used for debugging purposes?

One possibility is to turn this into a debug checker similar to debug.ViewExplodedGraph. That checker registers for a checkEndAnalysis() callback and traverses the node graph (see DebugCheckers.cpp). Can you do the same here? It doesn't look like you really need this to be a BugReporterVisitor -- and making it a debug checker would avoid outputting multiple copies for each diagnostic consumer.

You could also control file output with an analyzer-config option that takes an optional path.

[alexander-shaposhnikov]

lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

1976

spaces around '=' (maybe clang-format this diff ?)

[NoQ]

In D40809#954858, @dcoughlin wrote:

One possibility is to turn this into a debug checker similar to debug.ViewExplodedGraph. That checker registers for a checkEndAnalysis() callback and traverses the node graph (see DebugCheckers.cpp). Can you do the same here? It doesn't look like you really need this to be a BugReporterVisitor -- and making it a debug checker would avoid outputting multiple copies for each diagnostic consumer.

These prints are only for actual bugs, not for the whole graph. Even if we identify error nodes in the final graph, we're unlikely to identify which of them are suppressed by visitors.

[dcoughlin]

In D40809#954890, @NoQ wrote:

In D40809#954858, @dcoughlin wrote:

One possibility is to turn this into a debug checker similar to debug.ViewExplodedGraph. That checker registers for a checkEndAnalysis() callback and traverses the node graph (see DebugCheckers.cpp). Can you do the same here? It doesn't look like you really need this to be a BugReporterVisitor -- and making it a debug checker would avoid outputting multiple copies for each diagnostic consumer.

These prints are only for actual bugs, not for the whole graph. Even if we identify error nodes in the final graph, we're unlikely to identify which of them are suppressed by visitors.

As it stands, this is a debugging tool not a way to communicate error paths to end users. (I think that, too, would be very helpful but I'd like to see this as a debugging aid first.) The workflow for debugging would be more like viewing the exploded graph than (say) emitting html diagnostics.

My point is this: this is valuable as a debugging tool, we should get it committed as such. We can work on making it user facing separately.

[NoQ]

In D40809#955929, @dcoughlin wrote:

As it stands, this is a debugging tool not a way to communicate error paths to end users. (I think that, too, would be very helpful but I'd like to see this as a debugging aid first.) The workflow for debugging would be more like viewing the exploded graph than (say) emitting html diagnostics.

My point is this: this is valuable as a debugging tool, we should get it committed as such. We can work on making it user facing separately.

Per-report dumps are still much more useful for a debugging tool than whole-graph dumps. I guess such tool would be used on live code, not on reduced examples, and in this case there would be a *lot* of noise we'd want to avoid.

[george.karpenkov]

@dcoughlin my current iteration creates a PathDiagnosticConsumer which outputs HTML with this report. I think that makes much more sense (as essentially this is a way of visualizing the error path).

[george.karpenkov]

Fixed formatting, moved output to diagnostic consumer.

[george.karpenkov]

@dcoughlin @NoQ I think this version is reasonable enough to get committed. Another easy iteration would be to change visitor to simply add the diagnostic to path, and move the actual printing to CounterexampleDiagnostics.

[alexander-shaposhnikov]

Are there any plans to add tests for this ?

[george.karpenkov]

@alexshap That's a good question, and honestly I am not sure.
It is probably a good idea to have the tests which run the counterexample dumper and check that it does not crash.
As for the contents, I'm not sure: I would like to switch to generating HTML, and testing HTML output is IMO close to useless, because it has all the presentation stuff in it.
(it could have been possible to e.g. make the output mode which generates JSON, test that, and then use javascript templating to convert it to HTML, but that would not allow reusing existing code for outputting HTML formatted code with macros expanded properly)

[george.karpenkov]

Abandoned in favor of https://reviews.llvm.org/D41378

docs/ClangCommandLineReference.rst

 Run the static analyzer
 
 .. option:: --analyze-auto
 
 .. option:: --analyzer-no-default-checks
 
 .. option:: --analyzer-output<arg>
 
-Static analyzer report output format (html\|plist\|plist-multi-file\|plist-html\|text).
+Static analyzer report output format (html\|plist\|plist-multi-file\|plist-html\|text|counterexample).
 
 .. option:: -ansi, --ansi
 
 .. option:: -arch <arg>
 
 .. program:: clang1
 .. option:: -arch\_errors\_fatal
 .. program:: clang

include/clang/Driver/Options.td

 def _mhwdiv_EQ : Joined<["--"], "mhwdiv=">, Alias<mhwdiv_EQ>;
 def _mhwdiv : Separate<["--"], "mhwdiv">, Alias<mhwdiv_EQ>;
 def _CLASSPATH_EQ : Joined<["--"], "CLASSPATH=">, Alias<fclasspath_EQ>;
 def _CLASSPATH : Separate<["--"], "CLASSPATH">, Alias<fclasspath_EQ>;
 def _all_warnings : Flag<["--"], "all-warnings">, Alias<Wall>;
 def _analyze_auto : Flag<["--"], "analyze-auto">, Flags<[DriverOption]>;
 def _analyzer_no_default_checks : Flag<["--"], "analyzer-no-default-checks">, Flags<[DriverOption]>;
 def _analyzer_output : JoinedOrSeparate<["--"], "analyzer-output">, Flags<[DriverOption]>,
-  HelpText<"Static analyzer report output format (html|plist|plist-multi-file|plist-html|text).">;
+  HelpText<"Static analyzer report output format (html|plist|plist-multi-file|plist-html|text|counterexample).">;
 def _analyze : Flag<["--"], "analyze">, Flags<[DriverOption, CoreOption]>,
   HelpText<"Run the static analyzer">;
 def _assemble : Flag<["--"], "assemble">, Alias<S>;
 def _assert_EQ : Joined<["--"], "assert=">, Alias<A>;
 def _assert : Separate<["--"], "assert">, Alias<A>;
 def _bootclasspath_EQ : Joined<["--"], "bootclasspath=">, Alias<fbootclasspath_EQ>;
 def _bootclasspath : Separate<["--"], "bootclasspath">, Alias<fbootclasspath_EQ>;
 def _classpath_EQ : Joined<["--"], "classpath=">, Alias<fclasspath_EQ>;

include/clang/StaticAnalyzer/Core/Analyses.def

 #endif
 
 ANALYSIS_DIAGNOSTICS(HTML, "html", "Output analysis results using HTML", createHTMLDiagnosticConsumer)
 ANALYSIS_DIAGNOSTICS(HTML_SINGLE_FILE, "html-single-file", "Output analysis results using HTML (not allowing for multi-file bugs)", createHTMLSingleFileDiagnosticConsumer)
 ANALYSIS_DIAGNOSTICS(PLIST, "plist", "Output analysis results using Plists", createPlistDiagnosticConsumer)
 ANALYSIS_DIAGNOSTICS(PLIST_MULTI_FILE, "plist-multi-file", "Output analysis results using Plists (allowing for multi-file bugs)", createPlistMultiFileDiagnosticConsumer)
 ANALYSIS_DIAGNOSTICS(PLIST_HTML, "plist-html", "Output analysis results using HTML wrapped with Plists", createPlistHTMLDiagnosticConsumer)
 ANALYSIS_DIAGNOSTICS(TEXT, "text", "Text output of analysis results", createTextPathDiagnosticConsumer)
+ANALYSIS_DIAGNOSTICS(COUNTEREXAMPLE, "counterexample", "Output counterexample information using HTML", createCounterexampleDiagnosticsConsumer)
+
 
 #ifndef ANALYSIS_PURGE
 #define ANALYSIS_PURGE(NAME, CMDFLAG, DESC)
 #endif
 
 ANALYSIS_PURGE(PurgeStmt,  "statement", "Purge symbols, bindings, and constraints before every statement")
 ANALYSIS_PURGE(PurgeBlock, "block", "Purge symbols, bindings, and constraints before every basic block")
 ANALYSIS_PURGE(PurgeNone,  "none", "Do not purge symbols, bindings, or constraints")

include/clang/StaticAnalyzer/Core/AnalyzerOptions.h

public:
   /// This is controlled by the 'prune-paths' config option, which accepts the
   /// values "true" and "false".
   bool shouldPrunePaths();
 
   /// Returns true if 'static' initializers should be in conditional logic
   /// in the CFG.
   bool shouldConditionalizeStaticInitializers();
 
+  /// \return true if counterexamples should be dumped to stderr.
+  bool shouldDumpCounterexample();
+
   // Returns the size of the functions (in basic blocks), which should be
   // considered to be small enough to always inline.
   //
   // This is controlled by "ipa-always-inline-size" analyzer-config option.
   unsigned getAlwaysInlineSize();
 
   // Returns the bound on the number of basic blocks in an inlined function
   // (50 by default).

include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h

 ///
 /// \return Whether or not the function was able to add visitors for this
 ///         statement. Note that returning \c true does not actually imply
 ///         that any visitors were added.
 bool trackNullOrUndefValue(const ExplodedNode *N, const Stmt *S, BugReport &R,
                            bool IsArg = false,
                            bool EnableNullFPSuppression = true);
 
+/// \return visitor which performs counterexample printing.
+/// TODO: it is not very nice that the type is hidden...
+std::unique_ptr<BugReporterVisitor> getCounterexamplePrinter();
+
 const Expr *getDerefExpr(const Stmt *S);
 const Stmt *GetDenomExpr(const ExplodedNode *N);
 const Stmt *GetRetValExpr(const ExplodedNode *N);
 bool isDeclRefExprToReference(const Expr *E);
 
 
 } // end namespace clang
 } // end namespace ento
 } // end namespace bugreporter
 
 
 #endif

include/clang/StaticAnalyzer/Core/BugReporter/PathDiagnostic.h

public:
 
   virtual void FlushDiagnosticsImpl(std::vector<const PathDiagnostic *> &Diags,
                                     FilesMade *filesMade) = 0;
 
   virtual StringRef getName() const = 0;
 
   void HandlePathDiagnostic(std::unique_ptr<PathDiagnostic> D);
 
-  enum PathGenerationScheme { None, Minimal, Extensive, AlternateExtensive };
+  enum PathGenerationScheme {
+    None,
+    Minimal,
+    Extensive,
+    AlternateExtensive,
+    CounterexampleDump
+  };
   virtual PathGenerationScheme getGenerationScheme() const { return Minimal; }
   virtual bool supportsLogicalOpControlFlow() const { return false; }
   
   /// Return true if the PathDiagnosticConsumer supports individual
   /// PathDiagnostics that span multiple files.
   virtual bool supportsCrossFileDiagnostics() const { return false; }
 
 protected:

lib/StaticAnalyzer/Core/AnalyzerOptions.cpp

 bool AnalyzerOptions::shouldPrunePaths() {
   return getBooleanOption("prune-paths", true);
 }
 
 bool AnalyzerOptions::shouldConditionalizeStaticInitializers() {
   return getBooleanOption("cfg-conditional-static-initializers", true);
 }
 
+bool AnalyzerOptions::shouldDumpCounterexample() {
+  return getBooleanOption("dump-counterexample", false);
+}
+
 bool AnalyzerOptions::shouldInlineLambdas() {
   if (!InlineLambdas.hasValue())
     InlineLambdas = getBooleanOption("inline-lambdas", /*Default=*/true);
   return InlineLambdas.getValue();
 }
 
 bool AnalyzerOptions::shouldWidenLoops() {
   if (!WidenLoops.hasValue())

lib/StaticAnalyzer/Core/BugReporter.cpp

       V->VisitNode(N, Pred, PDB, *R);
 
     N = Pred;
   }
 
   return R->isValid();
 }
 
+/// Runs \c PrinterVisitor on the diagnostics.
+/// Does not run any other visitors.
+static bool GenerateCounterexampleDiagnostic(PathDiagnostic &PD,
+                                             PathDiagnosticBuilder &PDB,
+                                             const ExplodedNode *N) {
+  N = N->getFirstPred();
+  if (!N)
+    return true;
+
+  BugReport *R = PDB.getBugReport();
+  auto V = bugreporter::getCounterexamplePrinter();
+
+  while (const ExplodedNode *Pred = N->getFirstPred()) {
+    std::shared_ptr<PathDiagnosticPiece> Diag = V->VisitNode(N, Pred, PDB, *R);
+    N = Pred;
+  }
+  return R->isValid();
+}
+
 //===----------------------------------------------------------------------===//
 // "Minimal" path diagnostic generation algorithm.
 //===----------------------------------------------------------------------===//
 typedef std::pair<PathDiagnosticCallPiece*, const ExplodedNode*> StackDiagPair;
 typedef SmallVector<StackDiagPair, 6> StackDiagVector;
 
 static void updateStackPiecesWithMessage(PathDiagnosticPiece &P,
                                          StackDiagVector &CallStack) {

         GenerateExtensivePathDiagnostic(PD, PDB, N, LCM, visitors);
         break;
       case PathDiagnosticConsumer::Minimal:
         GenerateMinimalPathDiagnostic(PD, PDB, N, LCM, visitors);
         break;
       case PathDiagnosticConsumer::None:
         GenerateVisitorsOnlyPathDiagnostic(PD, PDB, N, visitors);
         break;
+      case PathDiagnosticConsumer::CounterexampleDump:
+        GenerateCounterexampleDiagnostic(PD, PDB, N);
+        break;
       }
 
       // Clean up the visitors we used.
       visitors.clear();
 
       // Did anything change while generating this path?
       finalReportConfigToken = R->getConfigurationChangeToken();
     } while (finalReportConfigToken != origReportConfigToken);

lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

 #include "clang/Analysis/CFGStmtMap.h"
 #include "clang/Lex/Lexer.h"
 #include "clang/StaticAnalyzer/Core/BugReporter/BugReporter.h"
 #include "clang/StaticAnalyzer/Core/BugReporter/PathDiagnostic.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExplodedGraph.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "llvm/ADT/SetVector.h"
 #include "llvm/ADT/SmallString.h"
 #include "llvm/ADT/StringExtras.h"
 #include "llvm/Support/raw_ostream.h"
+#include <cmath>
+#include <string.h>
 
 using namespace clang;
 using namespace ento;
 
 using llvm::FoldingSetNodeID;
 
 //===----------------------------------------------------------------------===//
 // Utility functions.
CXXSelfAssignmentBRVisitor::VisitNode(const ExplodedNode *Succ,
   Out << "Assuming " << Met->getParamDecl(0)->getName() <<
     ((Param == This) ? " == " : " != ") << "*this";
 
   auto Piece = std::make_shared<PathDiagnosticEventPiece>(L, Out.str());
   Piece->addRange(Met->getSourceRange());
 
   return std::move(Piece);
 }
+
+/// Export the counterexample to C.
+class PrinterVisitor final : public BugReporterVisitorImpl<PrinterVisitor> {
+
+  /// File ID followed by a line number.
+  llvm::SetVector<std::pair<FileID, unsigned>> VisitedLines;
+
+  /// Output stream to write into.
+  raw_ostream &Ostream;
+
+  /// State machine variables.
+  mutable bool DonePrinting = false;
+
+  /// Max number of chars used to display the filename.
+  static const unsigned MAX_FILENAME_MARGIN = 80;
+  static const unsigned MARGIN_SEP_LEN = 1;
+  static constexpr const char *const REPORT_SEPARATOR =
+      "/* ============================================================== */\n";
+
+public:
+  PrinterVisitor(raw_ostream &Ostream) : Ostream(Ostream) {}
+
+  PrinterVisitor() = delete;
+
+  void Profile(llvm::FoldingSetNodeID &ID) const override {
+    static int Tag = 0;
+    ID.AddPointer(&Tag);
+  }
+
+  std::shared_ptr<PathDiagnosticPiece> VisitNode(const ExplodedNode *N,
+                                                 const ExplodedNode *PrevN,
+                                                 BugReporterContext &BRC,
+                                                 BugReport &BR) override {
+    SourceManager &SM = BRC.getSourceManager();
+
+    if (DonePrinting) { // Printing was done, do nothing.
+      return nullptr;
+    } else if (!PrevN->getFirstPred()) { // Finished report, do printing.
+
+      // Went through the entire bug report, now print the lines in reverse
+      // order.
+      bool Status = doPrinting(SM);
+      if (!Status)
+        Ostream << "Error while printing\n";
+      Ostream << REPORT_SEPARATOR;
+      DonePrinting = true;
+      return nullptr;
+    } else if (const Stmt *S = PathDiagnosticLocation::getStmt(N)) {
+      SourceLocation Loc = S->getSourceRange().getBegin();
+      VisitedLines.insert(
+          std::make_pair(SM.getFileID(Loc), SM.getSpellingLineNumber(Loc)));
+    }
+    return nullptr;
+  }
+
+private:
+  /// Print locations serialized to \c VisitedLines.
+  bool doPrinting(SourceManager &SM) {
+    unsigned Margin = calculateMargin(SM);
+    for (auto It = VisitedLines.rbegin(), ItEnd = VisitedLines.rend();
+         It != ItEnd; ++It) {
+      FileID FID = It->first;
+      unsigned LineNo = It->second;
+      bool Status = printLine(SM, FID, LineNo, Margin);
+      if (!Status)
+        return false;
+    }
+    return true;
+  }
+
+  /// Print line \p LineNo from file \p FID, with left margin \p Margin.
+  /// \return \c true on success, \c false on failure.
+  bool printLine(SourceManager &SM, FileID FID, unsigned LineNo,
+                 unsigned Margin) {
+    SourceLocation Location = SM.translateLineCol(FID, LineNo, 1);
+    unsigned Offset = SM.getFileOffset(Location);
+
+    // Print location first.
+    int Status = printLocation(SM, Location, Margin);
+    if (!Status)
+      return false;
+
+    bool Invalid = false;
+    const char *BufferStart = SM.getBufferData(FID, &Invalid).data();
+    if (Invalid)
+      return false;
+
+    unsigned FileEndOffset = SM.getFileOffset(SM.getLocForEndOfFile(FID));
+    for (unsigned i = Offset; BufferStart[i] != '\n' && i < FileEndOffset; ++i)
+      Ostream << BufferStart[i];
+
+    Ostream << "\n";
+    return true;
+  }
+
+  /// Print location in left margin.
+  bool printLocation(SourceManager &SM, SourceLocation Loc, unsigned Margin) {
+    Loc = SM.getExpansionLoc(Loc);
+    PresumedLoc PLoc = SM.getPresumedLoc(Loc);
+    if (PLoc.isInvalid())
+      return false;
+
+    uint64_t SavedPos = Ostream.tell();
+    Ostream << PLoc.getFilename() << ":" << PLoc.getLine();
+    uint64_t Delta = Ostream.tell() - SavedPos;
+    assert(Margin >= Delta);
+    for (unsigned i = Delta; i < Margin; i++)
+      Ostream << " ";
+    Ostream << "|";
+
+    return true;
+  }
+
+  /// \return smallest margin required to fit all filenames present
+  /// in the counterexample.
+  unsigned calculateMargin(SourceManager &SM) {
+    unsigned Out = 0;
+    for (auto Pair : VisitedLines) {
+      FileID FID = Pair.first;
+      unsigned LineNo = Pair.second;
+      SourceLocation Loc = SM.translateLineCol(FID, LineNo, 1);
+      Loc = SM.getExpansionLoc(Loc);
+      PresumedLoc PLoc = SM.getPresumedLoc(Loc);
+      if (PLoc.isInvalid())
+        continue;
+
+      // Take logarithm to figure out number of chars required.
+      long LineMargin = 1 + std::lround(floor(log10(PLoc.getLine())));
+      size_t FilenameMargin = strnlen(PLoc.getFilename(), MAX_FILENAME_MARGIN);
+      assert(LineMargin > 0);
+      unsigned RequiredMargin = FilenameMargin + LineMargin + MARGIN_SEP_LEN;
+      if (RequiredMargin > Out)
+        Out = RequiredMargin;
+    }
+    return Out;
+  }
+};
+
+std::unique_ptr<BugReporterVisitor> bugreporter::getCounterexamplePrinter() {
+  return llvm::make_unique<PrinterVisitor>(llvm::errs());
+}

lib/StaticAnalyzer/Core/CMakeLists.txt

add_clang_library(clangStaticAnalyzerCore
   Checker.cpp
   CheckerContext.cpp
   CheckerHelpers.cpp
   CheckerManager.cpp
   CheckerRegistry.cpp
   CommonBugCategories.cpp
   ConstraintManager.cpp
   CoreEngine.cpp
+  CounterexampleDiagnostics.cpp
   DynamicTypeMap.cpp
   Environment.cpp
   ExplodedGraph.cpp
   ExprEngine.cpp
   ExprEngineC.cpp
   ExprEngineCXX.cpp
   ExprEngineCallAndReturn.cpp
   ExprEngineObjC.cpp

lib/StaticAnalyzer/Core/CounterexampleDiagnostics.cpp

+#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
+#include "clang/StaticAnalyzer/Core/BugReporter/PathDiagnostic.h"
+#include "clang/StaticAnalyzer/Core/PathDiagnosticConsumers.h"
+#include "llvm/ADT/StringRef.h"
+
+using namespace clang;
+using namespace ento;
+
+namespace {
+
+/// Dump the counterexample to stderr.
+class CounterexampleDiagnostics : public PathDiagnosticConsumer {
+
+public:
+  CounterexampleDiagnostics() {}
+
+  bool supportsCrossFileDiagnostics() const override { return false; }
+
+  ~CounterexampleDiagnostics() override { FlushDiagnostics(nullptr); }
+
+  StringRef getName() const override { return "CounterexampleDiagnostics"; }
+
+  /// Force usage of the counterexample visitor.
+  PathGenerationScheme getGenerationScheme() const override {
+    return CounterexampleDump;
+  }
+
+  void FlushDiagnosticsImpl(std::vector<const PathDiagnostic *> &Diags,
+                            FilesMade *filesMade) override {
+    // FIXME move counterexample dumping logic here.
+  }
+};
+
+} // end anonymous namespace
+
+void ento::createCounterexampleDiagnosticsConsumer(
+    AnalyzerOptions &AnalyzerOpts, PathDiagnosticConsumers &C,
+    const std::string &prefix, const Preprocessor &PP) {
+  C.push_back(new CounterexampleDiagnostics());
+}