SMV: avoid vars member in SMV parse tree

src/hw_cbmc_irep_ids.h

@@ -37,6 +37,7 @@ IREP_ID_ONE(smv_setin)
 IREP_ID_ONE(smv_setnotin)
 IREP_ID_ONE(smv_signed_cast)
 IREP_ID_ONE(smv_sizeof)
+IREP_ID_ONE(smv_submodule)
 IREP_ID_ONE(smv_swconst)
 IREP_ID_ONE(smv_union)
 IREP_ID_ONE(smv_unsigned_cast)

src/smvlang/expr2smv.cpp

@@ -1058,9 +1058,9 @@ std::string type2smv(const typet &type, const namespacet &ns)
   {
     return "set";
   }
-  else if(type.id()=="submodule")
+  else if(type.id() == ID_smv_submodule)
   {
-    auto code = type.get_string(ID_identifier);
+    auto code = id2string(to_smv_submodule_type(type).identifier());
     const exprt &e=(exprt &)type;
     if(e.has_operands())
     {

src/smvlang/parser.y

@@ -5,6 +5,7 @@
 #include "smv_expr.h"
 #include "smv_parser.h"
 #include "smv_typecheck.h"
+#include "smv_types.h"
 
 #include <util/mathematical_types.h>
 #include <util/std_expr.h>
@@ -657,14 +658,14 @@ simple_type_specifier:
 module_type_specifier:
              module_name
            {
-             init($$, "submodule");
-             stack_expr($$).set(ID_identifier,
+             init($$, ID_smv_submodule);
+             to_smv_submodule_type(stack_type($$)).identifier(
                            smv_module_symbol(stack_expr($1).id_string()));
            }
            | module_name '(' parameter_list ')'
            {
-             init($$, "submodule");
-             stack_expr($$).set(ID_identifier,
+             init($$, ID_smv_submodule);
+             to_smv_submodule_type(stack_type($$)).identifier(
                            smv_module_symbol(stack_expr($1).id_string()));
              stack_expr($$).operands().swap(stack_expr($3).operands());
            }

src/smvlang/smv_language.cpp

@@ -12,8 +12,10 @@ Author: Daniel Kroening, [email protected]
 #include <util/symbol_table.h>
 
 #include "expr2smv.h"
+#include "smv_expr.h"
 #include "smv_parser.h"
 #include "smv_typecheck.h"
+#include "smv_types.h"
 
 /*******************************************************************\
 
@@ -67,10 +69,10 @@ void smv_languaget::dependencies(
 
   const smv_parse_treet::modulet &smv_module=m_it->second;
 
-  for(smv_parse_treet::mc_varst::const_iterator it=smv_module.vars.begin();
-      it!=smv_module.vars.end(); it++)
-    if(it->second.type.id()=="submodule")
-      module_set.insert(it->second.type.get_string("identifier"));
+  for(auto &item : smv_module.items)
+    if(item.is_var() && item.expr.type().id() == ID_smv_submodule)
+      module_set.insert(
+        id2string(to_smv_submodule_type(item.expr.type()).identifier()));
 }
 
 /*******************************************************************\
@@ -143,29 +145,28 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &)
 
     out << "  VARIABLES:" << std::endl;
 
-    for(smv_parse_treet::mc_varst::const_iterator it=module.vars.begin();
-        it!=module.vars.end(); it++)
-      if(it->second.type.id()!="submodule")
+    for(auto &item : module.items)
+      if(item.is_var() && item.expr.type().id() != ID_smv_submodule)
       {
         symbol_tablet symbol_table;
         namespacet ns{symbol_table};
-        auto msg = type2smv(it->second.type, ns);
-        out << "    " << it->first << ": " << msg << ";\n";
+        auto identifier = to_smv_identifier_expr(item.expr).identifier();
+        auto msg = type2smv(item.expr.type(), ns);
+        out << "    " << identifier << ": " << msg << ";\n";
       }
 
     out << std::endl;
 
     out << "  SUBMODULES:" << std::endl;
 
-    for(smv_parse_treet::mc_varst::const_iterator
-        it=module.vars.begin();
-        it!=module.vars.end(); it++)
-      if(it->second.type.id()=="submodule")
+    for(auto &item : module.items)
+      if(item.is_var() && item.expr.type().id() == ID_smv_submodule)
       {
         symbol_tablet symbol_table;
         namespacet ns(symbol_table);
-        auto msg = type2smv(it->second.type, ns);
-        out << "    " << it->first << ": " << msg << ";\n";
+        auto identifier = to_smv_identifier_expr(item.expr).identifier();
+        auto msg = type2smv(item.expr.type(), ns);
+        out << "    " << identifier << ": " << msg << ";\n";
       }
 
     out << std::endl;

src/smvlang/smv_typecheck.cpp

@@ -196,7 +196,7 @@ void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module)
 {
   for(auto &item : smv_module.items)
   {
-    if(item.is_var() && item.expr.type().id() == "submodule")
+    if(item.is_var() && item.expr.type().id() == ID_smv_submodule)
     {
       exprt &inst =
         static_cast<exprt &>(static_cast<irept &>(item.expr.type()));
@@ -2167,7 +2167,7 @@ void smv_typecheckt::create_var_symbols(
       else
         symbol.pretty_name = strip_smv_prefix(symbol.name);
 
-      if(symbol.type.id() == "submodule")
+      if(symbol.type.id() == ID_smv_submodule)
         symbol.is_input = false;
       else
         symbol.is_input = true;

src/smvlang/smv_types.h

@@ -71,4 +71,46 @@ inline smv_enumeration_typet &to_smv_enumeration_type(typet &type)
   return static_cast<smv_enumeration_typet &>(type);
 }
 
+/// The type used for VAR declarations that are in fact module instantiations
+class smv_submodule_typet : public typet
+{
+public:
+  explicit smv_submodule_typet(irep_idt _identifier) : typet{ID_smv_submodule}
+  {
+    identifier(_identifier);
+  }
+
+  irep_idt identifier() const
+  {
+    return get(ID_identifier);
+  }
+
+  void identifier(irep_idt _identifier)
+  {
+    set(ID_identifier, _identifier);
+  }
+};
+
+/*! \brief Cast a generic typet to a \ref smv_submodule_typet
+ *
+ * This is an unchecked conversion. \a type must be known to be \ref
+ * smv_submodule_typet.
+ *
+ * \param type Source type
+ * \return Object of type \ref smv_submodule_typet
+ *
+ * \ingroup gr_std_types
+*/
+inline const smv_submodule_typet &to_smv_submodule_type(const typet &type)
+{
+  PRECONDITION(type.id() == ID_smv_submodule);
+  return static_cast<const smv_submodule_typet &>(type);
+}
+
+inline smv_submodule_typet &to_smv_submodule_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_smv_submodule);
+  return static_cast<smv_submodule_typet &>(type);
+}
+
 #endif // CPROVER_SMV_TYPES_H