From 8465313b48653edc35a2020234052994d2e599d9 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 22 Jun 2024 12:13:40 -0700
Subject: [PATCH] JSON output for the modules

This adds --json-modules, to get a JSON array with all the modules.
---
 regression/ebmc/CLI/json-modules.desc | 29 +++++++++++++++++++
 regression/ebmc/CLI/json-modules.v    |  5 ++++
 src/ebmc/ebmc_parse_options.cpp       |  4 ++-
 src/ebmc/ebmc_parse_options.h         |  2 +-
 src/ebmc/transition_system.cpp        | 17 +++++++++++
 src/trans-word-level/show_modules.cpp | 41 +++++++++++++++++++++++++--
 src/trans-word-level/show_modules.h   |  2 ++
 7 files changed, 95 insertions(+), 5 deletions(-)
 create mode 100644 regression/ebmc/CLI/json-modules.desc
 create mode 100644 regression/ebmc/CLI/json-modules.v

diff --git a/regression/ebmc/CLI/json-modules.desc b/regression/ebmc/CLI/json-modules.desc
new file mode 100644
index 000000000..83efd1894
--- /dev/null
+++ b/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$
+--
diff --git a/regression/ebmc/CLI/json-modules.v b/regression/ebmc/CLI/json-modules.v
new file mode 100644
index 000000000..ecf49ecd1
--- /dev/null
+++ b/regression/ebmc/CLI/json-modules.v
@@ -0,0 +1,5 @@
+module foo;
+endmodule
+
+module bar;
+endmodule
diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp
index d1029b152..a810542ea 100644
--- a/src/ebmc/ebmc_parse_options.cpp
+++ b/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"))
diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h
index 4e798052a..051413cf8 100644
--- a/src/ebmc/ebmc_parse_options.h
+++ b/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)"
diff --git a/src/ebmc/transition_system.cpp b/src/ebmc/transition_system.cpp
index dcbf8d54b..c340733f9 100644
--- a/src/ebmc/transition_system.cpp
+++ b/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;
diff --git a/src/trans-word-level/show_modules.cpp b/src/trans-word-level/show_modules.cpp
index 0bba0b907..4bea6ef05 100644
--- a/src/trans-word-level/show_modules.cpp
+++ b/src/trans-word-level/show_modules.cpp
@@ -6,11 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-#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;
+}
diff --git a/src/trans-word-level/show_modules.h b/src/trans-word-level/show_modules.h
index 17109db4a..caa8fe307 100644
--- a/src/trans-word-level/show_modules.h
+++ b/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