Skip to content

Commit 7c844fb

Browse files
authored
Merge pull request #3874 from tautschnig/symbol_exprt-optional
Use optionalt<symbol_exprt> when it isn't always set [blocks: #3766]
2 parents b3604d6 + f71df24 commit 7c844fb

File tree

3 files changed

+96
-59
lines changed

3 files changed

+96
-59
lines changed

src/goto-programs/remove_returns.cpp

Lines changed: 19 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -54,10 +54,11 @@ class remove_returnst
5454
void undo_function_calls(
5555
goto_programt &goto_program);
5656

57-
symbol_exprt get_or_create_return_value_symbol(const irep_idt &function_id);
57+
optionalt<symbol_exprt>
58+
get_or_create_return_value_symbol(const irep_idt &function_id);
5859
};
5960

60-
symbol_exprt
61+
optionalt<symbol_exprt>
6162
remove_returnst::get_or_create_return_value_symbol(const irep_idt &function_id)
6263
{
6364
const irep_idt symbol_name = id2string(function_id) + RETURN_VALUE_SUFFIX;
@@ -69,7 +70,7 @@ remove_returnst::get_or_create_return_value_symbol(const irep_idt &function_id)
6970
const typet &return_type = to_code_type(function_symbol.type).return_type();
7071

7172
if(return_type == empty_typet())
72-
return symbol_exprt();
73+
return {};
7374

7475
auxiliary_symbolt new_symbol;
7576
new_symbol.is_static_lifetime = true;
@@ -103,7 +104,7 @@ void remove_returnst::replace_returns(
103104
return;
104105

105106
// add return_value symbol to symbol_table, if not already created:
106-
symbol_exprt return_symbol = get_or_create_return_value_symbol(function_id);
107+
const auto return_symbol = get_or_create_return_value_symbol(function_id);
107108

108109
// look up the function symbol
109110
symbolt &function_symbol = *symbol_table.get_writeable(function_id);
@@ -122,11 +123,16 @@ void remove_returnst::replace_returns(
122123
i_it->code.operands().size() == 1,
123124
"return instructions should have one operand");
124125

125-
// replace "return x;" by "fkt#return_value=x;"
126-
code_assignt assignment(return_symbol, i_it->code.op0());
126+
if(return_symbol.has_value())
127+
{
128+
// replace "return x;" by "fkt#return_value=x;"
129+
code_assignt assignment(*return_symbol, i_it->code.op0());
127130

128-
// now turn the `return' into `assignment'
129-
i_it->make_assignment(assignment);
131+
// now turn the `return' into `assignment'
132+
i_it->make_assignment(assignment);
133+
}
134+
else
135+
i_it->make_skip();
130136
}
131137
}
132138
}
@@ -153,7 +159,7 @@ void remove_returnst::do_function_calls(
153159
const irep_idt function_id =
154160
to_symbol_expr(function_call.function()).get_identifier();
155161

156-
symbol_exprt return_value;
162+
optionalt<symbol_exprt> return_value;
157163
typet old_return_type;
158164
bool is_stub = function_is_stub(function_id);
159165

@@ -169,9 +175,9 @@ void remove_returnst::do_function_calls(
169175
// To simplify matters, create its return-value global now (if not
170176
// already done), and use that to determine its true return type.
171177
return_value = get_or_create_return_value_symbol(function_id);
172-
if(return_value == symbol_exprt()) // really void-typed?
178+
if(!return_value.has_value()) // really void-typed?
173179
continue;
174-
old_return_type = return_value.type();
180+
old_return_type = return_value->type();
175181
}
176182

177183
// Do we return anything?
@@ -194,7 +200,7 @@ void remove_returnst::do_function_calls(
194200
// from the return type in the declaration. We therefore do a
195201
// cast.
196202
rhs = typecast_exprt::conditional_cast(
197-
return_value, function_call.lhs().type());
203+
*return_value, function_call.lhs().type());
198204
}
199205
else
200206
rhs = side_effect_expr_nondett(
@@ -214,7 +220,7 @@ void remove_returnst::do_function_calls(
214220
goto_programt::targett t_d=goto_program.insert_after(t_a);
215221
t_d->make_dead();
216222
t_d->source_location=i_it->source_location;
217-
t_d->code = code_deadt(return_value);
223+
t_d->code = code_deadt(*return_value);
218224
t_d->function=i_it->function;
219225
}
220226
}

src/goto-programs/remove_virtual_functions.cpp

Lines changed: 47 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ class remove_virtual_functionst
5454
function_call_resolvert;
5555
void get_child_functions_rec(
5656
const irep_idt &,
57-
const symbol_exprt &,
57+
const optionalt<symbol_exprt> &,
5858
const irep_idt &,
5959
dispatch_table_entriest &,
6060
dispatch_table_entries_mapt &,
@@ -166,15 +166,17 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
166166
if(functions.size()==1 &&
167167
fallback_action==virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION)
168168
{
169-
if(functions.begin()->symbol_expr==symbol_exprt())
169+
if(!functions.front().symbol_expr.has_value())
170170
{
171171
target->make_skip();
172172
remove_skip(goto_program, target, next_target);
173173
}
174174
else
175175
{
176176
create_static_function_call(
177-
to_code_function_call(target->code), functions.front().symbol_expr, ns);
177+
to_code_function_call(target->code),
178+
*functions.front().symbol_expr,
179+
ns);
178180
}
179181
return next_target;
180182
}
@@ -195,7 +197,6 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
195197
goto_programt new_code_gotos;
196198

