added show_on_source for abstract domains

The abstract states are shown in a different color on the source code text
of the program, as opposed to the goto-program dump.  Indentation of the
output of the abstract is made to match the indentation of the source code.

Author: Daniel Kroening

src/goto-analyzer/Makefile

@@ -3,6 +3,7 @@ SRC = goto_analyzer_main.cpp \
       taint_analysis.cpp \
       taint_parser.cpp \
       unreachable_instructions.cpp \
+      show_on_source.cpp \
       static_show_domain.cpp \
       static_simplifier.cpp \
       static_verifier.cpp \

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -57,11 +57,12 @@ Author: Daniel Kroening, [email protected]
 #include <util/unicode.h>
 #include <util/version.h>
 
-#include "taint_analysis.h"
-#include "unreachable_instructions.h"
+#include "show_on_source.h"
 #include "static_show_domain.h"
 #include "static_simplifier.h"
 #include "static_verifier.h"
+#include "taint_analysis.h"
+#include "unreachable_instructions.h"
 
 goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(
   int argc,
@@ -626,7 +627,18 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
 
     if(options.get_bool_option("show"))
     {
-      static_show_domain(goto_model, *analyzer, options, out);
+      if(
+        options.get_bool_option("json") || options.get_bool_option("xml") ||
+        options.get_bool_option("dot") ||
+        options.get_bool_option("dependence-graph"))
+      {
+        static_show_domain(goto_model, *analyzer, options, out);
+      }
+      else
+      {
+        show_on_source(goto_model, *analyzer, get_message_handler());
+      }
+
       return CPROVER_EXIT_SUCCESS;
     }
     else if(options.get_bool_option("verify"))

src/goto-analyzer/show_on_source.cpp

@@ -0,0 +1,145 @@
+/*******************************************************************\
+
+Module: goto-analyzer
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "show_on_source.h"
+
+#include <util/file_util.h>
+#include <util/message.h>
+#include <util/unicode.h>
+
+#include <analyses/ai.h>
+
+#include <fstream>
+
+/// get the source files with non-top abstract states
+static std::set<std::string>
+get_source_files(const goto_modelt &goto_model, const ai_baset &ai)
+{
+  std::set<std::string> files;
+
+  for(const auto &f : goto_model.goto_functions.function_map)
+  {
+    forall_goto_program_instructions(i_it, f.second.body)
+    {
+      const auto abstract_state = ai.abstract_state_before(i_it);
+      if(abstract_state->is_top())
+        continue; // ignore
+
+      if(i_it->source_location.get_line().empty())
+        continue; // ignore
+
+      auto f = i_it->source_location.full_path();
+
+      if(!f.empty())
+        files.insert(f);
+    }
+  }
+
+  return files;
+}
+
+/// print a string with indent to match given sample line
+static void print_with_indent(
+  const std::string &src,
+  const std::string &indent_line,
+  std::ostream &out)
+{
+  const std::size_t p = indent_line.find_first_not_of(" \t");
+  const std::string indent =
+    p == std::string::npos ? std::string("") : std::string(indent_line, 0, p);
+  std::istringstream in(src);
+  std::string src_line;
+  while(std::getline(in, src_line))
+    out << indent << src_line << '\n';
+}
+
+/// output source code annotated with abstract states for given file
+void show_on_source(
+  const std::string &source_file,
+  const goto_modelt &goto_model,
+  const ai_baset &ai,
+  message_handlert &message_handler)
+{
+#ifdef _MSC_VER
+  std::ifstream in(widen(source_file));
+#else
+  std::ifstream in(source_file);
+#endif
+
+  messaget message(message_handler);
+
+  if(!in)
+  {
+    message.warning() << "Failed to open `" << source_file << "'"
+                      << messaget::eom;
+    return;
+  }
+
+  std::map<std::size_t, ai_baset::locationt> line_map;
+
+  // Collect line numbers with non-top abstract states.
+  // We pick the _first_ state for each line.
+  for(const auto &f : goto_model.goto_functions.function_map)
+  {
+    forall_goto_program_instructions(i_it, f.second.body)
+    {
+      auto abstract_state = ai.abstract_state_before(i_it);
+      if(abstract_state->is_top())
+        continue; // ignore
+
+      const auto line = i_it->source_location.get_line();
+
+      if(line.empty())
+        continue; // ignore
+
+      if(i_it->source_location.full_path() == source_file)
+      {
+        const std::size_t line_no = stoull(id2string(line));
+        if(line_map.find(line_no) == line_map.end())
+          line_map[line_no] = i_it;
+      }
+    }
+  }
+
+  // now print file to message handler
+  const namespacet ns(goto_model.symbol_table);
+
+  std::string line;
+  for(std::size_t line_no = 1; std::getline(in, line); line_no++)
+  {
+    const auto map_it = line_map.find(line_no);
+    if(map_it != line_map.end())
+    {
+      auto abstract_state = ai.abstract_state_before(map_it->second);
+      std::ostringstream state_str;
+      abstract_state->output(state_str, ai, ns);
+      if(!state_str.str().empty())
+      {
+        message.result() << messaget::blue;
+        print_with_indent(state_str.str(), line, message.result());
+        message.result() << messaget::reset;
+      }
+    }
+
+    message.result() << line << messaget::eom;
+  }
+}
+
+/// output source code annotated with abstract states
+void show_on_source(
+  const goto_modelt &goto_model,
+  const ai_baset &ai,
+  message_handlert &message_handler)
+{
+  // first gather the source files that have something to show
+  const auto source_files = get_source_files(goto_model, ai);
+
+  // now show file-by-file
+  for(const auto &source_file : source_files)
+    show_on_source(source_file, goto_model, ai, message_handler);
+}

src/goto-analyzer/show_on_source.h

@@ -0,0 +1,18 @@
+/*******************************************************************\
+
+Module: goto-analyzer
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_GOTO_ANALYZER_SHOW_ON_SOURCE_H
+#define CPROVER_GOTO_ANALYZER_SHOW_ON_SOURCE_H
+
+class ai_baset;
+class goto_modelt;
+class message_handlert;
+
+void show_on_source(const goto_modelt &, const ai_baset &, message_handlert &);
+
+#endif // CPROVER_GOTO_ANALYZER_SHOW_ON_SOURCE_H