From 4983832f0e72d1e1a01654a1f5c2d270d3db8602 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Tue, 19 Sep 2017 09:43:58 -0700 Subject: [PATCH] Fix issue #1074, improve non-fatal error handling (#1075) Commit 54d24c786d6a843cc72dfb5e377603349ea5e420 was changing CVC4 to handle certain non-fatal errors (such as calling get-unsat-core without a proceding unsat check-sat command) without terminating the solver. In the case of get-unsat-cores, the changes lead to the solver crashing because it was trying to print an unsat core initialized with the default constructor, so the member variable d_smt was NULL, which lead to a dereference of a null pointer. One of the issues of the way non-fatal errors were handled was that the error reporting was done in the invoke() method of the command instead of the printResult() method, which lead to the error described above and other issues such as a call to get-value printing a value after reporting an error. This commit aims to improve the design by adding a RecoverableModalException for errors that the solver can recover from and CommandRecoverableFailure to communicate that a command failed in a way that does not prohibit the solver from continuing to execute. The exception RecoverableModalException is thrown by the SMTEngine and the commands catch it and turn it into a CommandRecoverableFailure. The commit changes all error conditions from the commit above and adds a regression test for them. --- src/base/modal_exception.h | 14 ++++++++++ src/printer/smt2/smt2_printer.cpp | 22 +++++++++++----- src/proof/unsat_core.cpp | 3 +++ src/smt/command.cpp | 10 +++++++ src/smt/command.h | 18 +++++++++++++ src/smt/smt_engine.cpp | 29 ++++++++++----------- test/regress/regress0/Makefile.am | 3 ++- test/regress/regress0/non-fatal-errors.smt2 | 29 +++++++++++++++++++++ test/regress/run_regression | 10 +++++++ 9 files changed, 115 insertions(+), 23 deletions(-) create mode 100644 test/regress/regress0/non-fatal-errors.smt2 diff --git a/src/base/modal_exception.h b/src/base/modal_exception.h index fc1b8ac9e..0392ab470 100644 --- a/src/base/modal_exception.h +++ b/src/base/modal_exception.h @@ -42,6 +42,20 @@ public: } };/* class ModalException */ +/** + * Special case of ModalException that allows the execution of the solver to + * continue. + * + * TODO(#1108): This exception should not be needed anymore in future versions + * of the public API. + */ +class CVC4_PUBLIC RecoverableModalException : public CVC4::ModalException { + public: + RecoverableModalException(const std::string& msg) : ModalException(msg) {} + + RecoverableModalException(const char* msg) : ModalException(msg) {} +}; /* class RecoverableModalException */ + }/* CVC4 namespace */ #endif /* __CVC4__SMT__MODAL_EXCEPTION_H */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ae65311de..105e2c0dd 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -1114,11 +1114,11 @@ template static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) throw(); void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() { - - if(tryToStream(out, s, d_variant) || - tryToStream(out, s, d_variant) || - tryToStream(out, s, d_variant) || - tryToStream(out, s, d_variant)) { + if (tryToStream(out, s, d_variant) || + tryToStream(out, s, d_variant) || + tryToStream(out, s, d_variant) || + tryToStream(out, s, d_variant) || + tryToStream(out, s, d_variant)) { return; } @@ -1653,8 +1653,7 @@ static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v) #endif /* CVC4_COMPETITION_MODE */ } -static void toStream(std::ostream& out, const CommandFailure* s, Variant v) throw() { - string message = s->getMessage(); +static void errorToStream(std::ostream& out, std::string message, Variant v) { // escape all double-quotes size_t pos = 0; while((pos = message.find('"', pos)) != string::npos) { @@ -1664,6 +1663,15 @@ static void toStream(std::ostream& out, const CommandFailure* s, Variant v) thro out << "(error \"" << message << "\")" << endl; } +static void toStream(std::ostream& out, const CommandFailure* s, Variant v) { + errorToStream(out, s->getMessage(), v); +} + +static void toStream(std::ostream& out, const CommandRecoverableFailure* s, + Variant v) { + errorToStream(out, s->getMessage(), v); +} + template static bool tryToStream(std::ostream& out, const CommandStatus* s, Variant v) throw() { if(typeid(*s) == typeid(T)) { diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp index b056e0ef4..c8696868e 100644 --- a/src/proof/unsat_core.cpp +++ b/src/proof/unsat_core.cpp @@ -16,6 +16,7 @@ #include "proof/unsat_core.h" +#include "base/cvc4_assert.h" #include "expr/expr_iomanip.h" #include "options/base_options.h" #include "printer/printer.h" @@ -37,12 +38,14 @@ UnsatCore::const_iterator UnsatCore::end() const { } void UnsatCore::toStream(std::ostream& out) const { + Assert(d_smt != NULL); smt::SmtScope smts(d_smt); expr::ExprDag::Scope scope(out, false); Printer::getPrinter(options::outputLanguage())->toStream(out, *this); } void UnsatCore::toStream(std::ostream& out, const std::map& names) const { + Assert(d_smt != NULL); smt::SmtScope smts(d_smt); expr::ExprDag::Scope scope(out, false); Printer::getPrinter(options::outputLanguage())->toStream(out, *this, names); diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 2ca8b1fe3..70302088b 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1023,6 +1023,8 @@ void GetValueCommand::invoke(SmtEngine* smtEngine) { } d_result = em->mkExpr(kind::SEXPR, result); d_commandStatus = CommandSuccess::instance(); + } catch (RecoverableModalException& e) { + d_commandStatus = new CommandRecoverableFailure(e.what()); } catch(UnsafeInterruptException& e) { d_commandStatus = new CommandInterrupted(); } catch(exception& e) { @@ -1072,6 +1074,8 @@ void GetAssignmentCommand::invoke(SmtEngine* smtEngine) { try { d_result = smtEngine->getAssignment(); d_commandStatus = CommandSuccess::instance(); + } catch (RecoverableModalException& e) { + d_commandStatus = new CommandRecoverableFailure(e.what()); } catch(UnsafeInterruptException& e) { d_commandStatus = new CommandInterrupted(); } catch(exception& e) { @@ -1117,6 +1121,8 @@ void GetModelCommand::invoke(SmtEngine* smtEngine) { d_result = smtEngine->getModel(); d_smtEngine = smtEngine; d_commandStatus = CommandSuccess::instance(); + } catch (RecoverableModalException& e) { + d_commandStatus = new CommandRecoverableFailure(e.what()); } catch(UnsafeInterruptException& e) { d_commandStatus = new CommandInterrupted(); } catch(exception& e) { @@ -1166,6 +1172,8 @@ void GetProofCommand::invoke(SmtEngine* smtEngine) { d_smtEngine = smtEngine; d_result = smtEngine->getProof(); d_commandStatus = CommandSuccess::instance(); + } catch (RecoverableModalException& e) { + d_commandStatus = new CommandRecoverableFailure(e.what()); } catch(UnsafeInterruptException& e) { d_commandStatus = new CommandInterrupted(); } catch(exception& e) { @@ -1352,6 +1360,8 @@ void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) { try { d_result = smtEngine->getUnsatCore(); d_commandStatus = CommandSuccess::instance(); + } catch (RecoverableModalException& e) { + d_commandStatus = new CommandRecoverableFailure(e.what()); } catch(exception& e) { d_commandStatus = new CommandFailure(e.what()); } diff --git a/src/smt/command.h b/src/smt/command.h index 36e679885..2e0f4090e 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -189,6 +189,24 @@ public: std::string getMessage() const throw() { return d_message; } };/* class CommandFailure */ +/** + * The execution of the command resulted in a non-fatal error and further + * commands can be processed. This status is for example used when a user asks + * for an unsat core in a place that is not immediately preceded by an + * unsat/valid response. + */ +class CVC4_PUBLIC CommandRecoverableFailure : public CommandStatus { + std::string d_message; + + public: + CommandRecoverableFailure(std::string message) throw() : d_message(message) {} + CommandRecoverableFailure& clone() const { + return *new CommandRecoverableFailure(*this); + } + ~CommandRecoverableFailure() throw() {} + std::string getMessage() const throw() { return d_message; } +}; /* class CommandRecoverableFailure */ + class CVC4_PUBLIC Command { protected: /** diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b1a0a1acd..db7c65291 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -4656,6 +4656,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L return n.toExpr(); } +// TODO(#1108): Simplify the error reporting of this method. Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException) { Assert(ex.getExprManager() == d_exprManager); SmtScope smts(this); @@ -4675,9 +4676,7 @@ Expr SmtEngine::getValue(const Expr& ex) const throw(ModalException, TypeCheckin d_problemExtended) { const char* msg = "Cannot get value unless immediately preceded by SAT/INVALID or UNKNOWN response."; - //throw ModalException(msg); - Warning() << CommandFailure(msg); - return ex; + throw RecoverableModalException(msg); } // Substitute out any abstract values in ex. @@ -4767,6 +4766,7 @@ bool SmtEngine::addToAssignment(const Expr& ex) { return true; } +// TODO(#1108): Simplify the error reporting of this method. CVC4::SExpr SmtEngine::getAssignment() { Trace("smt") << "SMT getAssignment()" << endl; SmtScope smts(this); @@ -4786,9 +4786,7 @@ CVC4::SExpr SmtEngine::getAssignment() { const char* msg = "Cannot get the current assignment unless immediately " "preceded by SAT/INVALID or UNKNOWN response."; - //throw ModalException(msg); - Warning() << CommandFailure(msg); - return SExpr(vector()); + throw RecoverableModalException(msg); } if(d_assignments == NULL) { @@ -4867,6 +4865,7 @@ void SmtEngine::addToModelCommandAndDump(const Command& c, uint32_t flags, bool } } +// TODO(#1108): Simplify the error reporting of this method. Model* SmtEngine::getModel() { Trace("smt") << "SMT getModel()" << endl; SmtScope smts(this); @@ -4883,9 +4882,7 @@ Model* SmtEngine::getModel() { const char* msg = "Cannot get the current model unless immediately " "preceded by SAT/INVALID or UNKNOWN response."; - //throw ModalException(msg); - Warning() << CommandFailure(msg); - return NULL; + throw RecoverableModalException(msg); } if(!options::produceModels()) { const char* msg = @@ -5131,6 +5128,7 @@ void SmtEngine::checkModel(bool hardFailure) { Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl; } +// TODO(#1108): Simplify the error reporting of this method. UnsatCore SmtEngine::getUnsatCore() { Trace("smt") << "SMT getUnsatCore()" << endl; SmtScope smts(this); @@ -5145,9 +5143,9 @@ UnsatCore SmtEngine::getUnsatCore() { if(d_status.isNull() || d_status.asSatisfiabilityResult() != Result::UNSAT || d_problemExtended) { - //throw ModalException("Cannot get an unsat core unless immediately preceded by UNSAT/VALID response."); - Warning() << CommandFailure("Cannot get an unsat core unless immediately preceded by UNSAT/VALID response."); - return UnsatCore(); + throw RecoverableModalException( + "Cannot get an unsat core unless immediately preceded by UNSAT/VALID " + "response."); } d_proofManager->traceUnsatCore();// just to trigger core creation @@ -5157,6 +5155,7 @@ UnsatCore SmtEngine::getUnsatCore() { #endif /* IS_PROOFS_BUILD */ } +// TODO(#1108): Simplify the error reporting of this method. Proof* SmtEngine::getProof() { Trace("smt") << "SMT getProof()" << endl; SmtScope smts(this); @@ -5171,9 +5170,9 @@ Proof* SmtEngine::getProof() { if(d_status.isNull() || d_status.asSatisfiabilityResult() != Result::UNSAT || d_problemExtended) { - //throw ModalException("Cannot get a proof unless immediately preceded by UNSAT/VALID response."); - Warning() << CommandFailure("Cannot get a proof unless immediately preceded by UNSAT/VALID response."); - return NULL; + throw RecoverableModalException( + "Cannot get a proof unless immediately preceded by UNSAT/VALID " + "response."); } return ProofManager::getProof(this); diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 1368dd067..dbff6cff1 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -69,7 +69,8 @@ SMT2_TESTS = \ hung10_itesdk_output1.smt2 \ hung13sdk_output2.smt2 \ declare-funs.smt2 \ - declare-fun-is-match.smt2 + declare-fun-is-match.smt2 \ + non-fatal-errors.smt2 # Regression tests for PL inputs CVC_TESTS = \ diff --git a/test/regress/regress0/non-fatal-errors.smt2 b/test/regress/regress0/non-fatal-errors.smt2 new file mode 100644 index 000000000..1e1865883 --- /dev/null +++ b/test/regress/regress0/non-fatal-errors.smt2 @@ -0,0 +1,29 @@ +; SCRUBBER: sed 's/".*"/""/g' +; EXPECT: success +; EXPECT: success +; EXPECT: success +; EXPECT: success +; EXPECT: success +; EXPECT: success +; EXPECT: success +; EXPECT: (error "") +; EXPECT: (error "") +; EXPECT: (error "") +; EXPECT: (error "") +; EXPECT: (error "") +; EXPECT: success +; EXPECT: sat +(set-option :print-success true) +(set-option :produce-unsat-cores true) +(set-option :produce-models true) +(set-option :produce-proofs true) +(set-option :produce-assignments true) +(set-logic UF) +(declare-fun p () Bool) +(get-unsat-core) +(get-value (p)) +(get-proof) +(get-model) +(get-assignment) +(assert true) +(check-sat) diff --git a/test/regress/run_regression b/test/regress/run_regression index 536a3e8a5..5d4165597 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -130,6 +130,15 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then fi elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then lang=smt2 + + # If this test case requires unsat cores but CVC4 is not built with proof + # support, skip it. Note: checking $CVC4_REGRESSION_ARGS instead of $proof + # here because $proof is not set for the second run. + requires_proof=`grep '(get-unsat-core)' "$benchmark"` + if [[ ! "$CVC4_REGRESSION_ARGS" = *"--proof"* ]] && [ -n "$requires_proof" ]; then + exit 77 + fi + if test -e "$benchmark.expect"; then scrubber=`grep '^% SCRUBBER: ' "$benchmark.expect" | sed 's,^% SCRUBBER: ,,'` errscrubber=`grep '^% ERROR-SCRUBBER: ' "$benchmark.expect" | sed 's,^% ERROR-SCRUBBER: ,,'` @@ -288,6 +297,7 @@ if [ "$proof" = yes ]; then fi fi fi + if [ -z "$expected_error" ]; then # in case expected stderr output is empty, make sure we don't differ # by a newline, which we would if we echo "" >"$experrfile" -- 2.30.2