Introduce goto checker interfaces

goto_checkert: returns a trace or 'done'
goto_verifiert: uses goto_checkert to check a set of properties
property utilities

Author: peterschrammel

src/goto-checker/Makefile

@@ -1,4 +1,7 @@
 SRC = bmc_util.cpp \
+      incremental_goto_checker.cpp \
+      goto_verifier.cpp \
+      properties.cpp \
       solver_factory.cpp \
       symex_coverage.cpp \
       symex_bmc.cpp \

src/goto-checker/goto_verifier.cpp

@@ -0,0 +1,21 @@
+/*******************************************************************\
+
+Module: Goto Verifier Interface
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Goto Verifier Interface
+
+#include "goto_verifier.h"
+
+goto_verifiert::goto_verifiert(
+  const optionst &_options,
+  ui_message_handlert &ui_message_handler)
+  : options(_options),
+    ui_message_handler(ui_message_handler),
+    log(ui_message_handler)
+{
+}

src/goto-checker/goto_verifier.h

@@ -0,0 +1,58 @@
+/*******************************************************************\
+
+Module: Goto Verifier Interface
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Goto Verifier Interface
+
+#ifndef CPROVER_GOTO_CHECKER_GOTO_VERIFIER_H
+#define CPROVER_GOTO_CHECKER_GOTO_VERIFIER_H
+
+#include <util/optional.h>
+#include <util/options.h>
+#include <util/ui_message.h>
+
+#include "properties.h"
+
+/// An implementation of `goto_verifiert` checks all properties in
+/// a goto model. It typically uses, but doesn't have to use, an
+/// `incremental_goto_checkert` to iteratively determine the verification status
+/// of each property.
+class goto_verifiert
+{
+public:
+  goto_verifiert() = delete;
+  goto_verifiert(const goto_verifiert &) = delete;
+  virtual ~goto_verifiert() = default;
+
+  /// Check whether all properties hold.
+  /// \return PASS if all properties are PASS,
+  ///         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.
+  virtual resultt operator()() = 0;
+
+  /// Report results
+  virtual void report() = 0;
+
+  /// Returns the properties
+  const propertiest &get_properties()
+  {
+    return properties;
+  }
+
+protected:
+  goto_verifiert(const optionst &, ui_message_handlert &);
+
+  const optionst &options;
+  ui_message_handlert &ui_message_handler;
+  messaget log;
+  propertiest properties;
+};
+
+#endif // CPROVER_GOTO_CHECKER_GOTO_VERIFIER_H

src/goto-checker/incremental_goto_checker.cpp

@@ -0,0 +1,21 @@
+/*******************************************************************\
+
+Module: Incremental Goto Checker Interface
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Incremental Goto Checker Interface
+
+#include "incremental_goto_checker.h"
+
+incremental_goto_checkert::incremental_goto_checkert(
+  const optionst &options,
+  ui_message_handlert &ui_message_handler)
+  : options(options),
+    ui_message_handler(ui_message_handler),
+    log(ui_message_handler)
+{
+}

src/goto-checker/incremental_goto_checker.h

@@ -0,0 +1,78 @@
+/*******************************************************************\
+
+Module: Incremental Goto Checker Interface
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Incremental Goto Checker Interface
+
+#ifndef CPROVER_GOTO_CHECKER_INCREMENTAL_GOTO_CHECKER_H
+#define CPROVER_GOTO_CHECKER_INCREMENTAL_GOTO_CHECKER_H
+
+#include <util/ui_message.h>
+
+#include "properties.h"
+
+class goto_tracet;
+class optionst;
+
+/// An implementation of `incremental_goto_checkert` provides functionality for
+/// checking a set of properties and returning counterexamples
+/// one by one to the caller.
+/// An implementation of `incremental_goto_checkert` is responsible for
+/// maintaining the state of the analysis that it performs (e.g. goto-symex,
+/// solver, etc).
+/// An implementation of `incremental_goto_checkert` is not responsible for
+/// maintaining outcomes (e.g. property status, counterexamples, etc).
+/// However, an implementation may restrict the sets of properties it is asked
+/// to check on repeated invocations of its operator (e.g. only sequences of
+/// subsets of properties) to optimize the incremental algorithm it uses.
+class incremental_goto_checkert
+{
+public:
+  incremental_goto_checkert() = delete;
+  incremental_goto_checkert(const incremental_goto_checkert &) = delete;
+  virtual ~incremental_goto_checkert() = default;
+
+  enum class resultt
+  {
+    /// The goto checker may be able to find another FAILed property
+    /// if operator() is called again.
+    FOUND_FAIL,
+    /// The goto checker has returned all results for the given set
+    /// of properties.
+    DONE
+  };
+
+  /// Check whether the given properties with status NOT_CHECKED, UNKNOWN or
+  /// properties newly discovered by `goto_checkert` hold.
+  /// \param [out] properties: Properties updated to whether their status
+  ///   have been determined. Newly discovered properties are added.
+  /// \return whether the goto checker found a violated property (FOUND_FAIL) or
+  ///   whether it is DONE with the given properties.
+  /// After returning DONE, another call to operator() with the same
+  /// properties will return DONE and leave the properties' status unchanged.
+  /// If there is a property with status FAIL then its counterexample
+  /// can be retrieved by calling `build_error_trace` before any
+  /// subsequent call to operator().
+  /// `goto_checkert` derivatives shall be implemented in a way such
+  /// that repeated calls to operator() shall return when the next FAILed
+  /// property has been found until eventually it does not find any
+  /// failing properties any more.
+  virtual resultt operator()(propertiest &properties) = 0;
+
+  /// Builds and returns the counterexample
+  virtual goto_tracet build_error_trace() const = 0;
+
+protected:
+  incremental_goto_checkert(const optionst &, ui_message_handlert &);
+
+  const optionst &options;
+  ui_message_handlert &ui_message_handler;
+  messaget log;
+};
+
+#endif // CPROVER_GOTO_CHECKER_INCREMENTAL_GOTO_CHECKER_H

src/goto-checker/properties.cpp

@@ -0,0 +1,90 @@
+/*******************************************************************\
+
+Module: Properties
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Properties
+
+#include "properties.h"
+
+#include <util/invariant.h>
+
+std::string as_string(resultt result)
+{
+  switch(result)
+  {
+  case resultt::UNKNOWN:
+    return "UNKNOWN";
+  case resultt::PASS:
+    return "PASS";
+  case resultt::FAIL:
+    return "FAIL";
+  case resultt::ERROR:
+    return "ERROR";
+  }
+
+  UNREACHABLE;
+}
+
+std::string as_string(property_statust status)
+{
+  switch(status)
+  {
+  case property_statust::NOT_CHECKED:
+    return "NOT CHECKED";
+  case property_statust::UNKNOWN:
+    return "UNKNOWN";
+  case property_statust::NOT_REACHABLE:
+    return "UNREACHABLE";
+  case property_statust::PASS:
+    return "PASS";
+  case property_statust::FAIL:
+    return "FAIL";
+  case property_statust::ERROR:
+    return "ERROR";
+  }
+
+  UNREACHABLE;
+}
+
+property_infot::property_infot(
+  goto_programt::const_targett pc,
+  std::string description,
+  property_statust status)
+  : pc(pc), description(std::move(description)), status(status)
+{
+}
+
+/// Return the properties in the goto model and initialize them to NOT_CHECKED
+propertiest initialize_properties(const abstract_goto_modelt &goto_model)
+{
+  propertiest properties;
+  const auto &goto_functions = goto_model.get_goto_functions();
+  for(const auto &function_pair : goto_functions.function_map)
+  {
+    // don't collect properties from inlined functions
+    if(function_pair.second.is_inlined())
+      continue;
+
+    const goto_programt &goto_program = function_pair.second.body;
+
+    // need pointer to goto instruction
+    forall_goto_program_instructions(i_it, goto_program)
+    {
+      if(!i_it->is_assert())
+        continue;
+
+      std::string description = id2string(i_it->source_location.get_comment());
+      if(description.empty())
+        description = "assertion";
+      properties.emplace(
+        i_it->source_location.get_property_id(),
+        property_infot{i_it, description, property_statust::NOT_CHECKED});
+    }
+  }
+  return properties;
+}

src/goto-checker/properties.h

@@ -0,0 +1,76 @@
+/*******************************************************************\
+
+Module: Properties
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Properties
+
+#ifndef CPROVER_GOTO_CHECKER_PROPERTIES_H
+#define CPROVER_GOTO_CHECKER_PROPERTIES_H
+
+#include <unordered_map>
+
+#include <goto-programs/goto_model.h>
+
+/// The status of a property
+enum class property_statust
+{
+  /// The property was not checked (also used for initialization)
+  NOT_CHECKED,
+  /// The checker was unable to determine the status of the property
+  UNKNOWN,
+  /// The property was proven to be unreachable
+  NOT_REACHABLE,
+  /// The property was not violated
+  PASS,
+  /// The property was violated
+  FAIL,
+  /// An error occurred during goto checking
+  ERROR
+};
+
+std::string as_string(property_statust);
+
+/// The result of goto verifying
+enum class resultt
+{
+  /// No property was violated, neither was there an error
+  UNKNOWN,
+  /// No properties were violated
+  PASS,
+  /// Some properties were violated
+  FAIL,
+  /// An error occurred during goto checking
+  ERROR
+};
+
+std::string as_string(resultt);
+
+struct property_infot
+{
+  property_infot(
+    goto_programt::const_targett pc,
+    std::string description,
+    property_statust status);
+
+  /// A pointer to the corresponding goto instruction
+  goto_programt::const_targett pc;
+
+  /// A description (usually derived from the assertion's comment)
+  std::string description;
+
+  /// The status of the property
+  property_statust status;
+};
+
+/// A map of property IDs to property infos
+typedef std::unordered_map<irep_idt, property_infot> propertiest;
+
+/// Returns the properties in the goto model
+propertiest initialize_properties(const abstract_goto_modelt &);
+
+#endif // CPROVER_GOTO_CHECKER_PROPERTIES_H