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.

9 files changed, 132 insertions, 62 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()
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5d0459015..e489d2e21 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -155,6 +155,8 @@ set(regress_0_tests
   regress0/bug605.cvc
   regress0/bug639.smt2
   regress0/buggy-ite.smt2
+  regress0/bv/ackermann1.smt2
+  regress0/bv/ackermann2.smt2
   regress0/bv/bool-to-bv.smt2
   regress0/bv/bug260a.smt
   regress0/bv/bug260b.smt
@@ -340,6 +342,7 @@ set(regress_0_tests
   regress0/datatypes/cdt-non-canon-stream.smt2
   regress0/datatypes/coda_simp_model.smt2
   regress0/datatypes/conqueue-dt-enum-iloop.smt2
+  regress0/datatypes/data-nested-codata.smt2
   regress0/datatypes/datatype.cvc
   regress0/datatypes/datatype0.cvc
   regress0/datatypes/datatype1.cvc
@@ -434,8 +437,10 @@ set(regress_0_tests
   regress0/fmf/quant_real_univ.cvc
   regress0/fmf/sat-logic.smt2
   regress0/fmf/sc_bad_model_1221.smt2
+  regress0/fmf/sort-infer-typed-082718.smt2
   regress0/fmf/syn002-si-real-int.smt2
   regress0/fmf/tail_rec.smt2
+  regress0/fp/ext-rew-test.smt2
   regress0/fp/simple.smt2
   regress0/fuzz_1.smt
   regress0/fuzz_3.smt
@@ -496,9 +501,11 @@ set(regress_0_tests
   regress0/logops.05.cvc
   regress0/model-core.smt2
   regress0/nl/coeff-sat.smt2
+  regress0/nl/ext-rew-aggr-test.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2
   regress0/nl/nia-wrong-tl.smt2
+  regress0/nl/nlExtPurify-test.smt2
   regress0/nl/nta/cos-sig-value.smt2
   regress0/nl/nta/exp-n0.5-lb.smt2
   regress0/nl/nta/exp-n0.5-ub.smt2
@@ -512,6 +519,7 @@ set(regress_0_tests
   regress0/nl/subs0-unsat-confirm.smt2
   regress0/nl/very-easy-sat.smt2
   regress0/nl/very-simple-unsat.smt2
+  regress0/options/invalid_dump.smt2
   regress0/parallel-let.smt2
   regress0/parser/as.smt2
   regress0/parser/constraint.smt2
@@ -616,6 +624,7 @@ set(regress_0_tests
   regress0/quantifiers/issue1805.smt2
   regress0/quantifiers/issue2031-bv-var-elim.smt2
   regress0/quantifiers/issue2033-macro-arith.smt2
+  regress0/quantifiers/issue2035.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macros-int-real.smt2
   regress0/quantifiers/macros-real-arg.smt2
@@ -791,6 +800,7 @@ set(regress_0_tests
   regress0/simplification_bug2.smt
   regress0/smallcnf.cvc
   regress0/smt2output.smt2
+  regress0/smtlib/get-unsat-assumptions.smt2
   regress0/strings/bug001.smt2
   regress0/strings/bug002.smt2
   regress0/strings/bug612.smt2
@@ -811,12 +821,14 @@ set(regress_0_tests
   regress0/strings/norn-31.smt2
   regress0/strings/norn-simp-rew.smt2
   regress0/strings/repl-rewrites2.smt2
+  regress0/strings/rewrites-re-concat.smt2
   regress0/strings/rewrites-v2.smt2
   regress0/strings/std2.6.1.smt2
   regress0/strings/stoi-solve.smt2
   regress0/strings/str003.smt2
   regress0/strings/str004.smt2
   regress0/strings/str005.smt2
+  regress0/strings/str_unsound_ext_rew_eq.smt2
   regress0/strings/strings-charat.cvc
   regress0/strings/strings-native-simple.cvc
   regress0/strings/strip-endpoint-itos.smt2
@@ -830,6 +842,7 @@ set(regress_0_tests
   regress0/sygus/check-generic-red.sy
   regress0/sygus/const-var-test.sy
   regress0/sygus/dt-no-syntax.sy
+  regress0/sygus/hd-05-d1-prog-nogrammar.sy
   regress0/sygus/inv-different-var-order.sy
   regress0/sygus/let-ringer.sy
   regress0/sygus/let-simp.sy
@@ -1000,18 +1013,6 @@ set(regress_0_tests
   regress0/wiki.19.cvc
   regress0/wiki.20.cvc
   regress0/wiki.21.cvc
-  regress0/bv/ackermann1.smt2
-  regress0/bv/ackermann2.smt2
-  regress0/datatypes/data-nested-codata.smt2
-  regress0/fmf/sort-infer-typed-082718.smt2
-  regress0/fp/ext-rew-test.smt2
-  regress0/nl/ext-rew-aggr-test.smt2
-  regress0/nl/nlExtPurify-test.smt2
-  regress0/quantifiers/issue2035.smt2
-  regress0/smtlib/get-unsat-assumptions.smt2
-  regress0/strings/rewrites-re-concat.smt2
-  regress0/strings/str_unsound_ext_rew_eq.smt2
-  regress0/sygus/hd-05-d1-prog-nogrammar.sy
 )
 
 #-----------------------------------------------------------------------------#
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 194a4ddaf..5b2280b02 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -10,12 +10,12 @@ REG0_TESTS = \
 	regress0/arith/bug547.2.smt2 \
 	regress0/arith/bug569.smt2 \
 	regress0/arith/delta-minimized-row-vector-bug.smt \
+	regress0/arith/div-chainable.smt2 \
 	regress0/arith/div.01.smt2 \
 	regress0/arith/div.02.smt2 \
 	regress0/arith/div.04.smt2 \
 	regress0/arith/div.05.smt2 \
 	regress0/arith/div.07.smt2 \
-	regress0/arith/div-chainable.smt2 \
 	regress0/arith/fuzz_3-eq.smt \
 	regress0/arith/integers/arith-int-042.cvc \
 	regress0/arith/integers/arith-int-042.min.cvc \
@@ -343,6 +343,7 @@ REG0_TESTS = \
 	regress0/datatypes/cdt-non-canon-stream.smt2 \
 	regress0/datatypes/coda_simp_model.smt2 \
 	regress0/datatypes/conqueue-dt-enum-iloop.smt2 \
+	regress0/datatypes/data-nested-codata.smt2 \
 	regress0/datatypes/datatype.cvc \
 	regress0/datatypes/datatype0.cvc \
 	regress0/datatypes/datatype1.cvc \
@@ -350,7 +351,6 @@ REG0_TESTS = \
 	regress0/datatypes/datatype2.cvc \
 	regress0/datatypes/datatype3.cvc \
 	regress0/datatypes/datatype4.cvc \
-	regress0/datatypes/data-nested-codata.smt2 \
 	regress0/datatypes/dt-2.6.smt2 \
 	regress0/datatypes/dt-match-pat-param-2.6.smt2 \
 	regress0/datatypes/dt-param-2.6.smt2 \
@@ -441,8 +441,8 @@ REG0_TESTS = \
 	regress0/fmf/sort-infer-typed-082718.smt2 \
 	regress0/fmf/syn002-si-real-int.smt2 \
 	regress0/fmf/tail_rec.smt2 \
-	regress0/fp/simple.smt2 \
 	regress0/fp/ext-rew-test.smt2 \
+	regress0/fp/simple.smt2 \
 	regress0/fuzz_1.smt \
 	regress0/fuzz_3.smt \
 	regress0/get-value-incremental.smt2 \
@@ -520,6 +520,7 @@ REG0_TESTS = \
 	regress0/nl/subs0-unsat-confirm.smt2 \
 	regress0/nl/very-easy-sat.smt2 \
 	regress0/nl/very-simple-unsat.smt2 \
+	regress0/options/invalid_dump.smt2 \
 	regress0/parallel-let.smt2 \
 	regress0/parser/as.smt2 \
 	regress0/parser/constraint.smt2 \
@@ -827,10 +828,10 @@ REG0_TESTS = \
 	regress0/strings/str003.smt2 \
 	regress0/strings/str004.smt2 \
 	regress0/strings/str005.smt2 \
+	regress0/strings/str_unsound_ext_rew_eq.smt2 \
 	regress0/strings/strings-charat.cvc \
 	regress0/strings/strings-native-simple.cvc \
 	regress0/strings/strip-endpoint-itos.smt2 \
-	regress0/strings/str_unsound_ext_rew_eq.smt2 \
 	regress0/strings/substr-rewrites.smt2 \
 	regress0/strings/type001.smt2 \
 	regress0/strings/unsound-0908.smt2 \
diff --git a/test/regress/regress0/options/invalid_dump.smt2 b/test/regress/regress0/options/invalid_dump.smt2
new file mode 100644
index 000000000..9f92a7a64
--- /dev/null
+++ b/test/regress/regress0/options/invalid_dump.smt2
@@ -0,0 +1,4 @@
+; COMMAND-LINE: --dump invalidDumpTag
+; ERROR-SCRUBBER: grep -o "unknown option for --dump"
+; EXPECT-ERROR: unknown option for --dump
+; EXIT: 1