Skip to content

Commit b829c54

Browse files
authored
Merge pull request #6281 from diffblue/goto_instruction_function_call
introduce instructiont::call_function() and related methods
2 parents 04d2f06 + 41e54d7 commit b829c54

12 files changed

+124
-120
lines changed

src/analyses/constant_propagator.cpp

+7-19
Original file line numberDiff line numberDiff line change
@@ -192,8 +192,7 @@ void constant_propagator_domaint::transform(
192192
}
193193
else if(from->is_function_call())
194194
{
195-
const auto &function_call = from->get_function_call();
196-
const exprt &function=function_call.function();
195+
const exprt &function = from->call_function();
197196

198197
if(function.id()==ID_symbol)
199198
{
@@ -231,8 +230,8 @@ void constant_propagator_domaint::transform(
231230
const code_typet &code_type=to_code_type(symbol.type);
232231
const code_typet::parameterst &parameters=code_type.parameters();
233232

234-
const code_function_callt::argumentst &arguments=
235-
function_call.arguments();
233+
const code_function_callt::argumentst &arguments =
234+
from->call_arguments();
236235

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

782-
bool call_changed = false;
783-
784-
if(!constant_propagator_domaint::partial_evaluate(
785-
d.values, call.function(), ns))
786-
{
787-
call_changed = true;
788-
}
789-
790-
for(auto &arg : call.arguments())
791-
if(!constant_propagator_domaint::partial_evaluate(d.values, arg, ns))
792-
call_changed = true;
793-
794-
if(call_changed)
795-
it->set_function_call(call);
782+
for(auto &arg : it->call_arguments())
783+
constant_propagator_domaint::partial_evaluate(d.values, arg, ns);
796784
}
797785
else if(it->is_other())
798786
{

src/goto-programs/cfg.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -391,7 +391,7 @@ void cfg_baset<T, P, I>::compute_edges_function_call(
391391
goto_programt::const_targett next_PC,
392392
entryt &entry)
393393
{
394-
const exprt &function = instruction.get_function_call().function();
394+
const exprt &function = instruction.call_function();
395395

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

446446
if(function.id()!=ID_symbol)
447447
return;

src/goto-programs/goto_inline_class.cpp

+3-5
Original file line numberDiff line numberDiff line change
@@ -436,11 +436,9 @@ void goto_inlinet::get_call(
436436
{
437437
PRECONDITION(it->is_function_call());
438438

439-
const code_function_callt &call = it->get_function_call();
440-
441-
lhs=call.lhs();
442-
function=call.function();
443-
arguments=call.arguments();
439+
lhs = it->call_lhs();
440+
function = it->call_function();
441+
arguments = it->call_arguments();
444442
}
445443

446444
/// Inline all of the given call locations.

src/goto-programs/goto_program.cpp

+14-39
Original file line numberDiff line numberDiff line change
@@ -329,14 +329,11 @@ std::list<exprt> expressions_read(
329329
break;
330330

331331
case FUNCTION_CALL:
332-
{
333-
const code_function_callt &function_call = instruction.get_function_call();
334-
for(const auto &argument : function_call.arguments())
332+
for(const auto &argument : instruction.call_arguments())
335333
dest.push_back(argument);
336-
if(function_call.lhs().is_not_nil())
337-
parse_lhs_read(function_call.lhs(), dest);
334+
if(instruction.call_lhs().is_not_nil())
335+
parse_lhs_read(instruction.call_lhs(), dest);
338336
break;
339-
}
340337

341338
case ASSIGN:
342339
dest.push_back(instruction.assign_rhs());
@@ -371,12 +368,8 @@ std::list<exprt> expressions_written(
371368
switch(instruction.type)
372369
{
373370
case FUNCTION_CALL:
374-
{
375-
const code_function_callt &function_call =
376-
instruction.get_function_call();
377-
if(function_call.lhs().is_not_nil())
378-
dest.push_back(function_call.lhs());
379-
}
371+
if(instruction.call_lhs().is_not_nil())
372+
dest.push_back(instruction.call_lhs());
380373
break;
381374

382375
case ASSIGN:
@@ -999,35 +992,20 @@ void goto_programt::instructiont::transform(
999992

1000993
case FUNCTION_CALL:
1001994
{
1002-
auto new_call = get_function_call();
1003-
bool change = false;
1004-
1005-
auto new_lhs = f(new_call.lhs());
995+
auto new_lhs = f(call_lhs());
1006996
if(new_lhs.has_value())
1007-
{
1008-
new_call.lhs() = *new_lhs;
1009-
change = true;
1010-
}
997+
call_lhs() = *new_lhs;
1011998

1012-
auto new_function = f(new_call.function());
1013-
if(new_function.has_value())
1014-
{
1015-
new_call.function() = *new_function;
1016-
change = true;
1017-
}
999+
auto new_call_function = f(call_function());
1000+
if(new_call_function.has_value())
1001+
call_function() = *new_call_function;
10181002

1019-
for(auto &a : new_call.arguments())
1003+
for(auto &a : call_arguments())
10201004
{
10211005
auto new_a = f(a);
10221006
if(new_a.has_value())
1023-
{
10241007
a = *new_a;
1025-
change = true;
1026-
}
10271008
}
1028-
1029-
if(change)
1030-
set_function_call(new_call);
10311009
}
10321010
break;
10331011

@@ -1082,13 +1060,10 @@ void goto_programt::instructiont::apply(
10821060
break;
10831061

10841062
case FUNCTION_CALL:
1085-
{
1086-
const auto &call = get_function_call();
1087-
f(call.lhs());
1088-
for(auto &a : call.arguments())
1063+
f(call_lhs());
1064+
for(auto &a : call_arguments())
10891065
f(a);
1090-
}
1091-
break;
1066+
break;
10921067

10931068
case GOTO:
10941069
case ASSUME:

src/goto-programs/goto_program.h

+56
Original file line numberDiff line numberDiff line change
@@ -344,18 +344,74 @@ class goto_programt
344344
}
345345

346346
/// Get the function call for FUNCTION_CALL
347+
#if 1
348+
DEPRECATED(SINCE(
349+
2021,
350+
2,
351+
24,
352+
"Use call_function(), call_lhs(), call_arguments() instead"))
347353
const code_function_callt &get_function_call() const
348354
{
349355
PRECONDITION(is_function_call());
350356
return to_code_function_call(code);
351357
}
358+
#endif
359+
360+
/// Get the function that is called for FUNCTION_CALL
361+
const exprt &call_function() const
362+
{
363+
PRECONDITION(is_function_call());
364+
return to_code_function_call(code).function();
365+
}
366+
367+
/// Get the function that is called for FUNCTION_CALL
368+
exprt &call_function()
369+
{
370+
PRECONDITION(is_function_call());
371+
return to_code_function_call(code).function();
372+
}
373+
374+
/// Get the lhs of a FUNCTION_CALL (may be nil)
375+
const exprt &call_lhs() const
376+
{
377+
PRECONDITION(is_function_call());
378+
return to_code_function_call(code).lhs();
379+
}
380+
381+
/// Get the lhs of a FUNCTION_CALL (may be nil)
382+
exprt &call_lhs()
383+
{
384+
PRECONDITION(is_function_call());
385+
return to_code_function_call(code).lhs();
386+
}
387+
388+
/// Get the arguments of a FUNCTION_CALL
389+
const exprt::operandst &call_arguments() const
390+
{
391+
PRECONDITION(is_function_call());
392+
return to_code_function_call(code).arguments();
393+
}
394+
395+
/// Get the arguments of a FUNCTION_CALL
396+
exprt::operandst &call_arguments()
397+
{
398+
PRECONDITION(is_function_call());
399+
return to_code_function_call(code).arguments();
400+
}
352401

353402
/// Set the function call for FUNCTION_CALL
403+
#if 1
404+
DEPRECATED(SINCE(
405+
2021,
406+
2,
407+
24,
408+
"Use call_function(), call_lhs(), call_arguments() instead"))
354409
void set_function_call(code_function_callt c)
355410
{
356411
PRECONDITION(is_function_call());
357412
code = std::move(c);
358413
}
414+
#endif
359415

360416
/// Get the statement for OTHER
361417
const codet &get_other() const

src/goto-programs/instrument_preconditions.cpp

+9-10
Original file line numberDiff line numberDiff line change
@@ -64,14 +64,14 @@ void remove_preconditions(goto_programt &goto_program)
6464
}
6565

6666
replace_symbolt actuals_replace_map(
67-
const code_function_callt &call,
67+
const goto_programt::instructiont &call,
6868
const namespacet &ns)
6969
{
70-
PRECONDITION(call.function().id()==ID_symbol);
71-
const symbolt &s=ns.lookup(to_symbol_expr(call.function()));
70+
PRECONDITION(call.call_function().id() == ID_symbol);
71+
const symbolt &s = ns.lookup(to_symbol_expr(call.call_function()));
7272
const auto &code_type=to_code_type(s.type);
7373
const auto &parameters=code_type.parameters();
74-
const auto &arguments=call.arguments();
74+
const auto &arguments = call.call_arguments();
7575

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

107-
if(call.function().id()==ID_symbol)
107+
if(called_function.id() == ID_symbol)
108108
{
109-
auto preconditions=
110-
get_preconditions(to_symbol_expr(call.function()),
111-
goto_model.goto_functions);
109+
auto preconditions = get_preconditions(
110+
to_symbol_expr(called_function), goto_model.goto_functions);
112111

113112
source_locationt source_location=it->source_location;
114113

115-
replace_symbolt r=actuals_replace_map(call, ns);
114+
replace_symbolt r = actuals_replace_map(*it, ns);
116115

117116
// add before the call, with location of the call
118117
for(const auto &p : preconditions)

src/goto-programs/interpreter.cpp

+11-10
Original file line numberDiff line numberDiff line change
@@ -739,10 +739,12 @@ void interpretert::execute_assert()
739739

740740
void interpretert::execute_function_call()
741741
{
742-
const code_function_callt &function_call = pc->get_function_call();
742+
const auto &call_lhs = pc->call_lhs();
743+
const auto &call_function = pc->call_function();
744+
const auto &call_arguments = pc->call_arguments();
743745

744746
// function to be called
745-
mp_integer address=evaluate_address(function_call.function());
747+
mp_integer address = evaluate_address(call_function);
746748

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

770-
if(function_call.lhs().is_not_nil())
771-
return_value_address=
772-
evaluate_address(function_call.lhs());
772+
if(call_lhs.is_not_nil())
773+
return_value_address = evaluate_address(call_lhs);
773774
else
774775
return_value_address=0;
775776

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

779-
argument_values.resize(function_call.arguments().size());
780+
argument_values.resize(call_arguments.size());
780781

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

784785
// do the call
785786

@@ -821,8 +822,8 @@ void interpretert::execute_function_call()
821822
}
822823
else
823824
{
824-
list_input_varst::iterator it = function_input_vars.find(
825-
to_symbol_expr(function_call.function()).get_identifier());
825+
list_input_varst::iterator it =
826+
function_input_vars.find(to_symbol_expr(call_function).get_identifier());
826827

827828
if(it!=function_input_vars.end())
828829
{

src/goto-programs/label_function_pointer_call_sites.cpp

+5-6
Original file line numberDiff line numberDiff line change
@@ -21,14 +21,13 @@ void label_function_pointer_call_sites(goto_modelt &goto_model)
2121
for_each_instruction_if(
2222
goto_function.second,
2323
[](const goto_programt::targett it) {
24-
return it->is_function_call() && can_cast_expr<dereference_exprt>(
25-
it->get_function_call().function());
24+
return it->is_function_call() &&
25+
can_cast_expr<dereference_exprt>(it->call_function());
2626
},
2727
[&](goto_programt::targett &it) {
28-
auto const &function_call = it->get_function_call();
2928
auto const &function_pointer_dereference =
30-
to_dereference_expr(function_call.function());
31-
auto const &source_location = function_call.source_location();
29+
to_dereference_expr(it->call_function());
30+
auto const &source_location = it->source_location;
3231
auto const &goto_function_symbol_mode =
3332
goto_model.symbol_table.lookup_ref(goto_function.first).mode;
3433

@@ -43,7 +42,7 @@ void label_function_pointer_call_sites(goto_modelt &goto_model)
4342
function_call_site_symbol.pretty_name = call_site_symbol_name;
4443
function_call_site_symbol.type =
4544
function_pointer_dereference.pointer().type();
46-
function_call_site_symbol.location = function_call.source_location();
45+
function_call_site_symbol.location = source_location;
4746
function_call_site_symbol.is_lvalue = true;
4847
function_call_site_symbol.mode = goto_function_symbol_mode;
4948
return function_call_site_symbol;

0 commit comments

Comments
 (0)