Skip to content

Commit c4567f1

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 c4567f1

File tree

2 files changed

+60
-60
lines changed

2 files changed

+60
-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: 60 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,70 @@ 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 =
2116+
merge_complex_identifier(element.lhs());
2117+
auto location = to_equal_expr(element.expr).lhs().source_location();
20792118

20802119
// already used as enum?
20812120
if(enums.find(base_name) != enums.end())
20822121
{
2083-
throw errort{}.with_location(identifier_expr.source_location())
2122+
throw errort{}.with_location(location)
20842123
<< "identifier " << base_name << " already used as enum";
20852124
}
20862125

20872126
// already used as a parameter?
20882127
if(parameters.find(base_name) != parameters.end())
20892128
{
2090-
throw errort{}.with_location(identifier_expr.source_location())
2129+
throw errort{}.with_location(location)
20912130
<< "identifier " << base_name << " already used as a parameter";
20922131
}
20932132

20942133
// already used as variable?
20952134
if(vars.find(base_name) != vars.end())
20962135
{
2097-
throw errort{}.with_location(identifier_expr.source_location())
2136+
throw errort{}.with_location(location)
20982137
<< "identifier " << base_name << " already used as variable";
20992138
}
21002139

21012140
// already used as define?
21022141
if(defines.find(base_name) != defines.end())
21032142
{
2104-
throw errort{}.with_location(identifier_expr.source_location())
2143+
throw errort{}.with_location(location)
21052144
<< "identifier " << base_name << " already used as define";
21062145
}
21072146

@@ -2159,13 +2198,14 @@ void smv_typecheckt::create_var_symbols(
21592198
{
21602199
if(element.is_var() || element.is_ivar())
21612200
{
2162-
irep_idt base_name = to_smv_identifier_expr(element.expr).identifier();
2201+
irep_idt base_name = merge_complex_identifier(element.expr);
2202+
auto location = element.expr.source_location();
21632203
irep_idt identifier = module + "::var::" + id2string(base_name);
21642204

21652205
auto symbol_ptr = symbol_table.lookup(identifier);
21662206
if(symbol_ptr != nullptr)
21672207
{
2168-
throw errort{}.with_location(element.expr.source_location())
2208+
throw errort{}.with_location(location)
21692209
<< "variable " << base_name << " already declared, at "
21702210
<< symbol_ptr->location;
21712211
}
@@ -2192,20 +2232,21 @@ void smv_typecheckt::create_var_symbols(
21922232

21932233
symbol.is_state_var = false;
21942234
symbol.value = nil_exprt{};
2195-
symbol.location = element.expr.source_location();
2235+
symbol.location = location;
21962236

21972237
symbol_table.insert(std::move(symbol));
21982238
}
21992239
else if(element.is_define())
22002240
{
2201-
const auto &identifier_expr = to_smv_identifier_expr(element.lhs());
2202-
irep_idt base_name = identifier_expr.identifier();
2241+
irep_idt base_name =
2242+
merge_complex_identifier(element.lhs());
2243+
auto location = to_equal_expr(element.expr).lhs().source_location();
22032244
irep_idt identifier = module + "::var::" + id2string(base_name);
22042245

22052246
auto symbol_ptr = symbol_table.lookup(identifier);
22062247
if(symbol_ptr != nullptr)
22072248
{
2208-
throw errort{}.with_location(identifier_expr.source_location())
2249+
throw errort{}.with_location(location)
22092250
<< "variable `" << base_name << "' already declared, at "
22102251
<< symbol_ptr->location;
22112252
}
@@ -2227,7 +2268,7 @@ void smv_typecheckt::create_var_symbols(
22272268
symbol.value = nil_exprt{};
22282269
symbol.is_input = true;
22292270
symbol.is_state_var = false;
2230-
symbol.location = identifier_expr.source_location();
2271+
symbol.location = location;
22312272

22322273
symbol_table.insert(std::move(symbol));
22332274
}

0 commit comments

Comments
 (0)