Utilities for reporting overall result/status/exit code [depends: 3583, blocks: 3585]

src/cbmc/all_properties.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <chrono>
 
 #include <goto-checker/bmc_util.h>
+#include <goto-checker/report_util.h>
 
 #include <util/xml.h>
 #include <util/json.h>

src/cbmc/bmc.cpp

@@ -25,6 +25,7 @@ Author: Daniel Kroening, [email protected]
 #include <linking/static_lifetime_init.h>
 
 #include <goto-checker/bmc_util.h>
+#include <goto-checker/report_util.h>
 #include <goto-checker/solver_factory.h>
 
 #include "counterexample_beautification.h"

src/cbmc/fault_localization.cpp

@@ -27,6 +27,7 @@ Author: Peter Schrammel
 #include <goto-programs/xml_goto_trace.h>
 
 #include <goto-checker/bmc_util.h>
+#include <goto-checker/report_util.h>
 
 #include "counterexample_beautification.h"
 

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/bmc_util.cpp

@@ -225,58 +225,3 @@ void slice(
                    << " remaining after simplification" << messaget::eom;
 }
 
-void report_success(ui_message_handlert &ui_message_handler)
-{
-  messaget msg(ui_message_handler);
-  msg.result() << "VERIFICATION SUCCESSFUL" << messaget::eom;
-
-  switch(ui_message_handler.get_ui())
-  {
-  case ui_message_handlert::uit::PLAIN:
-    break;
-
-  case ui_message_handlert::uit::XML_UI:
-  {
-    xmlt xml("cprover-status");
-    xml.data = "SUCCESS";
-    msg.result() << xml;
-  }
-  break;
-
-  case ui_message_handlert::uit::JSON_UI:
-  {
-    json_objectt json_result;
-    json_result["cProverStatus"] = json_stringt("success");
-    msg.result() << json_result;
-  }
-  break;
-  }
-}
-
-void report_failure(ui_message_handlert &ui_message_handler)
-{
-  messaget msg(ui_message_handler);
-  msg.result() << "VERIFICATION FAILED" << messaget::eom;
-
-  switch(ui_message_handler.get_ui())
-  {
-  case ui_message_handlert::uit::PLAIN:
-    break;
-
-  case ui_message_handlert::uit::XML_UI:
-  {
-    xmlt xml("cprover-status");
-    xml.data = "FAILURE";
-    msg.result() << xml;
-  }
-  break;
-
-  case ui_message_handlert::uit::JSON_UI:
-  {
-    json_objectt json_result;
-    json_result["cProverStatus"] = json_stringt("failure");
-    msg.result() << json_result;
-  }
-  break;
-  }
-}

src/goto-checker/bmc_util.h

@@ -32,9 +32,6 @@ void convert_symex_target_equation(
   prop_convt &,
   message_handlert &);
 
-void report_failure(ui_message_handlert &);
-void report_success(ui_message_handlert &);
-
 void build_error_trace(
   goto_tracet &,
   const namespacet &,

src/goto-checker/properties.cpp

@@ -11,7 +11,10 @@ Author: Daniel Kroening, Peter Schrammel
 
 #include "properties.h"
 
+#include <util/exit_codes.h>
 #include <util/invariant.h>
+#include <util/json.h>
+#include <util/xml.h>
 
 std::string as_string(resultt result)
 {
@@ -88,3 +91,56 @@ 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;
+}
+
+int result_to_exit_code(resultt result)
+{
+  switch(result)
+  {
+  case resultt::PASS:
+    return CPROVER_EXIT_VERIFICATION_SAFE;
+  case resultt::FAIL:
+    return CPROVER_EXIT_VERIFICATION_UNSAFE;
+  case resultt::ERROR:
+    return CPROVER_EXIT_INTERNAL_ERROR;
+  case resultt::UNKNOWN:
+    return CPROVER_EXIT_VERIFICATION_INCONCLUSIVE;
+  }
+  UNREACHABLE;
+}
+
+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,17 @@ 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);
+
+int result_to_exit_code(resultt result);
+
+/// Return the number of properties with given \p status
+std::size_t count_properties(const propertiest &, property_statust);
+
 #endif // CPROVER_GOTO_CHECKER_PROPERTIES_H