goto-instrument: Replace calls to undefined functions by assume(false)

Refactoring: moving print-undefined-functions to the new source file.

Author: tautschnig

CHANGELOG

@@ -4,6 +4,7 @@
 * GOTO-INSTRUMENT: New option --list-calls-args
 * GOTO-INSTRUMENT: New option --print-path-lenghts
 * GOTO-ANALYZER: New option --unreachable-functions, --reachable-functions
+* GOTO-INSTRUMENT: New option --undefined-function-is-assume-false
 
 
 5.7

src/goto-instrument/Makefile

@@ -23,7 +23,8 @@ SRC = goto_instrument_parse_options.cpp rw_set.cpp \
       wmm/event_graph.cpp wmm/pair_collection.cpp \
       goto_instrument_main.cpp horn_encoding.cpp \
       thread_instrumentation.cpp skip_loops.cpp loop_utils.cpp \
-      code_contracts.cpp cover.cpp model_argc_argv.cpp
+      code_contracts.cpp cover.cpp model_argc_argv.cpp \
+      undefined_functions.cpp
 
 OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../cpp/cpp$(LIBEXT) \

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -89,6 +89,7 @@ Author: Daniel Kroening, [email protected]
 #include "code_contracts.h"
 #include "unwind.h"
 #include "model_argc_argv.h"
+#include "undefined_functions.h"
 
 /*******************************************************************\
 
@@ -628,11 +629,7 @@ int goto_instrument_parse_optionst::doit()
     if(cmdline.isset("list-undefined-functions"))
     {
       const namespacet ns(symbol_table);
-
-      Forall_goto_functions(it, goto_functions)
-        if(!ns.lookup(it->first).is_macro &&
-           !it->second.body_available())
-          std::cout << it->first << std::endl;
+      list_undefined_functions(goto_functions, ns, std::cout);
       return 0;
     }
 
@@ -769,6 +766,13 @@ int goto_instrument_parse_optionst::doit()
       remove_unused_functions(goto_functions, get_message_handler());
     }
 
+    if(cmdline.isset("undefined-function-is-assume-false"))
+    {
+      do_indirect_call_and_rtti_removal();
+
+      undefined_function_abort_path(goto_functions);
+    }
+
     // write new binary?
     if(cmdline.args.size()==2)
     {
@@ -1549,6 +1553,8 @@ 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(*)
+    " --undefined-function-is-assume-false\n"
+    "                              convert each call to an undefined function to assume(false)\n"
     "\n"
     "Loop transformations:\n"
     " --k-induction <k>            check loops with k-induction\n"

src/goto-instrument/goto_instrument_parse_options.h

@@ -69,7 +69,8 @@ Author: Daniel Kroening, [email protected]
   "(list-symbols)(list-undefined-functions)" \
   "(z3)(add-library)(show-dependence-graph)" \
   "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \
-  "(show-threaded)(list-calls-args)(print-path-lengths)"
+  "(show-threaded)(list-calls-args)(print-path-lengths)" \
+  "(undefined-function-is-assume-false)"
 
 class goto_instrument_parse_optionst:
   public parse_options_baset,

src/goto-instrument/undefined_functions.cpp

@@ -0,0 +1,81 @@
+/*******************************************************************\
+
+Module: Handling of functions without body
+
+Author: Michael Tautschnig
+
+Date: July 2016
+
+\*******************************************************************/
+
+#include <ostream>
+
+#include <goto-programs/goto_functions.h>
+
+#include "undefined_functions.h"
+
+/*******************************************************************\
+
+Function: list_undefined_functions
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void list_undefined_functions(
+  const goto_functionst &goto_functions,
+  const namespacet &ns,
+  std::ostream &os)
+{
+  forall_goto_functions(it, goto_functions)
+    if(!ns.lookup(it->first).is_macro &&
+       !it->second.body_available())
+      os << it->first << std::endl;
+}
+
+/*******************************************************************\
+
+Function: undefined_function_abort_path
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void undefined_function_abort_path(goto_functionst &goto_functions)
+{
+  Forall_goto_functions(it, 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;
+
+      const irep_idt &function=
+        to_symbol_expr(call.function()).get_identifier();
+
+      goto_functionst::function_mapt::const_iterator entry=
+        goto_functions.function_map.find(function);
+      assert(entry!=goto_functions.function_map.end());
+
+      if(entry->second.body_available())
+        continue;
+
+      ins.make_assumption(false_exprt());
+      ins.source_location.set_comment(
+        "`"+id2string(function)+"' is undefined");
+    }
+}

src/goto-instrument/undefined_functions.h

@@ -0,0 +1,25 @@
+/*******************************************************************\
+
+Module: Handling of functions without body
+
+Author: Michael Tautschnig
+
+Date: July 2016
+
+\*******************************************************************/
+
+#ifndef CPROVER_UNDEFINED_FUNCTIONS_H
+#define CPROVER_UNDEFINED_FUNCTIONS_H
+
+#include <iosfwd>
+
+class goto_functionst;
+
+void list_undefined_functions(
+  const goto_functionst &goto_functions,
+  const namespacet &ns,
+  std::ostream &os);
+
+void undefined_function_abort_path(goto_functionst &goto_functions);
+
+#endif