diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-18 21:05:48 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-18 21:05:48 -0700 |
commit | 64dcc865f8aae4fd1591bfec9ee117b360e9f9b3 (patch) | |
tree | 15515ed7bc4d6aef47ecd0d3f19a98d2753c25a4 /src | |
parent | e57e2c8911d0b39a59aad29330466c93c8081506 (diff) |
Add OptionException handling during initialization (#2466)
The initial motivation for this commit was that dump with an invalid tag
was leading to a segfault. The reason for the segfault was as follows:
1. `api::Solver` creates an `ExprManager`, which is stored in a
`unique_ptr` as a class member
2. The `api::Solver` tries to create an SmtEngine instance
3. The `SmtEnginePrivate` constructor subscribes to events in the
NodeManager and starts registering option listeners
4. When the `SmtEnginePrivate` gets to registerSetDumpModeListener, it
registers and notifies the DumpModeListener which calls
Dump::setDumpFromString, which fails with an `OptionException` due to
the invalid tag
5. While propagating the exception through `api::Solver`, the
`ExprManager` is deleted but the non-existent `SmtEnginePrivate` is
still subscribed to its events and there are still option listeners
registered. This leads to a segfault because the NodeManager tries to
notify the `SmtEnginePrivate` about deleted nodes
This commit fixes the issue by catching the `OptionException` in
`SmtEnginePrivate`, unsubscribing the `SmtEnginePrivate` from the
NodeManager events and deleting its option listener registrations before
rethrowing the exception. In addition, it changes the
`Options::registerAndNotify()` method to immediately delete a
registration if notifying the registration resulted in an
``OptionException`` (otherwise only the `ListenerCollection` knows about
the registration and complains about it in its destructor). Finally,
the commit adds a simple regression test for invalid dump tags.
Diffstat (limited to 'src')
-rw-r--r-- | src/options/CMakeLists.txt | 1 | ||||
-rw-r--r-- | src/options/Makefile.am | 1 | ||||
-rw-r--r-- | src/options/option_exception.cpp | 21 | ||||
-rw-r--r-- | src/options/option_exception.h | 14 | ||||
-rw-r--r-- | src/options/options_template.cpp | 15 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 104 |
6 files changed, 110 insertions, 46 deletions
diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index dd0e34578..c711567ab 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -21,6 +21,7 @@ libcvc4_add_sources( language.h open_ostream.cpp open_ostream.h + option_exception.cpp option_exception.h options.h options_handler.cpp diff --git a/src/options/Makefile.am b/src/options/Makefile.am index 54047efcc..498989c80 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -85,6 +85,7 @@ liboptions_la_SOURCES = \ language.h \ open_ostream.cpp \ open_ostream.h \ + option_exception.cpp \ option_exception.h \ options.h \ options_handler.cpp \ diff --git a/src/options/option_exception.cpp b/src/options/option_exception.cpp new file mode 100644 index 000000000..33e2e21d1 --- /dev/null +++ b/src/options/option_exception.cpp @@ -0,0 +1,21 @@ +/********************* */ +/*! \file option_exception.h + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Options-related exceptions + ** + ** Options-related exceptions. + **/ + +#include "options/option_exception.h" + +namespace CVC4 { +const std::string OptionException::s_errPrefix = "Error in option parsing: "; +} // namespace CVC4 diff --git a/src/options/option_exception.h b/src/options/option_exception.h index 97a9de770..63b8aa890 100644 --- a/src/options/option_exception.h +++ b/src/options/option_exception.h @@ -31,10 +31,20 @@ namespace CVC4 { */ class CVC4_PUBLIC OptionException : public CVC4::Exception { public: - OptionException(const std::string& s) - : CVC4::Exception("Error in option parsing: " + s) + OptionException(const std::string& s) : CVC4::Exception(s_errPrefix + s) {} + + /** + * Get the error message without the prefix that is automatically added for + * OptionExceptions. + */ + std::string getRawMessage() const { + return getMessage().substr(s_errPrefix.size()); } + + private: + /** The string to be added in front of the actual error message */ + static const std::string s_errPrefix; };/* class OptionException */ /** diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 609713ce8..85a9747fe 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -265,7 +265,20 @@ ListenerCollection::Registration* Options::registerAndNotify( ListenerCollection::Registration* registration = collection.registerListener(listener); if(notify) { - listener->notify(); + try + { + listener->notify(); + } + catch (OptionException& e) + { + // It can happen that listener->notify() throws an OptionException. In + // that case, we have to make sure that we delete the registration of our + // listener before rethrowing the exception. Otherwise the + // ListenerCollection deconstructor will complain that not all + // registrations have been removed before invoking the deconstructor. + delete registration; + throw OptionException(e.getRawMessage()); + } } return registration; } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 63c970920..e5db42a22 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -581,49 +581,67 @@ class SmtEnginePrivate : public NodeManagerListener { d_listenerRegistrations->add(d_resourceManager->registerHardListener( new HardResourceOutListener(d_smt))); - Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); - d_listenerRegistrations->add( - nodeManagerOptions.registerForceLogicListener( - new SetLogicListener(d_smt), true)); - - // Multiple options reuse BeforeSearchListener so registration requires an - // extra bit of care. - // We can safely not call notify on this before search listener at - // registration time. This d_smt cannot be beforeSearch at construction - // time. Therefore the BeforeSearchListener is a no-op. Therefore it does - // not have to be called. - d_listenerRegistrations->add( - nodeManagerOptions.registerBeforeSearchListener( - new BeforeSearchListener(d_smt))); - - // These do need registration calls. - d_listenerRegistrations->add( - nodeManagerOptions.registerSetDefaultExprDepthListener( - new SetDefaultExprDepthListener(), true)); - d_listenerRegistrations->add( - nodeManagerOptions.registerSetDefaultExprDagListener( - new SetDefaultExprDagListener(), true)); - d_listenerRegistrations->add( - nodeManagerOptions.registerSetPrintExprTypesListener( - new SetPrintExprTypesListener(), true)); - d_listenerRegistrations->add( - nodeManagerOptions.registerSetDumpModeListener( - new DumpModeListener(), true)); - d_listenerRegistrations->add( - nodeManagerOptions.registerSetPrintSuccessListener( - new PrintSuccessListener(), true)); - d_listenerRegistrations->add( - nodeManagerOptions.registerSetRegularOutputChannelListener( - new SetToDefaultSourceListener(&d_managedRegularChannel), true)); - d_listenerRegistrations->add( - nodeManagerOptions.registerSetDiagnosticOutputChannelListener( - new SetToDefaultSourceListener(&d_managedDiagnosticChannel), true)); - d_listenerRegistrations->add( - nodeManagerOptions.registerDumpToFileNameListener( - new SetToDefaultSourceListener(&d_managedDumpChannel), true)); - d_listenerRegistrations->add( - nodeManagerOptions.registerSetReplayLogFilename( - new SetToDefaultSourceListener(&d_managedReplayLog), true)); + try + { + Options& nodeManagerOptions = NodeManager::currentNM()->getOptions(); + d_listenerRegistrations->add( + nodeManagerOptions.registerForceLogicListener( + new SetLogicListener(d_smt), true)); + + // Multiple options reuse BeforeSearchListener so registration requires an + // extra bit of care. + // We can safely not call notify on this before search listener at + // registration time. This d_smt cannot be beforeSearch at construction + // time. Therefore the BeforeSearchListener is a no-op. Therefore it does + // not have to be called. + d_listenerRegistrations->add( + nodeManagerOptions.registerBeforeSearchListener( + new BeforeSearchListener(d_smt))); + + // These do need registration calls. + d_listenerRegistrations->add( + nodeManagerOptions.registerSetDefaultExprDepthListener( + new SetDefaultExprDepthListener(), true)); + d_listenerRegistrations->add( + nodeManagerOptions.registerSetDefaultExprDagListener( + new SetDefaultExprDagListener(), true)); + d_listenerRegistrations->add( + nodeManagerOptions.registerSetPrintExprTypesListener( + new SetPrintExprTypesListener(), true)); + d_listenerRegistrations->add( + nodeManagerOptions.registerSetDumpModeListener(new DumpModeListener(), + true)); + d_listenerRegistrations->add( + nodeManagerOptions.registerSetPrintSuccessListener( + new PrintSuccessListener(), true)); + d_listenerRegistrations->add( + nodeManagerOptions.registerSetRegularOutputChannelListener( + new SetToDefaultSourceListener(&d_managedRegularChannel), true)); + d_listenerRegistrations->add( + nodeManagerOptions.registerSetDiagnosticOutputChannelListener( + new SetToDefaultSourceListener(&d_managedDiagnosticChannel), + true)); + d_listenerRegistrations->add( + nodeManagerOptions.registerDumpToFileNameListener( + new SetToDefaultSourceListener(&d_managedDumpChannel), true)); + d_listenerRegistrations->add( + nodeManagerOptions.registerSetReplayLogFilename( + new SetToDefaultSourceListener(&d_managedReplayLog), true)); + } + catch (OptionException& e) + { + // Registering the option listeners can lead to OptionExceptions, e.g. + // when the user chooses a dump tag that does not exist. In that case, we + // have to make sure that we delete existing listener registrations and + // that we unsubscribe from NodeManager events. Otherwise we will have + // errors in the deconstructors of the NodeManager (because the + // NodeManager tries to notify an SmtEnginePrivate that does not exist) + // and the ListenerCollection (because not all registrations have been + // removed before calling the deconstructor). + delete d_listenerRegistrations; + d_smt.d_nodeManager->unsubscribeEvents(this); + throw OptionException(e.getRawMessage()); + } } ~SmtEnginePrivate() |