diff --git a/regression/Makefile b/regression/Makefile index b9c41ccd7dd..e9984116745 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -1,4 +1,5 @@ -DIRS = ansi-c cbmc cpp goto-instrument goto-instrument-unwind goto-analyzer + +DIRS = ansi-c cbmc cpp goto-instrument goto-instrument-unwind goto-analyzer inlining test: $(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;) diff --git a/regression/inlining/Makefile b/regression/inlining/Makefile new file mode 100644 index 00000000000..ad9e1fba484 --- /dev/null +++ b/regression/inlining/Makefile @@ -0,0 +1,20 @@ +default: tests.log + +test: + @./test.sh + +tests.log: ../test.pl + @./test.sh + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.java" "$$dir/*.out"; \ + fi; \ + done; + +clean: + find . -name '*.*~' | xargs rm -f + find . -name '*.out' | xargs rm -f + find . -name '*.o' | xargs rm -f + rm -f tests.log diff --git a/regression/inlining/chain.sh b/regression/inlining/chain.sh new file mode 100755 index 00000000000..ca99de27262 --- /dev/null +++ b/regression/inlining/chain.sh @@ -0,0 +1,19 @@ +#!/bin/bash + +set -e + +src=../../../src +goto_cc=$src/goto-cc/goto-cc +goto_instrument=$src/goto-instrument/goto-instrument +cbmc=$src/cbmc/cbmc + +name=${@:$#} +name=${name%.c} + +args=${@:1:$#-1} + +$goto_cc -o $name.o $name.c +$goto_instrument $args $name.o $name-new.o +$goto_instrument --show-goto-functions $name-new.o +$cbmc $name-new.o + diff --git a/regression/inlining/inline_01/main.c b/regression/inlining/inline_01/main.c new file mode 100644 index 00000000000..1d28a9b55fb --- /dev/null +++ b/regression/inlining/inline_01/main.c @@ -0,0 +1,24 @@ +#include + +int x; + +int h() { + return 9; +} + +void g(int i) { + x += i + h(); // += 12 +} + +void f(int i, int j) { + g(i); + x += i + j; // +=10 +} + +int main() +{ + x = 0; + f(3, 7); + assert(x == 22); +} + diff --git a/regression/inlining/inline_01/test.desc b/regression/inlining/inline_01/test.desc new file mode 100644 index 00000000000..36bbb89719e --- /dev/null +++ b/regression/inlining/inline_01/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +f[(].*[)];$ +g[(].*[)];$ +h[(].*[)];$ +^warning: ignoring diff --git a/regression/inlining/inline_02/main.c b/regression/inlining/inline_02/main.c new file mode 100644 index 00000000000..1d28a9b55fb --- /dev/null +++ b/regression/inlining/inline_02/main.c @@ -0,0 +1,24 @@ +#include + +int x; + +int h() { + return 9; +} + +void g(int i) { + x += i + h(); // += 12 +} + +void f(int i, int j) { + g(i); + x += i + j; // +=10 +} + +int main() +{ + x = 0; + f(3, 7); + assert(x == 22); +} + diff --git a/regression/inlining/inline_02/test.desc b/regression/inlining/inline_02/test.desc new file mode 100644 index 00000000000..ee604db74c9 --- /dev/null +++ b/regression/inlining/inline_02/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--partial-inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +f[(].*[)];$ +g[(].*[)];$ +h[(].*[)];$ +-- +^warning: ignoring diff --git a/regression/inlining/inline_03/main.c b/regression/inlining/inline_03/main.c new file mode 100644 index 00000000000..4f17f000fe2 --- /dev/null +++ b/regression/inlining/inline_03/main.c @@ -0,0 +1,24 @@ +#include + +int x; + +inline int h() { + return 9; +} + +void g(int i) { + x += i + h(); // += 12 +} + +void f(int i, int j) { + g(i); + x += i + j; // +=10 +} + +int main() +{ + x = 0; + f(3, 7); + assert(x == 22); +} + diff --git a/regression/inlining/inline_03/test.desc b/regression/inlining/inline_03/test.desc new file mode 100644 index 00000000000..4681dd60cea --- /dev/null +++ b/regression/inlining/inline_03/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--partial-inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +f[(].*[)];$ +g[(].*[)];$ +-- +h[(].*[)];$ +^warning: ignoring diff --git a/regression/inlining/inline_04/main.c b/regression/inlining/inline_04/main.c new file mode 100644 index 00000000000..5d062314336 --- /dev/null +++ b/regression/inlining/inline_04/main.c @@ -0,0 +1,28 @@ +#include + +int x; + +int h() { + return 9; +} + +void g(int i) { + x += i + h(); // += 12 +} + +void f(int i, int j) { + g(i); + x += i + j; // +=10 +} + +void other_func() {} + +int main() +{ + x = 0; + f(3, 7); + other_func(); + + assert(x == 22); +} + diff --git a/regression/inlining/inline_04/test.desc b/regression/inlining/inline_04/test.desc new file mode 100644 index 00000000000..b4f0cef0dfa --- /dev/null +++ b/regression/inlining/inline_04/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--function-inline main +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +g[(].*[)];$ +h[(].*[)];$ +-- +f[(].*[)];$ +other_func[(].*[)];$ +^warning: ignoring diff --git a/regression/inlining/inline_05/main.c b/regression/inlining/inline_05/main.c new file mode 100644 index 00000000000..27fd212ff2c --- /dev/null +++ b/regression/inlining/inline_05/main.c @@ -0,0 +1,38 @@ +#include + +int x; + +void f() +{ + x += 1; + + if(x < 10) + f(); +} + +void h() +{ + x += 1; + if(x < 20) + g(); +} + +void g() +{ + x += 1; + h(); +} + +int main() +{ + // direct recursion + x = 0; + f(); + assert(x == 1); + + // indirect recursion + x = 0; + g(); + assert(x == 2); +} + diff --git a/regression/inlining/inline_05/test.desc b/regression/inlining/inline_05/test.desc new file mode 100644 index 00000000000..c28e702b192 --- /dev/null +++ b/regression/inlining/inline_05/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +recursion.*ignored.*[`]f +recursion.*ignored.*[`]g +-- +^warning: ignoring diff --git a/regression/inlining/inline_06/main.c b/regression/inlining/inline_06/main.c new file mode 100644 index 00000000000..d82363e9984 --- /dev/null +++ b/regression/inlining/inline_06/main.c @@ -0,0 +1,38 @@ +#include + +int x; + +inline void f() +{ + x += 1; + + if(x < 10) + f(); +} + +inline void h() +{ + x += 1; + if(x < 20) + g(); +} + +inline void g() +{ + x += 1; + h(); +} + +int main() +{ + // direct recursion + x = 0; + f(); + assert(x == 10); + + // indirect recursion + x = 0; + g(); + assert(x == 20); +} + diff --git a/regression/inlining/inline_06/test.desc b/regression/inlining/inline_06/test.desc new file mode 100644 index 00000000000..70a8f0beafa --- /dev/null +++ b/regression/inlining/inline_06/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--partial-inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +recursion.*ignored.*[`]f +recursion.*ignored.*[`]g +-- +^warning: ignoring diff --git a/regression/inlining/inline_07/main.c b/regression/inlining/inline_07/main.c new file mode 100644 index 00000000000..27fd212ff2c --- /dev/null +++ b/regression/inlining/inline_07/main.c @@ -0,0 +1,38 @@ +#include + +int x; + +void f() +{ + x += 1; + + if(x < 10) + f(); +} + +void h() +{ + x += 1; + if(x < 20) + g(); +} + +void g() +{ + x += 1; + h(); +} + +int main() +{ + // direct recursion + x = 0; + f(); + assert(x == 1); + + // indirect recursion + x = 0; + g(); + assert(x == 2); +} + diff --git a/regression/inlining/inline_07/test.desc b/regression/inlining/inline_07/test.desc new file mode 100644 index 00000000000..94d9bb1c818 --- /dev/null +++ b/regression/inlining/inline_07/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--function-inline main +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +recursion.*ignored.*[`]f +recursion.*ignored.*[`]g +-- +^warning: ignoring diff --git a/regression/inlining/inline_08/main.c b/regression/inlining/inline_08/main.c new file mode 100644 index 00000000000..b81d8f7cec9 --- /dev/null +++ b/regression/inlining/inline_08/main.c @@ -0,0 +1,20 @@ +#include + +int x; + +int f() +{ + if(x) + return 1; + else + return 2; + + return 3; +} + +int main() +{ + int y; + y = f(); +} + diff --git a/regression/inlining/inline_08/test.desc b/regression/inlining/inline_08/test.desc new file mode 100644 index 00000000000..63e8a494a30 --- /dev/null +++ b/regression/inlining/inline_08/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +y = 1; +y = 2; +y = 3; +-- +^warning: ignoring diff --git a/regression/inlining/inline_09/main.c b/regression/inlining/inline_09/main.c new file mode 100644 index 00000000000..d56b26218c7 --- /dev/null +++ b/regression/inlining/inline_09/main.c @@ -0,0 +1,17 @@ +#include + +void f(int, char, float); + +int main() +{ + int x; + char c; + float a; + + x = 3; + c = 'a'; + a = 2.7; + + f(x, c, a); +} + diff --git a/regression/inlining/inline_09/test.desc b/regression/inlining/inline_09/test.desc new file mode 100644 index 00000000000..db81237a3ad --- /dev/null +++ b/regression/inlining/inline_09/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +^\s*x;$ +^\s*c;$ +^\s*a;$ +no body.*[`]f +-- +^warning: ignoring diff --git a/regression/inlining/inline_10/main.c b/regression/inlining/inline_10/main.c new file mode 100644 index 00000000000..4b8fd880a63 --- /dev/null +++ b/regression/inlining/inline_10/main.c @@ -0,0 +1,45 @@ +#include + +int x; + +// first pair + +void g1() +{ + x += 2; + f1(); +} + +void f1() +{ + x += 1; + g1(); +} + +// second pair + +void g2() +{ + x += 2; + f2(); +} + +void f2() +{ + x += 1; + g2(); +} + +int main() +{ + f1(); + x = 0; + g1(); + assert(x == 2); + + g2(); + x = 0; + g2(); + assert(x == 3); +} + diff --git a/regression/inlining/inline_10/test.desc b/regression/inlining/inline_10/test.desc new file mode 100644 index 00000000000..685d31432d9 --- /dev/null +++ b/regression/inlining/inline_10/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/inlining/inline_11/main.c b/regression/inlining/inline_11/main.c new file mode 100644 index 00000000000..786f7b504c6 --- /dev/null +++ b/regression/inlining/inline_11/main.c @@ -0,0 +1,20 @@ + +int x; + +void g() +{ + x = 3; +} + +void f() +{ + g(); + x = 1; +} + +int main() +{ + f(); + x = 2; +} + diff --git a/regression/inlining/inline_11/test.desc b/regression/inlining/inline_11/test.desc new file mode 100644 index 00000000000..562879b7646 --- /dev/null +++ b/regression/inlining/inline_11/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--inline +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +main[(].*[)]; +^warning: ignoring diff --git a/regression/inlining/inline_12/main.c b/regression/inlining/inline_12/main.c new file mode 100644 index 00000000000..561d8e320ec --- /dev/null +++ b/regression/inlining/inline_12/main.c @@ -0,0 +1,35 @@ + +int x; + +void i() +{ + +} + +void h() +{ + x = 7; + x = 8; + x = 9; + i(); + //i(); +} + +void g() +{ + +} + +void f() +{ + g(); + h(); + x = 1; +} + +int main() +{ + f(); + x = 2; +} + diff --git a/regression/inlining/inline_12/test.desc b/regression/inlining/inline_12/test.desc new file mode 100644 index 00000000000..9d6164ddcdc --- /dev/null +++ b/regression/inlining/inline_12/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--function-inline f --log - +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/inlining/test.sh b/regression/inlining/test.sh new file mode 100755 index 00000000000..8dd60cf2bc2 --- /dev/null +++ b/regression/inlining/test.sh @@ -0,0 +1,3 @@ +#!/bin/bash + +../test.pl -c '../chain.sh' $1 diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index dbd4bf69cda..f6e242f05a3 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -104,7 +105,8 @@ void goto_instrument_parse_optionst::eval_verbosity() if(cmdline.isset("verbosity")) { v=unsafe_string2unsigned(cmdline.get_value("verbosity")); - if(v>10) v=10; + if(v>10) + v=10; } ui_message_handler.set_verbosity(v); @@ -143,6 +145,7 @@ int goto_instrument_parse_optionst::doit() register_languages(); get_goto_program(); + instrument_goto_program(); { @@ -368,7 +371,11 @@ int goto_instrument_parse_optionst::doit() custom_bitvector_analysist custom_bitvector_analysis; custom_bitvector_analysis(goto_functions, ns); - custom_bitvector_analysis.check(ns, goto_functions, cmdline.isset("xml-ui"), std::cout); + custom_bitvector_analysis.check( + ns, + goto_functions, + cmdline.isset("xml-ui"), + std::cout); return 0; } @@ -440,7 +447,8 @@ int goto_instrument_parse_optionst::doit() const symbolt &symbol=ns.lookup(ID_main); symbol_exprt main(symbol.name, symbol.type); - std::cout << rw_set_functiont(value_set_analysis, ns, goto_functions, main); + std::cout << + rw_set_functiont(value_set_analysis, ns, goto_functions, main); return 0; } @@ -761,12 +769,16 @@ Function: goto_instrument_parse_optionst::do_function_pointer_removal void goto_instrument_parse_optionst::do_function_pointer_removal() { - if(function_pointer_removal_done) return; + if(function_pointer_removal_done) + return; + function_pointer_removal_done=true; status() << "Function Pointer Removal" << eom; remove_function_pointers( - symbol_table, goto_functions, cmdline.isset("pointer-check")); + symbol_table, + goto_functions, + cmdline.isset("pointer-check")); } /*******************************************************************\ @@ -783,7 +795,9 @@ Function: goto_instrument_parse_optionst::do_partial_inlining void goto_instrument_parse_optionst::do_partial_inlining() { - if(partial_inlining_done) return; + if(partial_inlining_done) + return; + partial_inlining_done=true; if(!cmdline.isset("inline")) @@ -808,7 +822,9 @@ Function: goto_instrument_parse_optionst::do_remove_returns void goto_instrument_parse_optionst::do_remove_returns() { - if(remove_returns_done) return; + if(remove_returns_done) + return; + remove_returns_done=true; status() << "Removing returns" << eom; @@ -979,6 +995,92 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset("remove-function-pointers")) do_function_pointer_removal(); + if(cmdline.isset("function-inline")) + { + std::string function=cmdline.get_value("function-inline"); + assert(!function.empty()); + + do_function_pointer_removal(); + + status() << "Inlining calls of function `" << function << "'" << eom; + + if(!cmdline.isset("log")) + { + goto_function_inline( + goto_functions, + function, + ns, + ui_message_handler, + true); + } + else + { + std::string filename=cmdline.get_value("log"); + bool have_file=!filename.empty() && filename!="-"; + + jsont result= + goto_function_inline_and_log( + goto_functions, + function, + ns, + ui_message_handler, + true); + + if(have_file) + { +#ifdef _MSC_VER + std::ofstream of(widen(filename)); +#else + std::ofstream of(filename); +#endif + if(!of) + throw "failed to open file "+filename; + + of << result; + of.close(); + } + else + { + std::cout << result << std::endl; + } + } + + goto_functions.update(); + goto_functions.compute_loop_numbers(); + } + + if(cmdline.isset("partial-inline")) + { + do_function_pointer_removal(); + + status() << "Partial inlining" << eom; + goto_partial_inline(goto_functions, ns, ui_message_handler, true); + + goto_functions.update(); + goto_functions.compute_loop_numbers(); + } + + // now do full inlining, if requested + if(cmdline.isset("inline")) + { + status() << "Function Pointer Removal" << eom; + remove_function_pointers( + symbol_table, + goto_functions, + cmdline.isset("pointer-check")); + + if(cmdline.isset("show-custom-bitvector-analysis") || + cmdline.isset("custom-bitvector-analysis")) + { + do_remove_returns(); + thread_exit_instrumentation(goto_functions); + mutex_init_instrumentation(symbol_table, goto_functions); + } + + status() << "Performing full inlining" << eom; + goto_inline(goto_functions, ns, ui_message_handler, true); + } + if(cmdline.isset("constant-propagator")) { do_function_pointer_removal(); @@ -1004,15 +1106,18 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset("stack-depth")) { status() << "Adding check for maximum call stack size" << eom; - stack_depth(symbol_table, goto_functions, - unsafe_string2unsigned(cmdline.get_value("stack-depth"))); + stack_depth( + symbol_table, + goto_functions, + unsafe_string2unsigned(cmdline.get_value("stack-depth"))); } // ignore default/user-specified initialization of variables with static // lifetime if(cmdline.isset("nondet-static")) { - status() << "Adding nondeterministic initialization of static/global variables" << eom; + status() << "Adding nondeterministic initialization of static/global " + "variables" << eom; nondet_static(ns, goto_functions); } @@ -1026,8 +1131,10 @@ void goto_instrument_parse_optionst::instrument_goto_program() if(cmdline.isset("string-abstraction")) { status() << "String Abstraction" << eom; - string_abstraction(symbol_table, - get_message_handler(), goto_functions); + string_abstraction( + symbol_table, + get_message_handler(), + goto_functions); } // some analyses require function pointer removal and partial inlining @@ -1040,7 +1147,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() { do_function_pointer_removal(); do_partial_inlining(); - + status() << "Pointer Analysis" << eom; value_set_analysist value_set_analysis(ns); value_set_analysis(goto_functions); @@ -1050,7 +1157,9 @@ void goto_instrument_parse_optionst::instrument_goto_program() // removing pointers status() << "Removing Pointers" << eom; remove_pointers( - goto_functions, symbol_table, value_set_analysis); + goto_functions, + symbol_table, + value_set_analysis); } if(cmdline.isset("race-check")) @@ -1089,12 +1198,15 @@ void goto_instrument_parse_optionst::instrument_goto_program() /* default: instruments all unsafe pairs */ inst_strategy=all; - const unsigned unwind_loops = - ( cmdline.isset("unwind")?unsafe_string2unsigned(cmdline.get_value("unwind")):0 ); - const unsigned max_var = - ( cmdline.isset("max-var")?unsafe_string2unsigned(cmdline.get_value("max-var")):0 ); - const unsigned max_po_trans = - ( cmdline.isset("max-po-trans")?unsafe_string2unsigned(cmdline.get_value("max-po-trans")):0 ); + const unsigned unwind_loops= + cmdline.isset("unwind")? + unsafe_string2unsigned(cmdline.get_value("unwind")):0; + const unsigned max_var= + cmdline.isset("max-var")? + unsafe_string2unsigned(cmdline.get_value("max-var")):0; + const unsigned max_po_trans= + cmdline.isset("max-po-trans")? + unsafe_string2unsigned(cmdline.get_value("max-po-trans")):0; if(mm=="tso") { @@ -1304,7 +1416,7 @@ void goto_instrument_parse_optionst::help() { std::cout << "\n" - "* * Goto-Instrument " CBMC_VERSION " - Copyright (C) 2008-2013 * *\n" + "* * Goto-Instrument " CBMC_VERSION " - Copyright (C) 2008-2013 * *\n" // NOLINT(*) "* * Daniel Kroening * *\n" "* * kroening@kroening.com * *\n" "\n" @@ -1321,7 +1433,7 @@ void goto_instrument_parse_optionst::help() " --dot generate CFG graph in DOT format\n" " --interpreter do concrete execution\n" " --count-eloc count effective lines of code\n" - " --list-eloc list full path names of lines containing code\n" + " --list-eloc list full path names of lines containing code\n" // NOLINT(*) "\n" "Diagnosis:\n" " --show-loops show the loops in the program\n" @@ -1330,30 +1442,30 @@ void goto_instrument_parse_optionst::help() " --list-symbols list symbols with type information\n" " --show-goto-functions show goto program\n" " --list-undefined-functions list functions without body\n" - " --show-struct-alignment show struct members that might be concurrently accessed\n" + " --show-struct-alignment show struct members that might be concurrently accessed\n" // NOLINT(*) " --show-natural-loops show natural loop heads\n" "\n" "Safety checks:\n" " --no-assertions ignore user assertions\n" GOTO_CHECK_HELP - " --uninitialized-check add checks for uninitialized locals (experimental)\n" + " --uninitialized-check add checks for uninitialized locals (experimental)\n" // NOLINT(*) " --error-label label check that label is unreachable\n" - " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" + " --stack-depth n add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*) " --race-check add floating-point data race checks\n" "\n" "Semantic transformations:\n" - " --nondet-volatile makes reads from volatile variables non-deterministic\n" + " --nondet-volatile makes reads from volatile variables non-deterministic\n" // NOLINT(*) " --unwind unwinds the loops times\n" " --unwindset L:B,... unwind loop L with a bound of B\n" " --unwindset-file read unwindset from file\n" " --partial-loops permit paths with partial loops\n" " --unwinding-assertions generate unwinding assertions\n" - " --continue-as-loops add loop for remaining iterations after unwound part\n" + " --continue-as-loops add loop for remaining iterations after unwound part\n" // NOLINT(*) " --isr instruments an interrupt service routine\n" " --mmio instruments memory-mapped I/O\n" - " --nondet-static add nondeterministic initialization of variables with static lifetime\n" + " --nondet-static add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*) " --check-invariant function instruments invariant checking function\n" - " --remove-pointers converts pointer arithmetic to base+offset expressions\n" + " --remove-pointers converts pointer arithmetic to base+offset expressions\n" // NOLINT(*) "\n" "Loop transformations:\n" " --k-induction check loops with k-induction\n" @@ -1361,34 +1473,37 @@ void goto_instrument_parse_optionst::help() " --base-case k-induction: do base-case\n" " --havoc-loops over-approximate all loops\n" " --accelerate add loop accelerators\n" - " --skip-loops add gotos to skip selected loops during execution\n" + " --skip-loops add gotos to skip selected loops during execution\n" // NOLINT(*) "\n" "Memory model instrumentations:\n" " --mm instruments a weak memory model\n" - " --scc detects critical cycles per SCC (one thread per SCC)\n" + " --scc detects critical cycles per SCC (one thread per SCC)\n" // NOLINT(*) " --one-event-per-cycle only instruments one event per cycle\n" " --minimum-interference instruments an optimal number of events\n" - " --my-events only instruments events whose ids appear in inst.evt\n" - " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" + " --my-events only instruments events whose ids appear in inst.evt\n" // NOLINT(*) + " --cfg-kill enables symbolic execution used to reduce spurious cycles\n" // NOLINT(*) " --no-dependencies no dependency analysis\n" " --no-po-rendering no representation of the threads in the dot\n" " --render-cluster-file clusterises the dot by files\n" " --render-cluster-function clusterises the dot by functions\n" "\n" "Slicing:\n" - " --reachability-slice slice away instructions that can't reach assertions\n" - " --full-slice slice away instructions that don't affect assertions\n" - " --property id slice with respect to specific property only\n" - " --slice-global-inits slice away initializations of unused global variables\n" + " --reachability-slice slice away instructions that can't reach assertions\n" // NOLINT(*) + " --full-slice slice away instructions that don't affect assertions\n" // NOLINT(*) + " --property id slice with respect to specific property only\n" // NOLINT(*) + " --slice-global-inits slice away initializations of unused global variables\n" // NOLINT(*) "\n" "Further transformations:\n" - " --constant-propagator propagate constants and simplify expressions\n" + " --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*) " --inline perform full inlining\n" - " --remove-function-pointers replace function pointers by case statement over function calls\n" + " --partial-inline perform partial inlining\n" + " --function-inline transitively inline all calls makes\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(*) " --add-library add models of C library functions\n" "\n" "Other options:\n" - " --use-system-headers with --dump-c/--dump-cpp: generate C source with includes\n" + " --use-system-headers with --dump-c/--dump-cpp: generate C source with includes\n" // NOLINT(*) " --version show version and exit\n" " --xml-ui use XML-formatted output\n" " --json-ui use JSON-formatted output\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 5c2c6bae3ac..23a1362159e 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -51,7 +51,8 @@ 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)(remove-function-pointers)" \ + "(inline)(partial-inline)(function-inline):(log):" \ + "(remove-function-pointers)" \ "(show-claims)(show-properties)(property):" \ "(show-symbol-table)(show-points-to)(show-rw-set)" \ "(cav11)" \ diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index f424f150640..aa788914562 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -17,7 +17,7 @@ SRC = goto_convert.cpp goto_convert_function_call.cpp \ goto_trace.cpp xml_goto_trace.cpp vcd_goto_trace.cpp \ graphml_witness.cpp remove_virtual_functions.cpp \ class_hierarchy.cpp show_goto_functions.cpp get_goto_model.cpp \ - slice_global_inits.cpp + slice_global_inits.cpp goto_inline_class.cpp INCLUDES= -I .. diff --git a/src/goto-programs/goto_inline.cpp b/src/goto-programs/goto_inline.cpp index 765aa290d7c..d392de25170 100644 --- a/src/goto-programs/goto_inline.cpp +++ b/src/goto-programs/goto_inline.cpp @@ -21,7 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ -Function: goto_inlinet::parameter_assignments +Function: goto_inline Inputs: @@ -31,130 +31,22 @@ Function: goto_inlinet::parameter_assignments \*******************************************************************/ -void goto_inlinet::parameter_assignments( - const source_locationt &source_location, - const irep_idt &function_name, - const code_typet &code_type, - const exprt::operandst &arguments, - goto_programt &dest) +void goto_inline( + goto_modelt &goto_model, + message_handlert &message_handler, + bool adjust_function) { - // iterates over the operands - exprt::operandst::const_iterator it1=arguments.begin(); - - const code_typet::parameterst ¶meter_types= - code_type.parameters(); - - // iterates over the types of the parameters - for(const auto ¶meter : parameter_types) - { - // this is the type the n-th argument should be - const typet &par_type=ns.follow(parameter.type()); - - const irep_idt &identifier=parameter.get_identifier(); - - if(identifier==irep_idt()) - { - error().source_location=source_location; - error() << "no identifier for function parameter" << eom; - throw 0; - } - - { - const symbolt &symbol=ns.lookup(identifier); - - goto_programt::targett decl=dest.add_instruction(); - decl->make_decl(); - decl->code=code_declt(symbol.symbol_expr()); - decl->code.add_source_location()=source_location; - decl->source_location=source_location; - decl->function=function_name; - } - - // this is the actual parameter - exprt actual; - - // if you run out of actual arguments there was a mismatch - if(it1==arguments.end()) - { - warning().source_location=source_location; - warning() << "call to `" << function_name << "': " - << "not enough arguments, " - << "inserting non-deterministic value" << eom; - - actual=side_effect_expr_nondett(par_type); - } - else - actual=*it1; - - // nil means "don't assign" - if(actual.is_nil()) - { - } - else - { - // it should be the same exact type as the parameter, - // subject to some exceptions - if(!base_type_eq(par_type, actual.type(), ns)) - { - const typet &f_partype = ns.follow(par_type); - const typet &f_acttype = ns.follow(actual.type()); - - // we are willing to do some conversion - if((f_partype.id()==ID_pointer && - f_acttype.id()==ID_pointer) || - (f_partype.id()==ID_pointer && - f_acttype.id()==ID_array && - f_partype.subtype()==f_acttype.subtype())) - { - actual.make_typecast(par_type); - } - else if((f_partype.id()==ID_signedbv || - f_partype.id()==ID_unsignedbv || - f_partype.id()==ID_bool) && - (f_acttype.id()==ID_signedbv || - f_acttype.id()==ID_unsignedbv || - f_acttype.id()==ID_bool)) - { - actual.make_typecast(par_type); - } - else - { - error().source_location=actual.find_source_location(); - - error() << "function call: argument `" << identifier - << "' type mismatch: argument is `" - // << from_type(ns, identifier, actual.type()) - << actual.type().pretty() - << "', parameter is `" - << from_type(ns, identifier, par_type) - << "'" << eom; - throw 0; - } - } - - // adds an assignment of the actual parameter to the formal parameter - code_assignt assignment(symbol_exprt(identifier, par_type), actual); - assignment.add_source_location()=source_location; - - dest.add_instruction(ASSIGN); - dest.instructions.back().source_location=source_location; - dest.instructions.back().code.swap(assignment); - dest.instructions.back().function=function_name; - } - - if(it1!=arguments.end()) - ++it1; - } - - if(it1!=arguments.end()) - { - // too many arguments -- we just ignore that, no harm done - } + const namespacet ns(goto_model.symbol_table); + goto_inline( + goto_model.goto_functions, + ns, + message_handler, + adjust_function); } /*******************************************************************\ -Function: goto_inlinet::parameter_destruction +Function: goto_inline Inputs: @@ -164,168 +56,72 @@ Function: goto_inlinet::parameter_destruction \*******************************************************************/ -void goto_inlinet::parameter_destruction( - const source_locationt &source_location, - const irep_idt &function_name, - const code_typet &code_type, - goto_programt &dest) +void goto_inline( + goto_functionst &goto_functions, + const namespacet &ns, + message_handlert &message_handler, + bool adjust_function) { - const code_typet::parameterst ¶meter_types= - code_type.parameters(); + goto_inlinet goto_inline( + goto_functions, + ns, + message_handler, + adjust_function); - // iterates over the types of the parameters - for(const auto ¶meter : parameter_types) - { - const irep_idt &identifier=parameter.get_identifier(); + typedef goto_functionst::goto_functiont goto_functiont; - if(identifier==irep_idt()) - { - error().source_location=source_location; - error() << "no identifier for function parameter" << eom; - throw 0; - } + // find entry point + goto_functionst::function_mapt::iterator it= + goto_functions.function_map.find(goto_functionst::entry_point()); - { - const symbolt &symbol=ns.lookup(identifier); - - goto_programt::targett dead=dest.add_instruction(); - dead->make_dead(); - dead->code=code_deadt(symbol.symbol_expr()); - dead->code.add_source_location()=source_location; - dead->source_location=source_location; - dead->function=function_name; - } - } -} + if(it==goto_functions.function_map.end()) + return; -/*******************************************************************\ + goto_functiont &goto_function=it->second; + assert(goto_function.body_available()); -Function: goto_inlinet::replace_return + // gather all calls + // we use non-transitive inlining to avoid the goto program + // copying that goto_inlinet would do otherwise + goto_inlinet::inline_mapt inline_map; - Inputs: + Forall_goto_functions(f_it, goto_functions) + { + goto_functiont &goto_function=f_it->second; - Outputs: + if(!goto_function.body_available()) + continue; - Purpose: + goto_inlinet::call_listt &call_list=inline_map[f_it->first]; -\*******************************************************************/ + goto_programt &goto_program=goto_function.body; -void goto_inlinet::replace_return( - goto_programt &dest, - const exprt &lhs, - const exprt &constrain) -{ - for(goto_programt::instructionst::iterator - it=dest.instructions.begin(); - it!=dest.instructions.end(); - it++) - { - if(it->is_return()) - { - #if 0 - if(lhs.is_not_nil()) + Forall_goto_program_instructions(i_it, goto_program) { - if(it->code.operands().size()!=1) - { - error().source_location=it->code.find_source_location(); - str << "return expects one operand!"; - warning_msg(); + if(!goto_inlinet::is_call(i_it)) continue; - } - - goto_programt tmp; - goto_programt::targett assignment=tmp.add_instruction(ASSIGN); - - code_assignt code_assign(lhs, it->code.op0()); - - // this may happen if the declared return type at the call site - // differs from the defined return type - if(code_assign.lhs().type()!= - code_assign.rhs().type()) - code_assign.rhs().make_typecast(code_assign.lhs().type()); - assignment->code=code_assign; - assignment->source_location=it->source_location; - assignment->function=it->function; - - if(constrain.is_not_nil() && !constrain.is_true()) - { - codet constrain(ID_bp_constrain); - constrain.reserve_operands(2); - constrain.move_to_operands(assignment->code); - constrain.copy_to_operands(constrain); - } - - dest.insert_before_swap(it, *assignment); - it++; + call_list.push_back(goto_inlinet::callt(i_it, false)); } - else if(!it->code.operands().empty()) - { - goto_programt tmp; - goto_programt::targett expression=tmp.add_instruction(OTHER); - - expression->code=codet(ID_expression); - expression->code.move_to_operands(it->code.op0()); - expression->source_location=it->source_location; - expression->function=it->function; + } - dest.insert_before_swap(it, *expression); - it++; - } + goto_inline.goto_inline( + goto_functionst::entry_point(), goto_function, inline_map, true); - it->make_goto(--dest.instructions.end()); - #else - if(lhs.is_not_nil()) - { - if(it->code.operands().size()!=1) - { - warning().source_location=it->code.find_source_location(); - warning() << "return expects one operand!\n" - << it->code.pretty() << eom; - continue; - } - - code_assignt code_assign(lhs, it->code.op0()); - - // this may happen if the declared return type at the call site - // differs from the defined return type - if(code_assign.lhs().type()!= - code_assign.rhs().type()) - code_assign.rhs().make_typecast(code_assign.lhs().type()); - - if(constrain.is_not_nil() && !constrain.is_true()) - { - codet constrain(ID_bp_constrain); - constrain.reserve_operands(2); - constrain.move_to_operands(code_assign); - constrain.copy_to_operands(constrain); - it->code=constrain; - it->type=OTHER; - } - else - { - it->code=code_assign; - it->type=ASSIGN; - } - - it++; - } - else if(!it->code.operands().empty()) - { - codet expression(ID_expression); - expression.move_to_operands(it->code.op0()); - it->code=expression; - it->type=OTHER; - it++; - } - #endif + // clean up + Forall_goto_functions(f_it, goto_functions) + { + if(f_it->first!=goto_functionst::entry_point()) + { + goto_functiont &goto_function=f_it->second; + goto_function.body.clear(); } } } /*******************************************************************\ -Function: replace_location +Function: goto_partial_inline Inputs: @@ -335,27 +131,24 @@ Function: replace_location \*******************************************************************/ -void replace_location( - source_locationt &dest, - const source_locationt &new_location) +void goto_partial_inline( + goto_modelt &goto_model, + message_handlert &message_handler, + unsigned smallfunc_limit, + bool adjust_function) { - // we copy, and then adjust for property_id, property_class - // and comment, if necessary - - irep_idt comment=dest.get_comment(); - irep_idt property_class=dest.get_property_class(); - irep_idt property_id=dest.get_property_id(); - - dest=new_location; - - if(comment!=irep_idt()) dest.set_comment(comment); - if(property_class!=irep_idt()) dest.set_property_class(property_class); - if(property_id!=irep_idt()) dest.set_property_id(property_id); + const namespacet ns(goto_model.symbol_table); + goto_partial_inline( + goto_model.goto_functions, + ns, + message_handler, + smallfunc_limit, + adjust_function); } /*******************************************************************\ -Function: replace_location +Function: goto_partial_inline Inputs: @@ -365,262 +158,82 @@ Function: replace_location \*******************************************************************/ -void replace_location( - exprt &dest, - const source_locationt &new_location) +void goto_partial_inline( + goto_functionst &goto_functions, + const namespacet &ns, + message_handlert &message_handler, + unsigned smallfunc_limit, + bool adjust_function) { - Forall_operands(it, dest) - replace_location(*it, new_location); - - if(dest.find(ID_C_source_location).is_not_nil()) - replace_location(dest.add_source_location(), new_location); -} - -/*******************************************************************\ - -Function: goto_inlinet::expand_function_call - - Inputs: - - Outputs: - - Purpose: + goto_inlinet goto_inline( + goto_functions, + ns, + message_handler, + adjust_function); -\*******************************************************************/ + typedef goto_functionst::goto_functiont goto_functiont; -void goto_inlinet::expand_function_call( - goto_programt &dest, - goto_programt::targett &target, - const exprt &lhs, - const symbol_exprt &function, - const exprt::operandst &arguments, - const exprt &constrain, - bool full) -{ - // look it up - const irep_idt identifier=function.get_identifier(); - - // we ignore certain calls - if(identifier=="__CPROVER_cleanup" || - identifier=="__CPROVER_set_must" || - identifier=="__CPROVER_set_may" || - identifier=="__CPROVER_clear_must" || - identifier=="__CPROVER_clear_may" || - identifier=="__CPROVER_cover") - { - target++; - return; // ignore - } + // gather all calls + goto_inlinet::inline_mapt inline_map; - // see if we are already expanding it - if(recursion_set.find(identifier)!=recursion_set.end()) + Forall_goto_functions(f_it, goto_functions) { - if(!full) - { - target++; - return; // simply ignore, we don't do full inlining, it's ok - } + goto_functiont &goto_function=f_it->second; - // it's really recursive, and we need full inlining. - // Uh. Buh. Give up. - warning().source_location=function.find_source_location(); - warning() << "recursion is ignored" << eom; - target->make_skip(); + if(!goto_function.body_available()) + continue; - target++; - return; - } + goto_programt &goto_program=goto_function.body; - goto_functionst::function_mapt::iterator m_it= - goto_functions.function_map.find(identifier); + goto_inlinet::call_listt &call_list=inline_map[f_it->first]; - if(m_it==goto_functions.function_map.end()) - { - if(!full) + Forall_goto_program_instructions(i_it, goto_program) { - target++; - return; // simply ignore, we don't do full inlining, it's ok - } + if(!goto_inlinet::is_call(i_it)) + continue; - error().source_location=function.find_source_location(); - error() << "failed to find function `" << identifier << "'" << eom; - throw 0; - } + exprt lhs; + exprt function_expr; + exprt::operandst arguments; + exprt constrain; - const goto_functionst::goto_functiont &f=m_it->second; + goto_inlinet::get_call(i_it, lhs, function_expr, arguments, constrain); - // see if we need to inline this - if(!full) - { - if(!f.body_available() || - (!f.is_inlined() && f.body.instructions.size() > smallfunc_limit)) - { - target++; - return; - } - } + if(function_expr.id()!=ID_symbol) + continue; - if(f.body_available()) - { - recursion_set.insert(identifier); + const symbol_exprt &symbol_expr=to_symbol_expr(function_expr); + const irep_idt id=symbol_expr.get_identifier(); - // first make sure that this one is already inlined - goto_inline_rec(m_it, full); + goto_functionst::function_mapt::const_iterator f_it= + goto_functions.function_map.find(id); - goto_programt tmp2; - tmp2.copy_from(f.body); + if(f_it==goto_functions.function_map.end()) + continue; - assert(tmp2.instructions.back().is_end_function()); - tmp2.instructions.back().type=LOCATION; + // called function + const goto_functiont &goto_function=f_it->second; - replace_return(tmp2, lhs, constrain); + if(!goto_function.body_available()) + continue; - goto_programt tmp; - parameter_assignments(target->source_location, identifier, f.type, arguments, tmp); - tmp.destructive_append(tmp2); - parameter_destruction(target->source_location, identifier, f.type, tmp); + const goto_programt &goto_program=goto_function.body; - if(f.is_hidden()) - { - source_locationt new_source_location= - function.find_source_location(); - - if(new_source_location.is_not_nil()) + if(goto_function.is_inlined() || + goto_program.instructions.size()<=smallfunc_limit) { - new_source_location.set_hide(); - - Forall_goto_program_instructions(it, tmp) - { - if(it->function==identifier) - { - // don't hide assignment to lhs - if(it->is_assign() && to_code_assign(it->code).lhs()==lhs) - { - } - else - { - replace_location(it->source_location, new_source_location); - replace_location(it->guard, new_source_location); - replace_location(it->code, new_source_location); - } - - it->function=target->function; - } - } + assert(goto_inlinet::is_call(i_it)); + call_list.push_back(goto_inlinet::callt(i_it, false)); } } - - // set up location instruction for function call - target->type=LOCATION; - target->code.clear(); - - goto_programt::targett next_target(target); - next_target++; - - dest.instructions.splice(next_target, tmp.instructions); - target=next_target; - - recursion_set.erase(identifier); } - else // no body available - { - if(no_body_set.insert(identifier).second) - { - 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); - } - - // now just kill call - target->type=LOCATION; - target->code.clear(); - target++; - - // insert tmp - dest.instructions.splice(target, tmp.instructions); - } -} - -/*******************************************************************\ - -Function: goto_inlinet::goto_inline - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void goto_inlinet::goto_inline(goto_programt &dest) -{ - goto_inline_rec(dest, true); - replace_return(dest, - static_cast(get_nil_irep()), - static_cast(get_nil_irep())); -} - -/*******************************************************************\ - -Function: goto_inlinet::goto_inline_rec - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void goto_inlinet::goto_inline_rec( - goto_functionst::function_mapt::iterator f_it, - bool full) -{ - // already done? - - if(finished_inlining_set.find(f_it->first)!= - finished_inlining_set.end()) - return; // yes - - // do it - - goto_inline_rec(f_it->second.body, full); - - // remember we did it - - finished_inlining_set.insert(f_it->first); + goto_inline.goto_inline(inline_map, false); } /*******************************************************************\ -Function: goto_inlinet::goto_inline_rec +Function: goto_function_inline Inputs: @@ -630,86 +243,23 @@ Function: goto_inlinet::goto_inline_rec \*******************************************************************/ -void goto_inlinet::goto_inline_rec(goto_programt &dest, bool full) -{ - bool changed=false; - - for(goto_programt::instructionst::iterator - it=dest.instructions.begin(); - it!=dest.instructions.end(); - ) // no it++, done by inline_instruction - { - if(inline_instruction(dest, full, it)) - changed=true; - } - - if(changed) - { - remove_skip(dest); - dest.update(); - } -} - -/*******************************************************************\ - -Function: goto_inlinet::inline_instruction - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -bool goto_inlinet::inline_instruction( - goto_programt &dest, - bool full, - goto_programt::targett &it) +void goto_function_inline( + goto_modelt &goto_model, + const irep_idt function, + message_handlert &message_handler, + bool adjust_function) { - if(it->is_function_call()) - { - const code_function_callt &call=to_code_function_call(it->code); - - if(call.function().id()==ID_symbol) - { - expand_function_call( - dest, it, call.lhs(), to_symbol_expr(call.function()), - call.arguments(), - static_cast(get_nil_irep()), full); - - return true; - } - } - else if(it->is_other()) - { - // these are for Boolean programs - if(it->code.get(ID_statement)==ID_bp_constrain && - it->code.operands().size()==2 && - it->code.op0().operands().size()==2 && - it->code.op0().op1().get(ID_statement)==ID_function_call) - { - expand_function_call( - dest, it, - it->code.op0().op0(), // lhs - to_symbol_expr(it->code.op0().op1().op0()), // function - it->code.op0().op1().op1().operands(), // arguments - it->code.op1(), // constraint - full); - - return true; - } - } - - // advance iterator - it++; - - return false; + const namespacet ns(goto_model.symbol_table); + goto_function_inline( + goto_model.goto_functions, + function, + ns, + message_handler); } /*******************************************************************\ -Function: goto_inline +Function: goto_function_inline Inputs: @@ -719,75 +269,51 @@ Function: goto_inline \*******************************************************************/ -void goto_inline( +void goto_function_inline( goto_functionst &goto_functions, + const irep_idt function, const namespacet &ns, - message_handlert &message_handler) + message_handlert &message_handler, + bool adjust_function) { - goto_inlinet goto_inline(goto_functions, ns, message_handler); - - try - { - // find entry point - goto_functionst::function_mapt::iterator it= - goto_functions.function_map.find(goto_functionst::entry_point()); - - if(it==goto_functions.function_map.end()) - return; - - goto_inline.goto_inline(it->second.body); - } - - catch(int) - { - goto_inline.error(); - throw 0; - } + goto_inlinet goto_inline( + goto_functions, + ns, + message_handler, + adjust_function); - catch(const char *e) - { - goto_inline.error() << e << messaget::eom; - throw 0; - } + goto_functionst::function_mapt::iterator f_it= + goto_functions.function_map.find(function); - catch(const std::string &e) - { - goto_inline.error() << e << messaget::eom; - throw 0; - } + if(f_it==goto_functions.function_map.end()) + return; - // clean up - for(goto_functionst::function_mapt::iterator - it=goto_functions.function_map.begin(); - it!=goto_functions.function_map.end(); - it++) - if(it->first!=goto_functionst::entry_point()) - it->second.body.clear(); -} + goto_functionst::goto_functiont &goto_function=f_it->second; -/*******************************************************************\ + if(!goto_function.body_available()) + return; -Function: goto_inline + // gather all calls + goto_inlinet::inline_mapt inline_map; - Inputs: + goto_inlinet::call_listt &call_list=inline_map[f_it->first]; - Outputs: + goto_programt &goto_program=goto_function.body; - Purpose: + Forall_goto_program_instructions(i_it, goto_program) + { + if(!goto_inlinet::is_call(i_it)) + continue; -\*******************************************************************/ + call_list.push_back(goto_inlinet::callt(i_it, true)); + } -void goto_inline( - goto_modelt &goto_model, - message_handlert &message_handler) -{ - const namespacet ns(goto_model.symbol_table); - goto_inline(goto_model.goto_functions, ns, message_handler); + goto_inline.goto_inline(function, goto_function, inline_map, true); } /*******************************************************************\ -Function: goto_partial_inline +Function: goto_function_inline_and_log Inputs: @@ -797,65 +323,48 @@ Function: goto_partial_inline \*******************************************************************/ -void goto_partial_inline( +jsont goto_function_inline_and_log( goto_functionst &goto_functions, + const irep_idt function, const namespacet &ns, message_handlert &message_handler, - unsigned _smallfunc_limit) + bool adjust_function) { goto_inlinet goto_inline( goto_functions, ns, - message_handler); + message_handler, + adjust_function); - goto_inline.smallfunc_limit=_smallfunc_limit; + goto_functionst::function_mapt::iterator f_it= + goto_functions.function_map.find(function); - try - { - for(goto_functionst::function_mapt::iterator - it=goto_functions.function_map.begin(); - it!=goto_functions.function_map.end(); - it++) - if(it->second.body_available()) - goto_inline.goto_inline_rec(it, false); - } + if(f_it==goto_functions.function_map.end()) + return jsont(); - catch(int) - { - goto_inline.error(); - throw 0; - } + goto_functionst::goto_functiont &goto_function=f_it->second; - catch(const char *e) - { - goto_inline.error() << e << messaget::eom; - throw 0; - } + if(!goto_function.body_available()) + return jsont(); - catch(const std::string &e) - { - goto_inline.error() << e << messaget::eom; - throw 0; - } -} + // gather all calls + goto_inlinet::inline_mapt inline_map; -/*******************************************************************\ + goto_inlinet::call_listt &call_list=inline_map[f_it->first]; -Function: goto_partial_inline + goto_programt &goto_program=goto_function.body; - Inputs: - - Outputs: + Forall_goto_program_instructions(i_it, goto_program) + { + if(!goto_inlinet::is_call(i_it)) + continue; - Purpose: + call_list.push_back(goto_inlinet::callt(i_it, true)); + } -\*******************************************************************/ + goto_inline.goto_inline(function, goto_function, inline_map, true); + goto_functions.update(); + goto_functions.compute_loop_numbers(); -void goto_partial_inline( - goto_modelt &goto_model, - message_handlert &message_handler, - unsigned _smallfunc_limit) -{ - const namespacet ns(goto_model.symbol_table); - goto_partial_inline(goto_model.goto_functions, ns, message_handler, _smallfunc_limit); + return goto_inline.output_inline_log_json(); } diff --git a/src/goto-programs/goto_inline.h b/src/goto-programs/goto_inline.h index da4cdb22ae2..33566319100 100644 --- a/src/goto-programs/goto_inline.h +++ b/src/goto-programs/goto_inline.h @@ -9,34 +9,61 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_GOTO_PROGRAMS_GOTO_INLINE_H #define CPROVER_GOTO_PROGRAMS_GOTO_INLINE_H +#include + #include "goto_model.h" class message_handlert; // do a full inlining + +void goto_inline( + goto_modelt &goto_model, + message_handlert &message_handler, + bool adjust_function=false); + void goto_inline( goto_functionst &goto_functions, const namespacet &ns, - message_handlert &message_handler); + message_handlert &message_handler, + bool adjust_function=false); -// do a full inlining -void goto_inline( - goto_modelt &goto_model, - message_handlert &message_handler); +// inline those functions marked as "inlined" and functions with less +// than _smallfunc_limit instructions -// inline those functions marked as "inlined" -// and functions with less than _smallfunc_limit instructions void goto_partial_inline( goto_modelt &goto_model, message_handlert &message_handler, - unsigned _smallfunc_limit = 0); + unsigned smallfunc_limit=0, + bool adjust_function=false); -// inline those functions marked as "inlined" -// and functions with less than _smallfunc_limit instructions void goto_partial_inline( goto_functionst &goto_functions, const namespacet &ns, message_handlert &message_handler, - unsigned _smallfunc_limit = 0); + unsigned smallfunc_limit=0, + bool adjust_function=false); + +// transitively inline all calls the given function makes + +void goto_function_inline( + goto_modelt &goto_model, + const irep_idt function, + message_handlert &message_handler, + bool adjust_function=false); + +void goto_function_inline( + goto_functionst &goto_functions, + const irep_idt function, + const namespacet &ns, + message_handlert &message_handler, + bool adjust_function=false); + +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); #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 new file mode 100644 index 00000000000..917d5c2b9fa --- /dev/null +++ b/src/goto-programs/goto_inline_class.cpp @@ -0,0 +1,1327 @@ +/*******************************************************************\ + +Module: Function Inlining + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +// #define DEBUG + +#ifdef DEBUG +#include +#endif + +#include + +#include +#include +#include +#include +#include +#include + +#include "remove_skip.h" +#include "goto_inline.h" +#include "goto_inline_class.h" + +/*******************************************************************\ + +Function: goto_inlinet::parameter_assignments + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_inlinet::parameter_assignments( + const goto_programt::targett target, + const irep_idt &function_name, // name of called function + const code_typet &code_type, // type of called function + const exprt::operandst &arguments, // arguments of call + goto_programt &dest) +{ + assert(is_call(target)); + assert(dest.empty()); + + const source_locationt &source_location=target->source_location; + + // iterates over the operands + exprt::operandst::const_iterator it1=arguments.begin(); + + const code_typet::parameterst ¶meter_types= + code_type.parameters(); + + // iterates over the types of the parameters + for(code_typet::parameterst::const_iterator + it2=parameter_types.begin(); + it2!=parameter_types.end(); + it2++) + { + const code_typet::parametert ¶meter=*it2; + + // this is the type the n-th argument should be + const typet &par_type=ns.follow(parameter.type()); + + const irep_idt &identifier=parameter.get_identifier(); + + if(identifier==irep_idt()) + { + error().source_location=source_location; + error() << "no identifier for function parameter" << eom; + throw 0; + } + + { + const symbolt &symbol=ns.lookup(identifier); + + goto_programt::targett decl=dest.add_instruction(); + decl->make_decl(); + decl->code=code_declt(symbol.symbol_expr()); + decl->code.add_source_location()=source_location; + decl->source_location=source_location; + decl->function=adjust_function?target->function:function_name; + } + + // this is the actual parameter + exprt actual; + + // if you run out of actual arguments there was a mismatch + if(it1==arguments.end()) + { + warning().source_location=source_location; + warning() << "call to `" << function_name << "': " + << "not enough arguments, " + << "inserting non-deterministic value" << eom; + + actual=side_effect_expr_nondett(par_type); + } + else + actual=*it1; + + // nil means "don't assign" + if(actual.is_nil()) + { + } + else + { + // it should be the same exact type as the parameter, + // subject to some exceptions + if(!base_type_eq(par_type, actual.type(), ns)) + { + const typet &f_partype=ns.follow(par_type); + const typet &f_acttype=ns.follow(actual.type()); + + // we are willing to do some conversion + if((f_partype.id()==ID_pointer && + f_acttype.id()==ID_pointer) || + (f_partype.id()==ID_pointer && + f_acttype.id()==ID_array && + f_partype.subtype()==f_acttype.subtype())) + { + actual.make_typecast(par_type); + } + else if((f_partype.id()==ID_signedbv || + f_partype.id()==ID_unsignedbv || + f_partype.id()==ID_bool) && + (f_acttype.id()==ID_signedbv || + f_acttype.id()==ID_unsignedbv || + f_acttype.id()==ID_bool)) + { + actual.make_typecast(par_type); + } + else + { + error().source_location=actual.find_source_location(); + + error() << "function call: argument `" << identifier + << "' type mismatch: argument is `" + // << from_type(ns, identifier, actual.type()) + << actual.type().pretty() + << "', parameter is `" + << from_type(ns, identifier, par_type) + << "'" << eom; + throw 0; + } + } + + // adds an assignment of the actual parameter to the formal parameter + code_assignt assignment(symbol_exprt(identifier, par_type), actual); + assignment.add_source_location()=source_location; + + dest.add_instruction(ASSIGN); + dest.instructions.back().source_location=source_location; + dest.instructions.back().code.swap(assignment); + dest.instructions.back().function= + adjust_function?target->function:function_name; + } + + if(it1!=arguments.end()) + ++it1; + } + + if(it1!=arguments.end()) + { + // too many arguments -- we just ignore that, no harm done + } +} + +/*******************************************************************\ + +Function: goto_inlinet::parameter_destruction + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_inlinet::parameter_destruction( + const goto_programt::targett target, + const irep_idt &function_name, // name of called function + const code_typet &code_type, // type of called function + goto_programt &dest) +{ + assert(is_call(target)); + assert(dest.empty()); + + const source_locationt &source_location=target->source_location; + + const code_typet::parameterst ¶meter_types= + code_type.parameters(); + + // iterates over the types of the parameters + for(code_typet::parameterst::const_iterator + it=parameter_types.begin(); + it!=parameter_types.end(); + it++) + { + const code_typet::parametert ¶meter=*it; + + const irep_idt &identifier=parameter.get_identifier(); + + if(identifier==irep_idt()) + { + error().source_location=source_location; + error() << "no identifier for function parameter" << eom; + throw 0; + } + + { + const symbolt &symbol=ns.lookup(identifier); + + goto_programt::targett dead=dest.add_instruction(); + dead->make_dead(); + dead->code=code_deadt(symbol.symbol_expr()); + dead->code.add_source_location()=source_location; + dead->source_location=source_location; + dead->function=adjust_function?target->function:function_name; + } + } +} + +/*******************************************************************\ + +Function: goto_inlinet::replace_return + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_inlinet::replace_return( + goto_programt &dest, // inlining this + const exprt &lhs, // lhs in caller + const exprt &constrain) +{ + for(goto_programt::instructionst::iterator + it=dest.instructions.begin(); + it!=dest.instructions.end(); + it++) + { + if(it->is_return()) + { + #if 0 + if(lhs.is_not_nil()) + { + if(it->code.operands().size()!=1) + { + error().source_location=it->code.find_source_location(); + str << "return expects one operand!"; + warning_msg(); + continue; + } + + goto_programt tmp; + goto_programt::targett assignment=tmp.add_instruction(ASSIGN); + + code_assignt code_assign(lhs, it->code.op0()); + + // this may happen if the declared return type at the call site + // differs from the defined return type + if(code_assign.lhs().type()!= + code_assign.rhs().type()) + code_assign.rhs().make_typecast(code_assign.lhs().type()); + + assignment->code=code_assign; + assignment->source_location=it->source_location; + assignment->function=it->function; + + if(constrain.is_not_nil() && !constrain.is_true()) + { + codet constrain(ID_bp_constrain); + constrain.reserve_operands(2); + constrain.move_to_operands(assignment->code); + constrain.copy_to_operands(constrain); + } + + dest.insert_before_swap(it, *assignment); + it++; + } + else if(!it->code.operands().empty()) + { + goto_programt tmp; + goto_programt::targett expression=tmp.add_instruction(OTHER); + + expression->code=codet(ID_expression); + expression->code.move_to_operands(it->code.op0()); + expression->source_location=it->source_location; + expression->function=it->function; + + dest.insert_before_swap(it, *expression); + it++; + } + + it->make_goto(--dest.instructions.end()); + #else + if(lhs.is_not_nil()) + { + if(it->code.operands().size()!=1) + { + warning().source_location=it->code.find_source_location(); + warning() << "return expects one operand!\n" + << it->code.pretty() << eom; + continue; + } + + code_assignt code_assign(lhs, it->code.op0()); + + // this may happen if the declared return type at the call site + // differs from the defined return type + if(code_assign.lhs().type()!= + code_assign.rhs().type()) + code_assign.rhs().make_typecast(code_assign.lhs().type()); + + if(constrain.is_not_nil() && !constrain.is_true()) + { + codet constrain(ID_bp_constrain); + constrain.reserve_operands(2); + constrain.move_to_operands(code_assign); + constrain.copy_to_operands(constrain); + it->code=constrain; + it->type=OTHER; + } + else + { + it->code=code_assign; + it->type=ASSIGN; + } + + it++; + } + else if(!it->code.operands().empty()) + { + codet expression(ID_expression); + expression.move_to_operands(it->code.op0()); + it->code=expression; + it->type=OTHER; + it++; + } + #endif + } + } +} + +/*******************************************************************\ + +Function: replace_location + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void replace_location( + source_locationt &dest, + const source_locationt &new_location) +{ + // we copy, and then adjust for property_id, property_class + // and comment, if necessary + + irep_idt comment=dest.get_comment(); + irep_idt property_class=dest.get_property_class(); + irep_idt property_id=dest.get_property_id(); + + dest=new_location; + + if(comment!=irep_idt()) + dest.set_comment(comment); + + if(property_class!=irep_idt()) + dest.set_property_class(property_class); + + if(property_id!=irep_idt()) + dest.set_property_id(property_id); +} + +/*******************************************************************\ + +Function: replace_location + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void replace_location( + exprt &dest, + const source_locationt &new_location) +{ + Forall_operands(it, dest) + replace_location(*it, new_location); + + if(dest.find(ID_C_source_location).is_not_nil()) + replace_location(dest.add_source_location(), new_location); +} + +/*******************************************************************\ + +Function: goto_inlinet::insert_function_body + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_inlinet::insert_function_body( + const goto_functiont &goto_function, + goto_programt &dest, + goto_programt::targett target, + const exprt &lhs, + const symbol_exprt &function, + const exprt::operandst &arguments, + const exprt &constrain) +{ + assert(is_call(target)); + assert(!dest.empty()); + assert(goto_function.body_available()); + + const irep_idt identifier=function.get_identifier(); + + goto_programt body; + body.copy_from(goto_function.body); + inline_log.copy_from(goto_function.body, body); + + goto_programt::instructiont &end=body.instructions.back(); + assert(end.is_end_function()); + end.type=LOCATION; + + if(adjust_function) + Forall_goto_program_instructions(i_it, body) + i_it->function=target->function; + + replace_return(body, lhs, constrain); + + goto_programt tmp1; + parameter_assignments( + target, + identifier, + goto_function.type, + arguments, + tmp1); + + goto_programt tmp2; + parameter_destruction(target, identifier, goto_function.type, tmp2); + + goto_programt tmp; + tmp.destructive_append(tmp1); // par assignment + tmp.destructive_append(body); // body + tmp.destructive_append(tmp2); // par destruction + + goto_programt::const_targett t_it; + t_it=goto_function.body.instructions.begin(); + unsigned begin_location_number=t_it->location_number; + t_it=--goto_function.body.instructions.end(); + assert(t_it->is_end_function()); + unsigned end_location_number=t_it->location_number; + + unsigned call_location_number=target->location_number; + + inline_log.add_segment( + tmp, + begin_location_number, + end_location_number, + call_location_number, + identifier); + +#if 0 + if(goto_function.is_hidden()) + { + source_locationt new_source_location= + function.find_source_location(); + + if(new_source_location.is_not_nil()) + { + new_source_location.set_hide(); + + Forall_goto_program_instructions(it, tmp) + { + if(it->function==identifier) + { + // don't hide assignment to lhs + if(it->is_assign() && to_code_assign(it->code).lhs()==lhs) + { + } + else + { + replace_location(it->source_location, new_source_location); + replace_location(it->guard, new_source_location); + replace_location(it->code, new_source_location); + } + + it->function=target->function; + } + } + } + } +#endif + + // kill call + target->type=LOCATION; + target->code.clear(); + target++; + + dest.destructive_insert(target, tmp); +} + +/*******************************************************************\ + +Function: goto_inlinet::insert_function_nobody + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_inlinet::insert_function_nobody( + goto_programt &dest, + const exprt &lhs, + goto_programt::targett target, + const symbol_exprt &function, + const exprt::operandst &arguments) +{ + assert(is_call(target)); + assert(!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); +} + +/*******************************************************************\ + +Function: goto_inlinet::expand_function_call + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_inlinet::expand_function_call( + goto_programt &dest, + const inline_mapt &inline_map, + const bool transitive, + const bool force_full, + goto_programt::targett target) +{ + assert(is_call(target)); + assert(!dest.empty()); + assert(!transitive || inline_map.empty()); + +#ifdef DEBUG + std::cout << "Expanding call:" << std::endl; + dest.output_instruction(ns, "", std::cout, target); +#endif + + exprt lhs; + exprt function_expr; + exprt::operandst arguments; + exprt constrain; + + get_call(target, lhs, function_expr, arguments, constrain); + + if(function_expr.id()!=ID_symbol) + return; + + const symbol_exprt &function=to_symbol_expr(function_expr); + + const irep_idt identifier=function.get_identifier(); + + if(is_ignored(identifier)) + return; + + // see if we are already expanding it + if(recursion_set.find(identifier)!=recursion_set.end()) + { + // it's recursive. + // Uh. Buh. Give up. + warning().source_location=function.find_source_location(); + warning() << "recursion is ignored on call to `" << identifier << "'" + << eom; + + if(force_full) + target->make_skip(); + + return; + } + + goto_functionst::function_mapt::iterator f_it= + goto_functions.function_map.find(identifier); + + if(f_it==goto_functions.function_map.end()) + { + warning().source_location=function.find_source_location(); + warning() << "missing function `" << identifier << "' is ignored" << eom; + + if(force_full) + target->make_skip(); + + return; + } + + // function to inline + goto_functiont &goto_function=f_it->second; + + if(goto_function.body_available()) + { + if(transitive) + { + const goto_functiont &cached= + goto_inline_transitive( + identifier, + goto_function, + force_full); + + // insert 'cached' into 'dest' at 'target' + insert_function_body( + cached, + dest, + target, + lhs, + function, + arguments, + constrain); + } + else + { + // inline non-transitively + goto_inline_nontransitive( + identifier, + goto_function, + inline_map, + force_full); + + // insert 'goto_function' into 'dest' at 'target' + insert_function_body( + goto_function, + dest, + target, + lhs, + function, + arguments, + constrain); + } + } + else // no body available + { + insert_function_nobody(dest, lhs, target, function, arguments); + } +} + +/*******************************************************************\ + +Function: goto_inlinet::get_call + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_inlinet::get_call( + goto_programt::const_targett it, + exprt &lhs, + exprt &function, + exprt::operandst &arguments, + exprt &constrain) +{ + assert(is_call(it)); + + if(it->is_function_call()) + { + const code_function_callt &call=to_code_function_call(it->code); + + lhs=call.lhs(); + function=call.function(); + arguments=call.arguments(); + constrain=static_cast(get_nil_irep()); + } + else + { + assert(is_bp_call(it)); + + lhs=it->code.op0().op0(); + function=to_symbol_expr(it->code.op0().op1().op0()); + arguments=it->code.op0().op1().op1().operands(); + constrain=it->code.op1(); + } +} + +/*******************************************************************\ + +Function: goto_inlinet::is_call + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool goto_inlinet::is_call(goto_programt::const_targett it) +{ + return it->is_function_call() || is_bp_call(it); +} + +/*******************************************************************\ + +Function: goto_inlinet::is_bp_call + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool goto_inlinet::is_bp_call(goto_programt::const_targett it) +{ + if(!it->is_other()) + return false; + + return it->code.get(ID_statement)==ID_bp_constrain && + it->code.operands().size()==2 && + it->code.op0().operands().size()==2 && + it->code.op0().op1().get(ID_statement)==ID_function_call; +} + +/*******************************************************************\ + +Function: goto_inline + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_inlinet::goto_inline( + const inline_mapt &inline_map, + const bool force_full) +{ + assert(check_inline_map(inline_map)); + + Forall_goto_functions(f_it, goto_functions) + { + const irep_idt identifier=f_it->first; + assert(!identifier.empty()); + goto_functiont &goto_function=f_it->second; + + if(!goto_function.body_available()) + continue; + + goto_inline(identifier, goto_function, inline_map, force_full); + } +} + +/*******************************************************************\ + +Function: goto_inline + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_inlinet::goto_inline( + const irep_idt identifier, + goto_functiont &goto_function, + const inline_mapt &inline_map, + const bool force_full) +{ + recursion_set.clear(); + + goto_inline_nontransitive( + identifier, + goto_function, + inline_map, + force_full); +} + +/*******************************************************************\ + +Function: goto_inline + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_inlinet::goto_inline_nontransitive( + const irep_idt identifier, + goto_functiont &goto_function, + const inline_mapt &inline_map, + const bool force_full) +{ + assert(goto_function.body_available()); + + finished_sett::const_iterator f_it=finished_set.find(identifier); + + if(f_it!=finished_set.end()) + return; + + assert(check_inline_map(identifier, inline_map)); + + goto_programt &goto_program=goto_function.body; + + const inline_mapt::const_iterator im_it=inline_map.find(identifier); + + if(im_it==inline_map.end()) + return; + + const call_listt &call_list=im_it->second; + + if(call_list.empty()) + return; + + recursion_set.insert(identifier); + + for(call_listt::const_iterator c_it=call_list.begin(); + c_it!=call_list.end(); c_it++) + { + const callt &call=*c_it; + const bool transitive=call.second; + + const inline_mapt &new_inline_map= + transitive?inline_mapt():inline_map; + + expand_function_call( + goto_program, + new_inline_map, + transitive, + force_full, + call.first); + } + + recursion_set.erase(identifier); + + // remove_skip(goto_program); + // goto_program.update(); // does not change loop ids + + finished_set.insert(identifier); +} + +/*******************************************************************\ + +Function: goto_inline_transitive + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +const goto_inlinet::goto_functiont &goto_inlinet::goto_inline_transitive( + const irep_idt identifier, + const goto_functiont &goto_function, + const bool force_full) +{ + assert(goto_function.body_available()); + + cachet::const_iterator c_it=cache.find(identifier); + + if(c_it!=cache.end()) + { + const goto_functiont &cached=c_it->second; + assert(cached.body_available()); + return cached; + } + + goto_functiont &cached=cache[identifier]; + assert(cached.body.empty()); + cached.copy_from(goto_function); // location numbers not changed + inline_log.copy_from(goto_function.body, cached.body); + + goto_programt &goto_program=cached.body; + + goto_programt::targetst call_list; + + for(goto_programt::targett i_it=goto_program.instructions.begin(); + i_it!=goto_program.instructions.end(); i_it++) + { + if(is_call(i_it)) + call_list.push_back(i_it); + } + + if(call_list.empty()) + return cached; + + recursion_set.insert(identifier); + + for(goto_programt::targetst::iterator c_it=call_list.begin(); + c_it!=call_list.end(); c_it++) + { + expand_function_call( + goto_program, + inline_mapt(), + true, + force_full, + *c_it); + } + + recursion_set.erase(identifier); + + // remove_skip(goto_program); + // goto_program.update(); // does not change loop ids + + return cached; +} + +/*******************************************************************\ + +Function: is_ignored + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool goto_inlinet::is_ignored(const irep_idt id) const +{ + return + id=="__CPROVER_cleanup" || + id=="__CPROVER_set_must" || + id=="__CPROVER_set_may" || + id=="__CPROVER_clear_must" || + id=="__CPROVER_clear_may" || + id=="__CPROVER_cover"; +} + +/*******************************************************************\ + +Function: check_inline_map + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool goto_inlinet::check_inline_map( + const irep_idt identifier, + const inline_mapt &inline_map) const +{ + goto_functionst::function_mapt::const_iterator f_it= + goto_functions.function_map.find(identifier); + + assert(f_it!=goto_functions.function_map.end()); + + inline_mapt::const_iterator im_it=inline_map.find(identifier); + + if(im_it==inline_map.end()) + return true; + + const call_listt &call_list=im_it->second; + + if(call_list.empty()) + return true; + + int ln=-1; + + for(call_listt::const_iterator c_it=call_list.begin(); + c_it!=call_list.end(); c_it++) + { + const callt &call=*c_it; + const goto_programt::const_targett target=call.first; + +#if 0 + // might not hold if call was previously inlined + if(target->function!=identifier) + return false; +#endif + + // location numbers increasing + if(static_cast(target->location_number)<=ln) + return false; + + if(!is_call(target)) + return false; + + ln=target->location_number; + } + + return true; +} + +/*******************************************************************\ + +Function: check_inline_map + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool goto_inlinet::check_inline_map(const inline_mapt &inline_map) const +{ + forall_goto_functions(f_it, goto_functions) + { + if(!check_inline_map(f_it->first, inline_map)) + return false; + } + + return true; +} + +/*******************************************************************\ + +Function: output_inline_map + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_inlinet::output_inline_map( + std::ostream &out, + const inline_mapt &inline_map) +{ + assert(check_inline_map(inline_map)); + + for(inline_mapt::const_iterator it=inline_map.begin(); + it!=inline_map.end(); it++) + { + const irep_idt id=it->first; + const call_listt &call_list=it->second; + + out << "Function: " << id << "\n"; + + goto_functionst::function_mapt::const_iterator f_it= + goto_functions.function_map.find(id); + + std::string call="-"; + + if(f_it!=goto_functions.function_map.end() && + !call_list.empty()) + { + const goto_functiont &goto_function=f_it->second; + assert(goto_function.body_available()); + + const goto_programt &goto_program=goto_function.body; + + for(call_listt::const_iterator c_it=call_list.begin(); + c_it!=call_list.end(); c_it++) + { + const callt &call=*c_it; + const goto_programt::const_targett target=call.first; + bool transitive=call.second; + + out << " Call:\n"; + goto_program.output_instruction(ns, "", out, target); + out << " Transitive: " << transitive << "\n"; + } + } + else + { + out << " -\n"; + } + } +} + +/*******************************************************************\ + +Function: cleanup + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +// remove segment that refer to the given goto program +void goto_inlinet::goto_inline_logt::cleanup( + const goto_programt &goto_program) +{ + forall_goto_program_instructions(it, goto_program) + log_map.erase(it); +} + +/*******************************************************************\ + +Function: cleanup + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_inlinet::goto_inline_logt::cleanup( + const goto_functionst::function_mapt &function_map) +{ + for(goto_functionst::function_mapt::const_iterator it= + function_map.begin(); it!=function_map.end(); it++) + { + const goto_functiont &goto_function=it->second; + + if(!goto_function.body_available()) + continue; + + cleanup(goto_function.body); + } +} + +/*******************************************************************\ + +Function: add_segment + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_inlinet::goto_inline_logt::add_segment( + const goto_programt &goto_program, + const unsigned begin_location_number, + const unsigned end_location_number, + const unsigned call_location_number, + const irep_idt function) +{ + assert(!goto_program.empty()); + assert(!function.empty()); + assert(end_location_number>=begin_location_number); + + goto_programt::const_targett start=goto_program.instructions.begin(); + assert(log_map.find(start)==log_map.end()); + + goto_programt::const_targett end=goto_program.instructions.end(); + end--; + + goto_inline_log_infot info; + info.begin_location_number=begin_location_number; + info.end_location_number=end_location_number; + info.call_location_number=call_location_number; + info.function=function; + info.end=end; + + log_map[start]=info; +} + +/*******************************************************************\ + +Function: copy_from + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_inlinet::goto_inline_logt::copy_from( + const goto_programt &from, + const goto_programt &to) +{ + assert(from.instructions.size()==to.instructions.size()); + + goto_programt::const_targett it1=from.instructions.begin(); + goto_programt::const_targett it2=to.instructions.begin(); + + for(; it1!=from.instructions.end(); it1++, it2++) + { + assert(it2!=to.instructions.end()); + assert(it1->location_number==it2->location_number); + + log_mapt::const_iterator l_it=log_map.find(it1); + if(l_it!=log_map.end()) + { + assert(log_map.find(it2)==log_map.end()); + + goto_inline_log_infot info=l_it->second; + goto_programt::const_targett end=info.end; + + // find end of new + goto_programt::const_targett tmp_it=it1; + goto_programt::const_targett new_end=it2; + while(tmp_it!=end) + { + new_end++; + tmp_it++; + } + + info.end=new_end; + + log_map[it2]=info; + } + } +} + +/*******************************************************************\ + +Function: output_inline_log_json + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +// call after goto_functions.update()! +jsont goto_inlinet::goto_inline_logt::output_inline_log_json() const +{ + json_objectt json_result; + json_arrayt &json_inlined=json_result["inlined"].make_array(); + + for(log_mapt::const_iterator it=log_map.begin(); + it!=log_map.end(); it++) + { + json_objectt &object=json_inlined.push_back().make_object(); + + goto_programt::const_targett start=it->first; + const goto_inline_log_infot &info=it->second; + goto_programt::const_targett end=info.end; + + assert(start->location_number<=end->location_number); + + object["call"]=json_numbert(std::to_string(info.call_location_number)); + object["function"]=json_stringt(info.function.c_str()); + + json_arrayt &json_orig=object["original_segment"].make_array(); + json_orig.push_back()=json_numbert(std::to_string( + info.begin_location_number)); + json_orig.push_back()=json_numbert(std::to_string( + info.end_location_number)); + + json_arrayt &json_new=object["inlined_segment"].make_array(); + json_new.push_back()=json_numbert(std::to_string(start->location_number)); + json_new.push_back()=json_numbert(std::to_string(end->location_number)); + } + + return json_result; +} diff --git a/src/goto-programs/goto_inline_class.h b/src/goto-programs/goto_inline_class.h index 8ffb33d010b..495ce7d9155 100644 --- a/src/goto-programs/goto_inline_class.h +++ b/src/goto-programs/goto_inline_class.h @@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include #include "goto_functions.h" @@ -19,46 +21,162 @@ class goto_inlinet:public messaget { public: goto_inlinet( - goto_functionst &_goto_functions, - const namespacet &_ns, - message_handlert &_message_handler): - messaget(_message_handler), - smallfunc_limit(0), - goto_functions(_goto_functions), - ns(_ns) + goto_functionst &goto_functions, + const namespacet &ns, + message_handlert &message_handler, + bool adjust_function): + messaget(message_handler), + goto_functions(goto_functions), + ns(ns), + adjust_function(adjust_function) { } - void goto_inline(goto_programt &dest); + typedef goto_functionst::goto_functiont goto_functiont; - void goto_inline_rec( - goto_functionst::function_mapt::iterator, - bool full); + // call that should be inlined + // false: inline non-transitively + // true: inline transitively + typedef std::pair callt; - void goto_inline_rec(goto_programt &dest, bool full); + // list of calls that should be inlined + typedef std::list call_listt; - // inline single instruction at 'target' - // returns true in case a change was done - // set 'full' to perform this recursively - bool inline_instruction( - goto_programt &dest, - bool full, - goto_programt::targett &target); + // list of calls per function that should be inlined + typedef std::map inline_mapt; + + // handle given goto function + // force_full: + // - true: put skip on recursion and issue warning + // - false: leave call on recursion + void goto_inline( + const irep_idt identifier, + goto_functiont &goto_function, + const inline_mapt &inline_map, + const bool force_full=false); - unsigned smallfunc_limit; + // handle all functions + void goto_inline( + const inline_mapt &inline_map, + const bool force_full=false); + + void output_inline_map( + std::ostream &out, + const inline_mapt &inline_map); + + // call after goto_functions.update()! + jsont output_inline_log_json() + { + inline_log.cleanup(cache); + return inline_log.output_inline_log_json(); + } + + // is bp call + static bool is_bp_call(goto_programt::const_targett target); + // is normal or bp call + static bool is_call(goto_programt::const_targett target); + // get call info of normal or bp call + static void get_call( + goto_programt::const_targett target, + exprt &lhs, + exprt &function, + exprt::operandst &arguments, + exprt &constrain); + + class goto_inline_logt + { + public: + class goto_inline_log_infot + { + public: + // original segment location numbers + unsigned begin_location_number; + unsigned end_location_number; + unsigned call_location_number; // original call location number + irep_idt function; // function from which segment was inlined + goto_programt::const_targett end; // segment end + }; + + // remove segment that refer to the given goto program + void cleanup(const goto_programt &goto_program); + + void cleanup(const goto_functionst::function_mapt &function_map); + + void add_segment( + const goto_programt &goto_program, + const unsigned begin_location_number, + const unsigned end_location_number, + const unsigned call_location_number, + const irep_idt function); + + void copy_from(const goto_programt &from, const goto_programt &to); + + // call after goto_functions.update()! + jsont output_inline_log_json() const; + + // map from segment start to inline info + typedef std::map< + goto_programt::const_targett, + goto_inline_log_infot> log_mapt; + + log_mapt log_map; + }; protected: goto_functionst &goto_functions; const namespacet &ns; + const bool adjust_function; + goto_inline_logt inline_log; + + void goto_inline_nontransitive( + const irep_idt identifier, + goto_functiont &goto_function, + const inline_mapt &inline_map, + const bool force_full); + + const goto_functiont &goto_inline_transitive( + const irep_idt identifier, + const goto_functiont &goto_function, + const bool force_full); + + bool check_inline_map(const inline_mapt &inline_map) const; + bool check_inline_map( + const irep_idt identifier, + const inline_mapt &inline_map) const; + + bool is_ignored(const irep_idt id) const; + + void clear() + { + cache.clear(); + finished_set.clear(); + recursion_set.clear(); + no_body_set.clear(); + } + void expand_function_call( goto_programt &dest, - goto_programt::targett &target, + const inline_mapt &inline_map, + const bool transitive, + const bool force_full, + goto_programt::targett target); + + void insert_function_body( + const goto_functiont &f, + goto_programt &dest, + goto_programt::targett target, const exprt &lhs, const symbol_exprt &function, const exprt::operandst &arguments, - const exprt &constrain, - bool recursive); + const exprt &constrain); + + 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, @@ -66,26 +184,30 @@ class goto_inlinet:public messaget const exprt &constrain); void parameter_assignments( - const source_locationt &source_location, + const goto_programt::targett target, const irep_idt &function_name, const code_typet &code_type, const exprt::operandst &arguments, goto_programt &dest); void parameter_destruction( - const source_locationt &source_location, + const goto_programt::targett target, const irep_idt &function_name, const code_typet &code_type, goto_programt &dest); + // goto functions that were already inlined transitively + typedef goto_functionst::function_mapt cachet; + cachet cache; + + typedef std::unordered_set finished_sett; + finished_sett finished_set; + typedef std::unordered_set recursion_sett; recursion_sett recursion_set; typedef std::unordered_set no_body_sett; no_body_sett no_body_set; - - typedef std::unordered_set finished_inlining_sett; - finished_inlining_sett finished_inlining_set; }; #endif // CPROVER_GOTO_PROGRAMS_GOTO_INLINE_CLASS_H