Show abstract states in program source code

regression/goto-analyzer/show-on-source/main.c

@@ -0,0 +1,12 @@
+int i = 1;
+
+int main()
+{
+  int j;
+  _Bool nondet;
+
+  if(j >= 1 && j <= 10)
+  {
+    i++;
+  }
+}

regression/goto-analyzer/show-on-source/main.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--intervals --show-on-source
+^EXIT=0$
+^SIGNAL=0$
+^  if\(j >= 1 && j <= 10\)$
+^    1 <= i <= 1$
+^    1 <= main::1::j <= 10$
+--
+^warning: ignoring

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,
@@ -191,6 +192,11 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("show", true);
     options.set_option("general-analysis", true);
   }
+  else if(cmdline.isset("show-on-source"))
+  {
+    options.set_option("show-on-source", true);
+    options.set_option("general-analysis", true);
+  }
   else if(cmdline.isset("verify"))
   {
     options.set_option("verify", true);
@@ -629,6 +635,11 @@ int goto_analyzer_parse_optionst::perform_analysis(const optionst &options)
       static_show_domain(goto_model, *analyzer, options, out);
       return CPROVER_EXIT_SUCCESS;
     }
+    else if(options.get_bool_option("show-on-source"))
+    {
+      show_on_source(goto_model, *analyzer, get_message_handler());
+      return CPROVER_EXIT_SUCCESS;
+    }
     else if(options.get_bool_option("verify"))
     {
       result = static_verifier(goto_model,
@@ -800,7 +811,8 @@ void goto_analyzer_parse_optionst::help()
     " goto-analyzer file.c ...     source file names\n"
     "\n"
     "Task options:\n"
-    " --show                       display the abstract domains\n"
+    " --show                       display the abstract states on the goto program\n" // NOLINT(*)
+    " --show-on-source             display the abstract states on the source\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     " --verify                     use the abstract domains to check assertions\n"
     // NOLINTNEXTLINE(whitespace/line_length)

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -145,7 +145,7 @@ class optionst;
   "(non-null)(show-non-null)" \
   "(constants)" \
   "(dependence-graph)" \
-  "(show)(verify)(simplify):" \
+  "(show)(verify)(simplify):(show-on-source)" \
   "(location-sensitive)(concurrent)" \
   "(no-simplify-slicing)" \
 // clang-format on

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 name of the file referred to at a location loc,
+/// if any
+static optionalt<std::string>
+show_location(const ai_baset &ai, ai_baset::locationt loc)
+{
+  const auto abstract_state = ai.abstract_state_before(loc);
+  if(abstract_state->is_top())
+    return {};
+
+  if(loc->source_location.get_line().empty())
+    return {};
+
+  return loc->source_location.full_path();
+}
+
+/// 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 file = show_location(ai, i_it);
+      if(file.has_value())
+        files.insert(file.value());
+    }
+  }
+
+  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)
+    {
+      const auto file = show_location(ai, i_it);
+      if(file.has_value() && file.value() == source_file)
+      {
+        const std::size_t line_no =
+          stoull(id2string(i_it->source_location.get_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