From 363f5e100297c73ddcfbe575e49f945b2e27909e Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 20 Jan 2019 11:46:49 +0000 Subject: [PATCH 1/3] Move witness output into separate interface Not all incremental_goto_checkert implementations can provide witnesses. --- src/goto-checker/incremental_goto_checker.h | 6 ---- src/goto-checker/witness_provider.h | 31 +++++++++++++++++++++ 2 files changed, 31 insertions(+), 6 deletions(-) create mode 100644 src/goto-checker/witness_provider.h diff --git a/src/goto-checker/incremental_goto_checker.h b/src/goto-checker/incremental_goto_checker.h index 7dbfb5081af..feb6dce3f9a 100644 --- a/src/goto-checker/incremental_goto_checker.h +++ b/src/goto-checker/incremental_goto_checker.h @@ -67,12 +67,6 @@ class incremental_goto_checkert /// 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 &); diff --git a/src/goto-checker/witness_provider.h b/src/goto-checker/witness_provider.h new file mode 100644 index 00000000000..5037765a3d9 --- /dev/null +++ b/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 From 7f59f248cf3ba68499d38c503e557284e5781f31 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 20 Jan 2019 12:10:29 +0000 Subject: [PATCH 2/3] Move trace returning into separate interface Not all incremental goto checker implementations may support traces. --- src/goto-checker/goto_trace_provider.h | 32 +++++++++++++++++++++ src/goto-checker/incremental_goto_checker.h | 3 -- 2 files changed, 32 insertions(+), 3 deletions(-) create mode 100644 src/goto-checker/goto_trace_provider.h diff --git a/src/goto-checker/goto_trace_provider.h b/src/goto-checker/goto_trace_provider.h new file mode 100644 index 00000000000..27f56c60c72 --- /dev/null +++ b/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 diff --git a/src/goto-checker/incremental_goto_checker.h b/src/goto-checker/incremental_goto_checker.h index feb6dce3f9a..c0c1cad2acc 100644 --- a/src/goto-checker/incremental_goto_checker.h +++ b/src/goto-checker/incremental_goto_checker.h @@ -64,9 +64,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; - protected: incremental_goto_checkert(const optionst &, ui_message_handlert &); From be514e3341104d075a5cb2f915e2f46e1f029c77 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sat, 19 Jan 2019 14:44:14 +0000 Subject: [PATCH 3/3] Return updated properties in incremental goto checker result The goto verifier might want to know which properties have been updated in the last call to the incremental goto checker, e.g. to output status information or report results continuously. --- src/goto-checker/all_properties_verifier.h | 4 +-- src/goto-checker/incremental_goto_checker.cpp | 7 +++++ src/goto-checker/incremental_goto_checker.h | 31 ++++++++++++++----- 3 files changed, 32 insertions(+), 10 deletions(-) diff --git a/src/goto-checker/all_properties_verifier.h b/src/goto-checker/all_properties_verifier.h index 391da10d977..4c65fe3b2ad 100644 --- a/src/goto-checker/all_properties_verifier.h +++ b/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 } diff --git a/src/goto-checker/incremental_goto_checker.cpp b/src/goto-checker/incremental_goto_checker.cpp index af0d4f07375..01c17fb7d18 100644 --- a/src/goto-checker/incremental_goto_checker.cpp +++ b/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 &updated_properties) + : progress(progress), updated_properties(updated_properties) +{ +} diff --git a/src/goto-checker/incremental_goto_checker.h b/src/goto-checker/incremental_goto_checker.h index c0c1cad2acc..134c1d55a05 100644 --- a/src/goto-checker/incremental_goto_checker.h +++ b/src/goto-checker/incremental_goto_checker.h @@ -37,14 +37,28 @@ 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 updated_properties; + + resultt() = default; + resultt( + progresst progress, + const std::vector &updated_properties); }; /// Check whether the given properties with status NOT_CHECKED, UNKNOWN or @@ -52,7 +66,8 @@ class incremental_goto_checkert /// \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