Merge pull request #1434 from diffblue/smv-identifier-checks

SMV: extract code for duplicate identifiers

Author: tautschnig

regression/smv/define/define2.desc

@@ -1,7 +1,7 @@
 CORE
 define2.smv
 
-^file .* line 6: variable `x' already declared.*$
+^file .* line 6: identifier x already used as variable$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/smv/define/define3.desc

@@ -1,7 +1,7 @@
 CORE
 define3.smv
 
-^file .* line 6: variable x already declared, at file .* line 3$
+^file .* line 6: identifier x already used as define$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/smv/enums/name_collision1.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 name_collision1.smv
 
-^EXIT=0$
+^file .* line 6: identifier red already used as enum$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This crashes.

regression/smv/enums/name_collision2.desc

@@ -1,7 +1,7 @@
 CORE
 name_collision2.smv
 
-^file .* line 8: enum red already declared, at file .* line 3$
+^file .* line 8: identifier red already used as variable$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/smv/enums/name_collision3.desc

@@ -1,9 +1,9 @@
-KNOWNBUG
+CORE
 name_collision3.smv
 
-^EXIT=0$
+^file .* line 8: identifier red already used as enum$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This crashes.

regression/smv/var/already_declared1.desc

@@ -1,7 +1,7 @@
 CORE
 already_declared1.smv
 
-^file .* line 6: variable x already declared, at file .* line 3$
+^file .* line 6: identifier x already used as variable$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/smv/var/already_declared2.desc

@@ -1,7 +1,7 @@
 CORE
 already_declared2.smv
 
-^file .* line 6: variable x already declared, at file .* line 3$
+^file .* line 6: identifier x already used as define$
 ^EXIT=2$
 ^SIGNAL=0$
 --

regression/smv/var/already_declared3.desc

@@ -1,7 +1,7 @@
 CORE
 already_declared3.smv
 
-^file .* line 8: variable x already declared, at file .* line 5$
+^file .* line 8: identifier x already used as variable$
 ^EXIT=2$
 ^SIGNAL=0$
 --

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,8 @@ class smv_typecheckt:public typecheckt
   void check_type(typet &);
   smv_ranget convert_type(const typet &);
 
+  void variable_checks(const smv_parse_treet::modulet &);
+
   void convert(smv_parse_treet::modulet::elementt &);
   void typecheck(smv_parse_treet::modulet::elementt &);
   void typecheck_expr_rec(exprt &, modet);
@@ -2126,7 +2126,7 @@ void smv_typecheckt::convert(smv_parse_treet::modulet::elementt &element)
 
 /*******************************************************************\
 
-Function: smv_typecheckt::create_var_symbols
+Function: smv_typecheckt::variable_checks
 
   Inputs:
 
@@ -2136,42 +2136,141 @@ Function: smv_typecheckt::create_var_symbols
 
 \*******************************************************************/
 
-void smv_typecheckt::create_var_symbols(
-  const smv_parse_treet::modulet::element_listt &elements,
-  const std::list<irep_idt> &module_parameters)
+void smv_typecheckt::variable_checks(const smv_parse_treet::modulet &module)
 {
-  const irep_idt mode = "SMV";
+  std::unordered_set<irep_idt, irep_id_hash> enums, defines, vars, parameters;
 
-  // 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)
+  for(const auto &parameter : module.parameters)
     parameters.insert(parameter);
 
-  for(const auto &element : elements)
+  for(const auto &element : module.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);
+      const auto &identifier_expr = to_smv_identifier_expr(element.expr);
+      irep_idt base_name = identifier_expr.identifier();
 
       // already used as enum?
       if(enums.find(base_name) != enums.end())
       {
-        throw errort{}.with_location(element.expr.source_location())
+        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(element.expr.source_location())
+        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(identifier_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(identifier_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(identifier_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(identifier_expr.source_location())
+          << "identifier " << base_name << " already used as define";
+      }
+
+      defines.insert(base_name);
+    }
+    else if(element.is_enum())
+    {
+      const auto &identifier_expr = to_smv_identifier_expr(element.expr);
+      irep_idt base_name = identifier_expr.identifier();
+
+      // 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(identifier_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(identifier_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 +2312,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 +2346,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 +2497,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);
+
   // 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