Skip to content

Commit a06ddb2

Browse files
kroeningkroening
committed
SMV: avoid some expression copies
References are changed to rvalue references to avoid some copying when populating the parse tree.
1 parent 82c9305 commit a06ddb2

File tree

2 files changed

+71
-63
lines changed

2 files changed

+71
-63
lines changed

‎src/smvlang/parser.y‎

Lines changed: 6 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -486,17 +486,14 @@ assignments: assignment
486486

487487
assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';'
488488
{
489-
binary($$, $3, ID_equal, $6);
490-
491489
if(stack_expr($1).id()==ID_smv_next)
492490
{
493-
exprt &op=to_binary_expr(stack_expr($$)).op0();
494-
unary_exprt tmp(ID_smv_next, std::move(op));
495-
tmp.swap(op);
496-
PARSER.module->add_assign_next(to_equal_expr(stack_expr($$)));
491+
PARSER.module->add_assign_next(
492+
unary_exprt{ID_smv_next, std::move(stack_expr($3))},
493+
std::move(stack_expr($6)));
497494
}
498495
else
499-
PARSER.module->add_assign_init(to_equal_expr(stack_expr($$)));
496+
PARSER.module->add_assign_init(std::move(stack_expr($3)), std::move(stack_expr($6)));
500497
}
501498
| assignment_var BECOMES_Token formula ';'
502499
{
@@ -528,8 +525,7 @@ assignment : assignment_head '(' assignment_var ')' BECOMES_Token formula ';'
528525
DATA_INVARIANT(false, "unexpected variable class");
529526
}
530527

531-
binary($$, $1, ID_equal, $3);
532-
PARSER.module->add_assign_current(to_equal_expr(stack_expr($$)));
528+
PARSER.module->add_assign_current(std::move(stack_expr($1)), std::move(stack_expr($3)));
533529
}
534530
;
535531

@@ -575,8 +571,7 @@ define : assignment_var BECOMES_Token formula ';'
575571
DATA_INVARIANT(false, "unexpected variable class");
576572
}
577573

578-
binary($$, $1, ID_equal, $3);
579-
PARSER.module->add_define(to_equal_expr(stack_expr($$)));
574+
PARSER.module->add_define(std::move(stack_expr($1)), std::move(stack_expr($3)));
580575
}
581576
;
582577

‎src/smvlang/smv_parse_tree.h‎

Lines changed: 65 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,13 @@ class smv_parse_treet
5454
FAIRNESS
5555
};
5656

57+
itemt(item_typet __item_type, exprt __expr, source_locationt __location)
58+
: item_type(__item_type),
59+
expr(std::move(__expr)),
60+
location(std::move(__location))
61+
{
62+
}
63+
5764
friend std::string to_string(item_typet i);
5865

5966
item_typet item_type;
@@ -118,100 +125,106 @@ class smv_parse_treet
118125
typedef std::list<itemt> item_listt;
119126
item_listt items;
120127

121-
void add_item(
122-
itemt::item_typet item_type,
123-
const exprt &expr,
124-
const source_locationt &location)
128+
void add_assign_current(exprt lhs, exprt rhs)
125129
{
126-
items.push_back(itemt());
127-
items.back().item_type=item_type;
128-
items.back().expr=expr;
129-
items.back().location=location;
130+
items.emplace_back(
131+
itemt::ASSIGN_CURRENT,
132+
binary_exprt{std::move(lhs), ID_equal, std::move(rhs)},
133+
source_locationt::nil());
130134
}
131135

132-
void add_assign_current(const equal_exprt &expr)
136+
void add_assign_init(exprt lhs, exprt rhs)
133137
{
134-
add_item(itemt::ASSIGN_CURRENT, expr, source_locationt::nil());
138+
items.emplace_back(
139+
itemt::ASSIGN_INIT,
140+
binary_exprt{std::move(lhs), ID_equal, std::move(rhs)},
141+
source_locationt::nil());
135142
}
136143

137-
void add_assign_init(const equal_exprt &expr)
144+
void add_assign_next(exprt lhs, exprt rhs)
138145
{
139-
add_item(itemt::ASSIGN_INIT, expr, source_locationt::nil());
146+
items.emplace_back(
147+
itemt::ASSIGN_NEXT,
148+
binary_exprt{std::move(lhs), ID_equal, std::move(rhs)},
149+
source_locationt::nil());
140150
}
141151

