Skip to content

Commit 2ccff6c

Browse files
tautschnigtautschnig
authored
Merge pull request #948 from diffblue/verilog_scope
Verilog: extract scope data structure from parser
2 parents c95629f + 9b9a149 commit 2ccff6c

File tree

7 files changed

+128
-102
lines changed

7 files changed

+128
-102
lines changed

‎src/verilog/Makefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ SRC = aval_bval_encoding.cpp \
1818
verilog_preprocessor.cpp \
1919
verilog_preprocessor_lex.yy.cpp \
2020
verilog_preprocessor_tokenizer.cpp \
21+
verilog_scope.cpp \
2122
verilog_simplifier.cpp \
2223
verilog_standard.cpp \
2324
verilog_symbol_table.cpp \

‎src/verilog/parser.y‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -28,8 +28,8 @@ Author: Daniel Kroening, kroening@cs.cmu.edu
2828
#define mts(x, y) stack_expr(x).move_to_sub((irept &)stack_expr(y))
2929
#define swapop(x, y) stack_expr(x).operands().swap(stack_expr(y).operands())
3030
#define addswap(x, y, z) stack_expr(x).add(y).swap(stack_expr(z))
31-
#define push_scope(x, y) PARSER.push_scope(x, y)
32-
#define pop_scope() PARSER.pop_scope();
31+
#define push_scope(x, y) PARSER.scopes.push_scope(x, y)
32+
#define pop_scope() PARSER.scopes.pop_scope();
3333

3434
int yyveriloglex();
3535
extern char *yyverilogtext;
@@ -1442,7 +1442,7 @@ net_declaration:
14421442
type_declaration:
14431443
TOK_TYPEDEF data_type new_identifier ';'
14441444
{ // add to the scope as a type name
1445-
auto &name = PARSER.add_name(stack_expr($3).get(ID_identifier), "");
1445+
auto &name = PARSER.scopes.add_name(stack_expr($3).get(ID_identifier), "");
14461446
name.is_type = true;
14471447

14481448
init($$, ID_decl);
@@ -1535,7 +1535,7 @@ data_type:
15351535

15361536
// We attach a dummy id to distinguish two syntactically
15371537
// identical enum types.
1538-
auto id = PARSER.current_scope->prefix + "enum-" + PARSER.get_next_id();
1538+
auto id = PARSER.scopes.current_scope->prefix + "enum-" + PARSER.get_next_id();
15391539
stack_expr($$).set(ID_identifier, id);
15401540
}
15411541
| TOK_STRING
@@ -1569,7 +1569,7 @@ enum_name_declaration:
15691569
TOK_NON_TYPE_IDENTIFIER enum_name_value_opt
15701570
{
15711571
init($$);
1572-
auto &scope = PARSER.add_name(stack_expr($1).id(), "");
1572+
auto &scope = PARSER.scopes.add_name(stack_expr($1).id(), "");
15731573
stack_expr($$).set(ID_base_name, scope.base_name());
15741574
stack_expr($$).set(ID_identifier, scope.identifier());
15751575
stack_expr($$).add(ID_value).swap(stack_expr($2));
@@ -4426,7 +4426,7 @@ type_identifier: TOK_TYPE_IDENTIFIER
44264426
init($$, ID_typedef_type);
44274427
auto base_name = stack_expr($1).id();
44284428
stack_expr($$).set(ID_base_name, base_name);
4429-
stack_expr($$).set(ID_identifier, PARSER.current_scope->prefix+id2string(base_name));
4429+
stack_expr($$).set(ID_identifier, PARSER.scopes.current_scope->prefix+id2string(base_name));
44304430
}
44314431
;
44324432

‎src/verilog/scanner.l‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -65,7 +65,7 @@ static void preprocessor()
6565
{ newstack(yyveriloglval); \
6666
irep_idt irep_id = text; \
6767
stack_expr(yyveriloglval).id(irep_id); \
68-
auto name = PARSER.lookup(irep_id); \
68+
auto name = PARSER.scopes.lookup(irep_id); \
6969
return name == nullptr ? TOK_NON_TYPE_IDENTIFIER : \
7070
name->is_type ? TOK_TYPE_IDENTIFIER : \
7171
TOK_NON_TYPE_IDENTIFIER; \

‎src/verilog/verilog_parser.cpp‎

Lines changed: 0 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -53,32 +53,3 @@ bool parse_verilog_file(const std::string &filename, verilog_standardt standard)
5353

5454
return verilog_parser.parse();
5555
}
56-
57-
/*******************************************************************\
58-
59-
Function: verilog_parsert::lookup
60-
61-
Inputs:
62-
63-
Outputs:
64-
65-
Purpose:
66-
67-
\*******************************************************************/
68-
69-
const verilog_parsert::scopet *verilog_parsert::lookup(irep_idt name) const
70-
{
71-
// we start from the current scope, and walk upwards to the root
72-
auto scope = current_scope;
73-
while(scope != nullptr)
74-
{
75-
auto name_it = scope->scope_map.find(name);
76-
if(name_it == scope->scope_map.end())
77-
scope = scope->parent;
78-
else
79-
return &name_it->second; // found it
80-
}
81-
82-
// not found, give up
83-
return nullptr;
84-
}

‎src/verilog/verilog_parser.h‎

Lines changed: 3 additions & 66 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
1313
#include <util/parser.h>
1414

1515
#include "verilog_parse_tree.h"
16+
#include "verilog_scope.h"
1617
#include "verilog_standard.h"
1718

1819
#include <map>
@@ -53,73 +54,9 @@ class verilog_parsert:public parsert
5354
}
5455

