goto-instrument: function pointer removal with value_set_fi

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.

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

@@ -0,0 +1,27 @@
+
+typedef void (*fp_t)(int, int);
+
+void add(int a, int b)
+{
+}
+void subtract(int a, int b)
+{
+}
+void multiply(int a, int b)
+{
+}
+
+int main()
+{
+  // fun_ptr_arr is an array of function pointers
+  void (*fun_ptr_arr[])(int, int) = {add, subtract, add};
+
+  // Multiply should not be added into the value set
+  fp_t other_fp = multiply;
+  void (*fun_ptr_arr2[])(int, int) = {multiply, subtract, add};
+
+  // the fp removal over-approximates and assumes this could be any pointer in the array
+  (*fun_ptr_arr[0])(1, 1);
+
+  return 0;
+}

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

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

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

@@ -0,0 +1,32 @@
+typedef void (*fp_t)(int, int);
+
+void add(int a, int b)
+{
+}
+void subtract(int a, int b)
+{
+}
+void multiply(int a, int b)
+{
+}
+
+int main()
+{
+  // fun_ptr_arr is an array of function pointers
+  struct my_struct
+  {
+    fp_t first_pointer;
+    fp_t second_pointer;
+  } struct1;
+
+  struct1.first_pointer = add;
+
+  // Multiply and subtract should not be added into the value set
+  fp_t other_fp = multiply;
+  struct1.second_pointer = subtract;
+
+  // this pointer can only be "add"
+  struct1.first_pointer(1, 1);
+
+  return 0;
+}

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

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

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

@@ -0,0 +1,21 @@
+#include <assert.h>
+
+typedef void (*fp_t)();
+
+void f()
+{
+}
+
+void g()
+{
+}
+
+int main(void)
+{
+  // the value set for fp is empty, defaults to standard function pointer removal behaviour
+  fp_t other_fp = g;
+  other_fp = f;
+
+  fp_t fp;
+  fp();
+}

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

@@ -0,0 +1,10 @@
+CORE
+test.c
+--value-set-fi-fp-removal
+^EXIT=0$
+^SIGNAL=0$
+^file test.c line 20 function main: replacing function pointer by 2 possible targets$
+--
+This test checks that the value-set-fi-based function pointer removal
+precisely identifies the function to call for a particular function pointer
+call.

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

@@ -0,0 +1,20 @@
+#include <assert.h>
+
+typedef void (*fp_t)();
+
+void f(int x)
+{
+}
+
+void g(int y)
+{
+}
+
+int main(void)
+{
+  // the value set is empty, defaults to standard function pointer removal behaviour
+  fp_t other_fp = g;
+
+  fp_t fp;
+  fp();
+}

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

@@ -0,0 +1,10 @@
+CORE
+test.c
+--value-set-fi-fp-removal
+^EXIT=0$
+^SIGNAL=0$
+^file test.c line 19 function main: replacing function pointer by 0 possible targets$
+--
+This test checks that the value-set-fi-based function pointer removal
+precisely identifies the function to call for a particular function pointer
+call.

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

@@ -0,0 +1,19 @@
+#include <assert.h>
+
+typedef void (*fp_t)(void);
+
+void f()
+{
+}
+
+void g()
+{
+}
+
+int main(void)
+{
+  fp_t fp = f;
+  fp_t decoy_fp = g;
+  fp_t *ptr_to_func_ptr = &fp; // a pointer to a function pointer
+  (*ptr_to_func_ptr)();
+}

regression/goto-instrument/value-set-fi-fp-removal6/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
@@ -1198,6 +1200,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, ui_message_handler);
+    do_indirect_call_and_rtti_removal();
+  }
+
   // replace function pointers, if explicitly requested
   if(cmdline.isset("remove-function-pointers"))
   {
@@ -1867,6 +1875,9 @@ 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\n" // NOLINT(*)
+    "                              over the possible assignments. If the set of possible assignments is empty the function pointer\n" // NOLINT(*)
+    "                              is removed using the standard remove-function-pointers pass. \n" // NOLINT(*)
     HELP_RESTRICT_FUNCTION_POINTER
     HELP_REMOVE_CALLS_NO_BODY
     HELP_REMOVE_CONST_FUNCTION_POINTERS

src/goto-instrument/goto_instrument_parse_options.h

@@ -83,6 +83,7 @@ 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)" \
   OPT_REMOVE_CONST_FUNCTION_POINTERS \
   "(print-internal-representation)" \
   "(remove-function-pointers)" \