Skip to content

Commit 9987308

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 9987308

File tree

2 files changed

+56
-62
lines changed

2 files changed

+56
-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: 56 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -153,6 +153,42 @@ class smv_typecheckt:public typecheckt
153153
}
154154
};
155155

156+
/*******************************************************************\
157+
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())) + '.' + id2string(member_expr.get_component_name());
176+
}
177+
else if(expr.id() == ID_index)
178+
{
179+
auto &index_expr = to_index_expr(expr);
180+
auto &index = index_expr.index();
181+
PRECONDITION(index.is_constant());
182+
auto index_string = id2string(to_constant_expr(index).get_value());
183+
return id2string(merge_complex_identifier(index_expr.array())) + '.' + index_string;
184+
}
185+
else
186+
{
187+
DATA_INVARIANT_WITH_DIAGNOSTICS(false, "unexpected complex_identifier", expr.pretty());
188+
}
189+
}
190+
191+
156192
/*******************************************************************\
157193
158194
Function: smv_typecheckt::convert_ports
@@ -2042,70 +2078,69 @@ void smv_typecheckt::variable_checks(const smv_parse_treet::modulet &module)
20422078
{
20432079
if(element.is_var() || element.is_ivar())
20442080
{
2045-
const auto &identifier_expr = to_smv_identifier_expr(element.expr);
2046-
irep_idt base_name = identifier_expr.identifier();
2081+
irep_idt base_name = merge_complex_identifier(element.expr);
2082+
auto location = element.expr.source_location();
20472083

20482084
// already used as enum?
20492085
if(enums.find(base_name) != enums.end())
20502086
{
2051-
throw errort{}.with_location(identifier_expr.source_location())
2087+
throw errort{}.with_location(location)
20522088
<< "identifier " << base_name << " already used as enum";
20532089
}
20542090

20552091
// already used as a parameter?
20562092
if(parameters.find(base_name) != parameters.end())
20572093
{
2058-
throw errort{}.with_location(identifier_expr.source_location())
2094+
throw errort{}.with_location(location)
20592095
<< "identifier " << base_name << " already used as a parameter";
20602096
}
20612097

20622098
// already used as variable?
20632099
if(vars.find(base_name) != vars.end())
20642100
{
2065-
throw errort{}.with_location(identifier_expr.source_location())
2101+
throw errort{}.with_location(location)
20662102
<< "identifier " << base_name << " already used as variable";
20672103
}
20682104

20692105
// already used as define?
20702106
if(defines.find(base_name) != defines.end())
20712107
{
2072-
throw errort{}.with_location(identifier_expr.source_location())
2108+
throw errort{}.with_location(location)
20732109
<< "identifier " << base_name << " already used as define";
20742110
}
20752111

20762112
vars.insert(base_name);
20772113
}
20782114
else if(element.is_define())
20792115
{
2080-
const auto &identifier_expr =
2081-
to_smv_identifier_expr(to_equal_expr(element.expr).lhs());
2082-
irep_idt base_name = identifier_expr.identifier();
2116+
irep_idt base_name = merge_complex_identifier(to_equal_expr(element.expr).lhs());
2117+
auto location = to_equal_expr(element.expr).lhs().source_location();
20832118

20842119
// already used as enum?
20852120
if(enums.find(base_name) != enums.end())
20862121
{
2087-
throw errort{}.with_location(identifier_expr.source_location())
2122+
throw errort{}.with_location(location)
20882123
<< "identifier " << base_name << " already used as enum";
20892124
}
20902125

20912126
// already used as a parameter?
20922127
if(parameters.find(base_name) != parameters.end())
20932128
{
2094-
throw errort{}.with_location(identifier_expr.source_location())
2129+
throw errort{}.with_location(location)
20952130
<< "identifier " << base_name << " already used as a parameter";
20962131
}
20972132

20982133
// already used as variable?
20992134
if(vars.find(base_name) != vars.end())
21002135
{
2101-
throw errort{}.with_location(identifier_expr.source_location())
2136+
throw errort{}.with_location(location)
21022137
<< "identifier " << base_name << " already used as variable";
21032138
}
21042139

21052140
// already used as define?
21062141
if(defines.find(base_name) != defines.end())
21072142
{
2108-
throw errort{}.with_location(identifier_expr.source_location())
2143+
throw errort{}.with_location(location)
21092144
<< "identifier " << base_name << " already used as define";
21102145
}
21112146

@@ -2163,13 +2198,14 @@ void smv_typecheckt::create_var_symbols(
21632198
{
21642199
if(element.is_var() || element.is_ivar())
21652200
{
2166-
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();
21672203
irep_idt identifier = module + "::var::" + id2string(base_name);
21682204

21692205
auto symbol_ptr = symbol_table.lookup(identifier);
21702206
if(symbol_ptr != nullptr)
21712207
{
2172-
throw errort{}.with_location(element.expr.source_location())
2208+
throw errort{}.with_location(location)
21732209
<< "variable " << base_name << " already declared, at "
21742210
<< symbol_ptr->location;
21752211
}
@@ -2196,21 +2232,20 @@ void smv_typecheckt::create_var_symbols(
21962232

21972233
symbol.is_state_var = false;
21982234
symbol.value = nil_exprt{};
2199-
symbol.location = element.expr.source_location();
2235+
symbol.location = location;
22002236

22012237
symbol_table.insert(std::move(symbol));
22022238
}
22032239
else if(element.is_define())
22042240
{
2205-
const auto &identifier_expr =
2206-
to_smv_identifier_expr(to_equal_expr(element.expr).lhs());
2207-
irep_idt base_name = identifier_expr.identifier();
2241+
irep_idt base_name = merge_complex_identifier(to_equal_expr(element.expr).lhs());
2242+
auto location = to_equal_expr(element.expr).lhs().source_location();
22082243
irep_idt identifier = module + "::var::" + id2string(base_name);
22092244

22102245
auto symbol_ptr = symbol_table.lookup(identifier);
22112246
if(symbol_ptr != nullptr)
22122247
{
2213-
throw errort{}.with_location(identifier_expr.source_location())
2248+
throw errort{}.with_location(location)
22142249
<< "variable `" << base_name << "' already declared, at "
22152250
<< symbol_ptr->location;
22162251
}
@@ -2232,7 +2267,7 @@ void smv_typecheckt::create_var_symbols(
22322267
symbol.value = nil_exprt{};
22332268
symbol.is_input = true;
22342269
symbol.is_state_var = false;
2235-
symbol.location = identifier_expr.source_location();
2270+
symbol.location = location;
22362271

22372272
symbol_table.insert(std::move(symbol));
22382273
}

0 commit comments

Comments
 (0)