diff --git a/src/ebmc/ebmc_base.cpp b/src/ebmc/ebmc_base.cpp index d082c7ab7..1dc8b596a 100644 --- a/src/ebmc/ebmc_base.cpp +++ b/src/ebmc/ebmc_base.cpp @@ -56,18 +56,6 @@ int ebmc_baset::get_properties() properties = ebmc_propertiest::from_command_line( cmdline, transition_system, message.get_message_handler()); - if(cmdline.isset("show-properties")) - { - show_properties(); - return 0; - } - - if(cmdline.isset("json-properties")) - { - json_properties(cmdline.get_value("json-properties")); - return 0; - } - return -1; // done } diff --git a/src/ebmc/ebmc_base.h b/src/ebmc/ebmc_base.h index 8ce407b2f..dafd7db8f 100644 --- a/src/ebmc/ebmc_base.h +++ b/src/ebmc/ebmc_base.h @@ -47,8 +47,6 @@ class ebmc_baset bool parse_property(const std::string &property); bool get_model_properties(); - void show_properties(); - void json_properties(const std::string &file_name); bool parse(); bool parse(const std::string &filename); diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index 5e01e3ca9..f9189eddb 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "property_checker.h" #include "random_traces.h" #include "ranking_function.h" +#include "show_properties.h" #include "show_trans.h" #include @@ -210,94 +211,97 @@ int ebmc_parse_optionst::doit() // get the transition system auto transition_system = get_transition_system(cmdline, ui_message_handler); + // get the properties + auto properties = ebmc_propertiest::from_command_line( + cmdline, transition_system, ui_message_handler); + + if(cmdline.isset("show-properties")) + { + show_properties(properties, ui_message_handler); + return 0; + } + + if(cmdline.isset("json-properties")) + { + json_properties(properties, cmdline.get_value("json-properties")); + return 0; + } + + // possibly apply liveness-to-safety + if(cmdline.isset("liveness-to-safety")) + liveness_to_safety(transition_system, properties); + + if(cmdline.isset("show-varmap")) + { + auto netlist = + make_netlist(transition_system, properties, ui_message_handler); + netlist.var_map.output(std::cout); + return 0; + } + + if(cmdline.isset("show-ldg")) { ebmc_baset ebmc_base(cmdline, ui_message_handler); ebmc_base.transition_system = std::move(transition_system); + ebmc_base.properties = std::move(properties); + ebmc_base.show_ldg(std::cout); + return 0; + } + + if(cmdline.isset("show-netlist")) + { + auto netlist = + make_netlist(transition_system, properties, ui_message_handler); + netlist.print(std::cout); + return 0; + } + + if(cmdline.isset("dot-netlist")) + { + auto netlist = + make_netlist(transition_system, properties, ui_message_handler); + auto filename = cmdline.value_opt("outfile").value_or("-"); + output_filet outfile{filename}; + outfile.stream() << "digraph netlist {\n"; + netlist.output_dot(outfile.stream()); + outfile.stream() << "}\n"; + return 0; + } + + if(cmdline.isset("smv-netlist")) + { + auto netlist = + make_netlist(transition_system, properties, ui_message_handler); + auto filename = cmdline.value_opt("outfile").value_or("-"); + output_filet outfile{filename}; + outfile.stream() << "-- Generated by EBMC " << EBMC_VERSION << '\n'; + outfile.stream() << "-- Generated from " + << transition_system.main_symbol->name << '\n'; + outfile.stream() << '\n'; + netlist.output_smv(outfile.stream()); + return 0; + } - auto result = ebmc_base.get_properties(); - - if(result != -1) - return result; - - // possibly apply liveness-to-safety - if(cmdline.isset("liveness-to-safety")) - liveness_to_safety(ebmc_base.transition_system, ebmc_base.properties); - - if(cmdline.isset("show-varmap")) - { - netlistt netlist; - if(ebmc_base.make_netlist(netlist)) - return 1; - netlist.var_map.output(std::cout); - return 0; - } - - if(cmdline.isset("show-ldg")) - { - ebmc_base.show_ldg(std::cout); - return 0; - } - - if(cmdline.isset("show-netlist")) - { - netlistt netlist; - if(ebmc_base.make_netlist(netlist)) - return 1; - netlist.print(std::cout); - return 0; - } - - if(cmdline.isset("dot-netlist")) - { - netlistt netlist; - if(ebmc_base.make_netlist(netlist)) - return 1; - auto filename = cmdline.value_opt("outfile").value_or("-"); - output_filet outfile{filename}; - outfile.stream() << "digraph netlist {\n"; - netlist.output_dot(outfile.stream()); - outfile.stream() << "}\n"; - return 0; - } - - if(cmdline.isset("smv-netlist")) - { - netlistt netlist; - if(ebmc_base.make_netlist(netlist)) - return 1; - auto filename = cmdline.value_opt("outfile").value_or("-"); - output_filet outfile{filename}; - outfile.stream() << "-- Generated by EBMC " << EBMC_VERSION << '\n'; - outfile.stream() << "-- Generated from " - << ebmc_base.transition_system.main_symbol->name - << '\n'; - outfile.stream() << '\n'; - netlist.output_smv(outfile.stream()); - return 0; - } - - if(cmdline.isset("cegar")) - { - auto netlist = make_netlist( - ebmc_base.transition_system, - ebmc_base.properties, - ui_message_handler); - const namespacet ns(ebmc_base.transition_system.symbol_table); - return do_bmc_cegar( - netlist, ebmc_base.properties, ns, ui_message_handler); - } - - if(cmdline.isset("compute-ct")) - return ebmc_base.do_compute_ct(); - - auto checker_result = property_checker( - cmdline, - ebmc_base.transition_system, - ebmc_base.properties, - ui_message_handler); - - return checker_result.exit_code(); + if(cmdline.isset("cegar")) + { + auto netlist = + make_netlist(transition_system, properties, ui_message_handler); + const namespacet ns(transition_system.symbol_table); + return do_bmc_cegar(netlist, properties, ns, ui_message_handler); } + + if(cmdline.isset("compute-ct")) + { + ebmc_baset ebmc_base(cmdline, ui_message_handler); + ebmc_base.transition_system = std::move(transition_system); + ebmc_base.properties = std::move(properties); + return ebmc_base.do_compute_ct(); + } + + auto checker_result = property_checker( + cmdline, transition_system, properties, ui_message_handler); + + return checker_result.exit_code(); } catch(const ebmc_errort &ebmc_error) { diff --git a/src/ebmc/show_properties.cpp b/src/ebmc/show_properties.cpp index aa84ab612..68c7edc08 100644 --- a/src/ebmc/show_properties.cpp +++ b/src/ebmc/show_properties.cpp @@ -1,25 +1,27 @@ /*******************************************************************\ -Module: Base for Verification Modules +Module: Show Properties Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include "show_properties.h" + #include #include #include #include -#include "ebmc_base.h" #include "ebmc_error.h" +#include "ebmc_properties.h" #include "output_file.h" #include /*******************************************************************\ -Function: ebmc_baset::show_properties +Function: show_properties Inputs: @@ -29,7 +31,9 @@ Function: ebmc_baset::show_properties \*******************************************************************/ -void ebmc_baset::show_properties() +void show_properties( + const ebmc_propertiest &properties, + ui_message_handlert &message_handler) { unsigned p_nr=1; @@ -49,8 +53,7 @@ void ebmc_baset::show_properties() for(const auto &p : properties.properties) { - switch(static_cast(message.get_message_handler()) - .get_ui()) + switch(message_handler.get_ui()) { case ui_message_handlert::uit::XML_UI: std::cout << make_xml(p, p_nr) << '\n'; @@ -70,7 +73,7 @@ void ebmc_baset::show_properties() /*******************************************************************\ -Function: ebmc_baset::json_properties +Function: json_properties Inputs: @@ -80,7 +83,9 @@ Function: ebmc_baset::json_properties \*******************************************************************/ -void ebmc_baset::json_properties(const std::string &file_name) +void json_properties( + const ebmc_propertiest &properties, + const std::string &file_name) { json_arrayt json; diff --git a/src/ebmc/show_properties.h b/src/ebmc/show_properties.h new file mode 100644 index 000000000..92371712b --- /dev/null +++ b/src/ebmc/show_properties.h @@ -0,0 +1,20 @@ +/*******************************************************************\ + +Module: Show Properties + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_EBMC_SHOW_PROPERTIES_H +#define CPROVER_EBMC_SHOW_PROPERTIES_H + +#include + +class ebmc_propertiest; +class ui_message_handlert; + +void show_properties(const ebmc_propertiest &, ui_message_handlert &); +void json_properties(const ebmc_propertiest &, const std::string &file_name); + +#endif