From bc2c0cd5bbd82df7200c0607598546696bc39346 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 12 Jun 2017 18:31:01 +0100 Subject: [PATCH 1/2] Inliner fixes --- .../goto_instrument_parse_options.cpp | 27 +++++-------------- src/goto-programs/goto_inline.cpp | 2 +- src/goto-programs/goto_inline_class.h | 1 - 3 files changed, 7 insertions(+), 23 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 51574c30b50..32600a7b5fd 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -992,7 +992,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(/*force=*/true); if(cmdline.isset("show-custom-bitvector-analysis") || cmdline.isset("custom-bitvector-analysis")) @@ -1003,7 +1003,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 +1111,12 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset("partial-inline")) { do_indirect_call_and_rtti_removal(); - do_partial_inlining(); - goto_model.goto_functions.update(); - goto_model.goto_functions.compute_loop_numbers(); - } - - // now do full inlining, if requested - if(cmdline.isset("inline")) - { - do_indirect_call_and_rtti_removal(/*force=*/true); + status() << "Partial inlining" << eom; + goto_partial_inline(goto_functions, ns, ui_message_handler, 0, true); - 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); - } - - status() << "Performing full inlining" << eom; - goto_inline(goto_model, get_message_handler(), true); + goto_functions.update(); + goto_functions.compute_loop_numbers(); } if(cmdline.isset("constant-propagator")) diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp index 62957297922..38dc8455c5c 100644 --- a/src/goto-programs/goto_inline.cpp +++ b/src/goto-programs/goto_inline.cpp @@ -79,7 +79,7 @@ void goto_inline( Forall_goto_program_instructions(i_it, goto_program) { - if(!i_it->is_function_call()) + if(!goto_inlinet::is_call(i_it)) continue; call_list.push_back(goto_inlinet::callt(i_it, false)); diff --git a/src/goto-programs/goto_inline_class.h b/src/goto-programs/goto_inline_class.h index 2dad1229191..bbeb1e8397c 100644 --- a/src/goto-programs/goto_inline_class.h +++ b/src/goto-programs/goto_inline_class.h @@ -6,7 +6,6 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ - #ifndef CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H #define CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H From 7e5922accfd399a1b247e16dd31f49465d918e9c Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 13 Jun 2017 18:12:55 +0100 Subject: [PATCH 2/2] remove functions without a body --- .../goto-instrument/inline_09/test.desc | 3 +- regression/goto-instrument/inline_16/main.c | 9 ++ .../goto-instrument/inline_16/test.desc | 12 ++ regression/goto-instrument/inline_17/main.c | 9 ++ .../goto-instrument/inline_17/test.desc | 10 ++ .../remove-calls-no-body1/main.c | 19 +++ .../remove-calls-no-body1/test.desc | 12 ++ .../remove-calls-no-body2/main.c | 21 +++ .../remove-calls-no-body2/test.desc | 15 ++ .../goto_instrument_parse_options.cpp | 25 +++- .../goto_instrument_parse_options.h | 4 +- src/goto-programs/Makefile | 1 + src/goto-programs/goto_inline.cpp | 2 +- src/goto-programs/goto_inline_class.cpp | 61 +-------- src/goto-programs/goto_inline_class.h | 8 +- src/goto-programs/remove_calls_no_body.cpp | 129 ++++++++++++++++++ src/goto-programs/remove_calls_no_body.h | 43 ++++++ 17 files changed, 315 insertions(+), 68 deletions(-) create mode 100644 regression/goto-instrument/inline_16/main.c create mode 100644 regression/goto-instrument/inline_16/test.desc create mode 100644 regression/goto-instrument/inline_17/main.c create mode 100644 regression/goto-instrument/inline_17/test.desc create mode 100644 regression/goto-instrument/remove-calls-no-body1/main.c create mode 100644 regression/goto-instrument/remove-calls-no-body1/test.desc create mode 100644 regression/goto-instrument/remove-calls-no-body2/main.c create mode 100644 regression/goto-instrument/remove-calls-no-body2/test.desc create mode 100644 src/goto-programs/remove_calls_no_body.cpp create mode 100644 src/goto-programs/remove_calls_no_body.h 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 32600a7b5fd..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(/*force=*/true); + do_indirect_call_and_rtti_removal(true); if(cmdline.isset("show-custom-bitvector-analysis") || cmdline.isset("custom-bitvector-analysis")) @@ -1113,10 +1118,21 @@ void goto_instrument_parse_optionst::instrument_goto_program() do_indirect_call_and_rtti_removal(); status() << "Partial inlining" << eom; - goto_partial_inline(goto_functions, ns, ui_message_handler, 0, true); + goto_partial_inline(goto_model, ui_message_handler, 0, true); + + goto_model.goto_functions.update(); + goto_model.goto_functions.compute_loop_numbers(); + } - goto_functions.update(); - goto_functions.compute_loop_numbers(); + if(cmdline.isset("remove-calls-no-body")) + { + 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); + + goto_model.goto_functions.update(); + goto_model.goto_functions.compute_loop_numbers(); } if(cmdline.isset("constant-propagator")) @@ -1545,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.cpp b/src/goto-programs/goto_inline.cpp index 38dc8455c5c..62957297922 100644 --- a/src/goto-programs/goto_inline.cpp +++ b/src/goto-programs/goto_inline.cpp @@ -79,7 +79,7 @@ void goto_inline( Forall_goto_program_instructions(i_it, goto_program) { - if(!goto_inlinet::is_call(i_it)) + if(!i_it->is_function_call()) continue; call_list.push_back(goto_inlinet::callt(i_it, false)); 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 bbeb1e8397c..de59b889cac 100644 --- a/src/goto-programs/goto_inline_class.h +++ b/src/goto-programs/goto_inline_class.h @@ -6,6 +6,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ + #ifndef CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H #define CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H @@ -171,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