Merge pull request #3585 from peterschrammel/all-properties-verifier

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

Author: tautschnig

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

@@ -144,3 +144,116 @@ count_properties(const propertiest &properties, property_statust status)
   }
   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

@@ -89,4 +89,14 @@ 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