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 81bb242cf4d6c5ca24b3c19128adc465a0e5a27b..90090df257bf2378dd89fed0742074606cf10da3 100644 (file)
--- 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 56bb21c2e7070ca54dc2593b34445f9e3ece4c92..cf1820de6d551dec0d72fff0d3f26bf782627f29 100644 (file)
--- a/src/options/managed_streams.h
+++ b/src/options/managed_streams.h
@@ -50,7 +50,8 @@ template <typename Stream>
 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<Stream, std::ostream>::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<Stream, std::istream>::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<Stream> d_stream;
+  Stream* d_nonowned;
+  std::shared_ptr<Stream> d_owned;
+  std::string d_description = "<null>";
 
  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 <typename Stream>
 std::ostream& operator<<(std::ostream& os, const ManagedStream<Stream>& ms)
 {
-  return os << "ManagedStream";
+  return os << ms.description();
 }
 
 /**
@@ -108,7 +115,10 @@ std::ostream& operator<<(std::ostream& os, const ManagedStream<Stream>& ms)
  */
 class ManagedErr : public ManagedStream<std::ostream>
 {
-  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<std::ostream>
  */
 class ManagedIn : public ManagedStream<std::istream>
 {
-  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<std::istream>
  */
 class ManagedOut : public ManagedStream<std::ostream>
 {
-  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 baced1e76740687e88177d160aa379f0da30621a..819bb94e4d6154246130674fae1a1e53d75a9406 100644 (file)
--- 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 (file)
index 0000000..21ea85a
--- /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)