Skip to content

introduce instructiont::call_function() and related methods #6281

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.

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 1 commit into from
Aug 9, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
26 changes: 7 additions & 19 deletions src/analyses/constant_propagator.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -192,8 +192,7 @@ void constant_propagator_domaint::transform(
}
else if(from->is_function_call())
{
const auto &function_call = from->get_function_call();
const exprt &function=function_call.function();
const exprt &function = from->call_function();

if(function.id()==ID_symbol)
{
Expand Down Expand Up @@ -231,8 +230,8 @@ void constant_propagator_domaint::transform(
const code_typet &code_type=to_code_type(symbol.type);
const code_typet::parameterst &parameters=code_type.parameters();

const code_function_callt::argumentst &arguments=
function_call.arguments();
const code_function_callt::argumentst &arguments =
from->call_arguments();

code_typet::parameterst::const_iterator p_it=parameters.begin();
for(const auto &arg : arguments)
Expand Down Expand Up @@ -777,22 +776,11 @@ void constant_propagator_ait::replace(
}
else if(it->is_function_call())
{
auto call = it->get_function_call();
constant_propagator_domaint::partial_evaluate(
d.values, it->call_function(), ns);

bool call_changed = false;

if(!constant_propagator_domaint::partial_evaluate(
d.values, call.function(), ns))
{
call_changed = true;
}

for(auto &arg : call.arguments())
if(!constant_propagator_domaint::partial_evaluate(d.values, arg, ns))
call_changed = true;

if(call_changed)
it->set_function_call(call);
for(auto &arg : it->call_arguments())
constant_propagator_domaint::partial_evaluate(d.values, arg, ns);
}
else if(it->is_other())
{
Expand Down
4 changes: 2 additions & 2 deletions src/goto-programs/cfg.h
Original file line number Diff line number Diff line change
Expand Up @@ -391,7 +391,7 @@ void cfg_baset<T, P, I>::compute_edges_function_call(
goto_programt::const_targett next_PC,
entryt &entry)
{
const exprt &function = instruction.get_function_call().function();
const exprt &function = instruction.call_function();

if(function.id()!=ID_symbol)
return;
Expand Down Expand Up @@ -441,7 +441,7 @@ void procedure_local_cfg_baset<T, P, I>::compute_edges_function_call(
goto_programt::const_targett next_PC,
typename cfg_baset<T, P, I>::entryt &entry)
{
const exprt &function = instruction.get_function_call().function();
const exprt &function = instruction.call_function();

if(function.id()!=ID_symbol)
return;
Expand Down
8 changes: 3 additions & 5 deletions src/goto-programs/goto_inline_class.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -436,11 +436,9 @@ void goto_inlinet::get_call(
{
PRECONDITION(it->is_function_call());

const code_function_callt &call = it->get_function_call();

lhs=call.lhs();
function=call.function();
arguments=call.arguments();
lhs = it->call_lhs();
function = it->call_function();
arguments = it->call_arguments();
}

/// Inline all of the given call locations.
Expand Down
53 changes: 14 additions & 39 deletions src/goto-programs/goto_program.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -329,14 +329,11 @@ std::list<exprt> expressions_read(
break;

case FUNCTION_CALL:
{
const code_function_callt &function_call = instruction.get_function_call();
for(const auto &argument : function_call.arguments())
for(const auto &argument : instruction.call_arguments())
dest.push_back(argument);
if(function_call.lhs().is_not_nil())
parse_lhs_read(function_call.lhs(), dest);
if(instruction.call_lhs().is_not_nil())
parse_lhs_read(instruction.call_lhs(), dest);
break;
}

case ASSIGN:
dest.push_back(instruction.assign_rhs());
Expand Down Expand Up @@ -371,12 +368,8 @@ std::list<exprt> expressions_written(
switch(instruction.type)
{
case FUNCTION_CALL:
{
const code_function_callt &function_call =
instruction.get_function_call();
if(function_call.lhs().is_not_nil())
dest.push_back(function_call.lhs());
}
if(instruction.call_lhs().is_not_nil())
dest.push_back(instruction.call_lhs());
break;

case ASSIGN:
Expand Down Expand Up @@ -999,35 +992,20 @@ void goto_programt::instructiont::transform(

case FUNCTION_CALL:
{
auto new_call = get_function_call();
bool change = false;

auto new_lhs = f(new_call.lhs());
auto new_lhs = f(call_lhs());
if(new_lhs.has_value())
{
new_call.lhs() = *new_lhs;
change = true;
}
call_lhs() = *new_lhs;

auto new_function = f(new_call.function());
if(new_function.has_value())
{
new_call.function() = *new_function;
change = true;
}
auto new_call_function = f(call_function());
if(new_call_function.has_value())
call_function() = *new_call_function;

for(auto &a : new_call.arguments())
for(auto &a : call_arguments())
{
auto new_a = f(a);
if(new_a.has_value())
{
a = *new_a;
change = true;
}
}

if(change)
set_function_call(new_call);
}
break;

Expand Down Expand Up @@ -1082,13 +1060,10 @@ void goto_programt::instructiont::apply(
break;

case FUNCTION_CALL:
{
const auto &call = get_function_call();
f(call.lhs());
for(auto &a : call.arguments())
f(call_lhs());
for(auto &a : call_arguments())
f(a);
}
break;
break;

case GOTO:
case ASSUME:
Expand Down
56 changes: 56 additions & 0 deletions src/goto-programs/goto_program.h
Original file line number Diff line number Diff line change
Expand Up @@ -344,18 +344,74 @@ class goto_programt
}

/// Get the function call for FUNCTION_CALL
#if 1
DEPRECATED(SINCE(
2021,
2,
24,
"Use call_function(), call_lhs(), call_arguments() instead"))
const code_function_callt &get_function_call() const
{
PRECONDITION(is_function_call());
return to_code_function_call(code);
}
#endif

/// Get the function that is called for FUNCTION_CALL
const exprt &call_function() const
{
PRECONDITION(is_function_call());
return to_code_function_call(code).function();
}

/// Get the function that is called for FUNCTION_CALL
exprt &call_function()
{
PRECONDITION(is_function_call());
return to_code_function_call(code).function();
}

/// Get the lhs of a FUNCTION_CALL (may be nil)
const exprt &call_lhs() const
{
PRECONDITION(is_function_call());
return to_code_function_call(code).lhs();
}

/// Get the lhs of a FUNCTION_CALL (may be nil)
exprt &call_lhs()
{
PRECONDITION(is_function_call());
return to_code_function_call(code).lhs();
}

/// Get the arguments of a FUNCTION_CALL
const exprt::operandst &call_arguments() const
{
PRECONDITION(is_function_call());
return to_code_function_call(code).arguments();
}

/// Get the arguments of a FUNCTION_CALL
exprt::operandst &call_arguments()
{
PRECONDITION(is_function_call());
return to_code_function_call(code).arguments();
}

/// Set the function call for FUNCTION_CALL
#if 1
DEPRECATED(SINCE(
2021,
2,
24,
"Use call_function(), call_lhs(), call_arguments() instead"))
void set_function_call(code_function_callt c)
{
PRECONDITION(is_function_call());
code = std::move(c);
}
#endif

/// Get the statement for OTHER
const codet &get_other() const
Expand Down
19 changes: 9 additions & 10 deletions src/goto-programs/instrument_preconditions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -64,14 +64,14 @@ void remove_preconditions(goto_programt &goto_program)
}

replace_symbolt actuals_replace_map(
const code_function_callt &call,
const goto_programt::instructiont &call,
const namespacet &ns)
{
PRECONDITION(call.function().id()==ID_symbol);
const symbolt &s=ns.lookup(to_symbol_expr(call.function()));
PRECONDITION(call.call_function().id() == ID_symbol);
const symbolt &s = ns.lookup(to_symbol_expr(call.call_function()));
const auto &code_type=to_code_type(s.type);
const auto &parameters=code_type.parameters();
const auto &arguments=call.arguments();
const auto &arguments = call.call_arguments();

replace_symbolt result;
std::size_t count=0;
Expand Down Expand Up @@ -102,17 +102,16 @@ void instrument_preconditions(
if(it->is_function_call())
{
// does the function we call have preconditions?
const auto &call = it->get_function_call();
const auto &called_function = it->call_function();

if(call.function().id()==ID_symbol)
if(called_function.id() == ID_symbol)
{
auto preconditions=
get_preconditions(to_symbol_expr(call.function()),
goto_model.goto_functions);
auto preconditions = get_preconditions(
to_symbol_expr(called_function), goto_model.goto_functions);

source_locationt source_location=it->source_location;

replace_symbolt r=actuals_replace_map(call, ns);
replace_symbolt r = actuals_replace_map(*it, ns);

// add before the call, with location of the call
for(const auto &p : preconditions)
Expand Down
21 changes: 11 additions & 10 deletions src/goto-programs/interpreter.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -739,10 +739,12 @@ void interpretert::execute_assert()

void interpretert::execute_function_call()
{
const code_function_callt &function_call = pc->get_function_call();
const auto &call_lhs = pc->call_lhs();
const auto &call_function = pc->call_function();
const auto &call_arguments = pc->call_arguments();

// function to be called
mp_integer address=evaluate_address(function_call.function());
mp_integer address = evaluate_address(call_function);

if(address==0)
throw "function call to NULL";
Expand All @@ -767,19 +769,18 @@ void interpretert::execute_function_call()
// return value
mp_integer return_value_address;

if(function_call.lhs().is_not_nil())
return_value_address=
evaluate_address(function_call.lhs());
if(call_lhs.is_not_nil())
return_value_address = evaluate_address(call_lhs);
else
return_value_address=0;

// values of the arguments
std::vector<mp_vectort> argument_values;

argument_values.resize(function_call.arguments().size());
argument_values.resize(call_arguments.size());

for(std::size_t i=0; i<function_call.arguments().size(); i++)
evaluate(function_call.arguments()[i], argument_values[i]);
for(std::size_t i = 0; i < call_arguments.size(); i++)
evaluate(call_arguments[i], argument_values[i]);

// do the call

Expand Down Expand Up @@ -821,8 +822,8 @@ void interpretert::execute_function_call()
}
else
{
list_input_varst::iterator it = function_input_vars.find(
to_symbol_expr(function_call.function()).get_identifier());
list_input_varst::iterator it =
function_input_vars.find(to_symbol_expr(call_function).get_identifier());

if(it!=function_input_vars.end())
{
Expand Down
11 changes: 5 additions & 6 deletions src/goto-programs/label_function_pointer_call_sites.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -21,14 +21,13 @@ void label_function_pointer_call_sites(goto_modelt &goto_model)
for_each_instruction_if(
goto_function.second,
[](const goto_programt::targett it) {
return it->is_function_call() && can_cast_expr<dereference_exprt>(
it->get_function_call().function());
return it->is_function_call() &&
can_cast_expr<dereference_exprt>(it->call_function());
},
[&](goto_programt::targett &it) {
auto const &function_call = it->get_function_call();
auto const &function_pointer_dereference =
to_dereference_expr(function_call.function());
auto const &source_location = function_call.source_location();
to_dereference_expr(it->call_function());
auto const &source_location = it->source_location;
auto const &goto_function_symbol_mode =
goto_model.symbol_table.lookup_ref(goto_function.first).mode;

Expand All @@ -43,7 +42,7 @@ void label_function_pointer_call_sites(goto_modelt &goto_model)
function_call_site_symbol.pretty_name = call_site_symbol_name;
function_call_site_symbol.type =
function_pointer_dereference.pointer().type();
function_call_site_symbol.location = function_call.source_location();
function_call_site_symbol.location = source_location;
function_call_site_symbol.is_lvalue = true;
function_call_site_symbol.mode = goto_function_symbol_mode;
return function_call_site_symbol;
Expand Down
Loading