goto-instrument: function pointer removal with value_set_fi

This adds a new option to goto-instrument for removing function pointers.
The points-to analysis is done using flow-insensitive value sets, which is
more precise than using the signature of the function to identify the
points-to set.

Author: Daniel Kroening

regression/goto-instrument/value-set-fi-fp-removal/test.c

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+typedef void (*fp_t)();
+
+void f()
+{
+}
+
+void g()
+{
+}
+
+int main(void)
+{
+  fp_t fp = f;
+  fp();
+
+  // this would fool an analysis that looks for functions whose address is taken
+  fp_t other_fp = g;
+}

regression/goto-instrument/value-set-fi-fp-removal/test.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--value-set-fi-fp-removal
+^EXIT=0$
+^SIGNAL=0$
+^  function: f$
+--
+^  function: g$
+--
+This test checks that the value-set-fi-based function pointer removal
+precisely identifies the function to call for a particular function pointer
+call.

src/goto-instrument/Makefile

@@ -67,6 +67,7 @@ SRC = accelerate/accelerate.cpp \
       uninitialized.cpp \
       unwind.cpp \
       unwindset.cpp \
+      value_set_fi_fp_removal.cpp \
       wmm/abstract_event.cpp \
       wmm/cycle_collection.cpp \
       wmm/data_dp.cpp \

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -54,6 +54,7 @@ Author: Daniel Kroening, [email protected]
 #include <pointer-analysis/goto_program_dereference.h>
 #include <pointer-analysis/show_value_sets.h>
 #include <pointer-analysis/value_set_analysis.h>
+#include <pointer-analysis/value_set_analysis_fi.h>
 
 #include <analyses/call_graph.h>
 #include <analyses/constant_propagator.h>
@@ -111,6 +112,7 @@ Author: Daniel Kroening, [email protected]
 #include "undefined_functions.h"
 #include "uninitialized.h"
 #include "unwind.h"
+#include "value_set_fi_fp_removal.h"
 #include "wmm/weak_memory.h"
 
 /// invoke main modules
@@ -293,6 +295,17 @@ int goto_instrument_parse_optionst::doit()
       return CPROVER_EXIT_SUCCESS;
     }
 
+    if(cmdline.isset("show-value-set-fi"))
+    {
+      namespacet ns(goto_model.symbol_table);
+      value_set_analysis_fit value_set(
+        ns, value_set_analysis_fit::track_optionst::TRACK_FUNCTION_POINTERS);
+
+      value_set(goto_model.goto_functions);
+      value_set.output(goto_model.goto_functions, std::cout);
+      return CPROVER_EXIT_SUCCESS;
+    }
+
     if(cmdline.isset("show-global-may-alias"))
     {
       do_indirect_call_and_rtti_removal();
@@ -906,7 +919,6 @@ int goto_instrument_parse_optionst::doit()
         "goto-instrument needs one input and one output file, aside from other "
         "flags");
     }
-
     help();
     return CPROVER_EXIT_USAGE_ERROR;
   }
@@ -1198,6 +1210,12 @@ void goto_instrument_parse_optionst::instrument_goto_program()
         exit(CPROVER_EXIT_USAGE_ERROR);
   }
 
+  if(cmdline.isset("value-set-fi-fp-removal"))
+  {
+    value_set_fi_fp_removal(goto_model);
+    do_indirect_call_and_rtti_removal();
+  }
+
   // replace function pointers, if explicitly requested
   if(cmdline.isset("remove-function-pointers"))
   {
@@ -1867,6 +1885,10 @@ void goto_instrument_parse_optionst::help()
     " --no-caching                 disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
     " --log <file>                 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(*)
+    " --value-set-fi-fp-removal    build flow-insensitive value set and replace function pointers by a case statement" // NOLINT(*)
+    "                              over the possible assignments. If the set of possible assignments is empty, the function pointer" // NOLINT(*)
+    "                              is not removed \n" // NOLINT(*)
+    " --remove-function-pointers   replace function pointers by case statement over all function calls with same signature\n" // NOLINT(*)
     HELP_RESTRICT_FUNCTION_POINTER
     HELP_REMOVE_CALLS_NO_BODY
     HELP_REMOVE_CONST_FUNCTION_POINTERS

src/goto-instrument/goto_instrument_parse_options.h

@@ -74,6 +74,7 @@ Author: Daniel Kroening, [email protected]
   OPT_SHOW_PROPERTIES \
   "(drop-unused-functions)" \
   "(show-value-sets)" \
+  "(show-value-set-fi)" \
   "(show-global-may-alias)" \
   "(show-local-bitvector-analysis)(show-custom-bitvector-analysis)" \
   "(show-escape-analysis)(escape-analysis)" \
@@ -83,6 +84,8 @@ Author: Daniel Kroening, [email protected]
   "(full-slice)(reachability-slice)(slice-global-inits)" \
   "(fp-reachability-slice):" \
   "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
+  "(value-set-fi-fp-removal)" \
+  "(conservative-value-set-fi-fp-removal)" \
   OPT_REMOVE_CONST_FUNCTION_POINTERS \
   "(print-internal-representation)" \
   "(remove-function-pointers)" \