diff --git a/regression/goto-instrument/replace-calls-01/main.c b/regression/goto-instrument/replace-calls-01/main.c new file mode 100644 index 00000000000..6d465e4702c --- /dev/null +++ b/regression/goto-instrument/replace-calls-01/main.c @@ -0,0 +1,17 @@ +int f(int a) +{ + return a; +} + +int g(int b) +{ + return b + 1; +} + +int main() +{ + int r; + + r = f(0); + assert(r == 1); +} diff --git a/regression/goto-instrument/replace-calls-01/test.desc b/regression/goto-instrument/replace-calls-01/test.desc new file mode 100644 index 00000000000..7c5582321b5 --- /dev/null +++ b/regression/goto-instrument/replace-calls-01/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--replace-calls f:g +g\(0\); +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +f\(0\); +^warning: ignoring diff --git a/regression/goto-instrument/replace-calls-02/main.c b/regression/goto-instrument/replace-calls-02/main.c new file mode 100644 index 00000000000..688997604b6 --- /dev/null +++ b/regression/goto-instrument/replace-calls-02/main.c @@ -0,0 +1,30 @@ +int f() +{ + return 0; +} + +int g() +{ + return 1; +} + +int h() +{ + return 2; +} + +int i() +{ + return 3; +} + +int main() +{ + int r; + + r = f(); + assert(r == 1); + + r = h(); + assert(r == 3); +} diff --git a/regression/goto-instrument/replace-calls-02/test.desc b/regression/goto-instrument/replace-calls-02/test.desc new file mode 100644 index 00000000000..a63737f5209 --- /dev/null +++ b/regression/goto-instrument/replace-calls-02/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--replace-calls f:g --replace-calls h:i +g\(\); +i\(\); +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +f\(\); +h\(\); +^warning: ignoring diff --git a/regression/goto-instrument/replace-calls-03/main.c b/regression/goto-instrument/replace-calls-03/main.c new file mode 100644 index 00000000000..ae6f92aa294 --- /dev/null +++ b/regression/goto-instrument/replace-calls-03/main.c @@ -0,0 +1,14 @@ +int f() +{ + return 0; +} + +char g() +{ + return 1; +} + +int main() +{ + f(); +} diff --git a/regression/goto-instrument/replace-calls-03/test.desc b/regression/goto-instrument/replace-calls-03/test.desc new file mode 100644 index 00000000000..736743235e7 --- /dev/null +++ b/regression/goto-instrument/replace-calls-03/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--replace-calls f:g +Functions f and g are not type-compatible +^EXIT=11$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/replace-calls-04/main.c b/regression/goto-instrument/replace-calls-04/main.c new file mode 100644 index 00000000000..db9da258cfb --- /dev/null +++ b/regression/goto-instrument/replace-calls-04/main.c @@ -0,0 +1,14 @@ +void f(int a) +{ + return 0; +} + +void g(unsigned a) +{ + return 1; +} + +int main() +{ + f(0); +} diff --git a/regression/goto-instrument/replace-calls-04/test.desc b/regression/goto-instrument/replace-calls-04/test.desc new file mode 100644 index 00000000000..736743235e7 --- /dev/null +++ b/regression/goto-instrument/replace-calls-04/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--replace-calls f:g +Functions f and g are not type-compatible +^EXIT=11$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/replace-calls-05/main.c b/regression/goto-instrument/replace-calls-05/main.c new file mode 100644 index 00000000000..7d7121aef27 --- /dev/null +++ b/regression/goto-instrument/replace-calls-05/main.c @@ -0,0 +1,8 @@ +void g() +{ +} + +int main() +{ + return 0; +} diff --git a/regression/goto-instrument/replace-calls-05/test.desc b/regression/goto-instrument/replace-calls-05/test.desc new file mode 100644 index 00000000000..b88d8154f9e --- /dev/null +++ b/regression/goto-instrument/replace-calls-05/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--replace-calls f:g --replace-calls h:f +Function f cannot both be replaced and be a replacement +^EXIT=11$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/goto-instrument/replace-calls-06/main.c b/regression/goto-instrument/replace-calls-06/main.c new file mode 100644 index 00000000000..ba8df000690 --- /dev/null +++ b/regression/goto-instrument/replace-calls-06/main.c @@ -0,0 +1,23 @@ +int f() +{ + return 0; +} + +int g() +{ + return 1; +} + +int main() +{ + int (*h)(void); + + h = g; + h = f; + + int r; + r = h(); + assert(r == 1); + + return 0; +} diff --git a/regression/goto-instrument/replace-calls-06/test.desc b/regression/goto-instrument/replace-calls-06/test.desc new file mode 100644 index 00000000000..2d08e72c37a --- /dev/null +++ b/regression/goto-instrument/replace-calls-06/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--replace-calls f:g +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +f\(\); +^warning: ignoring diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 4582509df7d..085e7e0094c 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1063,6 +1063,14 @@ void goto_instrument_parse_optionst::instrument_goto_program() do_remove_const_function_pointers_only(); } + if(cmdline.isset("replace-calls")) + { + do_indirect_call_and_rtti_removal(); + + replace_callst replace_calls; + replace_calls(goto_model, cmdline.get_values("replace-calls")); + } + if(cmdline.isset("function-inline")) { std::string function=cmdline.get_value("function-inline"); @@ -1628,6 +1636,7 @@ void goto_instrument_parse_optionst::help() " --model-argc-argv model up to command line arguments\n" // NOLINTNEXTLINE(whitespace/line_length) " --remove-function-body remove the implementation of function (may be repeated)\n" + HELP_REPLACE_CALLS "\n" "Other options:\n" " --no-system-headers with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*) diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 706083df63e..5f55a73792f 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -97,7 +98,9 @@ Author: Daniel Kroening, kroening@kroening.com OPT_REMOVE_CALLS_NO_BODY \ OPT_REPLACE_FUNCTION_BODY \ OPT_GOTO_PROGRAM_STATS \ - "(show-local-safe-pointers)(show-safe-dereferences)" + "(show-local-safe-pointers)(show-safe-dereferences)" \ + OPT_REPLACE_CALLS \ + // empty last line // clang-format on diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index a872810518d..3dfa58eed2b 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -6,7 +6,7 @@ SRC = adjust_float_expressions.cpp \ destructor.cpp \ elf_reader.cpp \ format_strings.cpp \ - initialize_goto_model.cpp \ + generate_function_bodies.cpp \ goto_asm.cpp \ goto_clean_expr.cpp \ goto_convert.cpp \ @@ -16,12 +16,13 @@ SRC = adjust_float_expressions.cpp \ goto_convert_side_effect.cpp \ goto_function.cpp \ goto_functions.cpp \ - goto_inline.cpp \ goto_inline_class.cpp \ + goto_inline.cpp \ goto_program.cpp \ goto_program_template.cpp \ goto_trace.cpp \ graphml_witness.cpp \ + initialize_goto_model.cpp \ instrument_preconditions.cpp \ interpreter.cpp \ interpreter_evaluate.cpp \ @@ -50,7 +51,7 @@ SRC = adjust_float_expressions.cpp \ remove_unused_functions.cpp \ remove_vector.cpp \ remove_virtual_functions.cpp \ - generate_function_bodies.cpp \ + replace_calls.cpp \ resolve_inherited_component.cpp \ safety_checker.cpp \ set_properties.cpp \ diff --git a/src/goto-programs/replace_calls.cpp b/src/goto-programs/replace_calls.cpp new file mode 100644 index 00000000000..2552dff0424 --- /dev/null +++ b/src/goto-programs/replace_calls.cpp @@ -0,0 +1,167 @@ +/*******************************************************************\ + +Module: Replace calls + +Author: Daniel Poetzl + +\*******************************************************************/ + +/// \file +/// Replace calls +/// Replaces calls to given functions with calls to other given functions. Needs +/// to be run after removing function pointer calls and before removing returns. + +#include "replace_calls.h" + +#include + +#include +#include +#include +#include +#include + +/// Replace function calls with calls to other functions +/// \param goto_model: goto model to modify +/// \param replacement_list: list of strings, with each string f:g denoting a +/// mapping between functions names; a mapping f -> g indicates that calls to +/// f should be replaced by calls to g +void replace_callst::operator()( + goto_modelt &goto_model, + const replacement_listt &replacement_list) const +{ + replacement_mapt replacement_map = parse_replacement_list(replacement_list); + (*this)(goto_model, replacement_map); +} + +/// Replace function calls with calls to other functions +/// \param goto_model: goto model to modify +/// \param replacement_map: mapping between function names; a mapping f -> g +/// indicates that calls to f should be replaced by calls to g +void replace_callst::operator()( + goto_modelt &goto_model, + const replacement_mapt &replacement_map) const +{ + const namespacet ns(goto_model.symbol_table); + goto_functionst &goto_functions = goto_model.goto_functions; + + check_replacement_map(replacement_map, goto_functions, ns); + + for(auto &p : goto_functions.function_map) + { + goto_functionst::goto_functiont &goto_function = p.second; + goto_programt &goto_program = goto_function.body; + + (*this)(goto_program, goto_functions, ns, replacement_map); + } +} + +void replace_callst::operator()( + goto_programt &goto_program, + const goto_functionst &goto_functions, + const namespacet &ns, + const replacement_mapt &replacement_map) const +{ + Forall_goto_program_instructions(it, goto_program) + { + goto_programt::instructiont &ins = *it; + + if(!ins.is_function_call()) + continue; + + code_function_callt &cfc = to_code_function_call(ins.code); + exprt &function = cfc.function(); + + PRECONDITION(function.id() == ID_symbol); + + symbol_exprt &se = to_symbol_expr(function); + const irep_idt &id = se.get_identifier(); + + auto f_it1 = goto_functions.function_map.find(id); + + DATA_INVARIANT( + f_it1 != goto_functions.function_map.end(), + "Called functions need to be present"); + + replacement_mapt::const_iterator r_it = replacement_map.find(id); + + if(r_it == replacement_map.end()) + continue; + + const irep_idt &new_id = r_it->second; + + auto f_it2 = goto_functions.function_map.find(new_id); + PRECONDITION(f_it2 != goto_functions.function_map.end()); + + PRECONDITION(base_type_eq(f_it1->second.type, f_it2->second.type, ns)); + + // check that returns have not been removed + goto_programt::const_targett next_it = std::next(it); + if(next_it != goto_program.instructions.end() && next_it->is_assign()) + { + const code_assignt &ca = to_code_assign(next_it->code); + const exprt &rhs = ca.rhs(); + + if(rhs.id() == ID_symbol) + { + const symbol_exprt &se = to_symbol_expr(rhs); + if(has_suffix(id2string(se.get_identifier()), RETURN_VALUE_SUFFIX)) + throw "Returns must not be removed before replacing calls"; + } + } + + // Finally modify the call + function.type() = f_it2->second.type; + se.set_identifier(new_id); + } +} + +replace_callst::replacement_mapt replace_callst::parse_replacement_list( + const replacement_listt &replacement_list) const +{ + replacement_mapt replacement_map; + + for(const std::string &s : replacement_list) + { + std::string original; + std::string replacement; + + split_string(s, ':', original, replacement, true); + + const auto r = + replacement_map.insert(std::make_pair(original, replacement)); + + if(!r.second) + throw "Conflicting replacement for function " + original; + } + + return replacement_map; +} + +void replace_callst::check_replacement_map( + const replacement_mapt &replacement_map, + const goto_functionst &goto_functions, + const namespacet &ns) const +{ + for(const auto &p : replacement_map) + { + if(replacement_map.find(p.second) != replacement_map.end()) + throw "Function " + id2string(p.second) + + " cannot both be replaced and " + "be a replacement"; + + auto it2 = goto_functions.function_map.find(p.second); + + if(it2 == goto_functions.function_map.end()) + throw "Replacement function " + id2string(p.second) + + " needs to be present"; + + auto it1 = goto_functions.function_map.find(p.first); + if(it1 != goto_functions.function_map.end()) + { + if(!base_type_eq(it1->second.type, it2->second.type, ns)) + throw "Functions " + id2string(p.first) + " and " + + id2string(p.second) + " are not type-compatible"; + } + } +} diff --git a/src/goto-programs/replace_calls.h b/src/goto-programs/replace_calls.h new file mode 100644 index 00000000000..628ec3726a9 --- /dev/null +++ b/src/goto-programs/replace_calls.h @@ -0,0 +1,53 @@ +/*******************************************************************\ + +Module: Replace calls + +Author: Daniel Poetzl + +\*******************************************************************/ + +/// \file +/// Replace calls to given functions with calls to other given +/// functions + +#ifndef CPROVER_GOTO_PROGRAMS_REPLACE_CALLS_H +#define CPROVER_GOTO_PROGRAMS_REPLACE_CALLS_H + +#include "goto_model.h" + +class replace_callst +{ +public: + typedef std::list replacement_listt; + typedef std::map replacement_mapt; + + void operator()( + goto_modelt &goto_model, + const replacement_listt &replacement_list) const; + + void operator()( + goto_modelt &goto_model, + const replacement_mapt &replacement_map) const; + +protected: + void operator()( + goto_programt &goto_program, + const goto_functionst &goto_functions, + const namespacet &ns, + const replacement_mapt &replacement_map) const; + + replacement_mapt + parse_replacement_list(const replacement_listt &replacement_list) const; + + void check_replacement_map( + const replacement_mapt &replacement_map, + const goto_functionst &goto_functions, + const namespacet &ns) const; +}; + +#define OPT_REPLACE_CALLS "(replace-calls):" + +#define HELP_REPLACE_CALLS \ + " --replace-calls f:g replace calls to f with calls to g\n" + +#endif // CPROVER_GOTO_PROGRAMS_REPLACE_CALLS_H