From fc89115748d68d105183b4b28b995faa6f094601 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 10 Nov 2025 08:37:17 -0800
Subject: [PATCH] SMV: cleanup ports/parameters in parse tree

The parse tree has both a ports and a parameters member.  This removes the
ports member, and changes the type of the parameters member to a list of
identifiers.
---
 src/smvlang/parser.y          | 20 +++++++-------------
 src/smvlang/smv_language.cpp  |  4 ++--
 src/smvlang/smv_parse_tree.h  |  4 +---
 src/smvlang/smv_typecheck.cpp |  4 ++--
 4 files changed, 12 insertions(+), 20 deletions(-)

diff --git a/src/smvlang/parser.y b/src/smvlang/parser.y
index b79e5cf00..c728bdd68 100644
--- a/src/smvlang/parser.y
+++ b/src/smvlang/parser.y
@@ -360,11 +360,13 @@ module_name: IDENTIFIER_Token
            | STRING_Token
            ;
 
-module_head: MODULE_Token module_name { new_module($2); }
+module_head: MODULE_Token module_name
+           {
+             new_module($2);
+           }
            | MODULE_Token module_name '(' module_parameters_opt ')'
            {
-             auto &module = new_module($2);
-             module.parameters = stack_expr($4);
+             new_module($2);
            }
            ;
 
@@ -579,24 +581,16 @@ var_list   : var_decl
 
 module_parameter: identifier
            {
-             const irep_idt &identifier=stack_expr($1).get(ID_identifier);
+             const irep_idt &identifier=stack_expr($1).id();
              smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
              var.var_class=smv_parse_treet::mc_vart::ARGUMENT;
-             PARSER.module->ports.push_back(identifier);
+             PARSER.module->parameters.push_back(identifier);
            }
            ;
 
 module_parameters:
              module_parameter
-           {
-             init($$);
-             mto($$, $1);
-           }
            | module_parameters ',' module_parameter
-           {
-             $$ = $1;
-             mto($$, $3);
-           }
            ;
 
 module_parameters_opt:
diff --git a/src/smvlang/smv_language.cpp b/src/smvlang/smv_language.cpp
index 30ed6e66b..78f278b17 100644
--- a/src/smvlang/smv_language.cpp
+++ b/src/smvlang/smv_language.cpp
@@ -136,8 +136,8 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &)
 
     out << "  PARAMETERS:\n";
 
-    for(auto &parameter : module.parameters.get_sub())
-      out << "    " << parameter.id() << '\n';
+    for(auto &parameter : module.parameters)
+      out << "    " << parameter << '\n';
 
     out << '\n';
 
diff --git a/src/smvlang/smv_parse_tree.h b/src/smvlang/smv_parse_tree.h
index f150515a7..30c5962ac 100644
--- a/src/smvlang/smv_parse_tree.h
+++ b/src/smvlang/smv_parse_tree.h
@@ -37,7 +37,7 @@ class smv_parse_treet
   struct modulet
   {
     irep_idt name, base_name;
-    irept parameters;
+    std::list<irep_idt> parameters;
 
     struct itemt
     {
@@ -288,8 +288,6 @@ class smv_parse_treet
 
     mc_varst vars;
     enum_sett enum_set;
-
-    std::list<irep_idt> ports;
   };
    
   typedef std::unordered_map<irep_idt, modulet, irep_id_hash> modulest;
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index 625edab91..7f5f79e21 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -169,9 +169,9 @@ void smv_typecheckt::convert_ports(
 {
   irept::subt &ports=dest.add(ID_ports).get_sub();
 
-  ports.reserve(smv_module.ports.size());
+  ports.reserve(smv_module.parameters.size());
 
-  for(const auto &port_name : smv_module.ports)
+  for(const auto &port_name : smv_module.parameters)
   {
     ports.push_back(exprt(ID_symbol));
     ports.back().set(