diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp index d57ad3d5c1a..7b6b219e84d 100644 --- a/src/goto-programs/goto_inline.cpp +++ b/src/goto-programs/goto_inline.cpp @@ -16,6 +16,13 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_inline_class.h" #include "goto_model.h" +/// Inline every function call into the entry_point() function. +/// Then delete the bodies of all of the other functions. +/// This is pretty drastic and can result in a very large program. +/// Caller is responsible for calling update(), compute_loop_numbers(), etc. +/// \param goto_model: Source of the symbol table and function map to use. +/// \param message_handler: Message handler used by goto_inlinet. +/// \param adjust_function: Replace location in inlined function with call site. void goto_inline( goto_modelt &goto_model, message_handlert &message_handler, @@ -29,6 +36,14 @@ void goto_inline( adjust_function); } +/// Inline every function call into the entry_point() function. +/// Then delete the bodies of all of the other functions. +/// This is pretty drastic and can result in a very large program. +/// Caller is responsible for calling update(), compute_loop_numbers(), etc. +/// \param goto_functions: The function map to use. +/// \param ns : The namespace to use. +/// \param message_handler: Message handler used by goto_inlinet. +/// \param adjust_function: Replace location in inlined function with call site. void goto_inline( goto_functionst &goto_functions, const namespacet &ns, @@ -96,11 +111,14 @@ void goto_inline( /// Inline all function calls to functions either marked as "inlined" or /// smaller than smallfunc_limit (by instruction count). +/// Unlike the goto_inline functions, this doesn't remove function +/// bodies after inlining. +/// Caller is responsible for calling update(), compute_loop_numbers(), etc. /// \param goto_model: Source of the symbol table and function map to use. /// \param message_handler: Message handler used by goto_inlinet. /// \param smallfunc_limit: The maximum number of instructions in functions to /// be inlined. -/// \param adjust_function: Tell goto_inlinet to adjust function. +/// \param adjust_function: Replace location in inlined function with call site. void goto_partial_inline( goto_modelt &goto_model, message_handlert &message_handler, @@ -118,13 +136,16 @@ void goto_partial_inline( /// Inline all function calls to functions either marked as "inlined" or /// smaller than smallfunc_limit (by instruction count). +/// Unlike the goto_inline functions, this doesn't remove function +/// bodies after inlining. +/// Caller is responsible for calling update(), compute_loop_numbers(), etc. /// \param goto_functions: The function map to use to find functions containing /// calls and function bodies. /// \param ns: Namespace used by goto_inlinet. /// \param message_handler: Message handler used by goto_inlinet. /// \param smallfunc_limit: The maximum number of instructions in functions to /// be inlined. -/// \param adjust_function: Tell goto_inlinet to adjust function. +/// \param adjust_function: Replace location in inlined function with call site. void goto_partial_inline( goto_functionst &goto_functions, const namespacet &ns, @@ -153,6 +174,9 @@ void goto_partial_inline( if(gf_entry.first == goto_functions.entry_point()) { // Don't inline any function calls made from the _start function. + // This is so that the convention of __CPROVER_start + // calling __CPROVER_initialize is maintained, so these can be + // augmented / replaced by later passes. continue; } @@ -205,11 +229,12 @@ void goto_partial_inline( goto_inline.goto_inline(inline_map, false); } -/// Inline all function calls made from a particular function +/// Transitively inline all function calls made from a particular function. +/// Caller is responsible for calling update(), compute_loop_numbers(), etc. /// \param goto_model: Source of the symbol table and function map to use. /// \param function: The function whose calls to inline. /// \param message_handler: Message handler used by goto_inlinet. -/// \param adjust_function: Tell goto_inlinet to adjust function. +/// \param adjust_function: Replace location in inlined function with call site. /// \param caching: Tell goto_inlinet to cache. void goto_function_inline( goto_modelt &goto_model, @@ -228,12 +253,13 @@ void goto_function_inline( caching); } -/// Inline all function calls made from a particular function +/// Transitively inline all function calls made from a particular function. +/// Caller is responsible for calling update(), compute_loop_numbers(), etc. /// \param goto_functions: The function map to use to find function bodies. /// \param function: The function whose calls to inline. /// \param ns: Namespace used by goto_inlinet. /// \param message_handler: Message handler used by goto_inlinet. -/// \param adjust_function: Tell goto_inlinet to adjust function. +/// \param adjust_function: Replace location in inlined function with call site. /// \param caching: Tell goto_inlinet to cache. void goto_function_inline( goto_functionst &goto_functions, diff --git a/src/goto-programs/goto_inline.h b/src/goto-programs/goto_inline.h index 543ae9fa9d8..c3db270cede 100644 --- a/src/goto-programs/goto_inline.h +++ b/src/goto-programs/goto_inline.h @@ -8,6 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Function Inlining +/// This gives a number of different interfaces to the function +/// inlining functionality of goto_inlinet. #ifndef CPROVER_GOTO_PROGRAMS_GOTO_INLINE_H #define 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 85dafc27f4c..534c2aaa2f0 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/src/goto-programs/goto_inline_class.cpp @@ -296,6 +296,8 @@ void goto_inlinet::insert_function_body( dest.destructive_insert(target, tmp); } +/// Inlines a single function call +/// Calls out to goto_inline_transitive or goto_inline_nontransitive void goto_inlinet::expand_function_call( goto_programt &dest, const inline_mapt &inline_map, @@ -441,6 +443,11 @@ void goto_inlinet::get_call( arguments=call.arguments(); } +/// Inline all of the given call locations. +/// This is the highest-level interface and calls the other goto_inline +/// \param inline_map : which call locations to inline. +/// \param force_full : true to break recursion with a SKIP, +/// false means detecting recursion is an error. void goto_inlinet::goto_inline( const inline_mapt &inline_map, const bool force_full) @@ -460,6 +467,13 @@ void goto_inlinet::goto_inline( } } +/// Inline all of the chosen calls in a given function. +/// This is main entry point for the functionality +/// \param identifier : the name of the caller function. +/// \param goto_function : the caller function itself. +/// \param inline_map : which call locations to inline. +/// \param force_full : true to break recursion with a SKIP, +/// false means detecting recursion is an error. void goto_inlinet::goto_inline( 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 e7bbabdaec1..71a1951b3dc 100644 --- a/src/goto-programs/goto_inline_class.h +++ b/src/goto-programs/goto_inline_class.h @@ -6,6 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +/// \file +/// Function Inlining +/// This is a class that encapsulates the state and functionality needed +/// to do inline multiple function calls. +/// goto_inline.h provides a number of more convenient interfaces. #ifndef CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H #define CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H @@ -20,6 +25,13 @@ Author: Daniel Kroening, kroening@kroening.com class goto_inlinet { public: + /// Sets up the class with the program to operate on. + /// + /// \param goto_functions : The map of functions to work on + /// \param ns : The corresponding namespace + /// \param message_handler : Used to log what is being inlined + /// \param adjust_function: Replace location in caller location. + /// \param caching : cache functions when in transitive mode goto_inlinet( goto_functionst &goto_functions, const namespacet &ns,