Merge pull request diffblue#180 from diffblue/feature/symbol_table_detailed_irept_dump

SEC-46: Extended HTML dump of symbols table (irept structure for types and initial values).

Author: marek-trtik

src/summaries/summary_dump.cpp

@@ -7,6 +7,7 @@
 #include <util/file_util.h>
 #include <util/msgstream.h>
 #include <util/simplify_expr.h>
+#include <util/unique_name.h>
 #include <algorithm>
 #include <fstream>
 #include <sstream>
@@ -471,13 +472,60 @@ std::string  dump_symbol_table_symbols_in_html(
           << to_html_text(symbol.location.as_string_with_cwd()) << "</td>\n";
     ostr << "        </tr>\n";
     ostr << "        <tr>\n";
-    ostr << "          <td>Type of symbol</td>\n";
+
+    const std::string &output_directory=fileutl_concatenate_file_paths(
+      fileutl_parse_path_in_pathname(pathname), "IREP");
+    fileutl_create_directory(output_directory);
+
+    struct localt
+    {
+      static bool exists_check(
+        const std::string &file_name_base,
+        const std::string &output_directory)
+      {
+        return fileutl_file_exists(fileutl_concatenate_file_paths(
+          output_directory, file_name_base+".txt"));
+      }
+    };
+    const auto exists_checker=std::bind(
+      &localt::exists_check,
+      std::placeholders::_1,
+      std::cref(output_directory));
+
+    std::string irep_dump_fname=get_unique_name(
+      as_string(symbol.name)+"__TYPE", exists_checker)+".txt";
+    {
+      std::fstream irep_out(
+        fileutl_concatenate_file_paths(output_directory, irep_dump_fname),
+        std::ios_base::out);
+      dump_irept(symbol.type, irep_out, "");
+    }
+
+    ostr << "          <td>Type of symbol ["
+            "<a href=\"./IREP/"
+         << irep_dump_fname
+         << "\">details</a>"
+            "]</td>\n";
     ostr << "          <td>"
           << to_html_text(from_type(namespacet(symbol_table), "", symbol.type))
           << "</td>\n";
     ostr << "        </tr>\n";
     ostr << "        <tr>\n";
-    ostr << "          <td>Initial value of symbol</td>\n";
+
+    irep_dump_fname=get_unique_name(
+      as_string(symbol.name)+"__INIT", exists_checker)+".txt";
+    {
+      std::fstream irep_out(
+        fileutl_concatenate_file_paths(output_directory, irep_dump_fname),
+        std::ios_base::out);
+      dump_irept(symbol.value, irep_out, "");
+    }
+
+    ostr << "          <td>Initial value of symbol ["
+            "<a href=\"./IREP/"
+         << irep_dump_fname
+         << "\">details</a>"
+            "]</td>\n";
     ostr << "          <td>";
     if(symbol.value.id()==ID_code)
       ostr << "&lt;function-body&gt;";

src/util/Makefile

@@ -1,4 +1,5 @@
 SRC = json_serializer.cpp \
+      unique_name.cpp \
       # No more source files
 
 INCLUDES= -I .. -I ../../cbmc/src

src/util/unique_name.cpp

@@ -0,0 +1,21 @@
+// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved.
+
+/// \file
+/// Utility for construction of a unique name (like file name).
+
+#include <util/unique_name.h>
+
+std::string uniqueify(const std::string &base, unsigned long uniqueness)
+{
+  return uniqueness==0UL?base:base+'_'+std::to_string(uniqueness);
+}
+
+std::string get_unique_name(
+  const std::string &base_name,
+  std::function<bool(const std::string &)> exists)
+{
+  unsigned long uniqueness=0UL;
+  while(exists(uniqueify(base_name, uniqueness)))
+    ++uniqueness;
+  return uniqueify(base_name, uniqueness);
+}

src/util/unique_name.h

@@ -0,0 +1,18 @@
+// Copyright 2016-2017 DiffBlue Limited. All Rights Reserved.
+
+/// \file
+/// Utility for construction of a unique name (like file name).
+
+#ifndef CPROVER_SECURITY_SCANNER_UTIL_UNIQUE_NAME_H
+#define CPROVER_SECURITY_SCANNER_UTIL_UNIQUE_NAME_H
+
+#include <string>
+#include <functional>
+
+std::string uniqueify(const std::string &base, unsigned long uniqueness);
+
+std::string get_unique_name(
+  const std::string &base_name,
+  std::function<bool(const std::string &)> exists);
+
+#endif