197199
exprt this_expr=code.arguments()[0];
198-
const auto &last_function_symbol=functions.back().symbol_expr;
199200

200201
const typet &this_type=this_expr.type();
201202
INVARIANT(this_type.id() == ID_pointer, "this parameter must be a pointer");
@@ -219,26 +220,29 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
219220

220221
// get initial identifier for grouping
221222
INVARIANT(!functions.empty(), "Function dispatch table cannot be empty.");
223+
const auto &last_function_symbol = functions.back().symbol_expr;
222224

223225
std::map<irep_idt, goto_programt::targett> calls;
224226
// Note backwards iteration, to get the fallback candidate first.
225227
for(auto it=functions.crbegin(), itend=functions.crend(); it!=itend; ++it)
226228
{
227229
const auto &fun=*it;
228-
auto insertit=calls.insert(
229-
{fun.symbol_expr.get_identifier(), goto_programt::targett()});
230+
irep_idt id_or_empty = fun.symbol_expr.has_value()
231+
? fun.symbol_expr->get_identifier()
232+
: irep_idt();
233+
auto insertit = calls.insert({id_or_empty, goto_programt::targett()});
230234

231235
// Only create one call sequence per possible target:
232236
if(insertit.second)
233237
{
234238
goto_programt::targett t1=new_code_calls.add_instruction();
235239
t1->source_location=vcall_source_loc;
236-
if(!fun.symbol_expr.get_identifier().empty())
240+
if(fun.symbol_expr.has_value())
237241
{
238242
// call function
239243
t1->make_function_call(code);
240244
create_static_function_call(
241-
to_code_function_call(t1->code), fun.symbol_expr, ns);
245+
to_code_function_call(t1->code), *fun.symbol_expr, ns);
242246
}
243247
else
244248
{
@@ -257,9 +261,12 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
257261
}
258262

259263
// Fall through to the default callee if possible:
260-
if(fallback_action ==
261-
virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION &&
262-
fun.symbol_expr == last_function_symbol)
264+
if(
265+
fallback_action ==
266+
virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION &&
267+
fun.symbol_expr.has_value() == last_function_symbol.has_value() &&
268+
(!fun.symbol_expr.has_value() ||
269+
*fun.symbol_expr == *last_function_symbol))
263270
{
264271
// Nothing to do
265272
}
@@ -271,8 +278,11 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
271278

272279
// If the previous GOTO goes to the same callee, join it
273280
// (e.g. turning IF x GOTO y into IF x || z GOTO y)
274-
if(it != functions.crbegin() &&
275-
std::prev(it)->symbol_expr == fun.symbol_expr)
281+
if(
282+
it != functions.crbegin() &&
283+
std::prev(it)->symbol_expr.has_value() == fun.symbol_expr.has_value() &&
284+
(!fun.symbol_expr.has_value() ||
285+
*(std::prev(it)->symbol_expr) == *fun.symbol_expr))
276286
{
277287
INVARIANT(
278288
!new_code_gotos.empty(),
@@ -337,7 +347,7 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
337347
/// \param resolve_function_call`: function to resolve abstract method call
338348
void remove_virtual_functionst::get_child_functions_rec(
339349
const irep_idt &this_id,
340-
const symbol_exprt &last_method_defn,
350+
const optionalt<symbol_exprt> &last_method_defn,
341351
const irep_idt &component_name,
342352
dispatch_table_entriest &functions,
343353
dispatch_table_entries_mapt &entry_map,
@@ -354,9 +364,10 @@ void remove_virtual_functionst::get_child_functions_rec(
354364
auto it = entry_map.find(child);
355365
if(
356366
it != entry_map.end() &&
357-
!has_prefix(
358-
id2string(it->second.symbol_expr.get_identifier()),
359-
"java::java.lang.Object"))
367+
(!it->second.symbol_expr.has_value() ||
368+
!has_prefix(
369+
id2string(it->second.symbol_expr->get_identifier()),
370+
"java::java.lang.Object")))
360371
{
361372
continue;
362373
}
@@ -365,13 +376,13 @@ void remove_virtual_functionst::get_child_functions_rec(
365376
if(method.is_not_nil())
366377
{
367378
function.symbol_expr=to_symbol_expr(method);
368-
function.symbol_expr.set(ID_C_class, child);
379+
function.symbol_expr->set(ID_C_class, child);
369380
}
370381
else
371382
{
372383
function.symbol_expr=last_method_defn;
373384
}
374-
if(function.symbol_expr == symbol_exprt())
385+
if(!function.symbol_expr.has_value())
375386
{
376387
const resolve_inherited_componentt::inherited_componentt
377388
&resolved_call = resolve_function_call(child, component_name);
@@ -383,12 +394,12 @@ void remove_virtual_functionst::get_child_functions_rec(
383394
resolved_call.get_full_component_identifier());
384395

385396
function.symbol_expr = called_symbol.symbol_expr();
386-
function.symbol_expr.set(
397+
function.symbol_expr->set(
387398
ID_C_class, resolved_call.get_class_identifier());
388399
}
389400
}
390401
functions.push_back(function);
391-
entry_map.insert({child, function});
402+
entry_map.emplace(child, function);
392403

393404
get_child_functions_rec(
394405
child,
@@ -426,7 +437,8 @@ void remove_virtual_functionst::get_functions(
426437
const resolve_inherited_componentt::inherited_componentt
427438
&resolved_call = get_virtual_call_target(class_id, function_name, false);
428439

429-
dispatch_table_entryt root_function;
440+
// might be an abstract function
441+
dispatch_table_entryt root_function(class_id);
430442

431443
if(resolved_call.is_valid())
432444
{
@@ -436,14 +448,9 @@ void remove_virtual_functionst::get_functions(
436448
symbol_table.lookup_ref(resolved_call.get_full_component_identifier());
437449

438450
root_function.symbol_expr=called_symbol.symbol_expr();
439-
root_function.symbol_expr.set(
451+
root_function.symbol_expr->set(
440452
ID_C_class, resolved_call.get_class_identifier());
441453
}
442-
else
443-
{
444-
// No definition here; this is an abstract function.
445-
root_function.class_id=class_id;
446-
}
447454

448455
// iterate over all children, transitively
449456
dispatch_table_entries_mapt entry_map;
@@ -455,7 +462,7 @@ void remove_virtual_functionst::get_functions(
455462
entry_map,
456463
resolve_function_call);
457464

458-
if(root_function.symbol_expr!=symbol_exprt())
465+
if(root_function.symbol_expr.has_value())
459466
functions.push_back(root_function);
460467

461468
// Sort for the identifier of the function call symbol expression, grouping
@@ -465,20 +472,21 @@ void remove_virtual_functionst::get_functions(
465472
std::sort(
466473
functions.begin(),
467474
functions.end(),
468-
[](const dispatch_table_entryt &a, dispatch_table_entryt &b)
469-
{
470-
if(
471-
has_prefix(
472-
id2string(a.symbol_expr.get_identifier()), "java::java.lang.Object"))
475+
[](const dispatch_table_entryt &a, const dispatch_table_entryt &b) {
476+
irep_idt a_id = a.symbol_expr.has_value()
477+
? a.symbol_expr->get_identifier()
478+
: irep_idt();
479+
irep_idt b_id = b.symbol_expr.has_value()
480+
? b.symbol_expr->get_identifier()
481+
: irep_idt();
482+
483+
if(has_prefix(id2string(a_id), "java::java.lang.Object"))
473484
return false;
474-
else if(
475-
has_prefix(
476-
id2string(b.symbol_expr.get_identifier()), "java::java.lang.Object"))
485+
else if(has_prefix(id2string(b_id), "java::java.lang.Object"))
477486
return true;
478487
else
479488
{
480-
int cmp = a.symbol_expr.get_identifier().compare(
481-
b.symbol_expr.get_identifier());
489+
int cmp = a_id.compare(b_id);
482490
if(cmp == 0)
483491
return a.class_id < b.class_id;
484492
else

src/goto-programs/remove_virtual_functions.h

Lines changed: 30 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Date: April 2016
1515
#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H
1616
#define CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H
1717

18+
#include <util/optional.h>
1819
#include <util/std_expr.h>
1920

2021
#include "class_hierarchy.h"
@@ -52,13 +53,35 @@ enum class virtual_dispatch_fallback_actiont
5253

5354
class dispatch_table_entryt
5455
{
55-
public:
56-
dispatch_table_entryt() = default;
57-
explicit dispatch_table_entryt(const irep_idt &_class_id) :
58-
class_id(_class_id)
59-
{}
60-
61-
symbol_exprt symbol_expr;
56+
public:
57+
explicit dispatch_table_entryt(const irep_idt &_class_id)
58+
: symbol_expr(), class_id(_class_id)
59+
{
60+
}
61+
62+
#if defined(__GNUC__) && __GNUC__ < 7
63+
// GCC up to version 6.5 warns about irept::data being used uninitialized upon
64+
// the move triggered by std::sort; using operator= works around this
65+
dispatch_table_entryt(dispatch_table_entryt &&other)
66+
{
67+
symbol_expr = other.symbol_expr;
68+
class_id = other.class_id;
69+
}
70+
71+
dispatch_table_entryt &operator=(const dispatch_table_entryt &other)
72+
{
73+
symbol_expr = other.symbol_expr;
74+
class_id = other.class_id;
75+
return *this;
76+
}
77+
78+
dispatch_table_entryt(const dispatch_table_entryt &other)
79+
: symbol_expr(other.symbol_expr), class_id(other.class_id)
80+
{
81+
}
82+
#endif
83+
84+
optionalt<symbol_exprt> symbol_expr;
6285
irep_idt class_id;
6386
};
6487

0 commit comments

Comments
 (0)