Skip to content

Commit 9b39167

Browse files
kroeningkroening
committed
SMV: do not merge identifiers in the parser
This moves the merging of complex identifiers from the SMV parser to the type checker.
1 parent 618dd08 commit 9b39167

File tree

2 files changed

+60
-62
lines changed

2 files changed

+60
-62
lines changed

‎src/smvlang/parser.y‎

Lines changed: 0 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -132,41 +132,6 @@ static void j_binary(YYSTYPE & dest, YYSTYPE & op1, const irep_idt &id, YYSTYPE
132132

133133
/*******************************************************************\
134134
135-
Function: merge_complex_identifier
136-
137-
Inputs:
138-
139-
Outputs:
140-
141-
Purpose:
142-
143-
\*******************************************************************/
144-
145-
irep_idt merge_complex_identifier(const exprt &expr)
146-
{
147-
if(expr.id() == ID_smv_identifier)
148-
return to_smv_identifier_expr(expr).identifier();
149-
else if(expr.id() == ID_member)
150-
{
151-
auto &member_expr = to_member_expr(expr);
152-
return id2string(merge_complex_identifier(member_expr.compound())) + '.' + id2string(member_expr.get_component_name());
153-
}
154-
else if(expr.id() == ID_index)
155-
{
156-
auto &index_expr = to_index_expr(expr);
157-
auto &index = index_expr.index();
158-
PRECONDITION(index.is_constant());
159-
auto index_string = id2string(to_constant_expr(index).get_value());
160-
return id2string(merge_complex_identifier(index_expr.array())) + '.' + index_string;
161-
}
162-
else
163-
{
164-
DATA_INVARIANT_WITH_DIAGNOSTICS(false, "unexpected complex_identifier", expr.pretty());
165-
}
166-
}
167-
168-
/*******************************************************************\
169-
170135
Function: new_module
171136
172137
Inputs:
@@ -910,12 +875,6 @@ identifier : IDENTIFIER_Token
910875
;
911876

912877
variable_identifier: complex_identifier
913-
{
914-
// Could be a variable, or an enum
915-
auto id = merge_complex_identifier(stack_expr($1));
916-
init($$, ID_smv_identifier);
917-
stack_expr($$).set(ID_identifier, id);
918-
}
919878
| STRING_Token
920879
{
921880
// Not in the NuSMV grammar.

‎src/smvlang/smv_typecheck.cpp‎

Lines changed: 60 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -155,6 +155,44 @@ class smv_typecheckt:public typecheckt
155155

156156
/*******************************************************************\
157157
158+
Function: merge_complex_identifier
159+
160+
Inputs:
161+
162+
Outputs:
163+
164+
Purpose:
165+
166+
\*******************************************************************/
167+
168+
irep_idt merge_complex_identifier(const exprt &expr)
169+
{
170+
if(expr.id() == ID_smv_identifier)
171+
return to_smv_identifier_expr(expr).identifier();
172+
else if(expr.id() == ID_member)
173+
{
174+
auto &member_expr = to_member_expr(expr);
175+
return id2string(merge_complex_identifier(member_expr.compound())) + '.' +
176+
id2string(member_expr.get_component_name());
177+
}
178+
else if(expr.id() == ID_index)
179+
{
180+
auto &index_expr = to_index_expr(expr);
181+
auto &index = index_expr.index();
182+
PRECONDITION(index.is_constant());
183+
auto index_string = id2string(to_constant_expr(index).get_value());
184+
return id2string(merge_complex_identifier(index_expr.array())) + '.' +
185+
index_string;
186+
}
187+
else
188+
{
189+
DATA_INVARIANT_WITH_DIAGNOSTICS(
190+
false, "unexpected complex_identifier", expr.pretty());
191+
}
192+
}
193+
194+
/*******************************************************************\
195+
158196
Function: smv_typecheckt::convert_ports
159197
160198
Inputs:
@@ -2042,70 +2080,70 @@ void smv_typecheckt::variable_checks(const smv_parse_treet::modulet &module)
20422080
{
20432081
if(element.is_var() || element.is_ivar())
20442082
{
2045-
const auto &identifier_expr = to_smv_identifier_expr(element.expr);
2046-
irep_idt base_name = identifier_expr.identifier();
2083+
irep_idt base_name = merge_complex_identifier(element.expr);
2084+
auto location = element.expr.source_location();
20472085

20482086
// already used as enum?
20492087
if(enums.find(base_name) != enums.end())
20502088
{
2051-
throw errort{}.with_location(identifier_expr.source_location())
2089+
throw errort{}.with_location(location)
20522090
<< "identifier " << base_name << " already used as enum";
20532091
}
20542092

20552093
// already used as a parameter?
20562094
if(parameters.find(base_name) != parameters.end())
20572095
{
2058-
throw errort{}.with_location(identifier_expr.source_location())
2096+
throw errort{}.with_location(location)
20592097
<< "identifier " << base_name << " already used as a parameter";
20602098
}
20612099

20622100
// already used as variable?
20632101
if(vars.find(base_name) != vars.end())
20642102
{
2065-
throw errort{}.with_location(identifier_expr.source_location())
2103+
throw errort{}.with_location(location)
20662104
<< "identifier " << base_name << " already used as variable";
20672105
}
20682106

20692107
// already used as define?
20702108
if(defines.find(base_name) != defines.end())
20712109
{
2072-
throw errort{}.with_location(identifier_expr.source_location())
2110+
throw errort{}.with_location(location)
20732111
<< "identifier " << base_name << " already used as define";
20742112
}
20752113

20762114
vars.insert(base_name);
20772115
}
20782116
else if(element.is_define())
20792117
{
2080-
const auto &identifier_expr =
2081-
to_smv_identifier_expr(to_equal_expr(element.expr).lhs());
2082-
irep_idt base_name = identifier_expr.identifier();
2118+
irep_idt base_name =
2119+
merge_complex_identifier(to_equal_expr(element.expr).lhs());
2120+
auto location = to_equal_expr(element.expr).lhs().source_location();
20832121

20842122
// already used as enum?
20852123
if(enums.find(base_name) != enums.end())
20862124
{
2087-
throw errort{}.with_location(identifier_expr.source_location())
2125+
throw errort{}.with_location(location)
20882126
<< "identifier " << base_name << " already used as enum";
20892127
}
20902128

20912129
// already used as a parameter?
20922130
if(parameters.find(base_name) != parameters.end())
20932131
{
2094-
throw errort{}.with_location(identifier_expr.source_location())
2132+
throw errort{}.with_location(location)
20952133
<< "identifier " << base_name << " already used as a parameter";
20962134
}
20972135

20982136
// already used as variable?
20992137
if(vars.find(base_name) != vars.end())
21002138
{
2101-
throw errort{}.with_location(identifier_expr.source_location())
2139+
throw errort{}.with_location(location)
21022140
<< "identifier " << base_name << " already used as variable";
21032141
}
21042142

21052143
// already used as define?
21062144
if(defines.find(base_name) != defines.end())
21072145
{
2108-
throw errort{}.with_location(identifier_expr.source_location())
2146+
throw errort{}.with_location(location)
21092147
<< "identifier " << base_name << " already used as define";
21102148
}
21112149

@@ -2163,13 +2201,14 @@ void smv_typecheckt::create_var_symbols(
21632201
{
21642202
if(element.is_var() || element.is_ivar())
21652203
{
2166-
irep_idt base_name = to_smv_identifier_expr(element.expr).identifier();
2204+
irep_idt base_name = merge_complex_identifier(element.expr);
2205+
auto location = element.expr.source_location();
21672206
irep_idt identifier = module + "::var::" + id2string(base_name);
21682207

21692208
auto symbol_ptr = symbol_table.lookup(identifier);
21702209
if(symbol_ptr != nullptr)
21712210
{
2172-
throw errort{}.with_location(element.expr.source_location())
2211+
throw errort{}.with_location(location)
21732212
<< "variable " << base_name << " already declared, at "
21742213
<< symbol_ptr->location;
21752214
}
@@ -2196,21 +2235,21 @@ void smv_typecheckt::create_var_symbols(
21962235

21972236
symbol.is_state_var = false;
21982237
symbol.value = nil_exprt{};
2199-
symbol.location = element.expr.source_location();
2238+
symbol.location = location;
22002239

22012240
symbol_table.insert(std::move(symbol));
22022241
}
22032242
else if(element.is_define())
22042243
{
2205-
const auto &identifier_expr =
2206-
to_smv_identifier_expr(to_equal_expr(element.expr).lhs());
2207-
irep_idt base_name = identifier_expr.identifier();
2244+
irep_idt base_name =
2245+
merge_complex_identifier(to_equal_expr(element.expr).lhs());
2246+
auto location = to_equal_expr(element.expr).lhs().source_location();
22082247
irep_idt identifier = module + "::var::" + id2string(base_name);
22092248

22102249
auto symbol_ptr = symbol_table.lookup(identifier);
22112250
if(symbol_ptr != nullptr)
22122251
{
2213-
throw errort{}.with_location(identifier_expr.source_location())
2252+
throw errort{}.with_location(location)
22142253
<< "variable `" << base_name << "' already declared, at "
22152254
<< symbol_ptr->location;
22162255
}
@@ -2232,7 +2271,7 @@ void smv_typecheckt::create_var_symbols(
22322271
symbol.value = nil_exprt{};
22332272
symbol.is_input = true;
22342273
symbol.is_state_var = false;
2235-
symbol.location = identifier_expr.source_location();
2274+
symbol.location = location;
22362275

22372276
symbol_table.insert(std::move(symbol));
22382277
}

0 commit comments

Comments
 (0)