diff --git a/src/goto-checker/Makefile b/src/goto-checker/Makefile index 7f37d465d4c..eeb45de1516 100644 --- a/src/goto-checker/Makefile +++ b/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 \ diff --git a/src/goto-checker/goto_verifier.cpp b/src/goto-checker/goto_verifier.cpp new file mode 100644 index 00000000000..3066d794015 --- /dev/null +++ b/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) +{ +} diff --git a/src/goto-checker/goto_verifier.h b/src/goto-checker/goto_verifier.h new file mode 100644 index 00000000000..6e16e9e750d --- /dev/null +++ b/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 +#include +#include + +#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 diff --git a/src/goto-checker/incremental_goto_checker.cpp b/src/goto-checker/incremental_goto_checker.cpp new file mode 100644 index 00000000000..af0d4f07375 --- /dev/null +++ b/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) +{ +} diff --git a/src/goto-checker/incremental_goto_checker.h b/src/goto-checker/incremental_goto_checker.h new file mode 100644 index 00000000000..feb6dce3f9a --- /dev/null +++ b/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 + +#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 diff --git a/src/goto-checker/properties.cpp b/src/goto-checker/properties.cpp new file mode 100644 index 00000000000..704891a1720 --- /dev/null +++ b/src/goto-checker/properties.cpp @@ -0,0 +1,90 @@ +/*******************************************************************\ + +Module: Properties + +Author: Daniel Kroening, Peter Schrammel + +\*******************************************************************/ + +/// \file +/// Properties + +#include "properties.h" + +#include + +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; +} diff --git a/src/goto-checker/properties.h b/src/goto-checker/properties.h new file mode 100644 index 00000000000..11050f24d8e --- /dev/null +++ b/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 + +#include + +/// 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 propertiest; + +/// Returns the properties in the goto model +propertiest initialize_properties(const abstract_goto_modelt &); + +#endif // CPROVER_GOTO_CHECKER_PROPERTIES_H