SMV: store module parse trees in a list

The modules in the SMV parse tree are now stored in a list in order to
preserve the original ordering as in the source file.

Author: kroening

src/smvlang/parser.y

@@ -181,7 +181,9 @@ static smv_parse_treet::modulet &new_module(YYSTYPE &module_name)
 {
   auto base_name = stack_expr(module_name).id_string();
   const std::string identifier=smv_module_symbol(base_name);
-  auto &module=PARSER.parse_tree.modules[identifier];
+  PARSER.parse_tree.module_list.push_back(smv_parse_treet::modulet{});
+  auto &module=PARSER.parse_tree.module_list.back();
+  PARSER.parse_tree.module_map[identifier] = --PARSER.parse_tree.module_list.end();
   module.name = identifier;
   module.base_name = base_name;
   PARSER.module = &module;

src/smvlang/smv_language.cpp

@@ -62,12 +62,13 @@ void smv_languaget::dependencies(
   const std::string &module, 
   std::set<std::string> &module_set)
 {
-  smv_parse_treet::modulest::const_iterator
-    m_it=smv_parse_tree.modules.find(module);
+  smv_parse_treet::module_mapt::const_iterator m_it =
+    smv_parse_tree.module_map.find(module);
 
-  if(m_it==smv_parse_tree.modules.end()) return;
+  if(m_it == smv_parse_tree.module_map.end())
+    return;
 
-  const smv_parse_treet::modulet &smv_module=m_it->second;
+  const smv_parse_treet::modulet &smv_module = *m_it->second;
 
   for(auto &element : smv_module.elements)
     if(element.is_var() && element.expr.type().id() == ID_smv_submodule)
@@ -89,10 +90,8 @@ Function: smv_languaget::modules_provided
 
 void smv_languaget::modules_provided(std::set<std::string> &module_set)
 {
-  for(smv_parse_treet::modulest::const_iterator
-      it=smv_parse_tree.modules.begin();
-      it!=smv_parse_tree.modules.end(); it++)
-    module_set.insert(id2string(it->second.name));
+  for(const auto &module : smv_parse_tree.module_list)
+    module_set.insert(id2string(module.name));
 }
 
 /*******************************************************************\

src/smvlang/smv_parse_tree.cpp

@@ -28,7 +28,8 @@ Function: smv_parse_treet::swap
 
 void smv_parse_treet::swap(smv_parse_treet &smv_parse_tree)
 {
-  smv_parse_tree.modules.swap(modules);
+  smv_parse_tree.module_list.swap(module_list);
+  smv_parse_tree.module_map.swap(module_map);
 }
 
 /*******************************************************************\
@@ -45,7 +46,8 @@ Function: smv_parse_treet::clear
 
 void smv_parse_treet::clear()
 {
-  modules.clear();
+  module_map.clear();
+  module_list.clear();
 }
 
 /*******************************************************************\
@@ -99,10 +101,8 @@ std::string to_string(smv_parse_treet::modulet::elementt::element_typet i)
 
 void smv_parse_treet::show(std::ostream &out) const
 {
-  for(auto &module_it : modules)
+  for(auto &module : module_list)
   {
-    auto &module = module_it.second;
-
     out << "Module: " << module.name << std::endl << std::endl;
 
     out << "  PARAMETERS:\n";

src/smvlang/smv_parse_tree.h

@@ -19,6 +19,11 @@ Author: Daniel Kroening, kroening@kroening.com
 class smv_parse_treet
 {
 public:
+  smv_parse_treet() = default;
+
+  // don't copy, contains pointers
+  smv_parse_treet(const smv_parse_treet &) = delete;
+
   typedef std::unordered_set<irep_idt, irep_id_hash> enum_sett;
 
   struct modulet
@@ -287,11 +292,14 @@ class smv_parse_treet
 
     enum_sett enum_set;
   };
-   
-  typedef std::unordered_map<irep_idt, modulet, irep_id_hash> modulest;
-  
-  modulest modules;
-  
+
+  using module_listt = std::list<modulet>;
+  module_listt module_list;
+
+  using module_mapt =
+    std::unordered_map<irep_idt, module_listt::iterator, irep_id_hash>;
+  module_mapt module_map;
+
   void swap(smv_parse_treet &smv_parse_tree);
   void clear();
 

src/smvlang/smv_typecheck.cpp

@@ -2552,14 +2552,14 @@ Function: smv_typecheckt::typecheck
 
 void smv_typecheckt::typecheck()
 {
-  smv_parse_treet::modulest::iterator it=smv_parse_tree.modules.find(module);
+  auto it = smv_parse_tree.module_map.find(module);
 
-  if(it==smv_parse_tree.modules.end())
+  if(it == smv_parse_tree.module_map.end())
   {
     throw errort() << "failed to find module " << module;
   }
 
-  convert(it->second);
+  convert(*it->second);
 }
 
 /*******************************************************************\