SMV: move check for duplicate declarations to type checker

This moves the check for duplicate declarations and definitions from the SMV
parser to the type checker.

Author: kroening

regression/smv/define/define2.desc

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

regression/smv/define/define4.desc

@@ -2,7 +2,7 @@ CORE
 define4.smv
 
 ^file .* line 6: variable `x' already defined.*$
-^EXIT=1$
+^EXIT=2$
 ^SIGNAL=0$
 --
 --

src/smvlang/parser.y

@@ -691,27 +691,7 @@ var_decl   : variable_identifier ':' type_specifier ';'
            {
              const irep_idt &identifier=stack_expr($1).get(ID_identifier);
              smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
-
-             switch(var.var_class)
-             {
-             case smv_parse_treet::mc_vart::UNKNOWN:
-               var.type=stack_type($3);
-               var.var_class=smv_parse_treet::mc_vart::DECLARED;
-               break;
-
-             case smv_parse_treet::mc_vart::DEFINED:
-             case smv_parse_treet::mc_vart::DECLARED:
-               break;
-
-             case smv_parse_treet::mc_vart::ARGUMENT:
-               yyerror("variable `"+id2string(identifier)+"' already declared as argument");
-               YYERROR;
-               break;
-
-             default:
-               DATA_INVARIANT(false, "unexpected variable class");
-             }
-
+             (void)var;
              PARSER.module->add_var(stack_expr($1), stack_type($3));
            }
            ;
@@ -735,32 +715,7 @@ assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';'
            {
              const irep_idt &identifier=stack_expr($1).get(ID_identifier);
              smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
-
-             switch(var.var_class)
-             {
-             case smv_parse_treet::mc_vart::UNKNOWN:
-               var.type.make_nil();
-               var.var_class=smv_parse_treet::mc_vart::DEFINED;
-               break;
-
-             case smv_parse_treet::mc_vart::DECLARED:
-               var.var_class=smv_parse_treet::mc_vart::DEFINED;
-               break;
-
-             case smv_parse_treet::mc_vart::DEFINED:
-               yyerror("variable `"+id2string(identifier)+"' already defined");
-               YYERROR;
-               break;
-             
-             case smv_parse_treet::mc_vart::ARGUMENT:
-               yyerror("variable `"+id2string(identifier)+"' already declared as argument");
-               YYERROR;
-               break;
-             
-             default:
-               DATA_INVARIANT(false, "unexpected variable class");
-             }
-
+             (void)var;
              PARSER.module->add_assign_current(std::move(stack_expr($1)), std::move(stack_expr($3)));
            }
            ;
@@ -781,33 +736,7 @@ define     : assignment_var BECOMES_Token formula ';'
            {
              const irep_idt &identifier=stack_expr($1).get(ID_identifier);
              smv_parse_treet::mc_vart &var=PARSER.module->vars[identifier];
-
-             switch(var.var_class)
-             {
-             case smv_parse_treet::mc_vart::UNKNOWN:
-               var.type.make_nil();
-               var.var_class=smv_parse_treet::mc_vart::DEFINED;
-               break;
-
-             case smv_parse_treet::mc_vart::DECLARED:
-               yyerror("variable `"+id2string(identifier)+"' already declared");
-               YYERROR;
-               break;
-
-             case smv_parse_treet::mc_vart::DEFINED:
-               yyerror("variable `"+id2string(identifier)+"' already defined");
-               YYERROR;
-               break;
-
-             case smv_parse_treet::mc_vart::ARGUMENT:
-               yyerror("variable `"+id2string(identifier)+"' already declared as argument");
-               YYERROR;
-               break;
-
-             default:
-               DATA_INVARIANT(false, "unexpected variable class");
-             }
-
+             (void)var;
              PARSER.module->add_define(std::move(stack_expr($1)), std::move(stack_expr($3)));
            }
            ;

src/smvlang/smv_typecheck.cpp

@@ -2120,6 +2120,15 @@ void smv_typecheckt::create_var_symbols(
         to_smv_identifier_expr(to_equal_expr(item.expr).lhs());
       irep_idt base_name = identifier_expr.identifier();
       irep_idt identifier = module + "::var::" + id2string(base_name);
+
+      auto symbol_ptr = symbol_table.lookup(identifier);
+      if(symbol_ptr != nullptr)
+      {
+        throw errort{}.with_location(identifier_expr.source_location())
+          << "variable `" << base_name << "' already declared, at "
+          << symbol_ptr->location;
+      }
+
       typet type;
       type.make_nil();
 
@@ -2200,7 +2209,7 @@ void smv_typecheckt::collect_define(const equal_exprt &expr)
   if(!result.second)
   {
     throw errort().with_location(expr.find_source_location())
-      << "symbol `" << identifier << "' defined twice";
+      << "variable `" << symbol.display_name() << "' already defined";
   }  
 }