From: Andres Noetzli Date: Mon, 17 Sep 2018 17:57:19 +0000 (-0700) Subject: Remove broken dumping support from portfolio build (#2470) X-Git-Tag: cvc5-1.0.0~4644 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4365cdd8c582e2d1a3d406f5395d4950270f8c83;p=cvc5.git Remove broken dumping support from portfolio build (#2470) Dumping support for portfolio builds was introduced in 84f26af22566f7c10dea45b399b944cb50b5e317 but as far as I can tell, the implementation has already been problematic in the original implementation. The current implementation has the following issues: - Dumping with a portfolio build (even when using the single threaded executable) results in a segfault. The reason is that the DumpChannel variable is declared as an `extern` and exists for the duration of the program. The problem is that it stores a `CommandSequence`, which indirectly may store nodes. When shutting down CVC4, the destructor of `DumpC` is called, which destroys the `CommandSequence`, which results in a segfault because the `NodeManager` does not exist anymore. The node manager is (indirectly) owned and destroyed by the `api::Solver` object. - Additionally, adding commands to the `CommandSequence` is not thread safe (it just calls `CommandSequence::addCommand()`, which in turn pushes back to a vector [0] (which is not thread safe [1]). A single instance of `DumpChannel` is shared among all threads (it is not declared `thread_local` [2]). - The `CommandSequence` in `DumpC` was not used in the original implementation and is still unused on master. The original commit mentions that the portfolio build stores the commands in the `CommandSequence` but not why. This commit removes the `CommandSequence` and related methods from `DumpC` to avoid the issue when destroying `DumpChannel`. It disables dumping for portfolio builds and adds a check at configure-time that not both options have been enabled simultaneously. Given that the option was not functional previously, the problematic implementation, and the fact that the dump of multiple threads wouldn't be very useful, disabling dumping for portfolio builds is unlikely to be problem. An improvement that could be made is to disable dumping support only for the pcvc4 binary and while enabling it for the single-threaded version, even when using `--with-portfolio`. However, we currently do not have the infrastructure for that (we use the same libcvc4 library for both binaries). [0] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/command.cpp#L756 [1] https://en.cppreference.com/w/cpp/container [2] https://github.com/CVC4/CVC4/blob/c2111c86973b8a80e20a3fdf3cbd0b2ff0dc7010/src/smt/dump.h#L117 --- diff --git a/configure.ac b/configure.ac index de4a410ad..81fff6c93 100644 --- a/configure.ac +++ b/configure.ac @@ -424,6 +424,16 @@ fi AM_CONDITIONAL([CVC4_CLN_IMP], [test $cvc4_cln_or_gmp = cln]) AM_CONDITIONAL([CVC4_GMP_IMP], [test $cvc4_cln_or_gmp = gmp]) +# Dumping cannot be used in a portfolio build. Disable dumping by default when +# a portfolio build has been requested, throw an error if dumping has been +# explicitly requested with a portfolio build. +if test "$with_portfolio" = yes; then + if test "$enable_dumping" = yes; then + AC_MSG_ERROR([Dumping is not supported with a portfolio build]) + fi + enable_dumping=no +fi + # construct the build string AC_MSG_CHECKING([for appropriate build string]) if test -z "$ac_confdir"; then diff --git a/src/smt/dump.h b/src/smt/dump.h index cdab598bb..9de8eb0ce 100644 --- a/src/smt/dump.h +++ b/src/smt/dump.h @@ -24,63 +24,49 @@ namespace CVC4 { -class CVC4_PUBLIC CVC4dumpstream { - -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - std::ostream* d_os; -#endif /* CVC4_DUMPING && !CVC4_MUZZLE */ - -#ifdef CVC4_PORTFOLIO - CommandSequence* d_commands; -#endif /* CVC4_PORTFOLIO */ +#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && !defined(CVC4_PORTFOLIO) +class CVC4_PUBLIC CVC4dumpstream +{ public: - CVC4dumpstream() -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO) - : d_os(NULL), d_commands(NULL) -#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - : d_os(NULL) -#elif defined(CVC4_PORTFOLIO) - : d_commands(NULL) -#endif /* CVC4_PORTFOLIO */ - { } - - CVC4dumpstream(std::ostream& os, CommandSequence& commands) -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) && defined(CVC4_PORTFOLIO) - : d_os(&os), d_commands(&commands) -#elif defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - : d_os(&os) -#elif defined(CVC4_PORTFOLIO) - : d_commands(&commands) -#endif /* CVC4_PORTFOLIO */ - { } + CVC4dumpstream() : d_os(nullptr) {} + CVC4dumpstream(std::ostream& os) : d_os(&os) {} CVC4dumpstream& operator<<(const Command& c) { -#if defined(CVC4_DUMPING) && !defined(CVC4_MUZZLE) - if(d_os != NULL) { + if (d_os != nullptr) + { (*d_os) << c << std::endl; } -#endif -#if defined(CVC4_PORTFOLIO) - if(d_commands != NULL) { - d_commands->addCommand(c.clone()); - } -#endif return *this; } -};/* class CVC4dumpstream */ -/** The dump class */ -class CVC4_PUBLIC DumpC { - std::set d_tags; - CommandSequence d_commands; + private: + std::ostream* d_os; +}; /* class CVC4dumpstream */ - static const std::string s_dumpHelp; +#else + +/** + * Dummy implementation of the dump stream when dumping is disabled or the + * build is muzzled. + */ +class CVC4_PUBLIC CVC4dumpstream +{ + public: + CVC4dumpstream() {} + CVC4dumpstream(std::ostream& os) {} + CVC4dumpstream& operator<<(const Command& c) { return *this; } +}; /* class CVC4dumpstream */ + +#endif /* CVC4_DUMPING && !CVC4_MUZZLE */ -public: +/** The dump class */ +class CVC4_PUBLIC DumpC +{ + public: CVC4dumpstream operator()(const char* tag) { if(!d_tags.empty() && d_tags.find(std::string(tag)) != d_tags.end()) { - return CVC4dumpstream(getStream(), d_commands); + return CVC4dumpstream(getStream()); } else { return CVC4dumpstream(); } @@ -88,15 +74,12 @@ public: CVC4dumpstream operator()(std::string tag) { if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { - return CVC4dumpstream(getStream(), d_commands); + return CVC4dumpstream(getStream()); } else { return CVC4dumpstream(); } } - void clear() { d_commands.clear(); } - const CommandSequence& getCommands() const { return d_commands; } - bool on (const char* tag) { d_tags.insert(std::string(tag)); return true; } bool on (std::string tag) { d_tags.insert(tag); return true; } bool off(const char* tag) { d_tags.erase (std::string(tag)); return false; } @@ -111,6 +94,13 @@ public: std::ostream* getStreamPointer(); void setDumpFromString(const std::string& optarg); + + private: + /** Set of dumping tags that are currently active. */ + std::set d_tags; + + /** The message printed on `--dump help`. */ + static const std::string s_dumpHelp; };/* class DumpC */ /** The dump singleton */