From 22fb7c18e8c72df1328775cb28cef58805ee3aa8 Mon Sep 17 00:00:00 2001 From: "konstantinos.pouliasis@gmail.com" Date: Thu, 7 Sep 2017 15:47:29 -0400 Subject: [PATCH] added splice-call feature in goto instrument It prepends a nullary function call say foo in the body of another call say moo when called as --splice-call moo,foo added tests --- .../goto-instrument/splice_call_01/main.c | 9 +++ .../goto-instrument/splice_call_01/test.desc | 7 ++ src/goto-instrument/Makefile | 1 + .../goto_instrument_parse_options.cpp | 15 ++++ .../goto_instrument_parse_options.h | 4 +- src/goto-instrument/splice_call.cpp | 79 +++++++++++++++++++ src/goto-instrument/splice_call.h | 27 +++++++ 7 files changed, 141 insertions(+), 1 deletion(-) create mode 100644 regression/goto-instrument/splice_call_01/main.c create mode 100644 regression/goto-instrument/splice_call_01/test.desc create mode 100644 src/goto-instrument/splice_call.cpp create mode 100644 src/goto-instrument/splice_call.h diff --git a/regression/goto-instrument/splice_call_01/main.c b/regression/goto-instrument/splice_call_01/main.c new file mode 100644 index 00000000000..563a264ae24 --- /dev/null +++ b/regression/goto-instrument/splice_call_01/main.c @@ -0,0 +1,9 @@ +void moo() +{ + return; +} + +int main() +{ + return 0; +} diff --git a/regression/goto-instrument/splice_call_01/test.desc b/regression/goto-instrument/splice_call_01/test.desc new file mode 100644 index 00000000000..c397504aeb0 --- /dev/null +++ b/regression/goto-instrument/splice_call_01/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--splice-call main,moo +activate-multi-line-match +moo\(\);\n.*function main.* +EXIT=0 +SIGNAL=0 \ No newline at end of file diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index 6d54c94fae3..da86474e7f1 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -46,6 +46,7 @@ SRC = accelerate/accelerate.cpp \ rw_set.cpp \ show_locations.cpp \ skip_loops.cpp \ + splice_call.cpp \ stack_depth.cpp \ thread_instrumentation.cpp \ undefined_functions.cpp \ diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 397dfc10536..da99f9a2be0 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -96,6 +96,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "model_argc_argv.h" #include "undefined_functions.h" #include "remove_function.h" +#include "splice_call.h" void goto_instrument_parse_optionst::eval_verbosity() { @@ -1408,6 +1409,19 @@ void goto_instrument_parse_optionst::instrument_goto_program() full_slicer(goto_model); } + // splice option + if(cmdline.isset("splice-call")) + { + status() << "Performing call splicing" << eom; + std::string callercallee=cmdline.get_value("splice-call"); + if(splice_call( + goto_model.goto_functions, + callercallee, + goto_model.symbol_table, + get_message_handler())) + throw 0; + } + // recalculate numbers, etc. goto_model.goto_functions.update(); } @@ -1474,6 +1488,7 @@ void goto_instrument_parse_optionst::help() " --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" // NOLINT(*) + " --splice-call caller,callee prepends a call to callee in the body of caller\n" // NOLINT(*) // NOLINTNEXTLINE(whitespace/line_length) " --undefined-function-is-assume-false\n" // NOLINTNEXTLINE(whitespace/line_length) " convert each call to an undefined function to assume(false)\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 2a921437603..04b3a8f7b2b 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -77,7 +77,9 @@ Author: Daniel Kroening, kroening@kroening.com "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \ "(show-threaded)(list-calls-args)(print-path-lengths)" \ "(undefined-function-is-assume-false)" \ - "(remove-function-body):" + "(remove-function-body):"\ + "(splice-call):" \ + class goto_instrument_parse_optionst: public parse_options_baset, diff --git a/src/goto-instrument/splice_call.cpp b/src/goto-instrument/splice_call.cpp new file mode 100644 index 00000000000..f8e13872d98 --- /dev/null +++ b/src/goto-instrument/splice_call.cpp @@ -0,0 +1,79 @@ +/*******************************************************************\ + +Module: Prepend/ splice a 0-ary function call in the beginning of a function +e.g. for setting/ modelling the global environment + +Author: Konstantinos Pouliasis + +Date: July 2017 + +\*******************************************************************/ + +/// \file +/// Prepend a nullary call to another function +// useful for context/ environment setting in arbitrary nodes + +#include "splice_call.h" +#include +#include +#include +#include +#include +#include + +// split the argument in caller/ callee two-position vector +// expect input as a string of two names glued with comma: "caller,callee" +static bool parse_caller_callee( + const std::string &callercallee, + std::vector &result) +{ + split_string(callercallee, ',', result); + return (result.size()!= 2); +} + +bool splice_call( + goto_functionst &goto_functions, + const std::string &callercallee, + const symbol_tablet &symbol_table, + message_handlert &message_handler) +{ + messaget message(message_handler); + const namespacet ns(symbol_table); + std::vector caller_callee; + if(parse_caller_callee(callercallee, caller_callee)) + { + message.error() << "Expecting two function names seperated by a comma" + << messaget::eom; + return true; + } + goto_functionst::function_mapt::iterator caller_fun= + goto_functions.function_map.find(caller_callee[0]); + goto_functionst::function_mapt::const_iterator callee_fun= + goto_functions.function_map.find(caller_callee[1]); + if(caller_fun==goto_functions.function_map.end()) + { + message.error() << "Caller function does not exist" << messaget::eom; + return true; + } + if(!caller_fun->second.body_available()) + { + message.error() << "Caller function has no available body" << messaget::eom; + return true; + } + if(callee_fun==goto_functions.function_map.end()) + { + message.error() << "Callee function does not exist" << messaget::eom; + return true; + } + goto_programt::const_targett start= + caller_fun->second.body.instructions.begin(); + goto_programt::targett g= + caller_fun->second.body.insert_before(start); + code_function_callt splice_call; + splice_call.function()=ns.lookup(callee_fun->first).symbol_expr(); + g->make_function_call(to_code_function_call(splice_call)); + + // update counters etc. + goto_functions.update(); + return false; +} diff --git a/src/goto-instrument/splice_call.h b/src/goto-instrument/splice_call.h new file mode 100644 index 00000000000..703946d2bba --- /dev/null +++ b/src/goto-instrument/splice_call.h @@ -0,0 +1,27 @@ +/*******************************************************************\ + +Module: Prepend/ splice a 0-ary function call in the beginning of a function +e.g. for setting/ modelling the global environment + +Author: Konstantinos Pouliasis + +Date: July 2017 + +\*******************************************************************/ + +/// \file +/// Harnessing for goto functions + +#ifndef CPROVER_GOTO_INSTRUMENT_SPLICE_CALL_H +#define CPROVER_GOTO_INSTRUMENT_SPLICE_CALL_H + +#include +class message_handlert; + +bool splice_call( + goto_functionst &goto_functions, + const std::string &callercallee, + const symbol_tablet &symbol_table, + message_handlert &message_handler); + +#endif // CPROVER_GOTO_INSTRUMENT_SPLICE_CALL_H