Verilog: extract scope data structure from parser

This extracts the scope data structure from the parser class into a separate
file, as the scopes need to be preserved until all Verilog parsing is
finished.

Author: kroening

src/verilog/Makefile

@@ -18,6 +18,7 @@ SRC = aval_bval_encoding.cpp \
       verilog_preprocessor.cpp \
       verilog_preprocessor_lex.yy.cpp \
       verilog_preprocessor_tokenizer.cpp \
+      verilog_scope.cpp \
       verilog_simplifier.cpp \
       verilog_standard.cpp \
       verilog_symbol_table.cpp \

src/verilog/parser.y

@@ -28,8 +28,8 @@ Author: Daniel Kroening, [email protected]
 #define mts(x, y) stack_expr(x).move_to_sub((irept &)stack_expr(y))
 #define swapop(x, y) stack_expr(x).operands().swap(stack_expr(y).operands())
 #define addswap(x, y, z) stack_expr(x).add(y).swap(stack_expr(z))
-#define push_scope(x, y) PARSER.push_scope(x, y)
-#define pop_scope() PARSER.pop_scope();
+#define push_scope(x, y) PARSER.scopes.push_scope(x, y)
+#define pop_scope() PARSER.scopes.pop_scope();
 
 int yyveriloglex();
 extern char *yyverilogtext;
@@ -1442,7 +1442,7 @@ net_declaration:
 type_declaration:
 	  TOK_TYPEDEF data_type new_identifier ';'
 		{ // add to the scope as a type name
-		  auto &name = PARSER.add_name(stack_expr($3).get(ID_identifier), "");
+		  auto &name = PARSER.scopes.add_name(stack_expr($3).get(ID_identifier), "");
 		  name.is_type = true;
 
 		  init($$, ID_decl);
@@ -1535,7 +1535,7 @@ data_type:
 
 	          // We attach a dummy id to distinguish two syntactically
 	          // identical enum types.
-	          auto id = PARSER.current_scope->prefix + "enum-" + PARSER.get_next_id();
+	          auto id = PARSER.scopes.current_scope->prefix + "enum-" + PARSER.get_next_id();
 	          stack_expr($$).set(ID_identifier, id);
 	        }
 	| TOK_STRING
@@ -1569,7 +1569,7 @@ enum_name_declaration:
 	  TOK_NON_TYPE_IDENTIFIER enum_name_value_opt
 	  {
 	    init($$);
-	    auto &scope = PARSER.add_name(stack_expr($1).id(), "");
+	    auto &scope = PARSER.scopes.add_name(stack_expr($1).id(), "");
 	    stack_expr($$).set(ID_base_name, scope.base_name());
 	    stack_expr($$).set(ID_identifier, scope.identifier());
 	    stack_expr($$).add(ID_value).swap(stack_expr($2));
@@ -4416,7 +4416,7 @@ type_identifier: TOK_TYPE_IDENTIFIER
 		  init($$, ID_typedef_type);
 		  auto base_name = stack_expr($1).id();
 		  stack_expr($$).set(ID_base_name, base_name);
-		  stack_expr($$).set(ID_identifier, PARSER.current_scope->prefix+id2string(base_name));
+		  stack_expr($$).set(ID_identifier, PARSER.scopes.current_scope->prefix+id2string(base_name));
 		}
 	;
 

src/verilog/scanner.l

@@ -65,7 +65,7 @@ static void preprocessor()
   { newstack(yyveriloglval); \
     irep_idt irep_id = text; \
     stack_expr(yyveriloglval).id(irep_id); \
-    auto name = PARSER.lookup(irep_id); \
+    auto name = PARSER.scopes.lookup(irep_id); \
     return name == nullptr ? TOK_NON_TYPE_IDENTIFIER : \
            name->is_type ?   TOK_TYPE_IDENTIFIER : \
                              TOK_NON_TYPE_IDENTIFIER; \

src/verilog/verilog_parser.cpp

@@ -53,32 +53,3 @@ bool parse_verilog_file(const std::string &filename, verilog_standardt standard)
 
   return verilog_parser.parse();
 }
