From: Gereon Kremer Date: Thu, 14 Oct 2021 22:16:58 +0000 (-0700) Subject: Improve ManagedStreams (#7367) X-Git-Tag: cvc5-1.0.0~1063 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b2329e04d3269587f968378db5fcdc0487dbbdb7;p=cvc5.git Improve ManagedStreams (#7367) This PR addresses #7361, but also a more general issue about regular-output-channel being able to hold stderr and diagnostic-output-channel being able to hold stdout. It therefore changes how non-owned streams are stored: beforehand, an explicit stream would always be owned by the ManagedStream (through a std::shared_ptr) and a nullptr implicitly stood for stdout, stderr or stdin. Now we explicitly hold a pointer to a non-owned stream for these special values. Fixes #7361. --- diff --git a/src/options/managed_streams.cpp b/src/options/managed_streams.cpp index 81bb242cf..90090df25 100644 --- a/src/options/managed_streams.cpp +++ b/src/options/managed_streams.cpp @@ -100,34 +100,54 @@ std::istream* openIStream(const std::string& filename) } } // namespace detail -std::ostream* ManagedErr::defaultValue() const { return &std::cerr; } +ManagedErr::ManagedErr() : ManagedStream(&std::cerr, "stderr") {} bool ManagedErr::specialCases(const std::string& value) { if (value == "stderr" || value == "--") { - d_stream.reset(); + d_nonowned = &std::cerr; + d_owned.reset(); + d_description = "stderr"; + return true; + } + else if (value == "stdout") + { + d_nonowned = &std::cout; + d_owned.reset(); + d_description = "stdout"; return true; } return false; } -std::istream* ManagedIn::defaultValue() const { return &std::cin; } +ManagedIn::ManagedIn() : ManagedStream(&std::cin, "stdin") {} bool ManagedIn::specialCases(const std::string& value) { if (value == "stdin" || value == "--") { - d_stream.reset(); + d_nonowned = &std::cin; + d_owned.reset(); + d_description = "stdin"; return true; } return false; } -std::ostream* ManagedOut::defaultValue() const { return &std::cout; } +ManagedOut::ManagedOut() : ManagedStream(&std::cout, "stdout") {} bool ManagedOut::specialCases(const std::string& value) { if (value == "stdout" || value == "--") { - d_stream.reset(); + d_nonowned = &std::cout; + d_owned.reset(); + d_description = "stdout"; + return true; + } + else if (value == "stderr") + { + d_nonowned = &std::cerr; + d_owned.reset(); + d_description = "stderr"; return true; } return false; diff --git a/src/options/managed_streams.h b/src/options/managed_streams.h index 56bb21c2e..cf1820de6 100644 --- a/src/options/managed_streams.h +++ b/src/options/managed_streams.h @@ -50,7 +50,8 @@ template class ManagedStream { public: - ManagedStream() {} + ManagedStream(Stream* nonowned, std::string description) + : d_nonowned(nonowned), d_description(std::move(description)) {} virtual ~ManagedStream() {} /** @@ -62,11 +63,15 @@ class ManagedStream if (specialCases(value)) return; if constexpr (std::is_same::value) { - d_stream.reset(detail::openOStream(value)); + d_nonowned = nullptr; + d_owned.reset(detail::openOStream(value)); + d_description = value; } else if constexpr (std::is_same::value) { - d_stream.reset(detail::openIStream(value)); + d_nonowned = nullptr; + d_owned.reset(detail::openIStream(value)); + d_description = value; } } @@ -75,12 +80,14 @@ class ManagedStream operator Stream&() const { return *getPtr(); } operator Stream*() const { return getPtr(); } + const std::string& description() const { return d_description; } + protected: - std::shared_ptr d_stream; + Stream* d_nonowned; + std::shared_ptr d_owned; + std::string d_description = ""; private: - /** Returns the value to be used if d_stream is not set. */ - virtual Stream* defaultValue() const = 0; /** * Check if there is a special case for this value. If so, the implementation * should set d_stream appropriately and return true to skip the default @@ -88,18 +95,18 @@ class ManagedStream */ virtual bool specialCases(const std::string& value) = 0; - /** Return the pointer, either from d_stream of from defaultValue(). */ + /** Return the pointer, either from d_nonowned or d_owned. */ Stream* getPtr() const { - if (d_stream) return d_stream.get(); - return defaultValue(); + if (d_nonowned != nullptr) return d_nonowned; + return d_owned.get(); } }; template std::ostream& operator<<(std::ostream& os, const ManagedStream& ms) { - return os << "ManagedStream"; + return os << ms.description(); } /** @@ -108,7 +115,10 @@ std::ostream& operator<<(std::ostream& os, const ManagedStream& ms) */ class ManagedErr : public ManagedStream { - std::ostream* defaultValue() const override final; + public: + ManagedErr(); + + private: bool specialCases(const std::string& value) override final; }; @@ -118,7 +128,10 @@ class ManagedErr : public ManagedStream */ class ManagedIn : public ManagedStream { - std::istream* defaultValue() const override final; + public: + ManagedIn(); + + private: bool specialCases(const std::string& value) override final; }; @@ -128,7 +141,10 @@ class ManagedIn : public ManagedStream */ class ManagedOut : public ManagedStream { - std::ostream* defaultValue() const override final; + public: + ManagedOut(); + + private: bool specialCases(const std::string& value) override final; }; diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index baced1e76..819bb94e4 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -769,6 +769,7 @@ set(regress_0_tests regress0/options/set-after-init.smt2 regress0/options/set-and-get-options.smt2 regress0/options/statistics.smt2 + regress0/options/stream-printing.smt2 regress0/parallel-let.smt2 regress0/parser/as.smt2 regress0/parser/bv_arity_smt2.6.smt2 diff --git a/test/regress/regress0/options/stream-printing.smt2 b/test/regress/regress0/options/stream-printing.smt2 new file mode 100644 index 000000000..21ea85aa1 --- /dev/null +++ b/test/regress/regress0/options/stream-printing.smt2 @@ -0,0 +1,18 @@ +; EXPECT: stdout +; EXPECT: stderr +; EXPECT: stdin +; EXPECT-ERROR: stderr +; EXPECT-ERROR: stdout +; EXPECT-ERROR: stdin + +(get-option :regular-output-channel) +(get-option :diagnostic-output-channel) +(get-option :in) + +(set-option :regular-output-channel stderr) +(set-option :diagnostic-output-channel stdout) +(set-option :in stdin) + +(get-option :regular-output-channel) +(get-option :diagnostic-output-channel) +(get-option :in)