From 4ab1e1b928077bc33bf7fdbd942f234670c89de0 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sat, 13 Dec 2025 10:51:20 -0800 Subject: [PATCH] factor out module list output This extracts the code for displaying lists of modules in various formats (plain text, XML, JSON) into a common class. --- regression/ebmc/CLI/show-modules-smv.desc | 3 + src/Makefile | 2 +- src/ebmc/Makefile | 1 + src/ebmc/build_transition_system.cpp | 13 ++- src/ebmc/show_modules.cpp | 97 ++++++++++++++++ src/ebmc/show_modules.h | 51 +++++++++ src/ebmc/transition_system.cpp | 1 - src/hw-cbmc/Makefile | 1 + src/hw-cbmc/hw_cbmc_parse_options.cpp | 5 +- src/smvlang/smv_ebmc_language.cpp | 33 +++--- src/trans-word-level/Makefile | 1 - src/trans-word-level/show_modules.cpp | 128 ---------------------- src/trans-word-level/show_modules.h | 20 ---- 13 files changed, 182 insertions(+), 174 deletions(-) create mode 100644 src/ebmc/show_modules.cpp create mode 100644 src/ebmc/show_modules.h delete mode 100644 src/trans-word-level/show_modules.cpp delete mode 100644 src/trans-word-level/show_modules.h diff --git a/regression/ebmc/CLI/show-modules-smv.desc b/regression/ebmc/CLI/show-modules-smv.desc index 0d28e7649..87703843d 100644 --- a/regression/ebmc/CLI/show-modules-smv.desc +++ b/regression/ebmc/CLI/show-modules-smv.desc @@ -4,16 +4,19 @@ show-modules-smv.smv activate-multi-line-match Module 1: Location: file show-modules-smv\.smv line 3 + Mode: SMV Identifier: smv::main Name: main Module 2: Location: file show-modules-smv\.smv line 8 + Mode: SMV Identifier: smv::bar Name: bar Module 3: Location: file show-modules-smv\.smv line 13 + Mode: SMV Identifier: smv::foo Name: foo ^EXIT=0$ diff --git a/src/Makefile b/src/Makefile index a1fc826b3..b5ded5f0f 100644 --- a/src/Makefile +++ b/src/Makefile @@ -21,7 +21,7 @@ ifneq ($(BUILD_ENV),MSVC) ebmc.dir: ic3.dir endif -hw-cbmc.dir: trans-word-level.dir trans-netlist.dir verilog.dir \ +hw-cbmc.dir: ebmc.dir trans-word-level.dir trans-netlist.dir verilog.dir \ vhdl.dir smvlang.dir cprover.dir temporal-logic.dir vlindex.dir: ebmc.dir cprover.dir verilog.dir diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile index e1973eb9e..de0fed92f 100644 --- a/src/ebmc/Makefile +++ b/src/ebmc/Makefile @@ -36,6 +36,7 @@ SRC = \ ranking_function.cpp \ report_results.cpp \ show_formula_solver.cpp \ + show_modules.cpp \ show_properties.cpp \ show_trans.cpp \ tautology_check.cpp \ diff --git a/src/ebmc/build_transition_system.cpp b/src/ebmc/build_transition_system.cpp index f14dc10b6..1026da6a5 100644 --- a/src/ebmc/build_transition_system.cpp +++ b/src/ebmc/build_transition_system.cpp @@ -20,12 +20,12 @@ Author: Daniel Kroening, dkr@amazon.com #include #include #include -#include #include "ebmc_error.h" #include "ebmc_language_file.h" #include "ebmc_version.h" #include "output_file.h" +#include "show_modules.h" #include "transition_system.h" #include @@ -228,22 +228,25 @@ int get_transition_system( if(cmdline.isset("show-modules")) { - show_modules(transition_system.symbol_table, std::cout); + show_modulest::from_symbol_table(transition_system.symbol_table) + .plain_text(std::cout); return 0; } if(cmdline.isset("modules-xml")) { auto filename = cmdline.get_value("modules-xml"); - auto outfile = output_filet{filename}; - show_modules_xml(transition_system.symbol_table, outfile.stream()); + auto out_file = output_filet{filename}; + show_modulest::from_symbol_table(transition_system.symbol_table) + .xml(out_file.stream()); return 0; } if(cmdline.isset("json-modules")) { auto out_file = output_filet{cmdline.get_value("json-modules")}; - json_modules(transition_system.symbol_table, out_file.stream()); + show_modulest::from_symbol_table(transition_system.symbol_table) + .json(out_file.stream()); return 0; } diff --git a/src/ebmc/show_modules.cpp b/src/ebmc/show_modules.cpp new file mode 100644 index 000000000..635b06004 --- /dev/null +++ b/src/ebmc/show_modules.cpp @@ -0,0 +1,97 @@ +/*******************************************************************\ + +Module: Show Modules + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "show_modules.h" + +#include +#include +#include + +void show_modulest::xml(std::ostream &out) const +{ + std::size_t count = 0; + + for(const auto &module : modules) + { + count++; + + xmlt xml("module"); + xml.new_element("number").data = std::to_string(count); // will go away + xml.set_attribute("number", std::to_string(count)); + + xmlt &l = xml.new_element(); + convert(module.source_location, l); + l.name = "location"; + + // these go away + xml.new_element("identifier").data = id2string(module.identifier); + xml.new_element("mode").data = id2string(module.mode); + xml.new_element("name").data = id2string(module.display_name); + + // these stay + xml.set_attribute("identifier", id2string(module.identifier)); + xml.set_attribute("mode", id2string(module.mode)); + xml.set_attribute("name", id2string(module.display_name)); + + out << xml; + } +} + +void show_modulest::plain_text(std::ostream &out) const +{ + std::size_t count = 0; + + for(const auto &module : modules) + { + count++; + + out << "Module " << count << ":" << '\n'; + + out << " Location: " << module.source_location << '\n'; + out << " Mode: " << module.mode << '\n'; + out << " Identifier: " << module.identifier << '\n'; + out << " Name: " << module.display_name << '\n' << '\n'; + } +} + +void show_modulest::json(std::ostream &out) const +{ + json_arrayt json_modules; + + for(const auto &module : modules) + { + json_objectt json_module; + json_module["location"] = ::json(module.source_location); + json_module["identifier"] = json_stringt{id2string(module.identifier)}; + json_module["mode"] = json_stringt{id2string(module.mode)}; + json_module["name"] = json_stringt{id2string(module.display_name)}; + + json_modules.push_back(std::move(json_module)); + } + + out << json_modules; +} + +show_modulest +show_modulest::from_symbol_table(const symbol_table_baset &symbol_table) +{ + show_modulest show_modules; + + for(const auto &s : symbol_table.symbols) + { + const symbolt &symbol = s.second; + + if(symbol.type.id() == ID_module) + { + show_modules.modules.emplace_back( + symbol.name, symbol.display_name(), symbol.mode, symbol.location); + } + } + + return show_modules; +} diff --git a/src/ebmc/show_modules.h b/src/ebmc/show_modules.h new file mode 100644 index 000000000..cf2b24b24 --- /dev/null +++ b/src/ebmc/show_modules.h @@ -0,0 +1,51 @@ +/*******************************************************************\ + +Module: Show Modules + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_EBMC_SHOW_MODULES_H +#define CPROVER_EBMC_SHOW_MODULES_H + +#include + +#include +#include +#include + +class symbol_table_baset; + +class show_modulest +{ +public: + struct modulet + { + modulet( + irep_idt _identifier, + irep_idt _display_name, + irep_idt _mode, + source_locationt _source_location) + : identifier(_identifier), + display_name(_display_name), + mode(_mode), + source_location(std::move(_source_location)) + { + } + + irep_idt identifier, display_name, mode; + source_locationt source_location; + }; + + using modulest = std::list; + modulest modules; + + void plain_text(std::ostream &) const; + void xml(std::ostream &) const; + void json(std::ostream &) const; + + static show_modulest from_symbol_table(const symbol_table_baset &); +}; + +#endif diff --git a/src/ebmc/transition_system.cpp b/src/ebmc/transition_system.cpp index 56a5fa911..5cee19308 100644 --- a/src/ebmc/transition_system.cpp +++ b/src/ebmc/transition_system.cpp @@ -20,7 +20,6 @@ Author: Daniel Kroening, dkr@amazon.com #include #include #include -#include #include #include "ebmc_error.h" diff --git a/src/hw-cbmc/Makefile b/src/hw-cbmc/Makefile index 7634c69de..e86cbb900 100644 --- a/src/hw-cbmc/Makefile +++ b/src/hw-cbmc/Makefile @@ -34,6 +34,7 @@ OBJ+= $(CPROVER_DIR)/goto-checker/goto-checker$(LIBEXT) \ $(CPROVER_DIR)/solvers/solvers$(LIBEXT) \ $(CPROVER_DIR)/util/util$(LIBEXT) \ $(CPROVER_DIR)/json/json$(LIBEXT) \ + ../ebmc/show_modules$(OBJEXT) \ ../temporal-logic/temporal-logic$(LIBEXT) \ ../trans-netlist/trans_trace$(OBJEXT) \ ../trans-word-level/trans-word-level$(LIBEXT) diff --git a/src/hw-cbmc/hw_cbmc_parse_options.cpp b/src/hw-cbmc/hw_cbmc_parse_options.cpp index 4c68ae063..9d41f6429 100644 --- a/src/hw-cbmc/hw_cbmc_parse_options.cpp +++ b/src/hw-cbmc/hw_cbmc_parse_options.cpp @@ -19,12 +19,12 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include #include #include -#include #include #include @@ -246,7 +246,8 @@ int hw_cbmc_parse_optionst::get_modules(std::list &bmc_constraints) { } else if(cmdline.isset("show-modules")) { - show_modules(goto_model.symbol_table, std::cout); + show_modulest::from_symbol_table(goto_model.symbol_table) + .plain_text(std::cout); return 0; // done } diff --git a/src/smvlang/smv_ebmc_language.cpp b/src/smvlang/smv_ebmc_language.cpp index 6de6be8b1..77a576e7a 100644 --- a/src/smvlang/smv_ebmc_language.cpp +++ b/src/smvlang/smv_ebmc_language.cpp @@ -16,6 +16,8 @@ Author: Daniel Kroening, dkr@amazon.com #include #include +#include +#include #include #include "smv_parser.h" @@ -70,31 +72,30 @@ std::optional smv_ebmc_languaget::transition_system() return {}; } - if(cmdline.isset("show-modules")) + if( + cmdline.isset("show-modules") || cmdline.isset("modules-xml") || + cmdline.isset("json-modules")) { - std::size_t count = 0; - auto &out = std::cout; + show_modulest show_modules; for(const auto &module : parse_tree.module_list) - { - count++; + show_modules.modules.emplace_back( + module.name, module.base_name, "SMV", module.source_location); - out << "Module " << count << ":" << '\n'; + auto filename = cmdline.value_opt("outfile").value_or("-"); + output_filet output_file{filename}; + auto &out = output_file.stream(); - out << " Location: " << module.source_location << '\n'; - out << " Identifier: " << module.name << '\n'; - out << " Name: " << module.base_name << '\n' << '\n'; - } + if(cmdline.isset("show-modules")) + show_modules.plain_text(out); + else if(cmdline.isset("modules-xml")) + show_modules.xml(out); + else if(cmdline.isset("json-modules")) + show_modules.json(out); return {}; } - if(cmdline.isset("modules-xml") || cmdline.isset("json-modules")) - { - //show_modules(cmdline, message_handler); - return {}; - } - if(cmdline.isset("show-module-hierarchy")) { //show_module_hierarchy(cmdline, message_handler); diff --git a/src/trans-word-level/Makefile b/src/trans-word-level/Makefile index 3e5b7a769..ebdfc4381 100644 --- a/src/trans-word-level/Makefile +++ b/src/trans-word-level/Makefile @@ -6,7 +6,6 @@ SRC = counterexample_word_level.cpp \ trans_trace_word_level.cpp \ instantiate_word_level.cpp \ sequence.cpp \ - show_modules.cpp \ show_module_hierarchy.cpp \ unwind.cpp \ word_level_trans.cpp diff --git a/src/trans-word-level/show_modules.cpp b/src/trans-word-level/show_modules.cpp deleted file mode 100644 index 4bea6ef05..000000000 --- a/src/trans-word-level/show_modules.cpp +++ /dev/null @@ -1,128 +0,0 @@ -/*******************************************************************\ - -Module: Show Modules - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#include "show_modules.h" - -#include -#include - -/*******************************************************************\ - -Function: show_modules_xml - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void show_modules_xml(const symbol_table_baset &symbol_table, std::ostream &out) -{ - std::size_t count = 0; - - for(const auto &s : symbol_table.symbols) - { - const symbolt &symbol = s.second; - - if(symbol.type.id() == ID_module) - { - count++; - - xmlt xml("module"); - xml.new_element("number").data = std::to_string(count); // will go away - xml.set_attribute("number", std::to_string(count)); - - xmlt &l = xml.new_element(); - convert(symbol.location, l); - l.name = "location"; - - // these go away - xml.new_element("identifier").data = id2string(symbol.name); - xml.new_element("mode").data = id2string(symbol.mode); - xml.new_element("name").data = id2string(symbol.display_name()); - - // these stay - xml.set_attribute("identifier", id2string(symbol.name)); - xml.set_attribute("mode", id2string(symbol.mode)); - xml.set_attribute("name", id2string(symbol.display_name())); - - out << xml; - } - } -} - -/*******************************************************************\ - -Function: show_modules - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void show_modules(const symbol_table_baset &symbol_table, std::ostream &out) -{ - std::size_t count = 0; - - for(const auto &s : symbol_table.symbols) - { - const symbolt &symbol=s.second; - - if(symbol.type.id()==ID_module) - { - count++; - - out << "Module " << count << ":" << '\n'; - - out << " Location: " << symbol.location << '\n'; - out << " Mode: " << symbol.mode << '\n'; - out << " Identifier: " << symbol.name << '\n'; - out << " Name: " << symbol.display_name() << '\n' << '\n'; - } - } -} - -/*******************************************************************\ - -Function: json_modules - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void json_modules(const symbol_table_baset &symbol_table, std::ostream &out) -{ - json_arrayt json_modules; - - for(const auto &s : symbol_table.symbols) - { - const symbolt &symbol = s.second; - - if(symbol.type.id() == ID_module) - { - json_objectt json_module; - json_module["location"] = json(symbol.location); - json_module["identifier"] = json_stringt{id2string(symbol.name)}; - json_module["mode"] = json_stringt{id2string(symbol.mode)}; - json_module["name"] = json_stringt{id2string(symbol.display_name())}; - - json_modules.push_back(std::move(json_module)); - } - } - - out << json_modules; -} diff --git a/src/trans-word-level/show_modules.h b/src/trans-word-level/show_modules.h deleted file mode 100644 index caa8fe307..000000000 --- a/src/trans-word-level/show_modules.h +++ /dev/null @@ -1,20 +0,0 @@ -/*******************************************************************\ - -Module: Show Modules - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -#ifndef CPROVER_TRANS_SHOW_MODULES_H -#define CPROVER_TRANS_SHOW_MODULES_H - -#include - -void show_modules(const symbol_table_baset &, std::ostream &); - -void show_modules_xml(const symbol_table_baset &, std::ostream &); - -void json_modules(const symbol_table_baset &, std::ostream &); - -#endif