All-properties verifier [depends: 3584, blocks: 3794]

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/all_properties_verifier.h

@@ -0,0 +1,61 @@
+/*******************************************************************\
+
+Module: Goto Verifier for Verifying all Properties
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Goto Verifier for Verifying all Properties
+
+#ifndef CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_H
+#define CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_H
+
+#include "goto_verifier.h"
+
+#include "incremental_goto_checker.h"
+#include "properties.h"
+#include "report_util.h"
+
+template <class incremental_goto_checkerT>
+class all_properties_verifiert : public goto_verifiert
+{
+public:
+  all_properties_verifiert(
+    const optionst &options,
+    ui_message_handlert &ui_message_handler,
+    abstract_goto_modelt &goto_model)
+    : goto_verifiert(options, ui_message_handler),
+      goto_model(goto_model),
+      incremental_goto_checker(options, ui_message_handler, goto_model)
+  {
+    properties = initialize_properties(goto_model);
+  }
+
+  resultt operator()() override
+  {
+    // have we got anything to check? otherwise we return PASS
+    if(!has_properties_to_check(properties))
+      return resultt::PASS;
+
+    while(incremental_goto_checker(properties) !=
+          incremental_goto_checkert::resultt::DONE)
+    {
+      // loop until we are done
+    }
+    return determine_result(properties);
+  }
+
+  void report() override
+  {
+    output_properties(properties, ui_message_handler);
+    output_overall_result(determine_result(properties), ui_message_handler);
+  }
+
+protected:
+  abstract_goto_modelt &goto_model;
+  incremental_goto_checkerT incremental_goto_checker;
+};
+
+#endif // CPROVER_GOTO_CHECKER_ALL_PROPERTIES_VERIFIER_H

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,169 @@ 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;
+}
+
+bool is_property_to_check(property_statust status)
+{
+  return status == property_statust::NOT_CHECKED ||
+         status == property_statust::UNKNOWN;
+}
+
+bool has_properties_to_check(const propertiest &properties)
+{
+  for(const auto &property_pair : properties)
+  {
+    if(is_property_to_check(property_pair.second.status))
+      return true;
+  }
+  return false;
+}
+
+/// Update with the preference order
+/// 1. old non-UNKNOWN/non-NOT_CHECKED status
+/// 2. new non-UNKNOWN/non-NOT_CHECKED status
+/// 3. UNKNOWN
+/// 4. NOT_CHECKED
+/// Suitable for updating property status
+property_statust &operator|=(property_statust &a, property_statust const &b)
+{
+  // non-monotonic use is likely a bug
+  PRECONDITION(
+    a == property_statust::NOT_CHECKED ||
+    (a == property_statust::UNKNOWN && b != property_statust::NOT_CHECKED) ||
+    a == b);
+  switch(a)
+  {
+  case property_statust::NOT_CHECKED:
+  case property_statust::UNKNOWN:
+    a = b;
+    return a;
+  case property_statust::ERROR:
+  case property_statust::PASS:
+  case property_statust::NOT_REACHABLE:
+  case property_statust::FAIL:
+    return a;
+  }
+  UNREACHABLE;
+}
+
+/// Update with the preference order
+/// 1. ERROR
+/// 2. FAIL
+/// 3. UNKNOWN
+/// 4. NOT_CHECKED
+/// 5. NOT_REACHABLE
+/// 6. PASS
+/// Suitable for computing overall results
+property_statust &operator&=(property_statust &a, property_statust const &b)
+{
+  switch(a)
+  {
+  case property_statust::ERROR:
+    a = b;
+    return a;
+  case property_statust::FAIL:
+    a = (b == property_statust::ERROR ? b : a);
+    return a;
+  case property_statust::UNKNOWN:
+    a = (b == property_statust::ERROR || b == property_statust::FAIL ? b : a);
+    return a;
+  case property_statust::NOT_CHECKED:
+    a =
+      (b != property_statust::PASS && b != property_statust::NOT_REACHABLE ? b
+                                                                           : a);
+    return a;
+  case property_statust::NOT_REACHABLE:
+    a = (b != property_statust::PASS ? b : a);
+    return a;
+  case property_statust::PASS:
+    a = (b == property_statust::PASS ? a : b);
+    return a;
+  }
+  UNREACHABLE;
+}
+
+/// Determines the overall result corresponding from the given properties
+/// That is PASS if all properties are PASS or NOT_CHECKED,
+///         FAIL if at least one property is FAIL and no property is ERROR,
+///         UNKNOWN if no property is FAIL or ERROR and
+///           at least one property is UNKNOWN,
+///         ERROR if at least one property is error.
+resultt determine_result(const propertiest &properties)
+{
+  property_statust status = property_statust::PASS;
+  for(const auto &property_pair : properties)
+  {
+    status &= property_pair.second.status;
+  }
+  switch(status)
+  {
+  case property_statust::NOT_CHECKED:
+    // If we have unchecked properties then we don't know.
+    return resultt::UNKNOWN;
+  case property_statust::UNKNOWN:
+    return resultt::UNKNOWN;
+  case property_statust::NOT_REACHABLE:
+    // If a property is not reachable then overall it's still a PASS.
+    return resultt::PASS;
+  case property_statust::PASS:
+    return resultt::PASS;
+  case property_statust::FAIL:
+    return resultt::FAIL;
+  case property_statust::ERROR:
+    return resultt::ERROR;
+  }
+  UNREACHABLE;
+}

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,27 @@ 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);
+
+/// Return true if the status is NOT_CHECKED or UNKNOWN
+bool is_property_to_check(property_statust);
+
+/// Return true if there as a property with NOT_CHECKED or UNKNOWN status
+bool has_properties_to_check(const propertiest &properties);
+
+property_statust &operator|=(property_statust &, property_statust const &);
+property_statust &operator&=(property_statust &, property_statust const &);
+resultt determine_result(const propertiest &properties);
+
 #endif // CPROVER_GOTO_CHECKER_PROPERTIES_H