Skip to content

Commit d0651a3

Browse files
tautschnigtautschnig
authored
Merge pull request #1483 from diffblue/smv-complex-identifier
SMV: do not merge identifiers in the parser
2 parents 67f679a + 7985a4b commit d0651a3

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:
@@ -2038,69 +2076,69 @@ void smv_typecheckt::variable_checks(const smv_parse_treet::modulet &module)
20382076
{
20392077
if(element.is_var() || element.is_ivar())
20402078
{
2041-
const auto &identifier_expr = to_smv_identifier_expr(element.expr);
2042-
irep_idt base_name = identifier_expr.identifier();
2079+
irep_idt base_name = merge_complex_identifier(element.expr);
2080+
auto location = element.expr.source_location();
20432081

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

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

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

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

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

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

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

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

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

@@ -2158,13 +2196,14 @@ void smv_typecheckt::create_var_symbols(
21582196
{
21592197
if(element.is_var() || element.is_ivar())
21602198
{
2161-
irep_idt base_name = to_smv_identifier_expr(element.expr).identifier();
2199+
irep_idt base_name = merge_complex_identifier(element.expr);
2200+
auto location = element.expr.source_location();
21622201
irep_idt identifier = module + "::var::" + id2string(base_name);
21632202

21642203
auto symbol_ptr = symbol_table.lookup(identifier);
21652204
if(symbol_ptr != nullptr)
21662205
{
2167-
throw errort{}.with_location(element.expr.source_location())
2206+
throw errort{}.with_location(location)
21682207
<< "variable " << base_name << " already declared, at "
21692208
<< symbol_ptr->location;
21702209
}
@@ -2191,20 +2230,20 @@ void smv_typecheckt::create_var_symbols(
21912230

21922231
symbol.is_state_var = false;
21932232
symbol.value = nil_exprt{};
2194-
symbol.location = element.expr.source_location();
2233+
symbol.location = location;
21952234

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

22042243
auto symbol_ptr = symbol_table.lookup(identifier);
22052244
if(symbol_ptr != nullptr)
22062245
{
2207-
throw errort{}.with_location(identifier_expr.source_location())
2246+
throw errort{}.with_location(location)
22082247
<< "variable `" << base_name << "' already declared, at "
22092248
<< symbol_ptr->location;
22102249
}
@@ -2226,7 +2265,7 @@ void smv_typecheckt::create_var_symbols(
22262265
symbol.value = nil_exprt{};
22272266
symbol.is_input = true;
22282267
symbol.is_state_var = false;
2229-
symbol.location = identifier_expr.source_location();
2268+
symbol.location = location;
22302269

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

0 commit comments

Comments
 (0)