Merge pull request #588 from diffblue/output_filet

kroening · web-flow · commit f59c64d0f434 · 2024-07-10T12:51:20.000-07:00
introduce output_filet
diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile
@@ -20,6 +20,7 @@ SRC = \
       live_signal.cpp \
       main.cpp \
       neural_liveness.cpp \
+      output_file.cpp \
       output_verilog.cpp \
       random_traces.cpp \
       ranking_function.cpp \
diff --git a/src/ebmc/ebmc_base.cpp b/src/ebmc/ebmc_base.cpp
@@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/config.h>
 #include <util/expr_util.h>
 #include <util/string2int.h>
-#include <util/unicode.h>
 
 #include <solvers/prop/literal_expr.h>
 #include <solvers/sat/satcheck.h>
@@ -29,10 +28,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
 #include "ebmc_version.h"
+#include "output_file.h"
 #include "report_results.h"
 
 #include <chrono>
-#include <fstream>
 #include <iostream>
 
 /*******************************************************************\
@@ -277,20 +276,13 @@ int ebmc_baset::do_bit_level_bmc()
   {
     if(cmdline.isset("outfile"))
     {
-      const std::string filename = cmdline.get_value("outfile");
-      std::ofstream out(widen_if_needed(filename));
+      auto outfile = output_filet{cmdline.get_value("outfile")};
 
-      if(!out)
-      {
-        message.error() << "Failed to open `" << filename << "'"
-                        << messaget::eom;
-        return 1;
-      }
-
-      message.status() << "Writing DIMACS CNF to `" << filename << "'"
+      message.status() << "Writing DIMACS CNF to `" << outfile.name() << "'"
                        << messaget::eom;
 
-      dimacs_cnf_writert dimacs_cnf_writer{out, message.get_message_handler()};
+      dimacs_cnf_writert dimacs_cnf_writer{
+        outfile.stream(), message.get_message_handler()};
 
       return do_bit_level_bmc(dimacs_cnf_writer, true);
     }
diff --git a/src/ebmc/ebmc_error.h b/src/ebmc/ebmc_error.h
@@ -9,8 +9,9 @@ Author: Daniel Kroening, dkr@amazon.com
 #ifndef EBMC_ERROR_H
 #define EBMC_ERROR_H
 
+#include <util/source_location.h>
+
 #include <sstream>
-#include <string>
 
 class ebmc_errort
 {
diff --git a/src/ebmc/neural_liveness.cpp b/src/ebmc/neural_liveness.cpp
@@ -13,14 +13,14 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <util/string2int.h>
 #include <util/tempdir.h>
 #include <util/tempfile.h>
-#include <util/unicode.h>
 
 #include <temporal-logic/temporal_expr.h>
 #include <verilog/sva_expr.h>
 
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
 #include "live_signal.h"
+#include "output_file.h"
 #include "random_traces.h"
 #include "ranking_function.h"
 #include "report_results.h"
@@ -199,13 +199,10 @@ neural_livenesst::dump_vcd_files(temp_dirt &temp_dir)
     [&, trace_nr = 0ull, outfile_prefix](trans_tracet trace) mutable -> void {
       namespacet ns(transition_system.symbol_table);
       auto filename = outfile_prefix + std::to_string(trace_nr + 1);
-      std::ofstream out(widen_if_needed(filename));
-
-      if(!out)
-        throw ebmc_errort() << "failed to write trace to " << filename;
-
-      message.progress() << "*** Writing " << filename << messaget::eom;
-      show_trans_trace_vcd(trace, message, ns, out);
+      auto outfile = output_filet{filename};
+      message.progress() << "*** Writing to " << outfile.name()
+                         << messaget::eom;
+      show_trans_trace_vcd(trace, message, ns, outfile.stream());
     };
 }
 
diff --git a/src/ebmc/output_file.cpp b/src/ebmc/output_file.cpp
@@ -0,0 +1,40 @@
+/*******************************************************************\
+
+Module: Output File Container
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "output_file.h"
+
+#include <util/unicode.h>
+
+#include "ebmc_error.h"
+
+#include <fstream>
+#include <iostream>
+
+output_filet::output_filet(std::string __file_name)
+  : _name(std::move(__file_name))
+{
+  if(_name == "-")
+  {
+    _stream = &std::cout;
+    delete_required = false;
+    _name = "stdout";
+  }
+  else
+  {
+    _stream = new std::ofstream(widen_if_needed(_name));
+    if(!_stream)
+      throw ebmc_errort() << "failed to open " << _name;
+    delete_required = true;
+  }
+}
+
+output_filet::~output_filet()
+{
+  if(delete_required)
+    delete _stream;
+}
diff --git a/src/ebmc/output_file.h b/src/ebmc/output_file.h
@@ -0,0 +1,41 @@
+/*******************************************************************\
+
+Module: Output File Container
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef EBMC_OUTPUT_FILE_H
+#define EBMC_OUTPUT_FILE_H
+
+#include <iosfwd>
+#include <string>
+
+class output_filet final
+{
+public:
+  /// Create a stream to the given file name,
+  /// our stdout if "-".
+  /// Throws ebmc_errort() if the file cannot be opened.
+  explicit output_filet(std::string __file_name);
+  ~output_filet();
+
+  std::ostream &stream()
+  {
+    return *_stream;
+  }
+
+  // the name of the file, or "stdout"
+  const std::string &name()
+  {
+    return _name;
+  }
+
+protected:
+  std::string _name;
+  bool delete_required;
+  std::ostream *_stream;
+};
+
+#endif
diff --git a/src/ebmc/random_traces.cpp b/src/ebmc/random_traces.cpp
@@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "ebmc_base.h"
 #include "ebmc_error.h"
+#include "output_file.h"
 #include "waveform.h"
 
 #include <algorithm>
@@ -182,15 +183,12 @@ int random_traces(const cmdlinet &cmdline, message_handlert &message_handler)
     {
       PRECONDITION(outfile_prefix.has_value());
       auto filename = outfile_prefix.value() + std::to_string(trace_nr + 1);
-      std::ofstream out(widen_if_needed(filename));
+      auto outfile = output_filet{filename};
 
-      if(!out)
-        throw ebmc_errort() << "failed to write trace to " << filename;
-
-      consolet::out() << "*** Writing " << filename << '\n';
+      consolet::out() << "*** Writing " << outfile.name() << '\n';
 
       messaget message(message_handler);
-      show_trans_trace_vcd(trace, message, ns, out);
+      show_trans_trace_vcd(trace, message, ns, outfile.stream());
     }
     else if(cmdline.isset("waveform"))
     {
@@ -294,23 +292,13 @@ int random_trace(const cmdlinet &cmdline, message_handlert &message_handler)
     else if(cmdline.isset("vcd"))
     {
       auto filename = cmdline.get_value("vcd");
-      messaget message(message_handler);
-
-      if(filename == "-")
-      {
-        show_trans_trace_vcd(trace, message, ns, std::cout);
-      }
-      else
-      {
-        std::ofstream out(widen_if_needed(filename));
-
-        if(!out)
-          throw ebmc_errort() << "failed to write trace to " << filename;
+      auto outfile = output_filet{filename};
 
+      if(filename != "-")
         consolet::out() << "*** Writing " << filename << '\n';
 
-        show_trans_trace_vcd(trace, message, ns, out);
-      }
+      messaget message(message_handler);
+      show_trans_trace_vcd(trace, message, ns, outfile.stream());
     }
     else // default
     {
@@ -352,13 +340,9 @@ void random_traces(
   auto consumer = [&, trace_nr = 0ull](trans_tracet trace) mutable -> void {
     namespacet ns(transition_system.symbol_table);
     auto filename = outfile_prefix + std::to_string(trace_nr + 1);
-    std::ofstream out(widen_if_needed(filename));
-
-    if(!out)
-      throw ebmc_errort() << "failed to write trace to " << filename;
-
+    auto outfile = output_filet{filename};
     messaget message(message_handler);
-    show_trans_trace_vcd(trace, message, ns, out);
+    show_trans_trace_vcd(trace, message, ns, outfile.stream());
 
     trace_nr++;
   };
diff --git a/src/ebmc/report_results.cpp b/src/ebmc/report_results.cpp
@@ -12,13 +12,12 @@ Author: Daniel Kroening, dkr@amazon.com
 #include "report_results.h"
 
 #include <util/json.h>
-#include <util/unicode.h>
 #include <util/xml.h>
 
 #include "ebmc_error.h"
+#include "output_file.h"
 #include "waveform.h"
 
-#include <fstream>
 #include <iostream>
 
 /*******************************************************************\
@@ -42,9 +41,7 @@ void report_results(
   if(cmdline.isset("json-result"))
   {
     auto filename = cmdline.get_value("json-result");
-    std::ofstream out(widen_if_needed(filename));
-    if(!out)
-      throw ebmc_errort() << "failed to open " << filename;
+    auto outfile = output_filet{filename};
 
     json_objectt json_results;
     auto &json_properties = json_results["properties"].make_array();
@@ -65,7 +62,7 @@ void report_results(
       json_properties.push_back(std::move(json_property));
     }
 
-    out << json_results;
+    outfile.stream() << json_results;
   }
 
   if(
@@ -167,10 +164,11 @@ void report_results(
       if(property.has_witness_trace())
       {
         std::string vcdfile = cmdline.get_value("vcd");
-        std::ofstream vcd(widen_if_needed(vcdfile));
+        auto outfile = output_filet{vcdfile};
 
         messaget message(message_handler);
-        show_trans_trace_vcd(property.witness_trace.value(), message, ns, vcd);
+        show_trans_trace_vcd(
+          property.witness_trace.value(), message, ns, outfile.stream());
 
         break;
       }
diff --git a/src/ebmc/show_properties.cpp b/src/ebmc/show_properties.cpp
@@ -8,12 +8,12 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/json.h>
 #include <util/json_irep.h>
-#include <util/unicode.h>
 #include <util/xml.h>
 #include <util/xml_irep.h>
 
 #include "ebmc_base.h"
 #include "ebmc_error.h"
+#include "output_file.h"
 
 #include <iostream>
 
@@ -97,16 +97,6 @@ void ebmc_baset::json_properties(const std::string &file_name)
     json.push_back(std::move(json_property));
   }
 
-  if(file_name == "-")
-  {
-    std::cout << json;
-  }
-  else
-  {
-    std::ofstream out(widen_if_needed(file_name));
-    if(!out)
-      throw ebmc_errort() << "failed to open " << file_name;
-
-    out << json;
-  }
+  auto outfile = output_filet{file_name};
+  outfile.stream() << json;
 }
diff --git a/src/ebmc/show_trans.cpp b/src/ebmc/show_trans.cpp
@@ -8,15 +8,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "show_trans.h"
 
-#include <util/unicode.h>
-
 #include <verilog/expr2verilog.h>
 
 #include "ebmc_base.h"
 #include "ebmc_version.h"
+#include "output_file.h"
 #include "output_verilog.h"
 
-#include <fstream>
 #include <iostream>
 
 /*******************************************************************\
@@ -268,17 +266,8 @@ int show_transt::show_trans_verilog_rtl()
   if(cmdline.isset("outfile"))
   {
     const std::string filename=cmdline.get_value("outfile");
-    std::ofstream out(widen_if_needed(filename));
-
-    if(!out)
-    {
-      std::cerr << "Failed to open `"
-                << filename
-                << "'" << '\n';
-      return 1;
-    }
-
-    show_trans_verilog_rtl(out);
+    auto outfile = output_filet{filename};
+    show_trans_verilog_rtl(outfile.stream());
   }
   else
     show_trans_verilog_rtl(std::cout);
@@ -306,17 +295,8 @@ int show_transt::show_trans_verilog_netlist()
   if(cmdline.isset("outfile"))
   {
     const std::string filename=cmdline.get_value("outfile");
-    std::ofstream out(widen_if_needed(filename));
-
-    if(!out)
-    {
-      std::cerr << "Failed to open `"
-                << filename
-                << "'" << '\n';
-      return 1;
-    }
-
-    show_trans_verilog_netlist(out);
+    auto outfile = output_filet{filename};
+    show_trans_verilog_netlist(outfile.stream());
   }
   else
     show_trans_verilog_netlist(std::cout);
diff --git a/src/ebmc/transition_system.cpp b/src/ebmc/transition_system.cpp

Original file line number	Diff line number	Diff line change
`@@ -9,8 +9,9 @@ Author: Daniel Kroening, dkr@amazon.com`
`9`	`9`	`#ifndef EBMC_ERROR_H`
`10`	`10`	`#define EBMC_ERROR_H`
`11`	`11`
	`12`	`+#include <util/source_location.h>`
	`13`	`+`
`12`	`14`	`#include <sstream>`
`13`		`-#include <string>`
`14`	`15`
`15`	`16`	`class ebmc_errort`
`16`	`17`	`{`