142-
void add_assign_next(const equal_exprt &expr)
152+
void add_invar(exprt expr)
143153
{
144-
add_item(itemt::ASSIGN_NEXT, expr, source_locationt::nil());
154+
items.emplace_back(
155+
itemt::INVAR, std::move(expr), source_locationt::nil());
145156
}
146157

147-
void add_invar(const exprt &expr)
158+
void add_ctlspec(exprt expr)
148159
{
149-
add_item(itemt::INVAR, expr, source_locationt::nil());
160+
items.emplace_back(
161+
itemt::CTLSPEC, std::move(expr), source_locationt::nil());
150162
}
151163

152-
void add_ctlspec(const exprt &expr)
164+
void add_ltlspec(exprt expr)
153165
{
154-
add_item(itemt::CTLSPEC, expr, source_locationt::nil());
166+
items.emplace_back(
167+
itemt::LTLSPEC, std::move(expr), source_locationt::nil());
155168
}
156169

157-
void add_ltlspec(const exprt &expr)
170+
void add_define(exprt lhs, exprt rhs)
158171
{
159-
add_item(itemt::LTLSPEC, expr, source_locationt::nil());
172+
items.emplace_back(
173+
itemt::DEFINE,
174+
binary_exprt{std::move(lhs), ID_equal, std::move(rhs)},
175+
source_locationt::nil());
160176
}
161177

162-
void add_define(const equal_exprt &expr)
163-
{
164-
add_item(itemt::DEFINE, expr, source_locationt::nil());
165-
}
166-
167-
void add_fairness(const exprt &expr)
178+
void add_fairness(exprt expr)
168179
{
169-
add_item(itemt::FAIRNESS, expr, source_locationt::nil());
180+
items.emplace_back(
181+
itemt::FAIRNESS, std::move(expr), source_locationt::nil());
170182
}
171-
172-
void add_init(const exprt &expr)
183+
184+
void add_init(exprt expr)
173185
{
174-
add_item(itemt::INIT, expr, source_locationt::nil());
186+
items.emplace_back(itemt::INIT, std::move(expr), source_locationt::nil());
175187
}
176-
177-
void add_trans(const exprt &expr)
188+
189+
void add_trans(exprt expr)
178190
{
179-
add_item(itemt::TRANS, expr, source_locationt::nil());
191+
items.emplace_back(
192+
itemt::TRANS, std::move(expr), source_locationt::nil());
180193
}
181-
182-
void add_invar(const exprt &expr, const source_locationt &location)
194+
195+
void add_invar(exprt expr, source_locationt location)
183196
{
184-
add_item(itemt::INVAR, expr, location);
197+
items.emplace_back(itemt::INVAR, std::move(expr), location);
185198
}
186199

187-
void add_ctlspec(const exprt &expr, const source_locationt &location)
200+
void add_ctlspec(exprt expr, source_locationt location)
188201
{
189-
add_item(itemt::CTLSPEC, expr, location);
202+
items.emplace_back(itemt::CTLSPEC, std::move(expr), std::move(location));
190203
}
191204

192-
void add_ltlspec(const exprt &expr, const source_locationt &location)
205+
void add_ltlspec(exprt expr, source_locationt location)
193206
{
194-
add_item(itemt::LTLSPEC, expr, location);
207+
items.emplace_back(itemt::LTLSPEC, std::move(expr), location);
195208
}
196-
197-
void add_define(const exprt &expr, const source_locationt &location)
209+
210+
void add_define(exprt expr, source_locationt location)
198211
{
199-
add_item(itemt::DEFINE, expr, location);
212+
items.emplace_back(itemt::DEFINE, std::move(expr), std::move(location));
200213
}
201-
202-
void add_fairness(const exprt &expr, const source_locationt &location)
214+
215+
void add_fairness(exprt expr, source_locationt location)
203216
{
204-
add_item(itemt::FAIRNESS, expr, location);
217+
items.emplace_back(itemt::FAIRNESS, std::move(expr), std::move(location));
205218
}
206-
207-
void add_init(const exprt &expr, const source_locationt &location)
219+
220+
void add_init(exprt expr, source_locationt location)
208221
{
209-
add_item(itemt::INIT, expr, location);
222+
items.emplace_back(itemt::INIT, std::move(expr), std::move(location));
210223
}
211-
212-
void add_trans(const exprt &expr, const source_locationt &location)
224+
225+
void add_trans(exprt expr, source_locationt location)
213226
{
214-
add_item(itemt::TRANS, expr, location);
227+
items.emplace_back(itemt::TRANS, std::move(expr), std::move(location));
215228
}
216229

217230
mc_varst vars;

0 commit comments

Comments
 (0)