SMV: submodule type

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

Author: kroening

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

@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #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()));
@@ -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