make-function-assume-false command line option

Blocks all paths through a function by replacing the function calls with assume_false.
This is similar to --undefined-function-is-assume-false, but gives the flexibility to havoc undefined functions and block specific functions without needing multiple calls to goto-instrument.

Needed for aggressive slicer work

Author: polgreen

src/goto-instrument/Makefile

@@ -34,6 +34,7 @@ SRC = accelerate/accelerate.cpp \
       interrupt.cpp \
       k_induction.cpp \
       loop_utils.cpp \
+      make_function_assume_false.cpp \
       mmio.cpp \
       model_argc_argv.cpp \
       nondet_static.cpp \

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -97,6 +97,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "model_argc_argv.h"
 #include "undefined_functions.h"
 #include "remove_function.h"
+#include "make_function_assume_false.h"
 #include "splice_call.h"
 
 void goto_instrument_parse_optionst::eval_verbosity()
@@ -939,6 +940,14 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       get_message_handler());
   }
 
+  if(cmdline.isset("make-function-assume-false"))
+  {
+    make_functions_assume_false(
+      goto_model,
+      cmdline.get_values("make-function-assume-false"),
+      get_message_handler());
+  }
+
   // we add the library in some cases, as some analyses benefit
 
   if(cmdline.isset("add-library") ||
@@ -1521,6 +1530,8 @@ void goto_instrument_parse_optionst::help()
     " --model-argc-argv <n>        model up to <n> command line arguments\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     " --remove-function-body <f>   remove the implementation of function <f> (may be repeated)\n"
+    " --make-function-assume-false <f>\n"
+    "                              replace calls to function <f> with assume(false) (may be repeated)\n" // NOLINT(*)
     "\n"
     "Other options:\n"
     " --no-system-headers          with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*)

src/goto-instrument/goto_instrument_parse_options.h

@@ -78,6 +78,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(show-threaded)(list-calls-args)(print-path-lengths)" \
   "(undefined-function-is-assume-false)" \
   "(remove-function-body):"\
+  "(make-function-assume-false):"\
   "(splice-call):" \
 
 

src/goto-instrument/make_function_assume_false.cpp

@@ -0,0 +1,99 @@
+/*******************************************************************\
+
+Module: Make function assume false
+
+Author: Elizabeth Polgreen
+
+Date: November 2017
+
+\*******************************************************************/
+
+/// \file
+/// Make function assume false
+
+#include "make_function_assume_false.h"
+
+#include <util/message.h>
+
+#include <goto-programs/goto_model.h>
+
+/// \brief Replace calls to the function with assume(false).
+/// This effectively blocks any paths through the function
+/// or depending on return values from the function.
+/// \param goto_model  input program to be modifier
+/// \param identifier  name of function to block
+/// \param message_handler  Error/status output
+void make_function_assume_false(
+  goto_modelt &goto_model,
+  const irep_idt &identifier,
+  message_handlert &message_handler)
+{
+  messaget message(message_handler);
+
+  goto_functionst::function_mapt::iterator entry =
+    goto_model.goto_functions.function_map.find(identifier);
+
+  if(entry==goto_model.goto_functions.function_map.end())
+  {
+    message.error() << "No function " << identifier
+                    << " in goto program" << messaget::eom;
+    return;
+  }
+  else if(entry->second.is_inlined())
+  {
+    message.warning() << "Function " << identifier << " is inlined, "
+                      << "instantiations will not be blocked"
+                      << messaget::eom;
+  }
+  else
+  {
+    message.status() << "Blocking all calls to " << identifier << messaget::eom;
+
+    Forall_goto_functions(it, goto_model.goto_functions)
+    {
+      Forall_goto_program_instructions(iit, it->second.body)
+      {
+        goto_programt::instructiont &ins = *iit;
+
+        if(!ins.is_function_call())
+          continue;
+
+        const code_function_callt &call = to_code_function_call(ins.code);
+
+        if(call.function().id() != ID_symbol)
+          continue;
+
+        if(to_symbol_expr(call.function()).get_identifier() == identifier)
+        {
+          ins.make_assumption(false_exprt());
+          ins.source_location.set_comment(
+              "`"+id2string(identifier)+"'"
+                  " is marked unusable by --make-function-assume-false");
+        }
+      }
+    }
+  }
+}
+
+/// \brief Replace calls to any functions in the list
+/// "functions" with assume(false).
+/// This effectively blocks any paths through the function
+/// or depending on return values from the function.
+/// \param functions   list of function names to block
+/// \param goto_model  input program to be modifier
+/// \param message_handler  Error/status output
+void make_functions_assume_false(
+    goto_modelt &goto_model,
+    const std::list<std::string> &functions,
+    message_handlert &message_handler)
+{
+  messaget message(message_handler);
+  for(const auto &func : functions)
+  {
+    make_function_assume_false(goto_model, func, message_handler);
+  }
+}
+
+
+
+

src/goto-instrument/make_function_assume_false.h

@@ -0,0 +1,32 @@
+/*******************************************************************\
+
+Module: Make function assume false
+
+Author: Elizabeth Polgreen
+
+Date: November 2017
+
+\*******************************************************************/
+
+/// \file
+/// Make function assume false
+
+#ifndef CPROVER_GOTO_INSTRUMENT_MAKE_FUNCTION_ASSUME_FALSE_H
+#define CPROVER_GOTO_INSTRUMENT_MAKE_FUNCTION_ASSUME_FALSE_H
+
+#include <list>
+#include <string>
+
+#include <util/irep.h>
+
+class goto_modelt;
+class message_handlert;
+
+void make_functions_assume_false(
+  goto_modelt &,
+  const std::list<std::string> &names,
+  message_handlert &);
+
+
+
+#endif /* CPROVER_GOTO_INSTRUMENT_MAKE_FUNCTION_ASSUME_FALSE_H */