From 4c484d157f3048537036ec038c4b0e4276374e16 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 11 Dec 2025 14:03:56 -0800
Subject: [PATCH] Implement --show-modules for SMV

This adds an implementation of --show-modules for the SMV front-end.
---
 regression/ebmc/CLI/show-modules-smv.desc | 21 +++++++++++++++++++++
 regression/ebmc/CLI/show-modules-smv.smv  | 15 +++++++++++++++
 src/smvlang/parser.y                      | 10 +++++++---
 src/smvlang/smv_ebmc_language.cpp         | 23 ++++++++++++++++++++---
 src/smvlang/smv_parse_tree.h              |  1 +
 5 files changed, 64 insertions(+), 6 deletions(-)
 create mode 100644 regression/ebmc/CLI/show-modules-smv.desc
 create mode 100644 regression/ebmc/CLI/show-modules-smv.smv

diff --git a/regression/ebmc/CLI/show-modules-smv.desc b/regression/ebmc/CLI/show-modules-smv.desc
new file mode 100644
index 000000000..0d28e7649
--- /dev/null
+++ b/regression/ebmc/CLI/show-modules-smv.desc
@@ -0,0 +1,21 @@
+CORE
+show-modules-smv.smv
+--show-modules
+activate-multi-line-match
+Module 1:
+  Location:   file show-modules-smv\.smv line 3
+  Identifier: smv::main
+  Name:       main
+
+Module 2:
+  Location:   file show-modules-smv\.smv line 8
+  Identifier: smv::bar
+  Name:       bar
+
+Module 3:
+  Location:   file show-modules-smv\.smv line 13
+  Identifier: smv::foo
+  Name:       foo
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/ebmc/CLI/show-modules-smv.smv b/regression/ebmc/CLI/show-modules-smv.smv
new file mode 100644
index 000000000..e046990d9
--- /dev/null
+++ b/regression/ebmc/CLI/show-modules-smv.smv
@@ -0,0 +1,15 @@
+-- from the NuSMV 2.7 manual
+
+MODULE main
+ VAR
+  a : bar;
+  m : foo(a);
+
+MODULE bar
+ VAR
+  q : boolean;
+  p : boolean;
+
+MODULE foo(c)
+ DEFINE
+  flag := c.q | c.p;
diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index 443a32a2d..70e14599a 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -177,7 +177,7 @@ Function: new_module
 
 \*******************************************************************/
 
-static smv_parse_treet::modulet &new_module(YYSTYPE &module_name)
+static smv_parse_treet::modulet &new_module(YYSTYPE &location, YYSTYPE &module_name)
 {
   auto base_name = stack_expr(module_name).id_string();
   const std::string identifier=smv_module_symbol(base_name);
@@ -186,6 +186,7 @@ static smv_parse_treet::modulet &new_module(YYSTYPE &module_name)
   PARSER.parse_tree.module_map[identifier] = --PARSER.parse_tree.module_list.end();
   module.name = identifier;
   module.base_name = base_name;
+  module.source_location = stack_expr(location).source_location();
   PARSER.module = &module;
   return module;
 }
@@ -363,8 +364,11 @@ module_name: IDENTIFIER_Token
            | STRING_Token
            ;
 
-module_head: MODULE_Token module_name { new_module($2); }
-           | MODULE_Token module_name { new_module($2); }
+module_keyword: MODULE_Token { init($$); /* for the location */ }
+           ;
+
+module_head: module_keyword module_name { new_module($1, $2); }
+           | module_keyword module_name { new_module($1, $2); }
              '(' module_parameters_opt ')'
            ;
 
diff --git a/src/smvlang/smv_ebmc_language.cpp b/src/smvlang/smv_ebmc_language.cpp
index 2177c062a..6de6be8b1 100644
--- a/src/smvlang/smv_ebmc_language.cpp
+++ b/src/smvlang/smv_ebmc_language.cpp
@@ -70,9 +70,26 @@ std::optional<transition_systemt> smv_ebmc_languaget::transition_system()
     return {};
   }
 
-  if(
-    cmdline.isset("show-modules") || cmdline.isset("modules-xml") ||
-    cmdline.isset("json-modules"))
+  if(cmdline.isset("show-modules"))
+  {
+    std::size_t count = 0;
+    auto &out = std::cout;
+
+    for(const auto &module : parse_tree.module_list)
+    {
+      count++;
+
+      out << "Module " << count << ":" << '\n';
+
+      out << "  Location:   " << module.source_location << '\n';
+      out << "  Identifier: " << module.name << '\n';
+      out << "  Name:       " << module.base_name << '\n' << '\n';
+    }
+
+    return {};
+  }
+
+  if(cmdline.isset("modules-xml") || cmdline.isset("json-modules"))
   {
     //show_modules(cmdline, message_handler);
     return {};
diff --git a/src/smvlang/smv_parse_tree.h b/src/smvlang/smv_parse_tree.h
index 82ed955e2..37cf2bf7f 100644
--- a/src/smvlang/smv_parse_tree.h
+++ b/src/smvlang/smv_parse_tree.h
@@ -29,6 +29,7 @@ class smv_parse_treet
 
   struct modulet
   {
+    source_locationt source_location;
     irep_idt name, base_name;
     std::vector<irep_idt> parameters;