Skip to content

Commit 7985a4b

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 2622669 commit 7985a4b

File tree

2 files changed

+58
-60
lines changed

2 files changed

+58
-60
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: 58 additions & 19 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:
@@ -2039,69 +2077,69 @@ void smv_typecheckt::variable_checks(const smv_parse_treet::modulet &module)
20392077
{
20402078
if(element.is_var() || element.is_ivar())
20412079
{
2042-
const auto &identifier_expr = to_smv_identifier_expr(element.expr);
2043-
irep_idt base_name = identifier_expr.identifier();
2080+
irep_idt base_name = merge_complex_identifier(element.expr);
2081+
auto location = element.expr.source_location();
20442082

20452083
// already used as enum?
20462084
if(enums.find(base_name) != enums.end())
20472085
{
2048-
throw errort{}.with_location(identifier_expr.source_location())
2086+
throw errort{}.with_location(location)
20492087
<< "identifier " << base_name << " already used as enum";
20502088
}
20512089

20522090
// already used as a parameter?
20532091
if(parameters.find(base_name) != parameters.end())
20542092
{
2055-
throw errort{}.with_location(identifier_expr.source_location())
2093+
throw errort{}.with_location(location)
20562094
<< "identifier " << base_name << " already used as a parameter";
20572095
}
20582096

20592097
// already used as variable?
20602098
if(vars.find(base_name) != vars.end())
20612099
{
2062-
throw errort{}.with_location(identifier_expr.source_location())
2100+
throw errort{}.with_location(location)
20632101
<< "identifier " << base_name << " already used as variable";
20642102
}
20652103

20662104
// already used as define?
20672105
if(defines.find(base_name) != defines.end())
20682106
{
2069-
throw errort{}.with_location(identifier_expr.source_location())
2107+
throw errort{}.with_location(location)
20702108
<< "identifier " << base_name << " already used as define";
20712109
}
20722110

20732111
vars.insert(base_name);
20742112
}
20752113
else if(element.is_define())
20762114
{
2077-
const auto &identifier_expr = to_smv_identifier_expr(element.lhs());
2078-
irep_idt base_name = identifier_expr.identifier();
2115+
irep_idt base_name = merge_complex_identifier(element.lhs());
2116+
auto location = to_equal_expr(element.expr).lhs().source_location();
20792117

20802118
// already used as enum?
20812119
if(enums.find(base_name) != enums.end())
20822120
{
2083-
throw errort{}.with_location(identifier_expr.source_location())
2121+
throw errort{}.with_location(location)
20842122
<< "identifier " << base_name << " already used as enum";
20852123
}
20862124

20872125
// already used as a parameter?
20882126
if(parameters.find(base_name) != parameters.end())
20892127
{
2090-
throw errort{}.with_location(identifier_expr.source_location())
2128+
throw errort{}.with_location(location)
20912129
<< "identifier " << base_name << " already used as a parameter";
20922130
}
20932131

20942132
// already used as variable?
20952133
if(vars.find(base_name) != vars.end())
20962134
{
2097-
throw errort{}.with_location(identifier_expr.source_location())
2135+
throw errort{}.with_location(location)
20982136
<< "identifier " << base_name << " already used as variable";
20992137
}
21002138

21012139
// already used as define?
21022140
if(defines.find(base_name) != defines.end())
21032141
{
2104-
throw errort{}.with_location(identifier_expr.source_location())
2142+
throw errort{}.with_location(location)
21052143
<< "identifier " << base_name << " already used as define";
21062144
}
21072145

@@ -2159,13 +2197,14 @@ void smv_typecheckt::create_var_symbols(
21592197
{
21602198
if(element.is_var() || element.is_ivar())
21612199
{
2162-
irep_idt base_name = to_smv_identifier_expr(element.expr).identifier();
2200+
irep_idt base_name = merge_complex_identifier(element.expr);
2201+
auto location = element.expr.source_location();
21632202
irep_idt identifier = module + "::var::" + id2string(base_name);
21642203

21652204
auto symbol_ptr = symbol_table.lookup(identifier);
21662205
if(symbol_ptr != nullptr)
21672206
{
2168-
throw errort{}.with_location(element.expr.source_location())
2207+
throw errort{}.with_location(location)
21692208
<< "variable " << base_name << " already declared, at "
21702209
<< symbol_ptr->location;
21712210
}
@@ -2192,20 +2231,20 @@ void smv_typecheckt::create_var_symbols(
21922231

21932232
symbol.is_state_var = false;
21942233
symbol.value = nil_exprt{};
2195-
symbol.location = element.expr.source_location();
2234+
symbol.location = location;
21962235

21972236
symbol_table.insert(std::move(symbol));
21982237
}
21992238
else if(element.is_define())
22002239
{
2201-
const auto &identifier_expr = to_smv_identifier_expr(element.lhs());
2202-
irep_idt base_name = identifier_expr.identifier();
2240+
irep_idt base_name = merge_complex_identifier(element.lhs());
2241+
auto location = to_equal_expr(element.expr).lhs().source_location();
22032242
irep_idt identifier = module + "::var::" + id2string(base_name);
22042243

22052244
auto symbol_ptr = symbol_table.lookup(identifier);
22062245
if(symbol_ptr != nullptr)
22072246
{
2208-
throw errort{}.with_location(identifier_expr.source_location())
2247+
throw errort{}.with_location(location)
22092248
<< "variable `" << base_name << "' already declared, at "
22102249
<< symbol_ptr->location;
22112250
}
@@ -2227,7 +2266,7 @@ void smv_typecheckt::create_var_symbols(
22272266
symbol.value = nil_exprt{};
22282267
symbol.is_input = true;
22292268
symbol.is_state_var = false;
2230-
symbol.location = identifier_expr.source_location();
2269+
symbol.location = location;
22312270

22322271
symbol_table.insert(std::move(symbol));
22332272
}

0 commit comments

Comments
 (0)