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 /test | |
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 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 25 | ||||
-rw-r--r-- | test/regress/Makefile.tests | 9 | ||||
-rw-r--r-- | test/regress/regress0/options/invalid_dump.smt2 | 4 |
3 files changed, 22 insertions, 16 deletions
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 |