new option --no-caching for use with inlining to disable caching of intermediate results
This commit is contained in:
parent
7a8961e0d0
commit
775bbef2ad
|
@ -0,0 +1,18 @@
|
|||
|
||||
int x;
|
||||
|
||||
void g()
|
||||
{
|
||||
x = 1;
|
||||
}
|
||||
|
||||
void f()
|
||||
{
|
||||
g();
|
||||
}
|
||||
|
||||
int main()
|
||||
{
|
||||
f();
|
||||
}
|
||||
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
main.c
|
||||
--function-inline main --log -
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
--
|
||||
^warning: ignoring
|
|
@ -0,0 +1,23 @@
|
|||
|
||||
int x;
|
||||
|
||||
void h()
|
||||
{
|
||||
x = 1;
|
||||
}
|
||||
|
||||
void g()
|
||||
{
|
||||
h();
|
||||
}
|
||||
|
||||
void f()
|
||||
{
|
||||
g();
|
||||
}
|
||||
|
||||
int main()
|
||||
{
|
||||
f();
|
||||
}
|
||||
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
main.c
|
||||
--function-inline main --log - --no-caching
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
--
|
||||
^warning: ignoring
|
|
@ -1052,6 +1052,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
|
|||
std::string function=cmdline.get_value("function-inline");
|
||||
assert(!function.empty());
|
||||
|
||||
bool caching=!cmdline.isset("no-caching");
|
||||
|
||||
do_indirect_call_and_rtti_removal();
|
||||
|
||||
status() << "Inlining calls of function `" << function << "'" << eom;
|
||||
|
@ -1063,7 +1065,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
|
|||
function,
|
||||
ns,
|
||||
ui_message_handler,
|
||||
true);
|
||||
true,
|
||||
caching);
|
||||
}
|
||||
else
|
||||
{
|
||||
|
@ -1076,7 +1079,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
|
|||
function,
|
||||
ns,
|
||||
ui_message_handler,
|
||||
true);
|
||||
true,
|
||||
caching);
|
||||
|
||||
if(have_file)
|
||||
{
|
||||
|
@ -1548,6 +1552,7 @@ void goto_instrument_parse_optionst::help()
|
|||
" --inline perform full inlining\n"
|
||||
" --partial-inline perform partial inlining\n"
|
||||
" --function-inline <function> transitively inline all calls <function> makes\n" // NOLINT(*)
|
||||
" --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
|
||||
" --log <file> 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(*)
|
||||
" --add-library add models of C library functions\n"
|
||||
|
|
|
@ -53,7 +53,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
"(show-struct-alignment)(interval-analysis)(show-intervals)" \
|
||||
"(show-uninitialized)(show-locations)" \
|
||||
"(full-slice)(reachability-slice)(slice-global-inits)" \
|
||||
"(inline)(partial-inline)(function-inline):(log):" \
|
||||
"(inline)(partial-inline)(function-inline):(log):(no-caching)" \
|
||||
"(remove-function-pointers)" \
|
||||
"(show-claims)(show-properties)(property):" \
|
||||
"(show-symbol-table)(show-points-to)(show-rw-set)" \
|
||||
|
|
|
@ -273,13 +273,15 @@ void goto_function_inline(
|
|||
const irep_idt function,
|
||||
const namespacet &ns,
|
||||
message_handlert &message_handler,
|
||||
bool adjust_function)
|
||||
bool adjust_function,
|
||||
bool caching)
|
||||
{
|
||||
goto_inlinet goto_inline(
|
||||
goto_functions,
|
||||
ns,
|
||||
message_handler,
|
||||
adjust_function);
|
||||
adjust_function,
|
||||
caching);
|
||||
|
||||
goto_functionst::function_mapt::iterator f_it=
|
||||
goto_functions.function_map.find(function);
|
||||
|
@ -327,13 +329,15 @@ jsont goto_function_inline_and_log(
|
|||
const irep_idt function,
|
||||
const namespacet &ns,
|
||||
message_handlert &message_handler,
|
||||
bool adjust_function)
|
||||
bool adjust_function,
|
||||
bool caching)
|
||||
{
|
||||
goto_inlinet goto_inline(
|
||||
goto_functions,
|
||||
ns,
|
||||
message_handler,
|
||||
adjust_function);
|
||||
adjust_function,
|
||||
caching);
|
||||
|
||||
goto_functionst::function_mapt::iterator f_it=
|
||||
goto_functions.function_map.find(function);
|
||||
|
@ -349,6 +353,7 @@ jsont goto_function_inline_and_log(
|
|||
// gather all calls
|
||||
goto_inlinet::inline_mapt inline_map;
|
||||
|
||||
// create empty call list
|
||||
goto_inlinet::call_listt &call_list=inline_map[f_it->first];
|
||||
|
||||
goto_programt &goto_program=goto_function.body;
|
||||
|
|
|
@ -50,20 +50,23 @@ void goto_function_inline(
|
|||
goto_modelt &goto_model,
|
||||
const irep_idt function,
|
||||
message_handlert &message_handler,
|
||||
bool adjust_function=false);
|
||||
bool adjust_function=false,
|
||||
bool caching=true);
|
||||
|
||||
void goto_function_inline(
|
||||
goto_functionst &goto_functions,
|
||||
const irep_idt function,
|
||||
const namespacet &ns,
|
||||
message_handlert &message_handler,
|
||||
bool adjust_function=false);
|
||||
bool adjust_function=false,
|
||||
bool caching=true);
|
||||
|
||||
jsont goto_function_inline_and_log(
|
||||
goto_functionst &goto_functions,
|
||||
const irep_idt function,
|
||||
const namespacet &ns,
|
||||
message_handlert &message_handler,
|
||||
bool adjust_function=false);
|
||||
bool adjust_function=false,
|
||||
bool caching=true);
|
||||
|
||||
#endif // CPROVER_GOTO_PROGRAMS_GOTO_INLINE_H
|
||||
|
|
|
@ -682,6 +682,12 @@ void goto_inlinet::expand_function_call(
|
|||
function,
|
||||
arguments,
|
||||
constrain);
|
||||
|
||||
if(!caching)
|
||||
{
|
||||
inline_log.cleanup(cached.body);
|
||||
cache.erase(identifier);
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
|
@ -1146,6 +1152,29 @@ void goto_inlinet::output_inline_map(
|
|||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: output_cache
|
||||
|
||||
Inputs:
|
||||
|
||||
Outputs:
|
||||
|
||||
Purpose:
|
||||
|
||||
\*******************************************************************/
|
||||
|
||||
void goto_inlinet::output_cache(std::ostream &out) const
|
||||
{
|
||||
for(auto it=cache.begin(); it!=cache.end(); it++)
|
||||
{
|
||||
if(it!=cache.begin())
|
||||
out << ", ";
|
||||
|
||||
out << it->first << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
/*******************************************************************\
|
||||
|
||||
Function: cleanup
|
||||
|
||||
Inputs:
|
||||
|
@ -1257,8 +1286,9 @@ void goto_inlinet::goto_inline_logt::copy_from(
|
|||
assert(it1->location_number==it2->location_number);
|
||||
|
||||
log_mapt::const_iterator l_it=log_map.find(it1);
|
||||
if(l_it!=log_map.end())
|
||||
if(l_it!=log_map.end()) // a segment starts here
|
||||
{
|
||||
// as 'to' is a fresh copy
|
||||
assert(log_map.find(it2)==log_map.end());
|
||||
|
||||
goto_inline_log_infot info=l_it->second;
|
||||
|
|
|
@ -24,11 +24,13 @@ public:
|
|||
goto_functionst &goto_functions,
|
||||
const namespacet &ns,
|
||||
message_handlert &message_handler,
|
||||
bool adjust_function):
|
||||
bool adjust_function,
|
||||
bool caching=true):
|
||||
messaget(message_handler),
|
||||
goto_functions(goto_functions),
|
||||
ns(ns),
|
||||
adjust_function(adjust_function)
|
||||
adjust_function(adjust_function),
|
||||
caching(caching)
|
||||
{
|
||||
}
|
||||
|
||||
|
@ -64,6 +66,8 @@ public:
|
|||
std::ostream &out,
|
||||
const inline_mapt &inline_map);
|
||||
|
||||
void output_cache(std::ostream &out) const;
|
||||
|
||||
// call after goto_functions.update()!
|
||||
jsont output_inline_log_json()
|
||||
{
|
||||
|
@ -127,6 +131,8 @@ protected:
|
|||
const namespacet &ns;
|
||||
|
||||
const bool adjust_function;
|
||||
const bool caching;
|
||||
|
||||
goto_inline_logt inline_log;
|
||||
|
||||
void goto_inline_nontransitive(
|
||||
|
|
Loading…
Reference in New Issue