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 = solver_factory.cpp \
+SRC = goto_checker.cpp \
+      goto_verifier.cpp \
+      properties.cpp \
+      solver_factory.cpp \
       # Empty last line
 
 INCLUDES= -I ..

src/goto-checker/goto_checker.cpp

@@ -0,0 +1,21 @@
+/*******************************************************************\
+
+Module: Goto Checker Interface
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Goto Checker Interface
+
+#include "goto_checker.h"
+
+goto_checkert::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/goto_checker.h

@@ -0,0 +1,70 @@
+/*******************************************************************\
+
+Module: Goto Checker Interface
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Goto Checker Interface
+
+#ifndef CPROVER_GOTO_CHECKER_GOTO_CHECKER_H
+#define CPROVER_GOTO_CHECKER_GOTO_CHECKER_H
+
+#include <goto-programs/goto_trace.h>
+
+#include <util/options.h>
+#include <util/ui_message.h>
+
+#include "properties.h"
+
+/// An implementation of `goto_checkert` provides functionality for
+/// checking a set of properties and returning counterexamples
+/// one by one to the caller.
+/// An implementation of `goto_checkert` is responsible for maintaining
+/// the state of the analysis that it performs (e.g. goto-symex, solver, etc).
+/// It is not responsible for maintaining outcomes (e.g. property results,
+/// counterexamples, etc). However, an implementation may restrict the
+/// sets of properties it is asked to check (e.g. only sequences of subsets).
+class goto_checkert
+{
+public:
+  enum class statust
+  {
+    /// The goto checker may be able to determine the results for more
+    /// properties if operator() is called again.
+    HAVE_MORE,
+    /// The goto checker has returned all results for the given set
+    /// of properties.
+    DONE
+  };
+
+  /// Check whether the given properties with status UNKNOWN or newly
+  /// discovered properties hold
+  /// \param [out] properties: Updates those properties whose
+  ///   results have been determined. Newly discovered properties are added.
+  /// \return whether the goto checker may HAVE_MORE results 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' results 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 the next FAILed
+  /// property until eventually not returning any FAILing properties.
+  virtual statust operator()(propertiest &properties) = 0;
+
+  /// This builds and returns the counterexample
+  virtual goto_tracet build_error_trace() const = 0;
+
+protected:
+  goto_checkert(const optionst &, ui_message_handlert &);
+
+  const optionst &options;
+  ui_message_handlert &ui_message_handler;
+  messaget log;
+};
+
+#endif // CPROVER_GOTO_CHECKER_GOTO_CHECKER_H

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,54 @@
+/*******************************************************************\
+
+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, a
+/// `goto_checkert` to iteratively determine the verification result
+/// of each property.
+class goto_verifiert
+{
+public:
+  /// 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/properties.cpp

@@ -0,0 +1,79 @@
+/*******************************************************************\
+
+Module: Properties
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Properties
+
+#include "properties.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_resultt result)
+{
+  switch(result)
+  {
+  case property_resultt::NOT_REACHED:
+    return "NOT REACHED";
+  case property_resultt::UNKNOWN:
+    return "UNKNOWN";
+  case property_resultt::NOT_REACHABLE:
+    return "UNREACHABLE";
+  case property_resultt::PASS:
+    return "PASS";
+  case property_resultt::FAIL:
+    return "FAIL";
+  case property_resultt::ERROR:
+    return "ERROR";
+  }
+
+  UNREACHABLE;
+}
+
+propertiest initialize_properties(const goto_modelt &goto_model)
+{
+  propertiest properties;
+  forall_goto_functions(it, goto_model.goto_functions)
+  {
+    if(
+      !it->second.is_inlined() ||
+      it->first == goto_model.goto_functions.entry_point())
+    {
+      const goto_programt &goto_program = it->second.body;
+
+      forall_goto_program_instructions(i_it, goto_program)
+      {
+        if(!i_it->is_assert())
+          continue;
+
+        const source_locationt &source_location = i_it->source_location;
+
+        irep_idt property_id = source_location.get_property_id();
+
+        property_infot &property = properties[property_id];
+        property.result = property_resultt::NOT_REACHED;
+        property.location = i_it;
+      }
+    }
+  }
+  return properties;
+}

src/goto-checker/properties.h

@@ -0,0 +1,74 @@
+/*******************************************************************\
+
+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>
+
+class json_objectt;
+class xmlt;
+
+/// The result status of a property
+enum class property_resultt
+{
+  /// The property was not reached (also used for initialization)
+  NOT_REACHED,
+  /// The status of the property is unknown
+  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_resultt result);
+
+/// The result of goto checking and 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 result);
+
+struct property_infot
+{
+  /// A pointer to the corresponding goto instruction
+  goto_programt::const_targett location;
+
+  /// A description (usually derived from the assertion's comment)
+  std::string description;
+
+  /// The status of the property
+  property_resultt result;
+};
+
+/// 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 goto_modelt &);
+
+#endif // CPROVER_GOTO_CHECKER_PROPERTIES_H