-
-/*******************************************************************\
-
-Function: verilog_parsert::lookup
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-const verilog_parsert::scopet *verilog_parsert::lookup(irep_idt name) const
-{
-  // we start from the current scope, and walk upwards to the root
-  auto scope = current_scope;
-  while(scope != nullptr)
-  {
-    auto name_it = scope->scope_map.find(name);
-    if(name_it == scope->scope_map.end())
-      scope = scope->parent;
-    else
-      return &name_it->second; // found it
-  }
-
-  // not found, give up
-  return nullptr;
-}

src/verilog/verilog_parser.h

@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/parser.h>
 
 #include "verilog_parse_tree.h"
+#include "verilog_scope.h"
 #include "verilog_standard.h"
 
 #include <map>
@@ -53,73 +54,9 @@ class verilog_parsert:public parsert
   }
 
   // parser scopes and identifiers
-  struct scopet
-  {
-    scopet() : parent(nullptr), prefix("Verilog::")
-    {
-    }
-
-    explicit scopet(
-      irep_idt _base_name,
-      const std::string &separator,
-      scopet *_parent)
-      : parent(_parent),
-        __base_name(_base_name),
-        prefix(id2string(_parent->prefix) + id2string(_base_name) + separator)
-    {
-    }
-
-    scopet *parent = nullptr;
-    bool is_type = false;
-    irep_idt __base_name;
-    std::string prefix;
-
-    irep_idt identifier() const
-    {
-      PRECONDITION(parent != nullptr);
-      return parent->prefix + id2string(__base_name);
-    }
-
-    const irep_idt &base_name() const
-    {
-      return __base_name;
-    }
-
-    // sub-scopes
-    using scope_mapt = std::map<irep_idt, scopet>;
-    scope_mapt scope_map;
-  };
-
-  scopet top_scope, *current_scope = &top_scope;
-
-  scopet &add_name(irep_idt _base_name, const std::string &separator)
-  {
-    auto result = current_scope->scope_map.emplace(
-      _base_name, scopet{_base_name, separator, current_scope});
-    return result.first->second;
-  }
-
-  // Create the given sub-scope of the current scope.
-  void push_scope(irep_idt _base_name, const std::string &separator)
-  {
-    current_scope = &add_name(_base_name, separator);
-  }
+  using scopet = verilog_scopet;
 
-  void pop_scope()
-  {
-    PRECONDITION(current_scope->parent != nullptr);
-    current_scope = current_scope->parent;
-  }
-
-  // Look up an identifier, starting from the current scope,
-  // going upwards until found. Returns nullptr when not found.
-  const scopet *lookup(irep_idt base_name) const;
-
-  bool is_type(irep_idt base_name) const
-  {
-    auto scope_ptr = lookup(base_name);
-    return scope_ptr == nullptr ? false : scope_ptr->is_type;
-  }
+  verilog_scopest scopes;
 
   // These are used for anonymous gate instances
   // and to create a unique identifier for enum types.

src/verilog/verilog_scope.cpp

@@ -0,0 +1,26 @@
+/*******************************************************************\
+
+Module: Verilog Scope
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "verilog_scope.h"
+
+const verilog_scopet *verilog_scopest::lookup(irep_idt name) const
+{
+  // we start from the current scope, and walk upwards to the root
+  auto scope = current_scope;
+  while(scope != nullptr)
+  {
+    auto name_it = scope->scope_map.find(name);
+    if(name_it == scope->scope_map.end())
+      scope = scope->parent;
+    else
+      return &name_it->second; // found it
+  }
+
+  // not found, give up
+  return nullptr;
+}

src/verilog/verilog_scope.h

@@ -0,0 +1,91 @@
+/*******************************************************************\
+
+Module: Verilog Scopes
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_VERILOG_SCOPE_H
+#define CPROVER_VERILOG_SCOPE_H
+
+#include <util/irep.h>
+
+#include <map>
+
+// parser scopes and identifiers
+struct verilog_scopet
+{
+  verilog_scopet() : parent(nullptr), prefix("Verilog::")
+  {
+  }
+
+  verilog_scopet(
+    irep_idt _base_name,
+    const std::string &separator,
+    verilog_scopet *_parent)
+    : parent(_parent),
+      __base_name(_base_name),
+      prefix(id2string(_parent->prefix) + id2string(_base_name) + separator)
+  {
+  }
+
+  verilog_scopet *parent = nullptr;
+  bool is_type = false;
+  irep_idt __base_name;
+  std::string prefix;
+
+  irep_idt identifier() const
+  {
+    PRECONDITION(parent != nullptr);
+    return parent->prefix + id2string(__base_name);
+  }
+
+  const irep_idt &base_name() const
+  {
+    return __base_name;
+  }
+
+  // sub-scopes
+  using scope_mapt = std::map<irep_idt, verilog_scopet>;
+  scope_mapt scope_map;
+};
+
+class verilog_scopest
+{
+public:
+  using scopet = verilog_scopet;
+
+  scopet top_scope, *current_scope = &top_scope;
+
+  scopet &add_name(irep_idt _base_name, const std::string &separator)
+  {
+    auto result = current_scope->scope_map.emplace(
+      _base_name, scopet{_base_name, separator, current_scope});
+    return result.first->second;
+  }
+
+  // Create the given sub-scope of the current scope.
+  void push_scope(irep_idt _base_name, const std::string &separator)
+  {
+    current_scope = &add_name(_base_name, separator);
+  }
+
+  void pop_scope()
+  {
+    PRECONDITION(current_scope->parent != nullptr);
+    current_scope = current_scope->parent;
+  }
+
+  // Look up an identifier, starting from the current scope,
+  // going upwards until found. Returns nullptr when not found.
+  const scopet *lookup(irep_idt base_name) const;
+
+  bool is_type(irep_idt base_name) const
+  {
+    auto scope_ptr = lookup(base_name);
+    return scope_ptr == nullptr ? false : scope_ptr->is_type;
+  }
+};
+
+#endif