Merge pull request #5240 from thk123/logging-structured-data

Logging structured data

Author: Thomas Kiley

src/goto-checker/symex_bmc_incremental_one_loop.cpp

@@ -137,27 +137,8 @@ bool symex_bmc_incremental_one_loopt::resume(
 }
 void symex_bmc_incremental_one_loopt::log_unwinding(unsigned unwind)
 {
-  const std::string unwind_num = std::to_string(unwind);
-  switch(output_ui)
-  {
-  case ui_message_handlert::uit::PLAIN:
-  {
-    log.statistics() << "Current unwinding: " << unwind_num << messaget::eom;
-    break;
-  }
-  case ui_message_handlert::uit::XML_UI:
-  {
-    xmlt xml("current-unwinding");
-    xml.data = unwind_num;
-    log.statistics() << xml << messaget::eom;
-    break;
-  }
-  case ui_message_handlert::uit::JSON_UI:
-  {
-    json_objectt json;
-    json["currentUnwinding"] = json_numbert(unwind_num);
-    log.statistics() << json << messaget::eom;
-    break;
-  }
-  }
+  structured_datat data{{{labelt({"current", "unwinding"}),
+                          structured_data_entryt::data_node(
+                            json_numbert{std::to_string(unwind)})}}};
+  log.statistics() << data;
 }

src/util/Makefile

@@ -87,6 +87,7 @@ SRC = allocate_objects.cpp \
       string_container.cpp \
       string_hash.cpp \
       string_utils.cpp \
+      structured_data.cpp \
       symbol.cpp \
       symbol_table_base.cpp \
       symbol_table.cpp \

src/util/json.cpp

@@ -8,6 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "json.h"
 
+#include "structured_data.h"
+
 #include <algorithm>
 #include <ostream>
 
@@ -204,3 +206,31 @@ bool operator==(const jsont &left, const jsont &right)
   }
   UNREACHABLE;
 }
+
+jsont json_node(const structured_data_entryt &entry)
+{
+  if(entry.is_leaf())
+    return entry.leaf_object();
+  else
+  {
+    json_objectt result;
+    for(const auto sub_entry : entry.children())
+    {
+      result[sub_entry.first.camel_case()] = json_node(sub_entry.second);
+    }
+    return std::move(result);
+  }
+}
+
+jsont to_json(const structured_datat &data)
+{
+  if(data.data().size() == 0)
+    return jsont{};
+
+  json_objectt result;
+  for(const auto sub_entry : data.data())
+  {
+    result[sub_entry.first.camel_case()] = json_node(sub_entry.second);
+  }
+  return std::move(result);
+}

src/util/json.h

@@ -18,6 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "irep.h"
 #include "range.h"
 
+class structured_datat;
+
 class json_objectt;
 class json_arrayt;
 
@@ -465,4 +467,27 @@ inline const json_stringt &to_json_string(const jsont &json)
 
 bool operator==(const jsont &left, const jsont &right);
 
+/// Convert the structured_datat into an json object. For example, the
+/// structured data:
+/// structured_datat data{
+///   {{labelt{{"my", "data"}},
+///      structured_data_entryt::entry(
+///        {{labelt{{"my", "number"}},
+///           structured_data_entryt::data_node(json_numbert("10"))},
+///         {labelt{{"my", "string"}},
+///           structured_data_entryt::data_node(json_stringt("hi"))}})}}};
+///
+/// Will produce:
+/// ```json
+/// {
+///   "myData": {
+///      "myNumber": 10
+///      "myString": "hi"
+///    }
+///  }
+/// ```
+/// \param data: The structured data to convert.
+/// \return The json object as specified.
+jsont to_json(const structured_datat &data);
+
 #endif // CPROVER_UTIL_JSON_H

src/util/message.cpp

@@ -64,6 +64,11 @@ void message_handlert::print(
     message_count.resize(level+1, 0);
   ++message_count[level];
 }
