Skip to content

Use optionalt<symbol_exprt> when it isn't always set [blocks: #3766] #3874

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Jan 22, 2019
Merged

Use optionalt<symbol_exprt> when it isn't always set [blocks: #3766] #3874

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6b2b950
Use optionalt<symbol_exprt> when it isn't always set
tautschnig Jan 21, 2019
f71df24
Work around spurious warning raised up to GCC 6.5
tautschnig Jan 21, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 19 additions & 13 deletions src/goto-programs/remove_returns.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,10 +54,11 @@ class remove_returnst
void undo_function_calls(
goto_programt &goto_program);

symbol_exprt get_or_create_return_value_symbol(const irep_idt &function_id);
optionalt<symbol_exprt>
get_or_create_return_value_symbol(const irep_idt &function_id);
};

symbol_exprt
optionalt<symbol_exprt>
remove_returnst::get_or_create_return_value_symbol(const irep_idt &function_id)
{
const irep_idt symbol_name = id2string(function_id) + RETURN_VALUE_SUFFIX;
Expand All @@ -69,7 +70,7 @@ remove_returnst::get_or_create_return_value_symbol(const irep_idt &function_id)
const typet &return_type = to_code_type(function_symbol.type).return_type();

if(return_type == empty_typet())
return symbol_exprt();
return {};

auxiliary_symbolt new_symbol;
new_symbol.is_static_lifetime = true;
Expand Down Expand Up @@ -103,7 +104,7 @@ void remove_returnst::replace_returns(
return;

// add return_value symbol to symbol_table, if not already created:
symbol_exprt return_symbol = get_or_create_return_value_symbol(function_id);
const auto return_symbol = get_or_create_return_value_symbol(function_id);

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

// replace "return x;" by "fkt#return_value=x;"
code_assignt assignment(return_symbol, i_it->code.op0());
if(return_symbol.has_value())
{
// replace "return x;" by "fkt#return_value=x;"
code_assignt assignment(*return_symbol, i_it->code.op0());

// now turn the `return' into `assignment'
i_it->make_assignment(assignment);
// now turn the `return' into `assignment'
i_it->make_assignment(assignment);
}
else
i_it->make_skip();
}
}
}
Expand All @@ -153,7 +159,7 @@ void remove_returnst::do_function_calls(
const irep_idt function_id =
to_symbol_expr(function_call.function()).get_identifier();

symbol_exprt return_value;
optionalt<symbol_exprt> return_value;
typet old_return_type;
bool is_stub = function_is_stub(function_id);

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

// Do we return anything?
Expand All @@ -194,7 +200,7 @@ void remove_returnst::do_function_calls(
// from the return type in the declaration. We therefore do a
// cast.
rhs = typecast_exprt::conditional_cast(
return_value, function_call.lhs().type());
*return_value, function_call.lhs().type());
}
else
rhs = side_effect_expr_nondett(
Expand All @@ -214,7 +220,7 @@ void remove_returnst::do_function_calls(
goto_programt::targett t_d=goto_program.insert_after(t_a);
t_d->make_dead();
t_d->source_location=i_it->source_location;
t_d->code = code_deadt(return_value);
t_d->code = code_deadt(*return_value);
t_d->function=i_it->function;
}
}
Expand Down
86 changes: 47 additions & 39 deletions src/goto-programs/remove_virtual_functions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ class remove_virtual_functionst
function_call_resolvert;
void get_child_functions_rec(
const irep_idt &,
const symbol_exprt &,
const optionalt<symbol_exprt> &,
const irep_idt &,
dispatch_table_entriest &,
dispatch_table_entries_mapt &,
Expand Down Expand Up @@ -166,15 +166,17 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
if(functions.size()==1 &&
fallback_action==virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION)
{
if(functions.begin()->symbol_expr==symbol_exprt())
if(!functions.front().symbol_expr.has_value())
{
target->make_skip();
remove_skip(goto_program, target, next_target);
}
else
{
create_static_function_call(
to_code_function_call(target->code), functions.front().symbol_expr, ns);
to_code_function_call(target->code),
*functions.front().symbol_expr,
ns);
}
return next_target;
}
Expand All @@ -195,7 +197,6 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
goto_programt new_code_gotos;

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

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

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

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

