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.

5 files changed, 49 insertions, 3 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;
 }