From 64dcc865f8aae4fd1591bfec9ee117b360e9f9b3 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 18 Oct 2018 21:05:48 -0700 Subject: 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. --- src/options/CMakeLists.txt | 1 + src/options/Makefile.am | 1 + src/options/option_exception.cpp | 21 +++++++++++++++++++++ src/options/option_exception.h | 14 ++++++++++++-- src/options/options_template.cpp | 15 ++++++++++++++- 5 files changed, 49 insertions(+), 3 deletions(-) create mode 100644 src/options/option_exception.cpp (limited to 'src/options') 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; } -- cgit v1.2.3