Merge pull request #1360 from KPouliasis/konst_splice_call

added splice-call feature in goto instrument

Author: Daniel Kroening

regression/goto-instrument/splice_call_01/main.c

@@ -0,0 +1,9 @@
+void moo()
+{
+  return;
+}
+
+int main()
+{
+  return 0;
+}

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

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 \

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -96,6 +96,7 @@ Author: Daniel Kroening, [email protected]
 #include "model_argc_argv.h"
 #include "undefined_functions.h"
 #include "remove_function.h"
+#include "splice_call.h"
 
 void goto_instrument_parse_optionst::eval_verbosity()
 {
@@ -1392,6 +1393,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();
 }
@@ -1458,6 +1472,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"

src/goto-instrument/goto_instrument_parse_options.h

@@ -77,7 +77,9 @@ Author: Daniel Kroening, [email protected]
   "(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,

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 <util/message.h>
+#include <util/string2int.h>
+#include <util/string_utils.h>
+#include <util/language.h>
+#include <goto-programs/goto_functions.h>
+#include <algorithm>
+
+// 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<std::string> &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<std::string> 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;
+}

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 <goto-programs/goto_functions.h>
+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