5556
// parser scopes and identifiers
56-
struct scopet
57-
{
58-
scopet() : parent(nullptr), prefix("Verilog::")
59-
{
60-
}
61-
62-
explicit scopet(
63-
irep_idt _base_name,
64-
const std::string &separator,
65-
scopet *_parent)
66-
: parent(_parent),
67-
__base_name(_base_name),
68-
prefix(id2string(_parent->prefix) + id2string(_base_name) + separator)
69-
{
70-
}
71-
72-
scopet *parent = nullptr;
73-
bool is_type = false;
74-
irep_idt __base_name;
75-
std::string prefix;
76-
77-
irep_idt identifier() const
78-
{
79-
PRECONDITION(parent != nullptr);
80-
return parent->prefix + id2string(__base_name);
81-
}
82-
83-
const irep_idt &base_name() const
84-
{
85-
return __base_name;
86-
}
87-
88-
// sub-scopes
89-
using scope_mapt = std::map<irep_idt, scopet>;
90-
scope_mapt scope_map;
91-
};
92-
93-
scopet top_scope, *current_scope = &top_scope;
94-
95-
scopet &add_name(irep_idt _base_name, const std::string &separator)
96-
{
97-
auto result = current_scope->scope_map.emplace(
98-
_base_name, scopet{_base_name, separator, current_scope});
99-
return result.first->second;
100-
}
101-
102-
// Create the given sub-scope of the current scope.
103-
void push_scope(irep_idt _base_name, const std::string &separator)
104-
{
105-
current_scope = &add_name(_base_name, separator);
106-
}
57+
using scopet = verilog_scopet;
10758

108-
void pop_scope()
109-
{
110-
PRECONDITION(current_scope->parent != nullptr);
111-
current_scope = current_scope->parent;
112-
}
113-
114-
// Look up an identifier, starting from the current scope,
115-
// going upwards until found. Returns nullptr when not found.
116-
const scopet *lookup(irep_idt base_name) const;
117-
118-
bool is_type(irep_idt base_name) const
119-
{
120-
auto scope_ptr = lookup(base_name);
121-
return scope_ptr == nullptr ? false : scope_ptr->is_type;
122-
}
59+
verilog_scopest scopes;
12360

12461
// These are used for anonymous gate instances
12562
// and to create a unique identifier for enum types.

‎src/verilog/verilog_scope.cpp‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
/*******************************************************************\
2+
3+
Module: Verilog Scope
4+
5+
Author: Daniel Kroening, dkr@amazon.com
6+
7+
\*******************************************************************/
8+
9+
#include "verilog_scope.h"
10+
11+
const verilog_scopet *verilog_scopest::lookup(irep_idt name) const
12+
{
13+
// we start from the current scope, and walk upwards to the root
14+
auto scope = current_scope;
15+
while(scope != nullptr)
16+
{
17+
auto name_it = scope->scope_map.find(name);
18+
if(name_it == scope->scope_map.end())
19+
scope = scope->parent;
20+
else
21+
return &name_it->second; // found it
22+
}
23+
24+
// not found, give up
25+
return nullptr;
26+
}

‎src/verilog/verilog_scope.h‎

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
/*******************************************************************\
2+
3+
Module: Verilog Scopes
4+
5+
Author: Daniel Kroening, dkr@amazon.com
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_VERILOG_SCOPE_H
10+
#define CPROVER_VERILOG_SCOPE_H
11+
12+
#include <util/irep.h>
13+
14+
#include <map>
15+
16+
// parser scopes and identifiers
17+
struct verilog_scopet
18+
{
19+
verilog_scopet() : parent(nullptr), prefix("Verilog::")
20+
{
21+
}
22+
23+
verilog_scopet(
24+
irep_idt _base_name,
25+
const std::string &separator,
26+
verilog_scopet *_parent)
27+
: parent(_parent),
28+
__base_name(_base_name),
29+
prefix(id2string(_parent->prefix) + id2string(_base_name) + separator)
30+
{
31+
}
32+
33+
verilog_scopet *parent = nullptr;
34+
bool is_type = false;
35+
irep_idt __base_name;
36+
std::string prefix;
37+
38+
irep_idt identifier() const
39+
{
40+
PRECONDITION(parent != nullptr);
41+
return parent->prefix + id2string(__base_name);
42+
}
43+
44+
const irep_idt &base_name() const
45+
{
46+
return __base_name;
47+
}
48+
49+
// sub-scopes
50+
using scope_mapt = std::map<irep_idt, verilog_scopet>;
51+
scope_mapt scope_map;
52+
};
53+
54+
class verilog_scopest
55+
{
56+
public:
57+
using scopet = verilog_scopet;
58+
59+
scopet top_scope, *current_scope = &top_scope;
60+
61+
scopet &add_name(irep_idt _base_name, const std::string &separator)
62+
{
63+
auto result = current_scope->scope_map.emplace(
64+
_base_name, scopet{_base_name, separator, current_scope});
65+
return result.first->second;
66+
}
67+
68+
// Create the given sub-scope of the current scope.
69+
void push_scope(irep_idt _base_name, const std::string &separator)
70+
{
71+
current_scope = &add_name(_base_name, separator);
72+
}
73+
74+
void pop_scope()
75+
{
76+
PRECONDITION(current_scope->parent != nullptr);
77+
current_scope = current_scope->parent;
78+
}
79+
80+
// Look up an identifier, starting from the current scope,
81+
// going upwards until found. Returns nullptr when not found.
82+
const scopet *lookup(irep_idt base_name) const;
83+
84+
bool is_type(irep_idt base_name) const
85+
{
86+
auto scope_ptr = lookup(base_name);
87+
return scope_ptr == nullptr ? false : scope_ptr->is_type;
88+
}
89+
};
90+
91+
#endif

0 commit comments

Comments
 (0)