// Only create one call sequence per possible target:
if(insertit.second)
{
goto_programt::targett t1=new_code_calls.add_instruction();
t1->source_location=vcall_source_loc;
if(!fun.symbol_expr.get_identifier().empty())
if(fun.symbol_expr.has_value())
{
// call function
t1->make_function_call(code);
create_static_function_call(
to_code_function_call(t1->code), fun.symbol_expr, ns);
to_code_function_call(t1->code), *fun.symbol_expr, ns);
}
else
{
Expand All @@ -257,9 +261,12 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
}

// Fall through to the default callee if possible:
if(fallback_action ==
virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION &&
fun.symbol_expr == last_function_symbol)
if(
fallback_action ==
virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION &&
fun.symbol_expr.has_value() == last_function_symbol.has_value() &&
(!fun.symbol_expr.has_value() ||
*fun.symbol_expr == *last_function_symbol))
{
// Nothing to do
}
Expand All @@ -271,8 +278,11 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(

// If the previous GOTO goes to the same callee, join it
// (e.g. turning IF x GOTO y into IF x || z GOTO y)
if(it != functions.crbegin() &&
std::prev(it)->symbol_expr == fun.symbol_expr)
if(
it != functions.crbegin() &&
std::prev(it)->symbol_expr.has_value() == fun.symbol_expr.has_value() &&
(!fun.symbol_expr.has_value() ||
*(std::prev(it)->symbol_expr) == *fun.symbol_expr))
{
INVARIANT(
!new_code_gotos.empty(),
Expand Down Expand Up @@ -337,7 +347,7 @@ goto_programt::targett remove_virtual_functionst::remove_virtual_function(
/// \param resolve_function_call`: function to resolve abstract method call
void remove_virtual_functionst::get_child_functions_rec(
const irep_idt &this_id,
const symbol_exprt &last_method_defn,
const optionalt<symbol_exprt> &last_method_defn,
const irep_idt &component_name,
dispatch_table_entriest &functions,
dispatch_table_entries_mapt &entry_map,
Expand All @@ -354,9 +364,10 @@ void remove_virtual_functionst::get_child_functions_rec(
auto it = entry_map.find(child);
if(
it != entry_map.end() &&
!has_prefix(
id2string(it->second.symbol_expr.get_identifier()),
"java::java.lang.Object"))
(!it->second.symbol_expr.has_value() ||
!has_prefix(
id2string(it->second.symbol_expr->get_identifier()),
"java::java.lang.Object")))
{
continue;
}
Expand All @@ -365,13 +376,13 @@ void remove_virtual_functionst::get_child_functions_rec(
if(method.is_not_nil())
{
function.symbol_expr=to_symbol_expr(method);
function.symbol_expr.set(ID_C_class, child);
function.symbol_expr->set(ID_C_class, child);
}
else
{
function.symbol_expr=last_method_defn;
}
if(function.symbol_expr == symbol_exprt())
if(!function.symbol_expr.has_value())
{
const resolve_inherited_componentt::inherited_componentt
&resolved_call = resolve_function_call(child, component_name);
Expand All @@ -383,12 +394,12 @@ void remove_virtual_functionst::get_child_functions_rec(
resolved_call.get_full_component_identifier());

function.symbol_expr = called_symbol.symbol_expr();
function.symbol_expr.set(
function.symbol_expr->set(
ID_C_class, resolved_call.get_class_identifier());
}
}
functions.push_back(function);
entry_map.insert({child, function});
entry_map.emplace(child, function);

get_child_functions_rec(
child,
Expand Down Expand Up @@ -426,7 +437,8 @@ void remove_virtual_functionst::get_functions(
const resolve_inherited_componentt::inherited_componentt
&resolved_call = get_virtual_call_target(class_id, function_name, false);

dispatch_table_entryt root_function;
// might be an abstract function
dispatch_table_entryt root_function(class_id);

if(resolved_call.is_valid())
{
Expand All @@ -436,14 +448,9 @@ void remove_virtual_functionst::get_functions(
symbol_table.lookup_ref(resolved_call.get_full_component_identifier());

root_function.symbol_expr=called_symbol.symbol_expr();
root_function.symbol_expr.set(
root_function.symbol_expr->set(
ID_C_class, resolved_call.get_class_identifier());
}
else
{
// No definition here; this is an abstract function.
root_function.class_id=class_id;
}

// iterate over all children, transitively
dispatch_table_entries_mapt entry_map;
Expand All @@ -455,7 +462,7 @@ void remove_virtual_functionst::get_functions(
entry_map,
resolve_function_call);

if(root_function.symbol_expr!=symbol_exprt())
if(root_function.symbol_expr.has_value())
functions.push_back(root_function);

// Sort for the identifier of the function call symbol expression, grouping
Expand All @@ -465,20 +472,21 @@ void remove_virtual_functionst::get_functions(
std::sort(
functions.begin(),
functions.end(),
[](const dispatch_table_entryt &a, dispatch_table_entryt &b)
{
if(
has_prefix(
id2string(a.symbol_expr.get_identifier()), "java::java.lang.Object"))
[](const dispatch_table_entryt &a, const dispatch_table_entryt &b) {
irep_idt a_id = a.symbol_expr.has_value()
? a.symbol_expr->get_identifier()
: irep_idt();
irep_idt b_id = b.symbol_expr.has_value()
? b.symbol_expr->get_identifier()
: irep_idt();

if(has_prefix(id2string(a_id), "java::java.lang.Object"))
return false;
else if(
has_prefix(
id2string(b.symbol_expr.get_identifier()), "java::java.lang.Object"))
else if(has_prefix(id2string(b_id), "java::java.lang.Object"))
return true;
else
{
int cmp = a.symbol_expr.get_identifier().compare(
b.symbol_expr.get_identifier());
int cmp = a_id.compare(b_id);
if(cmp == 0)
return a.class_id < b.class_id;
else
Expand Down
37 changes: 30 additions & 7 deletions src/goto-programs/remove_virtual_functions.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ Date: April 2016
#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H
#define CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H

#include <util/optional.h>
#include <util/std_expr.h>

#include "class_hierarchy.h"
Expand Down Expand Up @@ -52,13 +53,35 @@ enum class virtual_dispatch_fallback_actiont

class dispatch_table_entryt
{
public:
dispatch_table_entryt() = default;
explicit dispatch_table_entryt(const irep_idt &_class_id) :
class_id(_class_id)
{}

symbol_exprt symbol_expr;
public:
explicit dispatch_table_entryt(const irep_idt &_class_id)
: symbol_expr(), class_id(_class_id)
{
}

#if defined(__GNUC__) && __GNUC__ < 7
// GCC up to version 6.5 warns about irept::data being used uninitialized upon
// the move triggered by std::sort; using operator= works around this
dispatch_table_entryt(dispatch_table_entryt &&other)
{
symbol_expr = other.symbol_expr;
class_id = other.class_id;
}

dispatch_table_entryt &operator=(const dispatch_table_entryt &other)
{
symbol_expr = other.symbol_expr;
class_id = other.class_id;
return *this;
}

dispatch_table_entryt(const dispatch_table_entryt &other)
: symbol_expr(other.symbol_expr), class_id(other.class_id)
{
}
#endif

optionalt<symbol_exprt> symbol_expr;
irep_idt class_id;
};

Expand Down