SMV: submodule type

This introduces a class to document the existing SMV submodule type.

Author: kroening

src/hw_cbmc_irep_ids.h

@@ -36,6 +36,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

@@ -1020,9 +1020,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/smv_language.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include "expr2smv.h"
 #include "smv_parser.h"
 #include "smv_typecheck.h"
+#include "smv_types.h"
 
 /*******************************************************************\
 
@@ -69,8 +70,9 @@ void smv_languaget::dependencies(
 
   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"));
+    if(it->second.type.id() == ID_smv_submodule)
+      module_set.insert(
+        id2string(to_smv_submodule_type(it->second.type).identifier()));
 }
 
 /*******************************************************************\
@@ -145,7 +147,7 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &)
 
     for(smv_parse_treet::mc_varst::const_iterator it=module.vars.begin();
         it!=module.vars.end(); it++)
-      if(it->second.type.id()!="submodule")
+      if(it->second.type.id() != ID_smv_submodule)
       {
         symbol_tablet symbol_table;
         namespacet ns{symbol_table};
@@ -160,7 +162,7 @@ void smv_languaget::show_parse(std::ostream &out, message_handlert &)
     for(smv_parse_treet::mc_varst::const_iterator
         it=module.vars.begin();
         it!=module.vars.end(); it++)
-      if(it->second.type.id()=="submodule")
+      if(it->second.type.id() == ID_smv_submodule)
       {
         symbol_tablet symbol_table;
         namespacet ns(symbol_table);

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()));
@@ -2103,7 +2103,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,35 @@ inline smv_enumeration_typet &to_smv_enumeration_type(typet &type)
   return static_cast<smv_enumeration_typet &>(type);
 }
 
+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);
+  }
+};
+
+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