diff --git a/regression/goto-instrument/inline_09/test.desc b/regression/goto-instrument/inline_09/test.desc index db81237a3ad..b759f98597d 100644 --- a/regression/goto-instrument/inline_09/test.desc +++ b/regression/goto-instrument/inline_09/test.desc @@ -1,6 +1,6 @@ CORE main.c ---inline +--inline --remove-calls-no-body ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ @@ -9,4 +9,5 @@ main.c ^\s*a;$ no body.*[`]f -- +f\(\) ^warning: ignoring diff --git a/regression/goto-instrument/inline_16/main.c b/regression/goto-instrument/inline_16/main.c new file mode 100644 index 00000000000..751732260c5 --- /dev/null +++ b/regression/goto-instrument/inline_16/main.c @@ -0,0 +1,9 @@ +void func1(); + +int main() +{ + int ret; + + func1(); + ret = func2(); +} diff --git a/regression/goto-instrument/inline_16/test.desc b/regression/goto-instrument/inline_16/test.desc new file mode 100644 index 00000000000..9c0b7504b3c --- /dev/null +++ b/regression/goto-instrument/inline_16/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +func1\(\) +ret.*=.*func2\(\) +no body for function.*func1 +no body for function.*func2 +-- +^warning: ignoring diff --git a/regression/goto-instrument/inline_17/main.c b/regression/goto-instrument/inline_17/main.c new file mode 100644 index 00000000000..7a8350bc7de --- /dev/null +++ b/regression/goto-instrument/inline_17/main.c @@ -0,0 +1,9 @@ +void func1() +{ + func2(); +} + +int main() +{ + func1(); +} diff --git a/regression/goto-instrument/inline_17/test.desc b/regression/goto-instrument/inline_17/test.desc new file mode 100644 index 00000000000..7f43650ebe1 --- /dev/null +++ b/regression/goto-instrument/inline_17/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--function-inline func1 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +func1\(\) +func2\(\) +-- +^warning: ignoring diff --git a/regression/goto-instrument/remove-calls-no-body1/main.c b/regression/goto-instrument/remove-calls-no-body1/main.c new file mode 100644 index 00000000000..5aaa689adc6 --- /dev/null +++ b/regression/goto-instrument/remove-calls-no-body1/main.c @@ -0,0 +1,19 @@ +void func1(); + +void func3() +{ +} + +void func4() +{ + func1(); + func2(); +} + +void main() +{ + func1(); + func2(); + func3(); + func4(); +} diff --git a/regression/goto-instrument/remove-calls-no-body1/test.desc b/regression/goto-instrument/remove-calls-no-body1/test.desc new file mode 100644 index 00000000000..352bd62bced --- /dev/null +++ b/regression/goto-instrument/remove-calls-no-body1/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--remove-calls-no-body +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +func3\(\) +func4\(\) +-- +func1\(\) +func2\(\) +^warning: ignoring diff --git a/regression/goto-instrument/remove-calls-no-body2/main.c b/regression/goto-instrument/remove-calls-no-body2/main.c new file mode 100644 index 00000000000..d214adaf489 --- /dev/null +++ b/regression/goto-instrument/remove-calls-no-body2/main.c @@ -0,0 +1,21 @@ +int func1(int arg1, int arg2); + +void func3() +{ +} + +void func4() +{ + func1(567, 285); + func2(); +} + +void main() +{ + int ret1; + + ret1 = func1(567, 285); + func2(); + func3(); + func4(); +} diff --git a/regression/goto-instrument/remove-calls-no-body2/test.desc b/regression/goto-instrument/remove-calls-no-body2/test.desc new file mode 100644 index 00000000000..29c4bb40375 --- /dev/null +++ b/regression/goto-instrument/remove-calls-no-body2/test.desc @@ -0,0 +1,15 @@ +CORE +main.c +--remove-calls-no-body +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +func3\(\) +func4\(\) +567; +285; +ret1.*=.*NONDET +-- +func1\(.*\) +func2\(.*\) +^warning: ignoring diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 51574c30b50..a371065d8f6 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include #include @@ -729,6 +730,10 @@ int goto_instrument_parse_optionst::doit() status() << "Performing full inlining" << eom; goto_inline(goto_model, get_message_handler()); + status() << "Removing calls to functions without a body" << eom; + remove_calls_no_bodyt remove_calls_no_body; + remove_calls_no_body(goto_model.goto_functions); + status() << "Accelerating" << eom; accelerate_functions( goto_model, get_message_handler(), cmdline.isset("z3")); @@ -992,7 +997,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() // now do full inlining, if requested if(cmdline.isset("inline")) { - do_indirect_call_and_rtti_removal(); + do_indirect_call_and_rtti_removal(true); if(cmdline.isset("show-custom-bitvector-analysis") || cmdline.isset("custom-bitvector-analysis")) @@ -1003,7 +1008,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() } status() << "Performing full inlining" << eom; - goto_inline(goto_model, get_message_handler()); + goto_inline(goto_model, get_message_handler(), true); } if(cmdline.isset("show-custom-bitvector-analysis") || @@ -1111,27 +1116,23 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset("partial-inline")) { do_indirect_call_and_rtti_removal(); - do_partial_inlining(); + + status() << "Partial inlining" << eom; + goto_partial_inline(goto_model, ui_message_handler, 0, true); goto_model.goto_functions.update(); goto_model.goto_functions.compute_loop_numbers(); } - // now do full inlining, if requested - if(cmdline.isset("inline")) + if(cmdline.isset("remove-calls-no-body")) { - do_indirect_call_and_rtti_removal(/*force=*/true); + status() << "Removing calls to functions without a body" << eom; - if(cmdline.isset("show-custom-bitvector-analysis") || - cmdline.isset("custom-bitvector-analysis")) - { - do_remove_returns(); - thread_exit_instrumentation(goto_model); - mutex_init_instrumentation(goto_model); - } + remove_calls_no_bodyt remove_calls_no_body; + remove_calls_no_body(goto_model.goto_functions); - status() << "Performing full inlining" << eom; - goto_inline(goto_model, get_message_handler(), true); + goto_model.goto_functions.update(); + goto_model.goto_functions.compute_loop_numbers(); } if(cmdline.isset("constant-propagator")) @@ -1560,6 +1561,7 @@ void goto_instrument_parse_optionst::help() " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*) " --log log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*) " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*) + HELP_REMOVE_CALLS_NO_BODY HELP_REMOVE_CONST_FUNCTION_POINTERS " --add-library add models of C library functions\n" " --model-argc-argv model up to command line arguments\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 77e69dded9f..4c9ead8d0dc 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -19,6 +19,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -84,7 +85,8 @@ Author: Daniel Kroening, kroening@kroening.com "(show-threaded)(list-calls-args)(print-path-lengths)" \ "(undefined-function-is-assume-false)" \ "(remove-function-body):"\ - "(splice-call):" + "(splice-call):" \ + OPT_REMOVE_CALLS_NO_BODY // clang-format on class goto_instrument_parse_optionst: diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index e01482d883a..6ac8abfae36 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -40,6 +40,7 @@ SRC = basic_blocks.cpp \ read_goto_binary.cpp \ rebuild_goto_start_function.cpp \ remove_asm.cpp \ + remove_calls_no_body.cpp \ remove_complex.cpp \ remove_const_function_pointers.cpp \ remove_exceptions.cpp \ diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index d24f5257ef4..c58a85aa9be 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -380,59 +380,6 @@ void goto_inlinet::insert_function_body( dest.destructive_insert(target, tmp); } -void goto_inlinet::insert_function_nobody( - goto_programt &dest, - const exprt &lhs, - goto_programt::targett target, - const symbol_exprt &function, - const exprt::operandst &arguments) -{ - PRECONDITION(target->is_function_call()); - PRECONDITION(!dest.empty()); - - const irep_idt identifier=function.get_identifier(); - - if(no_body_set.insert(identifier).second) // newly inserted - { - warning().source_location=function.find_source_location(); - warning() << "no body for function `" << identifier << "'" << eom; - } - - goto_programt tmp; - - // evaluate function arguments -- they might have - // pointer dereferencing or the like - forall_expr(it, arguments) - { - goto_programt::targett t=tmp.add_instruction(); - t->make_other(code_expressiont(*it)); - t->source_location=target->source_location; - t->function=target->function; - } - - // return value - if(lhs.is_not_nil()) - { - side_effect_expr_nondett rhs(lhs.type()); - rhs.add_source_location()=target->source_location; - - code_assignt code(lhs, rhs); - code.add_source_location()=target->source_location; - - goto_programt::targett t=tmp.add_instruction(ASSIGN); - t->source_location=target->source_location; - t->function=target->function; - t->code.swap(code); - } - - // kill call - target->type=LOCATION; - target->code.clear(); - target++; - - dest.destructive_insert(target, tmp); -} - void goto_inlinet::expand_function_call( goto_programt &dest, const inline_mapt &inline_map, @@ -551,7 +498,13 @@ void goto_inlinet::expand_function_call( } else // no body available { - insert_function_nobody(dest, lhs, target, function, arguments); + const irep_idt identifier = function.get_identifier(); + + if(no_body_set.insert(identifier).second) // newly inserted + { + warning().source_location = function.find_source_location(); + warning() << "no body for function `" << identifier << "'" << eom; + } } } diff --git a/src/goto-programs/goto_inline_class.h b/src/goto-programs/goto_inline_class.h index 2dad1229191..de59b889cac 100644 --- a/src/goto-programs/goto_inline_class.h +++ b/src/goto-programs/goto_inline_class.h @@ -172,13 +172,6 @@ class goto_inlinet:public messaget const symbol_exprt &function, const exprt::operandst &arguments); - void insert_function_nobody( - goto_programt &dest, - const exprt &lhs, - goto_programt::targett target, - const symbol_exprt &function, - const exprt::operandst &arguments); - void replace_return( goto_programt &body, const exprt &lhs); diff --git a/src/goto-programs/remove_calls_no_body.cpp b/src/goto-programs/remove_calls_no_body.cpp new file mode 100644 index 00000000000..b8e46c41edf --- /dev/null +++ b/src/goto-programs/remove_calls_no_body.cpp @@ -0,0 +1,129 @@ +/*******************************************************************\ + +Module: Remove calls to functions without a body + +Author: Daniel Poetzl + +\*******************************************************************/ + +/// \file +/// Remove calls to functions without a body + +#include +#include "remove_calls_no_body.h" + +/// Remove a single call +/// \param goto_program: goto program to modify +/// \param target: iterator pointing to the call +/// \param lhs: lhs of the call to which the return value is assigned +/// \param arguments: arguments of the call +void remove_calls_no_bodyt::remove_call_no_body( + goto_programt &goto_program, + goto_programt::targett target, + const exprt &lhs, + const exprt::operandst &arguments) +{ + PRECONDITION(target->is_function_call()); + PRECONDITION(!goto_program.empty()); + + goto_programt tmp; + + // evaluate function arguments -- they might have + // pointer dereferencing or the like + for(const exprt &argument : arguments) + { + goto_programt::targett t = tmp.add_instruction(); + t->make_other(code_expressiont(argument)); + t->source_location = target->source_location; + t->function = target->function; + } + + // return value + if(lhs.is_not_nil()) + { + side_effect_expr_nondett rhs(lhs.type()); + rhs.add_source_location() = target->source_location; + + code_assignt code(lhs, rhs); + code.add_source_location() = target->source_location; + + goto_programt::targett t = tmp.add_instruction(ASSIGN); + t->source_location = target->source_location; + t->function = target->function; + t->code.swap(code); + } + + // kill call + target->type = LOCATION; + target->code.clear(); + target++; + + goto_program.destructive_insert(target, tmp); +} + +/// Check if instruction is a call to an opaque function through an ordinary +/// (non-function pointer) call. +/// \param target: iterator pointing to the instruction to check +/// \param goto_functions: all goto function to look up call target +bool remove_calls_no_bodyt::is_opaque_function_call( + const goto_programt::const_targett target, + const goto_functionst &goto_functions) +{ + if(!target->is_function_call()) + return false; + + const code_function_callt &cfc = to_code_function_call(target->code); + const exprt &f = cfc.function(); + + if(f.id() != ID_symbol) + return false; + + const symbol_exprt &se = to_symbol_expr(f); + const irep_idt id = se.get_identifier(); + + goto_functionst::function_mapt::const_iterator f_it = + goto_functions.function_map.find(id); + + if(f_it != goto_functions.function_map.end()) + { + return !f_it->second.body_available(); + } + + return false; +} + +/// Remove calls to functions without a body and replace them with evaluations +/// of the arguments of the call and a nondet assignment to the variable taking +/// the return value. +/// \param goto_program: goto program to operate on +/// \param goto_functions: all goto functions; for looking up functions which +/// the goto program may call +void remove_calls_no_bodyt:: +operator()(goto_programt &goto_program, const goto_functionst &goto_functions) +{ + for(goto_programt::targett it = goto_program.instructions.begin(); + it != goto_program.instructions.end();) // no it++ + { + if(is_opaque_function_call(it, goto_functions)) + { + const code_function_callt &cfc = to_code_function_call(it->code); + remove_call_no_body(goto_program, it, cfc.lhs(), cfc.arguments()); + } + else + { + it++; + } + } +} + +/// Remove calls to functions without a body and replace them with evaluations +/// of the arguments of the call and a nondet assignment to the variable taking +/// the return value. +/// \param goto_functions: goto functions to operate on +void remove_calls_no_bodyt::operator()(goto_functionst &goto_functions) +{ + Forall_goto_functions(f_it, goto_functions) + { + (*this)(f_it->second.body, goto_functions); + } +} diff --git a/src/goto-programs/remove_calls_no_body.h b/src/goto-programs/remove_calls_no_body.h new file mode 100644 index 00000000000..de10c426f2e --- /dev/null +++ b/src/goto-programs/remove_calls_no_body.h @@ -0,0 +1,43 @@ +/*******************************************************************\ + +Module: Remove calls to functions without a body + +Author: Daniel Poetzl + +\*******************************************************************/ + +/// \file +/// Remove calls to functions without a body + +#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_CALLS_NO_BODY_H +#define CPROVER_GOTO_PROGRAMS_REMOVE_CALLS_NO_BODY_H + +#include "goto_functions.h" + +class remove_calls_no_bodyt +{ +protected: + bool is_opaque_function_call( + const goto_programt::const_targett target, + const goto_functionst &goto_functions); + + void remove_call_no_body( + goto_programt &dest, + goto_programt::targett target, + const exprt &lhs, + const exprt::operandst &arguments); + +public: + void operator()( + goto_programt &goto_program, + const goto_functionst &goto_functions); + + void operator()(goto_functionst &goto_functions); +}; + +#define OPT_REMOVE_CALLS_NO_BODY "(remove-calls-no-body)" + +#define HELP_REMOVE_CALLS_NO_BODY \ + " --remove-calls-no-body remove calls to functions without a body\n" + +#endif // CPROVER_GOTO_PROGRAMS_REMOVE_CALLS_NO_BODY_H