factor out module list output

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$

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

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 \

src/ebmc/build_transition_system.cpp

@@ -20,12 +20,12 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <langapi/mode.h>
 #include <smvlang/smv_ebmc_language.h>
 #include <trans-word-level/show_module_hierarchy.h>
-#include <trans-word-level/show_modules.h>
 
 #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 <fstream>
@@ -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;
   }
 

src/ebmc/show_modules.cpp

@@ -0,0 +1,97 @@
+/*******************************************************************\
+
+Module: Show Modules
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "show_modules.h"
+
+#include <util/json_irep.h>
+#include <util/symbol_table_base.h>
+#include <util/xml_irep.h>
+
+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;
+}

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 <util/source_location.h>
+
+#include <iosfwd>
+#include <list>
+#include <string>
+
+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<modulet>;
+  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

src/ebmc/transition_system.cpp

@@ -20,7 +20,6 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <langapi/language_util.h>
 #include <langapi/mode.h>
 #include <trans-word-level/show_module_hierarchy.h>
-#include <trans-word-level/show_modules.h>
 #include <verilog/verilog_types.h>
 
 #include "ebmc_error.h"

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)

src/hw-cbmc/hw_cbmc_parse_options.cpp

@@ -19,12 +19,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/show_properties.h>
 
 #include <ansi-c/goto-conversion/goto_convert_functions.h>
+#include <ebmc/show_modules.h>
 #include <goto-checker/all_properties_verifier_with_trace_storage.h>
 #include <goto-checker/goto_verifier.h>
 #include <goto-checker/multi_path_symex_checker.h>
 #include <goto-checker/solver_factory.h>
 #include <langapi/mode.h>
-#include <trans-word-level/show_modules.h>
 #include <trans-word-level/trans_trace_word_level.h>
 #include <trans-word-level/unwind.h>
 
@@ -246,7 +246,8 @@ int hw_cbmc_parse_optionst::get_modules(std::list<exprt> &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
   }
 

src/smvlang/smv_ebmc_language.cpp

@@ -16,6 +16,8 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <util/unicode.h>
 
 #include <ebmc/ebmc_error.h>
+#include <ebmc/output_file.h>
+#include <ebmc/show_modules.h>
 #include <ebmc/transition_system.h>
 
 #include "smv_parser.h"
@@ -70,31 +72,30 @@ std::optional<transition_systemt> 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);

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