diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-18 21:05:48 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-10-18 21:05:48 -0700 |
commit | 64dcc865f8aae4fd1591bfec9ee117b360e9f9b3 (patch) | |
tree | 15515ed7bc4d6aef47ecd0d3f19a98d2753c25a4 /cmake | |
parent | e57e2c8911d0b39a59aad29330466c93c8081506 (diff) |
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.
Diffstat (limited to 'cmake')
0 files changed, 0 insertions, 0 deletions