SMV: flatten hierarchy on parse tree

SMV module flattening is now implemented as an operation on SMV parse trees,
as opposed to an operation on a symbol table post type checking.

Author: kroening

regression/smv/modules/parameters2.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 parameters2.smv
 
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This yields a type-checking error.

regression/smv/modules/use_before_declaration1.desc

@@ -0,0 +1,7 @@
+CORE
+use_before_declaration1.smv
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/smv/modules/use_before_declaration1.smv

@@ -0,0 +1,10 @@
+MODULE main
+
+-- you can use modules before they are declared
+SPEC sub.something = 123
+
+VAR sub : my-module;
+
+MODULE my-module
+
+DEFINE something := 123;

src/smvlang/smv_parse_tree.h

@@ -29,7 +29,7 @@ class smv_parse_treet
   struct modulet
   {
     irep_idt name, base_name;
-    std::list<irep_idt> parameters;
+    std::vector<irep_idt> parameters;
 
     struct elementt
     {

src/smvlang/smv_typecheck.cpp

@@ -60,6 +60,7 @@ class smv_typecheckt:public typecheckt
   } modet;
 
   void convert(smv_parse_treet::modulet &);
+
   void create_var_symbols(const smv_parse_treet::modulet::element_listt &);
 
   void collect_define(const equal_exprt &);
@@ -104,16 +105,14 @@ class smv_typecheckt:public typecheckt
     smv_parse_treet::modulet &,
     const irep_idt &identifier,
     const irep_idt &instance,
-    const exprt::operandst &operands,
+    const exprt::operandst &arguments,
     const source_locationt &);
 
   typet
   type_union(const typet &type1, const typet &type2, const source_locationt &);
 
   typedef std::map<irep_idt, exprt> rename_mapt;
 
-  void instantiate_rename(exprt &, const rename_mapt &rename_map);
-
   void convert_ports(smv_parse_treet::modulet &, typet &dest);
 
   // for defines