+void message_handlert::print(unsigned level, const structured_datat &data)
+{
+  // default to just printing out the data in a format
+  print(level, to_pretty(data));
+}
 
 messaget::~messaget()
 {

src/util/message.h

@@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "deprecate.h"
 #include "invariant.h"
 #include "source_location.h"
+#include "structured_data.h"
 
 class json_objectt;
 class jsont;
@@ -36,6 +37,8 @@ class message_handlert
 
   virtual void print(unsigned level, const jsont &json) = 0;
 
+  virtual void print(unsigned level, const structured_datat &data);
+
   virtual void print(
     unsigned level,
     const std::string &message,
@@ -256,6 +259,17 @@ class messaget
 
     mstreamt &operator<<(const json_objectt &data);
 
+    mstreamt &operator<<(const structured_datat &data)
+    {
+      if(this->tellp() > 0)
+        *this << eom; // force end of previous message
+      if(message.message_handler)
+      {
+        message.message_handler->print(message_level, data);
+      }
+      return *this;
+    }
+
     template <class T>
     mstreamt &operator << (const T &x)
     {

src/util/string_utils.cpp

@@ -167,3 +167,11 @@ std::string escape_non_alnum(const std::string &to_escape)
   }
   return escaped.str();
 }
+std::string capitalize(const std::string &str)
+{
+  if(str.empty())
+    return str;
+  std::string capitalized = str;
+  capitalized[0] = toupper(capitalized[0]);
+  return capitalized;
+}

src/util/string_utils.h

@@ -18,6 +18,8 @@ Author: Daniel Poetzl
 
 std::string strip_string(const std::string &s);
 
+std::string capitalize(const std::string &str);
+
 /// Given a string s, split into a sequence of substrings when separated by
 /// specified delimiter.
 /// \param s: The string to split up

src/util/structured_data.cpp

@@ -0,0 +1,172 @@
+/*******************************************************************\
+
+Module: Classes for representing generic structured data
+
+Author: Thomas Kiley
+
+\*******************************************************************/
+
+#include "structured_data.h"
+#include "range.h"
+#include "string_utils.h"
+#include <algorithm>
+
+labelt::labelt(std::vector<std::string> components) : components(components)
+{
+  PRECONDITION(!components.empty());
+  PRECONDITION(std::all_of(
+    components.begin(), components.end(), [](const std::string &component) {
+      return !component.empty() &&
+             std::none_of(component.begin(), component.end(), ::isupper);
+    }));
+}
+
+std::string labelt::camel_case() const
+{
+  std::ostringstream output;
+  output << *components.begin();
+  join_strings(
+    output, std::next(components.begin()), components.end(), "", capitalize);
+  return output.str();
+}
+
+std::string labelt::snake_case() const
+{
+  std::ostringstream output;
+  join_strings(output, components.begin(), components.end(), '_');
+  return output.str();
+}
+
+std::string labelt::kebab_case() const
+{
+  std::ostringstream output;
+  join_strings(output, components.begin(), components.end(), '-');
+  return output.str();
+}
+
+std::string labelt::pretty() const
+{
+  std::ostringstream output;
+  const auto range =
+    make_range(components.begin(), std::next(components.begin()))
+      .map(capitalize)
+      .concat(make_range(std::next(components.begin()), components.end()));
+
+  join_strings(output, range.begin(), range.end(), ' ');
+  return output.str();
+}
+
+bool labelt::operator<(const labelt &other) const
+{
+  return components < other.components;
+}
+
+structured_data_entryt structured_data_entryt::data_node(const jsont &data)
+{
+  // Structured data (e.g. arrays and objects) should use an entry
+  PRECONDITION(!(data.is_array() || data.is_object()));
+  return structured_data_entryt(data);
+}
+
+structured_data_entryt
+structured_data_entryt::entry(std::map<labelt, structured_data_entryt> children)
+{
+  return structured_data_entryt(std::move(children));
+}
+
+structured_data_entryt::structured_data_entryt(jsont data)
+  : data(std::move(data))
+{
+}
+
+structured_data_entryt::structured_data_entryt(
+  std::map<labelt, structured_data_entryt> children)
+  : _children(std::move(children))
+{
+}
+
+bool structured_data_entryt::is_leaf() const
+{
+  return _children.empty();
+}
+
+std::string structured_data_entryt::leaf_data() const
+{
+  return data.value;
+}
+const std::map<labelt, structured_data_entryt> &
+structured_data_entryt::children() const
+{
+  return _children;
+}
+
+jsont structured_data_entryt::leaf_object() const
+{
+  return data;
+}
+
+structured_datat::structured_datat(
+  std::map<labelt, structured_data_entryt> data)
+  : _data(std::move(data))
+{
+}
+
+std::vector<std::string>
+pretty_node(const std::pair<labelt, structured_data_entryt> &entry)
+{
+  const labelt &label = entry.first;
+  const structured_data_entryt &data = entry.second;
+  if(data.is_leaf())
+  {
+    std::ostringstream line;
+    line << label.pretty() << ": " << data.leaf_data();
+    return {line.str()};
+  }
+  else
+  {
+    const auto indent = [](const std::string &line) { return "\t" + line; };
+
+    const auto &children = data.children();
+    std::vector<std::vector<std::string>> lines =
+      make_range(children)
+        .map(pretty_node)
+        .map([&](std::vector<std::string> sub_lines) {
+          return make_range(sub_lines)
+            .map(indent)
+            .collect<std::vector<std::string>>();
+        })
+        .collect<std::vector<std::vector<std::string>>>();
+
+    std::vector<std::string> result;
+    for(const auto &sub_lines : lines)
+    {
+      result.insert(result.end(), sub_lines.begin(), sub_lines.end());
+    }
+    return result;
+  }
+}
+
+std::string to_pretty(const structured_datat &data)
+{
+  if(data.data().empty())
+    return "";
+
+  std::vector<std::vector<std::string>> lines =
+    make_range(data.data())
+      .map(pretty_node)
+      .collect<std::vector<std::vector<std::string>>>();
+  std::vector<std::string> flattened_lines;
+  for(const auto &line_section : lines)
+  {
+    flattened_lines.insert(
+      flattened_lines.end(), line_section.begin(), line_section.end());
+  }
+  std::ostringstream output;
+  join_strings(output, flattened_lines.begin(), flattened_lines.end(), "\n");
+  return output.str();
+}
+
+const std::map<labelt, structured_data_entryt> &structured_datat::data() const
+{
+  return _data;
+}