Merge pull request #178 from diffblue/show-module-hierarchy

ebmc: add --show-module-hierarchy

regression/verilog/modules/show-module-hierarchy1.desc

@@ -0,0 +1,13 @@
+CORE
+show-module-hierarchy1.v
+--show-module-hierarchy
+^main:$
+^  inner main\.inner_instance1$
+^    leaf1 main\.inner_instance1\.leaf1_instance$
+^    leaf2 main\.inner_instance1\.leaf2_instance$
+^  inner main\.inner_instance2$
+^    leaf1 main\.inner_instance2\.leaf1_instance$
+^    leaf2 main\.inner_instance2\.leaf2_instance$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/verilog/modules/show-module-hierarchy1.v

@@ -0,0 +1,15 @@
+module leaf1;
+endmodule
+
+module leaf2;
+endmodule
+
+module inner;
+  leaf1 leaf1_instance();
+  leaf2 leaf2_instance();
+endmodule
+
+module main;
+  inner inner_instance1();
+  inner inner_instance2();
+endmodule

src/ebmc/ebmc_parse_options.cpp

@@ -105,6 +105,9 @@ int ebmc_parse_optionst::doit()
     if(cmdline.isset("show-modules") || cmdline.isset("modules-xml"))
       return show_modules(cmdline, ui_message_handler);
 
+    if(cmdline.isset("show-module-hierarchy"))
+      return show_module_hierarchy(cmdline, ui_message_handler);
+
     if(cmdline.isset("show-symbol-table"))
       return show_symbol_table(cmdline, ui_message_handler);
 
@@ -382,6 +385,7 @@ void ebmc_parse_optionst::help()
     " {y--preprocess}                \t output the preprocessed source file\n"
     " {y--show-parse}                \t show parse trees\n"
     " {y--show-modules}              \t show a list of the modules\n"
+    " {y--show-module-hierarchy}     \t show the hierarchy of module instantiations\n"
     " {y--show-varmap}               \t show variable map\n"
     " {y--show-netlist}              \t show netlist\n"
     " {y--show-ldg}                  \t show latch dependencies\n"

src/ebmc/ebmc_parse_options.h

@@ -25,7 +25,8 @@ class ebmc_parse_optionst:public parse_options_baset
         "(diameter)(ediameter)"
         "(diatest)(statebits):(bound):(max-bound):"
         "(show-parse)(show-varmap)(show-symbol-table)(show-netlist)"
-        "(show-ldg)(show-modules)(show-trans)(show-bdds)(show-formula)"
+        "(show-ldg)(show-modules)(show-module-hierarchy)"
+        "(show-trans)(show-bdds)(show-formula)"
         "(modules-xml):"
         "(show-properties)(property):p:(trace)"
         "(dimacs)(module):(top):"

src/ebmc/transition_system.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include <langapi/language_file.h>
 #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 "ebmc_error.h"
@@ -232,6 +233,17 @@ int get_transition_system(
   if(get_main(cmdline, message_handler, transition_system))
     return 1;
 
+  if(cmdline.isset("show-module-hierarchy"))
+  {
+    DATA_INVARIANT(
+      transition_system.main_symbol != nullptr, "must have main_symbol");
+    show_module_hierarchy(
+      transition_system.symbol_table,
+      *transition_system.main_symbol,
+      std::cout);
+    return 0;
+  }
+
   // --reset given?
   if(cmdline.isset("reset"))
   {
@@ -282,6 +294,15 @@ int show_modules(const cmdlinet &cmdline, message_handlert &message_handler)
     cmdline, message_handler, dummy_transition_system);
 }
 
+int show_module_hierarchy(
+  const cmdlinet &cmdline,
+  message_handlert &message_handler)
+{
+  transition_systemt dummy_transition_system;
+  return get_transition_system(
+    cmdline, message_handler, dummy_transition_system);
+}
+
 int show_symbol_table(
   const cmdlinet &cmdline,
   message_handlert &message_handler)

src/ebmc/transition_system.h

@@ -28,6 +28,7 @@ transition_systemt get_transition_system(const cmdlinet &, message_handlert &);
 int preprocess(const cmdlinet &, message_handlert &);
 int show_parse(const cmdlinet &, message_handlert &);
 int show_modules(const cmdlinet &, message_handlert &);
+int show_module_hierarchy(const cmdlinet &, message_handlert &);
 int show_symbol_table(const cmdlinet &, message_handlert &);
 
 #endif // CPROVER_EBMC_TRANSITION_SYSTEM_H

src/trans-word-level/Makefile

@@ -1,6 +1,12 @@
-SRC = get_trans.cpp show_modules.cpp unwind.cpp	word_level_trans.cpp \
-      property.cpp counterexample_word_level.cpp \
-      trans_trace_word_level.cpp instantiate_word_level.cpp
+SRC = get_trans.cpp \
+      show_modules.cpp \
+      show_module_hierarchy.cpp \
+      unwind.cpp \
+      word_level_trans.cpp \
+      property.cpp \
+      counterexample_word_level.cpp \
+      trans_trace_word_level.cpp \
+      instantiate_word_level.cpp
 
 include ../config.inc
 include ../common

src/trans-word-level/show_module_hierarchy.cpp

@@ -0,0 +1,60 @@
+/*******************************************************************\
+
+Module: Show Module Hierarchy
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "show_module_hierarchy.h"
+
+#include <util/namespace.h>
+
+std::size_t hierarchy_depth(const irep_idt &identifier)
+{
+  auto &as_string = id2string(identifier);
+  return std::count(as_string.begin(), as_string.end(), '.');
+}
+
+void show_module_hierarchy(
+  const symbol_table_baset &symbol_table,
+  const symbolt &main_symbol,
+  std::ostream &out)
+{
+  // Get the sorted list of symbols and
+  // find any module instances in the given module.
+  std::vector<irep_idt> instances;
+
+  for(auto &identifier : symbol_table.sorted_symbol_names())
+  {
+    const auto &symbol = symbol_table.lookup_ref(identifier);
+    if(
+      symbol.type.id() == ID_module_instance &&
+      symbol.module == main_symbol.name)
+    {
+      instances.push_back(identifier);
+    }
+  }
+
+  // now display them as a tree, using the 'main_symbol' as the root
+  out << main_symbol.display_name() << ':' << '\n';
+
+  for(const auto &identifier : instances)
+  {
+    const auto &symbol = symbol_table.lookup_ref(identifier);
+
+    // indent according to depth in the hierarchy
+    out << std::string(hierarchy_depth(identifier) * 2, ' ');
+
+    // output type
+    auto instance_module = symbol.value.get(ID_module);
+    if(!instance_module.empty())
+    {
+      const auto &module_symbol = symbol_table.lookup_ref(instance_module);
+      out << module_symbol.pretty_name << ' ';
+    }
+
+    // then instance name
+    out << symbol.display_name() << '\n';
+  }
+}

src/trans-word-level/show_module_hierarchy.h

@@ -0,0 +1,19 @@
+/*******************************************************************\
+
+Module: Show Module Hierarchy
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_TRANS_WORD_LEVEL_SHOW_MODULE_HIERARCHY_H
+#define CPROVER_TRANS_WORD_LEVEL_SHOW_MODULE_HIERARCHY_H
+
+#include <util/symbol_table_base.h>
+
+void show_module_hierarchy(
+  const symbol_table_baset &,
+  const symbolt &main_symbol,
+  std::ostream &);
+
+#endif