@@ -196,8 +195,14 @@ Function: smv_typecheckt::flatten_hierarchy
 
 void smv_typecheckt::flatten_hierarchy(smv_parse_treet::modulet &smv_module)
 {
-  for(auto &element : smv_module.elements)
+  // Not using ranged for since we will append to the list we are
+  // iterating over! This avoids recursion.
+  for(auto element_it = smv_module.elements.begin();
+      element_it != smv_module.elements.end();
+      ++element_it)
   {
+    auto &element = *element_it;
+
     if(element.is_var() && element.expr.type().id() == ID_smv_submodule)
     {
       exprt &inst =
@@ -235,195 +240,66 @@ void smv_typecheckt::instantiate(
   smv_parse_treet::modulet &smv_module,
   const irep_idt &identifier,
   const irep_idt &instance,
-  const exprt::operandst &operands,
+  const exprt::operandst &arguments,
   const source_locationt &location)
 {
-  symbol_table_baset::symbolst::const_iterator s_it =
-    symbol_table.symbols.find(identifier);
+  // Find the module
+  auto module_it = smv_parse_tree.module_map.find(identifier);
 
-  if(s_it==symbol_table.symbols.end())
+  if(module_it == smv_parse_tree.module_map.end())
   {
     throw errort().with_location(location)
       << "submodule `" << identifier << "' not found";
   }
 
-  if(s_it->second.type.id()!=ID_module)
-  {
-    throw errort().with_location(location)
-      << "submodule `" << identifier << "' not a module";
-  }
-
-  const irept::subt &ports=s_it->second.type.find(ID_ports).get_sub();
-
-  // do the arguments/ports
+  const auto &instantiated_module = *module_it->second;
+  const auto &parameters = instantiated_module.parameters;
 
-  if(ports.size()!=operands.size())
+  // map the arguments to parameters
+  if(parameters.size() != arguments.size())
   {
     throw errort().with_location(location)
       << "submodule `" << identifier << "' has wrong number of arguments";
   }
 
-  std::set<irep_idt> port_identifiers;
-  rename_mapt rename_map;
-
-  for(std::size_t i = 0; i < ports.size(); i++)
-  {
-    const irep_idt &identifier=ports[i].get(ID_identifier);
-    rename_map.insert(std::pair<irep_idt, exprt>(identifier, operands[i]));
-    port_identifiers.insert(identifier);
-  }
-
-  // do the variables
-
-  std::string new_prefix=
-    id2string(smv_module.name)+"::var::"+id2string(instance)+".";
-
-  std::set<irep_idt> var_identifiers;
-
-  for(auto v_it=symbol_table.symbol_module_map.lower_bound(identifier);
-      v_it!=symbol_table.symbol_module_map.upper_bound(identifier);
-      v_it++)
-  {
-    symbol_table_baset::symbolst::const_iterator s_it2 =
-      symbol_table.symbols.find(v_it->second);
-
-    if(s_it2==symbol_table.symbols.end())
-    {
-      throw errort() << "symbol `" << v_it->second << "' not found";
-    }
-
-    if(port_identifiers.find(s_it2->first) != port_identifiers.end())
-    {
-    }
-    else if(s_it2->second.type.id() == ID_module)
-    {
-    }
-    else
-    {
-      symbolt symbol(s_it2->second);
-
-      symbol.name=new_prefix+id2string(symbol.base_name);
-      symbol.module=smv_module.name;
-
-      if(smv_module.name == "smv::main")
-      {
-        symbol.pretty_name =
-          id2string(instance) + '.' + id2string(symbol.base_name);
-      }
-      else
-      {
-        symbol.pretty_name = strip_smv_prefix(symbol.name);
-      }
-
-      rename_map.insert(
-          std::pair<irep_idt, exprt>(s_it2->first, symbol.symbol_expr()));
-
-      var_identifiers.insert(symbol.name);
-
-      symbol_table.add(symbol);
-    }
-  }
-
-  // fix values (macros)
-
-  for(const auto &v_id : var_identifiers)
-  {
-    auto s_it2 = symbol_table.get_writeable(v_id);
-
-    if(s_it2==nullptr)
-    {
-      throw errort() << "symbol `" << v_id << "' not found";
-    }
-
-    symbolt &symbol=*s_it2;
-
-    if(!symbol.value.is_nil())
-    {
-      instantiate_rename(symbol.value, rename_map);
-      typecheck(symbol.value, OTHER);
-      convert_expr_to(symbol.value, symbol.type);
-    }
-  }
-
-  // get the transition system
-
-  const transt &trans=to_trans_expr(s_it->second.value);
+  rename_mapt parameter_map;
 
-  std::string old_prefix=id2string(s_it->first)+"::var::";
-
-  // do the transition system
-
-  if(!trans.invar().is_true())
-  {
-    exprt tmp(trans.invar());
-    instantiate_rename(tmp, rename_map);
-    smv_module.add_invar(tmp);
-  }
-    
-  if(!trans.init().is_true())
-  {
-    exprt tmp(trans.init());
-    instantiate_rename(tmp, rename_map);
-    smv_module.add_init(tmp);
-  }
-    
-  if(!trans.trans().is_true())
+  for(std::size_t i = 0; i < parameters.size(); i++)
   {
-    exprt tmp(trans.trans());
-    instantiate_rename(tmp, rename_map);
-    smv_module.add_trans(tmp);
+    parameter_map.emplace(parameters[i], arguments[i]);
   }
 
-}
-
-/*******************************************************************\
-
-Function: smv_typecheckt::instantiate_rename
-
-  Inputs:
-
- Outputs:
-
- Purpose:
+  const std::string prefix = id2string(instance) + '.';
 
-\*******************************************************************/
-
-void smv_typecheckt::instantiate_rename(
-  exprt &expr,
-  const rename_mapt &rename_map)
-{
-  for(auto &op : expr.operands())
-    instantiate_rename(op, rename_map);
-
-  if(expr.id()==ID_symbol || expr.id()==ID_next_symbol)
+  // copy the parse tree elements
+  for(auto &src_element : instantiated_module.elements)
   {
-    const irep_idt &old_identifier=expr.get(ID_identifier);
-    bool next=expr.id()==ID_next_symbol;
-
-    rename_mapt::const_iterator it=
-      rename_map.find(old_identifier);
+    auto copy = src_element;
 
-    if(it!=rename_map.end())
-    {
-      expr=it->second;
-
-      if(next)
+    // replace the parameter identifiers,
+    // and add the prefix to non-parameter identifiers
+    copy.expr.visit_post(
+      [&parameter_map, &prefix](exprt &expr)
       {
-        if(expr.id()==ID_symbol)
-        {
-          expr=it->second;
-          expr.id(ID_next_symbol);
-        }
-        else
+        if(expr.id() == ID_smv_identifier)
         {
-          throw errort().with_location(expr.find_source_location())
-            << "expected symbol expression here, but got "
-            << to_string(it->second);
+          auto identifier = to_smv_identifier_expr(expr).identifier();
+          auto parameter_it = parameter_map.find(identifier);
+          if(parameter_it != parameter_map.end())
+          {
+            expr = parameter_it->second;
+          }
+          else
+          {
+            // add the prefix
+            to_smv_identifier_expr(expr).identifier(
+              prefix + id2string(identifier));
+          }
         }
-      }
-      else
-        expr=it->second;
-    }
+      });
+
+    // add to main parse tree
+    smv_module.elements.push_back(copy);
   }
 }
 
@@ -2497,10 +2373,10 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
 
   define_map.clear();
 
-  // check for re-use of variables/defines/parameter identifiers
-  variable_checks(smv_module);
+  // expand the module hierarchy
+  flatten_hierarchy(smv_module);
 
-  // variables/defines first, can be used before their declaration
+  // Now do variables/defines, which can be used before their declaration
   create_var_symbols(smv_module.elements);
 
   // transition relation
@@ -2524,8 +2400,6 @@ void smv_typecheckt::convert(smv_parse_treet::modulet &smv_module)
       if(!element.is_var() && !element.is_ivar())
         convert(element);
 
-    flatten_hierarchy(smv_module);
-
     // we first need to collect all the defines
 
     for(auto &element : smv_module.elements)
@@ -2631,6 +2505,13 @@ Function: smv_typecheckt::typecheck
 
 void smv_typecheckt::typecheck()
 {
+  if(module != "smv::main")
+    return;
+
+  // check all modules for duplicate identifiers
+  for(auto &module : smv_parse_tree.module_list)
+    variable_checks(module);
+
   auto it = smv_parse_tree.module_map.find(module);
 
   if(it == smv_parse_tree.module_map.end())