diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp index 7b6b219e84d..7ecdaa7a6fc 100644 --- a/src/goto-programs/goto_inline.cpp +++ b/src/goto-programs/goto_inline.cpp @@ -354,3 +354,36 @@ jsont goto_function_inline_and_log( return goto_inline.output_inline_log_json(); } + +/// Transitively inline all function calls found in a particular program. +/// Caller is responsible for calling update(), compute_loop_numbers(), etc. +/// \param goto_functions: The function map to use to find function bodies. +/// \param goto_program: The program whose calls to inline. +/// \param ns: Namespace used by goto_inlinet. +/// \param message_handler: Message handler used by goto_inlinet. +/// \param adjust_function: Replace location in inlined function with call site. +/// \param caching: Tell goto_inlinet to cache. +void goto_program_inline( + goto_functionst &goto_functions, + goto_programt &goto_program, + const namespacet &ns, + message_handlert &message_handler, + bool adjust_function, + bool caching) +{ + goto_inlinet goto_inline( + goto_functions, ns, message_handler, adjust_function, caching); + + // gather all calls found in the program + goto_inlinet::call_listt call_list; + + Forall_goto_program_instructions(i_it, goto_program) + { + if(!i_it->is_function_call()) + continue; + + call_list.push_back(goto_inlinet::callt(i_it, true)); + } + + goto_inline.goto_inline(call_list, goto_program, true); +} diff --git a/src/goto-programs/goto_inline.h b/src/goto-programs/goto_inline.h index c3db270cede..71cffe45244 100644 --- a/src/goto-programs/goto_inline.h +++ b/src/goto-programs/goto_inline.h @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com class goto_functionst; class goto_modelt; +class goto_programt; class message_handlert; class namespacet; @@ -74,4 +75,12 @@ jsont goto_function_inline_and_log( bool adjust_function=false, bool caching=true); +void goto_program_inline( + goto_functionst &goto_functions, + goto_programt &goto_program, + const namespacet &ns, + message_handlert &message_handler, + bool adjust_function = false, + bool caching = true); + #endif // CPROVER_GOTO_PROGRAMS_GOTO_INLINE_H diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index e553f4cee96..15ffd84048e 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -488,6 +488,21 @@ void goto_inlinet::goto_inline( force_full); } +void goto_inlinet::goto_inline( + const goto_inlinet::call_listt &call_list, + goto_programt &goto_program, + const bool force_full) +{ + recursion_set.clear(); + for(const auto &call : call_list) + { + // each top level call in the program gets its own fresh inline map + const inline_mapt inline_map; + expand_function_call( + goto_program, inline_map, call.second, force_full, call.first); + } +} + void goto_inlinet::goto_inline_nontransitive( const irep_idt identifier, goto_functiont &goto_function, diff --git a/src/goto-programs/goto_inline_class.h b/src/goto-programs/goto_inline_class.h index 71a1951b3dc..4fb97bdac73 100644 --- a/src/goto-programs/goto_inline_class.h +++ b/src/goto-programs/goto_inline_class.h @@ -69,6 +69,16 @@ class goto_inlinet const inline_mapt &inline_map, const bool force_full=false); + /// \brief Inline specified calls in a given program. + /// \param call_list : calls to inline in the `goto_program`. + /// \param goto_program : goto program to inline `calls_list` in. + /// \param force_full : true to break recursion with a SKIP, + /// false means detecting recursion is an error. + void goto_inline( + const goto_inlinet::call_listt &call_list, + goto_programt &goto_program, + const bool force_full = false); + // handle all functions void goto_inline( const inline_mapt &inline_map, diff --git a/unit/Makefile b/unit/Makefile index 6bc34935e2c..fbe92974ce9 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -66,6 +66,7 @@ SRC += analyses/ai/ai.cpp \ goto-programs/goto_program_declaration.cpp \ goto-programs/goto_program_function_call.cpp \ goto-programs/goto_program_goto_target.cpp \ + goto-programs/goto_program_goto_program_inline.cpp \ goto-programs/goto_program_symbol_type_table_consistency.cpp \ goto-programs/goto_program_table_consistency.cpp \ goto-programs/goto_program_validate.cpp \ diff --git a/unit/goto-programs/goto_program_goto_program_inline.cpp b/unit/goto-programs/goto_program_goto_program_inline.cpp new file mode 100644 index 00000000000..06d1e475723 --- /dev/null +++ b/unit/goto-programs/goto_program_goto_program_inline.cpp @@ -0,0 +1,67 @@ +/*******************************************************************\ + +Module: Inline calls in program unit tests + +Author: Remi Delmas + +\*******************************************************************/ + +#include + +#include + +#include +#include + +TEST_CASE("Goto program inline", "[core][goto-programs][goto_program_inline]") +{ + const std::string code = R"( + int x; + int y; + void f() { y = 0; } + void g() { x = 0; f(); } + void h() { g(); } + void main() { h(); } + )"; + + goto_modelt goto_model = get_goto_model_from_c(code); + + auto &function = goto_model.goto_functions.function_map.at("h"); + + null_message_handlert message_handler; + goto_program_inline( + goto_model.goto_functions, + function.body, + namespacet(goto_model.symbol_table), + message_handler); + + static int assign_count = 0; + for_each_instruction_if( + function, + [&](goto_programt::const_targett it) { + return it->is_function_call() || it->is_assign(); + }, + [&](goto_programt::const_targett it) { + if(it->is_function_call()) + { + // there are no calls left + FAIL(); + } + + if(it->is_assign()) + { + // the two assignments were inlined + const auto &lhs = it->assign_lhs(); + if(assign_count == 0) + { + REQUIRE(to_symbol_expr(lhs).get_identifier() == "x"); + } + else if(assign_count == 1) + { + REQUIRE(to_symbol_expr(lhs).get_identifier() == "y"); + } + assign_count++; + } + }); + REQUIRE(assign_count == 2); +}