Property reporting utilities [blocks: 3584]

src/goto-checker/Makefile

@@ -2,6 +2,7 @@ SRC = bmc_util.cpp \
       incremental_goto_checker.cpp \
       goto_verifier.cpp \
       properties.cpp \
+      report_util.cpp \
       solver_factory.cpp \
       symex_coverage.cpp \
       symex_bmc.cpp \

src/goto-checker/properties.cpp

@@ -12,6 +12,8 @@ Author: Daniel Kroening, Peter Schrammel
 #include "properties.h"
 
 #include <util/invariant.h>
+#include <util/json.h>
+#include <util/xml.h>
 
 std::string as_string(resultt result)
 {
@@ -88,3 +90,40 @@ propertiest initialize_properties(const abstract_goto_modelt &goto_model)
   }
   return properties;
 }
+
+std::string
+as_string(const irep_idt &property_id, const property_infot &property_info)
+{
+  return "[" + id2string(property_id) + "] " + property_info.description +
+         ": " + as_string(property_info.status);
+}
+
+xmlt xml(const irep_idt &property_id, const property_infot &property_info)
+{
+  xmlt xml_result("result");
+  xml_result.set_attribute("property", id2string(property_id));
+  xml_result.set_attribute("status", as_string(property_info.status));
+  return xml_result;
+}
+
+json_objectt
+json(const irep_idt &property_id, const property_infot &property_info)
+{
+  json_objectt result;
+  result["property"] = json_stringt(property_id);
+  result["description"] = json_stringt(property_info.description);
+  result["status"] = json_stringt(as_string(property_info.status));
+  return result;
+}
+
+std::size_t
+count_properties(const propertiest &properties, property_statust status)
+{
+  std::size_t count = 0;
+  for(const auto &property_pair : properties)
+  {
+    if(property_pair.second.status == status)
+      ++count;
+  }
+  return count;
+}

src/goto-checker/properties.h

@@ -16,6 +16,9 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include <goto-programs/goto_model.h>
 
+class json_objectt;
+class xmlt;
+
 /// The status of a property
 enum class property_statust
 {
@@ -73,4 +76,15 @@ typedef std::unordered_map<irep_idt, property_infot> propertiest;
 /// Returns the properties in the goto model
 propertiest initialize_properties(const abstract_goto_modelt &);
 
+std::string
+as_string(const irep_idt &property_id, const property_infot &property_info);
+
+xmlt xml(const irep_idt &property_id, const property_infot &property_info);
+
+json_objectt
+json(const irep_idt &property_id, const property_infot &property_info);
+
+/// Return the number of properties with given \p status
+std::size_t count_properties(const propertiest &, property_statust);
+
 #endif // CPROVER_GOTO_CHECKER_PROPERTIES_H

src/goto-checker/report_util.cpp

@@ -0,0 +1,130 @@
+/*******************************************************************\
+
+Module: Bounded Model Checking Utilities
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Bounded Model Checking Utilities
+
+#include "report_util.h"
+
+#include <algorithm>
+
+#include <util/json.h>
+#include <util/ui_message.h>
+#include <util/xml.h>
+
+void output_properties(
+  const propertiest &properties,
+  ui_message_handlert &ui_message_handler)
+{
+  messaget log(ui_message_handler);
+  switch(ui_message_handler.get_ui())
+  {
+  case ui_message_handlert::uit::PLAIN:
+  {
+    log.result() << "\n** Results:" << messaget::eom;
+    // collect properties in a vector
+    std::vector<propertiest::const_iterator> sorted_properties;
+    for(auto p_it = properties.begin(); p_it != properties.end(); p_it++)
+      sorted_properties.push_back(p_it);
+    // now determine an ordering for those goals:
+    // 1. alphabetical ordering of file name
+    // 2. numerical ordering of line number
+    // 3. alphabetical ordering of goal ID
+    std::sort(
+      sorted_properties.begin(),
+      sorted_properties.end(),
+      [](propertiest::const_iterator pit1, propertiest::const_iterator pit2) {
+        const auto &p1 = pit1->second.pc->source_location;
+        const auto &p2 = pit2->second.pc->source_location;
+        if(p1.get_file() != p2.get_file())
+          return id2string(p1.get_file()) < id2string(p2.get_file());
+        else if(!p1.get_line().empty() && !p2.get_line().empty())
+          return std::stoul(id2string(p1.get_line())) <
+                 std::stoul(id2string(p2.get_line()));
+        else
+          return id2string(pit1->first) < id2string(pit2->first);
+      });
+    // now show in the order we have determined
+    irep_idt previous_function;
+    irep_idt current_file;
+    for(const auto &p : sorted_properties)
+    {
+      const auto &l = p->second.pc->source_location;
+      if(l.get_function() != previous_function)
+      {
+        if(!previous_function.empty())
+          log.result() << '\n';
+        previous_function = l.get_function();
+        if(!previous_function.empty())
+        {
+          current_file = l.get_file();
+          if(!current_file.empty())
+            log.result() << current_file << ' ';
+          if(!l.get_function().empty())
+            log.result() << "function " << l.get_function();
+          log.result() << messaget::eom;
+        }
+      }
+      log.result() << messaget::faint << '[' << p->first << "] "
+                   << messaget::reset;
+      if(l.get_file() != current_file)
+        log.result() << "file " << l.get_file() << ' ';
+      if(!l.get_line().empty())
+        log.result() << "line " << l.get_line() << ' ';
+      log.result() << p->second.description << ": ";
+      switch(p->second.status)
+      {
+      case property_statust::NOT_CHECKED:
+        log.result() << messaget::magenta;
+        break;
+      case property_statust::UNKNOWN:
+        log.result() << messaget::yellow;
+        break;
+      case property_statust::NOT_REACHABLE:
+        log.result() << messaget::bright_green;
+        break;
+      case property_statust::PASS:
+        log.result() << messaget::green;
+        break;
+      case property_statust::FAIL:
+        log.result() << messaget::red;
+        break;
+      case property_statust::ERROR:
+        log.result() << messaget::bright_red;
+        break;
+      }
+      log.result() << as_string(p->second.status) << messaget::reset
+                   << messaget::eom;
+    }
+    log.status() << "\n** "
+                 << count_properties(properties, property_statust::FAIL)
+                 << " of " << properties.size() << " failed" << messaget::eom;
+    break;
+  }
+  case ui_message_handlert::uit::XML_UI:
+  {
+    for(const auto &property_pair : properties)
+    {
+      log.result() << xml(property_pair.first, property_pair.second);
+    }
+    break;
+  }
+  case ui_message_handlert::uit::JSON_UI:
+  {
+    json_stream_objectt &json_result =
+      ui_message_handler.get_json_stream().push_back_stream_object();
+    json_stream_arrayt &result_array =
+      json_result.push_back_stream_array("result");
+    for(const auto &property_pair : properties)
+    {
+      result_array.push_back(json(property_pair.first, property_pair.second));
+    }
+    break;
+  }
+  }
+}

src/goto-checker/report_util.h

@@ -0,0 +1,23 @@
+/*******************************************************************\
+
+Module: Bounded Model Checking Utilities
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Bounded Model Checking Utilities
+
+#ifndef CPROVER_GOTO_CHECKER_REPORT_UTIL_H
+#define CPROVER_GOTO_CHECKER_REPORT_UTIL_H
+
+#include "properties.h"
+
+class ui_message_handlert;
+
+void output_properties(
+  const propertiest &properties,
+  ui_message_handlert &ui_message_handler);
+
+#endif // CPROVER_GOTO_CHECKER_REPORT_UTIL_H