Verilog: elaboration per compilation unit

IEEE 1800 2017 3.12.1 requires compliant tools to compile "compilation
units" separately, with a compilation unit scope.

This breaks out a function that elaborates a compilation unit by itself.

Author: kroening

src/verilog/Makefile

@@ -6,6 +6,7 @@ SRC = aval_bval_encoding.cpp \
       verilog_bits.cpp \
       verilog_ebmc_language.cpp \
       verilog_elaborate.cpp \
+      verilog_elaborate_compilation_unit.cpp \
       verilog_elaborate_module_instances.cpp \
       verilog_elaborate_type.cpp \
       verilog_expr.cpp \

src/verilog/verilog_ebmc_language.cpp

@@ -22,6 +22,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include <langapi/language_util.h>
 #include <trans-word-level/show_module_hierarchy.h>
 
+#include "verilog_elaborate_compilation_unit.h"
 #include "verilog_language.h"
 #include "verilog_parser.h"
 #include "verilog_preprocessor.h"
@@ -412,25 +413,16 @@ show_modules(const verilog_ebmc_languaget::parse_treest &parse_trees)
   return result;
 }
 
-void verilog_ebmc_languaget::copy_parse_tree(
-  const parse_treet &parse_tree,
-  symbol_tablet &dest)
+symbol_tablet verilog_ebmc_languaget::elaborate_compilation_units(
+  const parse_treest &parse_trees)
 {
-  for(auto &item : parse_tree.items)
-  {
-    if(item.id() == ID_verilog_module || item.id() == ID_verilog_checker)
-    {
-      auto identifier =
-        verilog_module_symbol(to_verilog_module_source(item).base_name());
-      copy_module_source(item, identifier, dest);
-    }
-    else if(item.id() == ID_verilog_package)
-    {
-      auto identifier =
-        verilog_package_identifier(to_verilog_module_source(item).base_name());
-      copy_module_source(item, identifier, dest);
-    }
-  }
+  symbol_tablet symbol_table;
+
+  for(auto &parse_tree : parse_trees)
+    verilog_elaborate_compilation_unit(
+      parse_tree, symbol_table, message_handler);
+
+  return symbol_table;
 }
 
 std::optional<transition_systemt> verilog_ebmc_languaget::transition_system()
@@ -481,10 +473,7 @@ std::optional<transition_systemt> verilog_ebmc_languaget::transition_system()
   //
   // copy the parse trees into the symbol table
   //
-  symbol_tablet symbol_table;
-
-  for(auto &parse_tree : parse_trees)
-    copy_parse_tree(parse_tree, symbol_table);
+  symbol_tablet symbol_table = elaborate_compilation_units(parse_trees);
 
   //
   // type checking

src/verilog/verilog_ebmc_language.h

@@ -67,6 +67,7 @@ class verilog_ebmc_languaget : public ebmc_languaget
 
   std::map<irep_idt, modulet> module_map;
 
+  symbol_tablet elaborate_compilation_units(const parse_treest &);
   transition_systemt typecheck(const parse_treest &, symbol_tablet &&);
   void typecheck_module(modulet &, symbol_tablet &);
 };

src/verilog/verilog_elaborate_compilation_unit.cpp

@@ -0,0 +1,33 @@
+/*******************************************************************\
+
+Module: Elaboration of Verilog Compilation Units
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#include "verilog_elaborate_compilation_unit.h"
+
+#include "verilog_typecheck.h"
+
+void verilog_elaborate_compilation_unit(
+  const verilog_parse_treet &parse_tree,
+  symbol_table_baset &symbol_table,
+  message_handlert &message_handler)
+{
+  for(auto &item : parse_tree.items)
+  {
+    if(item.id() == ID_verilog_module || item.id() == ID_verilog_checker)
+    {
+      auto identifier =
+        verilog_module_symbol(to_verilog_module_source(item).base_name());
+      copy_module_source(item, identifier, symbol_table);
+    }
+    else if(item.id() == ID_verilog_package)
+    {
+      auto identifier =
+        verilog_package_identifier(to_verilog_module_source(item).base_name());
+      copy_module_source(item, identifier, symbol_table);
+    }
+  }
+}

src/verilog/verilog_elaborate_compilation_unit.h

@@ -0,0 +1,23 @@
+/*******************************************************************\
+
+Module: Elaboration of Verilog Compilation Units
+
+Author: Daniel Kroening, dkr@amazon.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_VERILOG_ELABORATE_COMPILATION_UNIT_H
+#define CPROVER_VERILOG_ELABORATE_COMPILATION_UNIT_H
+
+#include <util/message.h>
+#include <util/symbol_table_base.h>
+
+#include "verilog_parse_tree.h"
+
+/// throws ebmc_errort on failure
+void verilog_elaborate_compilation_unit(
+  const verilog_parse_treet &,
+  symbol_table_baset &,
+  message_handlert &);
+
+#endif // CPROVER_VERILOG_ELABORATE_UNIT_H