From: Andres Noetzli Date: Fri, 19 Oct 2018 04:05:48 +0000 (-0700) Subject: Add OptionException handling during initialization (#2466) X-Git-Tag: cvc5-1.0.0~4403 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=64dcc865f8aae4fd1591bfec9ee117b360e9f9b3;p=cvc5.git 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. --- 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