From daf9e9758a197bf4cc4e319eb67286c2dcc4c7e4 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 10 Nov 2025 11:38:23 -0800
Subject: [PATCH] SMV: catch variables that have the same identifier as a
 parameter

This errors variable and enum declarations that use the same identifier as a
previously defined module parameter.
---
 regression/smv/define/define9.desc        |  8 +++++
 regression/smv/define/define9.smv         | 10 +++++++
 regression/smv/var/already_declared4.desc |  3 +-
 src/smvlang/smv_typecheck.cpp             | 36 +++++++++++++++++++++--
 4 files changed, 52 insertions(+), 5 deletions(-)
 create mode 100644 regression/smv/define/define9.desc
 create mode 100644 regression/smv/define/define9.smv

diff --git a/regression/smv/define/define9.desc b/regression/smv/define/define9.desc
new file mode 100644
index 000000000..416ce95d3
--- /dev/null
+++ b/regression/smv/define/define9.desc
@@ -0,0 +1,8 @@
+CORE
+define9.smv
+
+^file .* line 4: identifier x already used as a parameter$
+^EXIT=2$
+^SIGNAL=0$
+--
+--
diff --git a/regression/smv/define/define9.smv b/regression/smv/define/define9.smv
new file mode 100644
index 000000000..763e54aad
--- /dev/null
+++ b/regression/smv/define/define9.smv
@@ -0,0 +1,10 @@
+MODULE some-module(x)
+
+-- x is already declared as a parameter
+DEFINE x := 123;
+
+INIT x = 123
+
+MODULE main
+
+VAR instance : some-module(124);
diff --git a/regression/smv/var/already_declared4.desc b/regression/smv/var/already_declared4.desc
index 9df5fac5c..e9831d8be 100644
--- a/regression/smv/var/already_declared4.desc
+++ b/regression/smv/var/already_declared4.desc
@@ -1,8 +1,7 @@
-KNOWNBUG
+CORE
 already_declared4.smv
 
 ^EXIT=2$
 ^SIGNAL=0$
 --
 --
-This should be errored.
diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp
index 91a68783c..aeec7fa0b 100644
--- a/src/smvlang/smv_typecheck.cpp
+++ b/src/smvlang/smv_typecheck.cpp
@@ -60,7 +60,9 @@ class smv_typecheckt:public typecheckt
   } modet;
 
   void convert(smv_parse_treet::modulet &);
-  void create_var_symbols(const smv_parse_treet::modulet::item_listt &);
+  void create_var_symbols(
+    const smv_parse_treet::modulet::item_listt &,
+    const std::list<irep_idt> &module_parameters);
 
   void collect_define(const equal_exprt &);
   void convert_defines(exprt::operandst &invar);
@@ -2133,13 +2135,20 @@ Function: smv_typecheckt::create_var_symbols
 \*******************************************************************/
 
 void smv_typecheckt::create_var_symbols(
-  const smv_parse_treet::modulet::item_listt &items)
+  const smv_parse_treet::modulet::item_listt &items,
+  const std::list<irep_idt> &module_parameters)
 {
   const irep_idt mode = "SMV";
 
   // to catch variables that have the same name as enums
   std::unordered_set<irep_idt, irep_id_hash> enums;
 
+  // to catch re-use of parameter identifiers
+  std::unordered_set<irep_idt, irep_id_hash> parameters;
+
+  for(const auto &parameter : module_parameters)
+    parameters.insert(parameter);
+
   for(const auto &item : items)
   {
     if(item.is_var() || item.is_ivar())
@@ -2154,6 +2163,13 @@ void smv_typecheckt::create_var_symbols(
           << "identifier " << base_name << " already used as enum";
       }
 
+      // already used as a parameter?
+      if(parameters.find(base_name) != parameters.end())
+      {
+        throw errort{}.with_location(item.expr.source_location())
+          << "identifier " << base_name << " already used as a parameter";
+      }
+
       auto symbol_ptr = symbol_table.lookup(identifier);
       if(symbol_ptr != nullptr)
       {
@@ -2202,6 +2218,13 @@ void smv_typecheckt::create_var_symbols(
           << "identifier " << base_name << " already used as enum";
       }
 
+      // already used as a parameter?
+      if(parameters.find(base_name) != parameters.end())
+      {
+        throw errort{}.with_location(identifier_expr.source_location())
+          << "identifier " << base_name << " already used as a parameter";
+      }
+
       auto symbol_ptr = symbol_table.lookup(identifier);
       if(symbol_ptr != nullptr)
       {
@@ -2236,6 +2259,13 @@ void smv_typecheckt::create_var_symbols(
       irep_idt base_name = to_smv_identifier_expr(item.expr).identifier();
       irep_idt identifier = module + "::var::" + id2string(base_name);
 
+      // already used as a parameter?
+      if(parameters.find(base_name) != parameters.end())
+      {
+        throw errort{}.with_location(item.expr.source_location())
+          << "identifier " << base_name << " already used as a parameter";
+      }
+
       auto symbol_ptr = symbol_table.lookup(identifier);
       if(symbol_ptr != nullptr)
       {
@@ -2390,7 +2420,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
   define_map.clear();
 
   // variables/defines first, can be used before their declaration
-  create_var_symbols(smv_module.items);
+  create_var_symbols(smv_module.items, smv_module.parameters);
 
   // transition relation