SMV: extract code for duplicate identifiers

This extracts the code that checks for re-use of parameter/define/enum
identifiers into a separate method.

Author: kroening

src/smvlang/smv_typecheck.cpp

@@ -60,9 +60,7 @@ class smv_typecheckt:public typecheckt
   } modet;
 
   void convert(smv_parse_treet::modulet &);
-  void create_var_symbols(
-    const smv_parse_treet::modulet::element_listt &,
-    const std::list<irep_idt> &module_parameters);
+  void create_var_symbols(const smv_parse_treet::modulet::element_listt &);
 
   void collect_define(const equal_exprt &);
   void convert_defines(exprt::operandst &invar);
@@ -88,6 +86,10 @@ class smv_typecheckt:public typecheckt
   void check_type(typet &);
   smv_ranget convert_type(const typet &);
 
+  void variable_checks(
+    const smv_parse_treet::modulet::element_listt &,
+    const std::list<irep_idt> &module_parameters);
+
   void convert(smv_parse_treet::modulet::elementt &);
   void typecheck(smv_parse_treet::modulet::elementt &);
   void typecheck_expr_rec(exprt &, modet);
@@ -2126,7 +2128,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet::elementt &element)
 
 /*******************************************************************\
 
-Function: smv_typecheckt::create_var_symbols
+Function: smv_typecheckt::variable_checks
 
   Inputs:
 
@@ -2136,17 +2138,11 @@ Function: smv_typecheckt::create_var_symbols
 
 \*******************************************************************/
 
-void smv_typecheckt::create_var_symbols(
+void smv_typecheckt::variable_checks(
   const smv_parse_treet::modulet::element_listt &elements,
   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;
+  std::unordered_set<irep_idt, irep_id_hash> enums, defines, vars, parameters;
 
   for(const auto &parameter : module_parameters)
     parameters.insert(parameter);
@@ -2156,7 +2152,6 @@ void smv_typecheckt::create_var_symbols(
     if(element.is_var() || element.is_ivar())
     {
       irep_idt base_name = to_smv_identifier_expr(element.expr).identifier();
-      irep_idt identifier = module + "::var::" + id2string(base_name);
 
       // already used as enum?
       if(enums.find(base_name) != enums.end())
@@ -2172,6 +2167,112 @@ void smv_typecheckt::create_var_symbols(
           << "identifier " << base_name << " already used as a parameter";
       }
 
+      // already used as variable?
+      if(vars.find(base_name) != vars.end())
+      {
+        throw errort{}.with_location(element.expr.source_location())
+          << "identifier " << base_name << " already used as variable";
+      }
+
+      // already used as define?
+      if(defines.find(base_name) != defines.end())
+      {
+        throw errort{}.with_location(element.expr.source_location())
+          << "identifier " << base_name << " already used as define";
+      }
+
+      vars.insert(base_name);
+    }
+    else if(element.is_define())
+    {
+      const auto &identifier_expr =
+        to_smv_identifier_expr(to_equal_expr(element.expr).lhs());
+      irep_idt base_name = identifier_expr.identifier();
+
+      // already used as enum?
+      if(enums.find(base_name) != enums.end())
+      {
+        throw errort{}.with_location(identifier_expr.source_location())
+          << "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";
+      }
+
+      // already used as variable?
+      if(vars.find(base_name) != vars.end())
+      {
+        throw errort{}.with_location(element.expr.source_location())
+          << "identifier " << base_name << " already used as variable";
+      }
+
+      // already used as define?
+      if(defines.find(base_name) != defines.end())
+      {
+        throw errort{}.with_location(element.expr.source_location())
+          << "identifier " << base_name << " already used as define";
+      }
+
+      defines.insert(base_name);
+    }
+    else if(element.is_enum())
+    {
+      irep_idt base_name = to_smv_identifier_expr(element.expr).identifier();
+
+      // already used as a parameter?
+      if(parameters.find(base_name) != parameters.end())
+      {
+        throw errort{}.with_location(element.expr.source_location())
+          << "identifier " << base_name << " already used as a parameter";
+      }
+
+      // already used as variable?
+      if(vars.find(base_name) != vars.end())
+      {
+        throw errort{}.with_location(element.expr.source_location())
+          << "identifier " << base_name << " already used as variable";
+      }
+
+      // already used as define?
+      if(defines.find(base_name) != defines.end())
+      {
+        throw errort{}.with_location(element.expr.source_location())
+          << "identifier " << base_name << " already used as define";
+      }
+
+      enums.insert(base_name);
+    }
+  }
+}
+
+/*******************************************************************\
+
+Function: smv_typecheckt::create_var_symbols
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void smv_typecheckt::create_var_symbols(
+  const smv_parse_treet::modulet::element_listt &elements)
+{
+  const irep_idt mode = "SMV";
+
+  for(const auto &element : elements)
+  {
+    if(element.is_var() || element.is_ivar())
+    {
+      irep_idt base_name = to_smv_identifier_expr(element.expr).identifier();
+      irep_idt identifier = module + "::var::" + id2string(base_name);
+
       auto symbol_ptr = symbol_table.lookup(identifier);
       if(symbol_ptr != nullptr)
       {
@@ -2213,20 +2314,6 @@ void smv_typecheckt::create_var_symbols(
       irep_idt base_name = identifier_expr.identifier();
       irep_idt identifier = module + "::var::" + id2string(base_name);
 
-      // already used as enum?
-      if(enums.find(base_name) != enums.end())
-      {
-        throw errort{}.with_location(identifier_expr.source_location())
-          << "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)
       {
@@ -2261,22 +2348,13 @@ void smv_typecheckt::create_var_symbols(
       irep_idt base_name = to_smv_identifier_expr(element.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(element.expr.source_location())
-          << "identifier " << base_name << " already used as a parameter";
-      }
-
       auto symbol_ptr = symbol_table.lookup(identifier);
       if(symbol_ptr != nullptr)
       {
         throw errort{}.with_location(element.expr.source_location())
           << "enum " << base_name << " already declared, at "
           << symbol_ptr->location;
       }
-
-      enums.insert(base_name);
     }
   }
 }
@@ -2421,8 +2499,11 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
 
   define_map.clear();
 
+  // check for re-use of variables/defines/parameter identifiers
+  variable_checks(smv_module.elements, smv_module.parameters);
+
   // variables/defines first, can be used before their declaration
-  create_var_symbols(smv_module.elements, smv_module.parameters);
+  create_var_symbols(smv_module.elements);
 
   // transition relation