Merge pull request #3860 from peterschrammel/goto-checker-interface-fixes

Goto checker interface enhancements [blocks: 3794]

Author: peterschrammel

src/goto-checker/all_properties_verifier.h

@@ -39,8 +39,8 @@ class all_properties_verifiert : public goto_verifiert
     if(!has_properties_to_check(properties))
       return resultt::PASS;
 
-    while(incremental_goto_checker(properties) !=
-          incremental_goto_checkert::resultt::DONE)
+    while(incremental_goto_checker(properties).progress !=
+          incremental_goto_checkert::resultt::progresst::DONE)
     {
       // loop until we are done
     }

src/goto-checker/goto_trace_provider.h

@@ -0,0 +1,32 @@
+/*******************************************************************\
+
+Module: Interface for returning Goto Traces from Goto Checkers
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Interface for returning Goto Traces from Goto Checkers
+
+#ifndef CPROVER_GOTO_CHECKER_GOTO_TRACE_PROVIDER_H
+#define CPROVER_GOTO_CHECKER_GOTO_TRACE_PROVIDER_H
+
+class goto_tracet;
+class namespacet;
+
+/// An implementation of `incremental_goto_checkert`
+/// may implement this interface to provide goto traces.
+class goto_trace_providert
+{
+public:
+  /// Builds and returns a trace
+  virtual goto_tracet build_trace() const = 0;
+
+  /// Returns the namespace associated with the traces
+  virtual const namespacet &get_namespace() const = 0;
+
+  virtual ~goto_trace_providert() = default;
+};
+
+#endif // CPROVER_GOTO_CHECKER_GOTO_TRACE_PROVIDER_H

src/goto-checker/incremental_goto_checker.cpp

@@ -19,3 +19,10 @@ incremental_goto_checkert::incremental_goto_checkert(
     log(ui_message_handler)
 {
 }
+
+incremental_goto_checkert::resultt::resultt(
+  progresst progress,
+  const std::vector<irep_idt> &updated_properties)
+  : progress(progress), updated_properties(updated_properties)
+{
+}

src/goto-checker/incremental_goto_checker.h

@@ -37,22 +37,37 @@ class incremental_goto_checkert
   incremental_goto_checkert(const incremental_goto_checkert &) = delete;
   virtual ~incremental_goto_checkert() = default;
 
-  enum class resultt
+  struct 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
+    enum class progresst
+    {
+      /// 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
+    };
+
+    progresst progress = progresst::DONE;
+
+    /// Changed properties since the last call to
+    /// `incremental_goto_checkert::operator()`
+    std::vector<irep_idt> updated_properties;
+
+    resultt() = default;
+    resultt(
+      progresst progress,
+      const std::vector<irep_idt> &updated_properties);
   };
 
   /// 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.
+  ///   whether it is DONE with the given properties, together with
+  ///   the properties whose status changed since the last call to operator().
   /// 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
@@ -64,15 +79,6 @@ class incremental_goto_checkert
   /// failing properties any more.
   virtual resultt operator()(propertiest &properties) = 0;
 
-  /// Builds and returns the counterexample
-  virtual goto_tracet build_error_trace() const = 0;
-
-  // Outputs an error witness in GraphML format (see `graphml_witnesst`)
-  virtual void output_error_witness(const goto_tracet &) = 0;
-
-  // Outputs a proof in GraphML format (see `graphml_witnesst`)
-  virtual void output_proof() = 0;
-
 protected:
   incremental_goto_checkert(const optionst &, ui_message_handlert &);
 

src/goto-checker/witness_provider.h

@@ -0,0 +1,31 @@
+/*******************************************************************\
+
+Module: Interface for outputting GraphML Witnesses for Goto Checkers
+
+Author: Daniel Kroening, Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// Interface for outputting GraphML Witnesses for Goto Checkers
+
+#ifndef CPROVER_GOTO_CHECKER_WITNESS_PROVIDER_H
+#define CPROVER_GOTO_CHECKER_WITNESS_PROVIDER_H
+
+class goto_tracet;
+
+/// An implementation of `incremental_goto_checkert`
+/// may implement this interface to provide GraphML witnesses.
+class witness_providert
+{
+public:
+  virtual ~witness_providert() = default;
+
+  // Outputs an error witness in GraphML format (see `graphml_witnesst`)
+  virtual void output_error_witness(const goto_tracet &) = 0;
+
+  // Outputs a proof in GraphML format (see `graphml_witnesst`)
+  virtual void output_proof() = 0;
+};
+
+#endif // CPROVER_GOTO_CHECKER_WITNESS_PROVIDER_H