Add OptionException handling during initialization (#2466)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 19 Oct 2018 04:05:48 +0000 (21:05 -0700)
committerGitHub <noreply@github.com>
Fri, 19 Oct 2018 04:05:48 +0000 (21:05 -0700)
commit64dcc865f8aae4fd1591bfec9ee117b360e9f9b3
tree15515ed7bc4d6aef47ecd0d3f19a98d2753c25a4
parente57e2c8911d0b39a59aad29330466c93c8081506
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
src/options/Makefile.am
src/options/option_exception.cpp [new file with mode: 0644]
src/options/option_exception.h
src/options/options_template.cpp
src/smt/smt_engine.cpp
test/regress/CMakeLists.txt
test/regress/Makefile.tests
test/regress/regress0/options/invalid_dump.smt2 [new file with mode: 0644]