JSON output for the modules

regression/ebmc/CLI/json-modules.desc

@@ -0,0 +1,29 @@
+CORE
+json-modules.v
+--json-modules -
+activate-multi-line-match
+\[
+  \{
+    "identifier": "Verilog::foo",
+    "location": \{
+      "file": "json-modules\.v",
+      "line": "1",
+      "workingDirectory": ".*"
+    \},
+    "mode": "Verilog",
+    "name": "foo"
+  \},
+  \{
+    "identifier": "Verilog::bar",
+    "location": \{
+      "file": "json-modules.v",
+      "line": "4",
+      "workingDirectory": ".*"
+    \},
+    "mode": "Verilog",
+    "name": "bar"
+  \}
+\]
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/CLI/json-modules.v

@@ -0,0 +1,5 @@
+module foo;
+endmodule
+
+module bar;
+endmodule

src/ebmc/ebmc_parse_options.cpp

@@ -103,7 +103,9 @@ int ebmc_parse_optionst::doit()
     if(cmdline.isset("show-parse"))
       return show_parse(cmdline, ui_message_handler);
 
-    if(cmdline.isset("show-modules") || cmdline.isset("modules-xml"))
+    if(
+      cmdline.isset("show-modules") || cmdline.isset("modules-xml") ||
+      cmdline.isset("json-modules"))
       return show_modules(cmdline, ui_message_handler);
 
     if(cmdline.isset("show-module-hierarchy"))

src/ebmc/ebmc_parse_options.h

@@ -33,7 +33,7 @@ class ebmc_parse_optionst:public parse_options_baset
         "(dimacs)(module):(top):"
         "(po)(cegar)(k-induction)(2pi)(bound2):"
         "(outfile):(xml-ui)(verbosity):(gui)"
-        "(json-result):(json-properties):"
+        "(json-modules):(json-properties):(json-result):"
         "(neural-liveness)(neural-engine):"
         "(reset):"
         "(version)(verilog-rtl)(verilog-netlist)"

src/ebmc/transition_system.cpp

@@ -280,6 +280,23 @@ int get_transition_system(
     return 0;
   }
 
+  if(cmdline.isset("json-modules"))
+  {
+    auto file_name = cmdline.get_value("json-modules");
+    if(file_name == "-")
+    {
+      json_modules(transition_system.symbol_table, std::cout);
+    }
+    else
+    {
+      std::ofstream out(widen_if_needed(file_name));
+      if(!out)
+        throw ebmc_errort() << "failed to open " << file_name;
+      json_modules(transition_system.symbol_table, out);
+    }
+    return 0;
+  }
+
   if(cmdline.isset("show-symbol-table"))
   {
     std::cout << transition_system.symbol_table;

src/trans-word-level/show_modules.cpp

@@ -6,11 +6,11 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include <util/xml.h>
-#include <util/xml_irep.h>
-
 #include "show_modules.h"
 
+#include <util/json_irep.h>
+#include <util/xml_irep.h>
+
 /*******************************************************************\
 
 Function: show_modules_xml
@@ -91,3 +91,38 @@ void show_modules(const symbol_table_baset &symbol_table, std::ostream &out)
     }
   }
 }
+
+/*******************************************************************\
+
+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;
+}

src/trans-word-level/show_modules.h

@@ -15,4 +15,6 @@ 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