From e7e444a5b593ca6f0119f7d3fc2a13f91bc7e9c1 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 4 Jul 2024 17:50:31 +0100 Subject: [PATCH] introduce output_filet This introduces a new class output_filet, which * given a filename, opens the file for writing, and provides an std::ostream for it; if this fails, an appropriate exception is thrown. * given "-", provides a pointer to std::cout --- src/ebmc/Makefile | 1 + src/ebmc/ebmc_base.cpp | 18 +++++---------- src/ebmc/ebmc_error.h | 3 ++- src/ebmc/neural_liveness.cpp | 13 +++++------ src/ebmc/output_file.cpp | 40 +++++++++++++++++++++++++++++++++ src/ebmc/output_file.h | 41 ++++++++++++++++++++++++++++++++++ src/ebmc/random_traces.cpp | 36 +++++++++-------------------- src/ebmc/report_results.cpp | 14 +++++------- src/ebmc/show_properties.cpp | 16 +++---------- src/ebmc/show_trans.cpp | 30 +++++-------------------- src/ebmc/transition_system.cpp | 7 +++--- 11 files changed, 121 insertions(+), 98 deletions(-) create mode 100644 src/ebmc/output_file.cpp create mode 100644 src/ebmc/output_file.h diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile index 9ce056121..d96667378 100644 --- 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 index a3cc292a4..03a5d4944 100644 --- a/src/ebmc/ebmc_base.cpp +++ b/src/ebmc/ebmc_base.cpp @@ -12,7 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -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 -#include #include /*******************************************************************\ @@ -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 index 947dbddff..f8d04a018 100644 --- 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 + #include -#include class ebmc_errort { diff --git a/src/ebmc/neural_liveness.cpp b/src/ebmc/neural_liveness.cpp index d72bc2e2b..5c2856f09 100644 --- a/src/ebmc/neural_liveness.cpp +++ b/src/ebmc/neural_liveness.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, dkr@amazon.com #include #include #include -#include #include #include @@ -21,6 +20,7 @@ Author: Daniel Kroening, dkr@amazon.com #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 new file mode 100644 index 000000000..628ff0b48 --- /dev/null +++ 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 + +#include "ebmc_error.h" + +#include +#include + +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 new file mode 100644 index 000000000..189bf5732 --- /dev/null +++ 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 +#include + +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 index ac546de19..67c17bdd4 100644 --- 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 @@ -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 index 07c989e7b..2f45f347b 100644 --- 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 -#include #include #include "ebmc_error.h" +#include "output_file.h" #include "waveform.h" -#include #include /*******************************************************************\ @@ -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 index 58b9b7692..aa84ab612 100644 --- a/src/ebmc/show_properties.cpp +++ b/src/ebmc/show_properties.cpp @@ -8,12 +8,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include "ebmc_base.h" #include "ebmc_error.h" +#include "output_file.h" #include @@ -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 index 8de6b587a..0c1a2bbc3 100644 --- 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 - #include #include "ebmc_base.h" #include "ebmc_version.h" +#include "output_file.h" #include "output_verilog.h" -#include #include /*******************************************************************\ @@ -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 index c340733f9..c442e9238 100644 --- a/src/ebmc/transition_system.cpp +++ b/src/ebmc/transition_system.cpp @@ -25,6 +25,7 @@ Author: Daniel Kroening, dkr@amazon.com #include "ebmc_error.h" #include "ebmc_version.h" +#include "output_file.h" #include #include @@ -273,10 +274,8 @@ int get_transition_system( if(cmdline.isset("modules-xml")) { auto filename = cmdline.get_value("modules-xml"); - std::ofstream out(widen_if_needed(filename)); - if(!out) - throw ebmc_errort() << "failed to open " << filename; - show_modules_xml(transition_system.symbol_table, out); + auto outfile = output_filet{filename}; + show_modules_xml(transition_system.symbol_table, outfile.stream()); return 0; }