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.

Author: kroening

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/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