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.

Author: kroening

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> 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(item.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