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.

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

@@ -0,0 +1,30 @@
+
+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,34 @@
+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)
+{
+  fp_t fp;
+  fp();
+
+  // the value set is empty, defaults to standard function pointer removal behaviour
+  fp_t other_fp = g;
+  other_fp = f;
+}

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 16 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)
+{
+  fp_t fp;
+  fp();
+
+  // the value set is empty, defaults to standard function pointer removal behaviour
+  fp_t other_fp = g;
+}

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

@@ -0,0 +1,11 @@
+CORE
+test.c
+--value-set-fi-fp-removal
+^EXIT=0$
+^SIGNAL=0$
+^file test.c line 16 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,20 @@
+#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
@@ -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,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)" \
@@ -107,6 +109,8 @@ Author: Daniel Kroening, [email protected]
   "(show-threaded)(list-calls-args)" \
   "(undefined-function-is-assume-false)" \
   "(remove-function-body):"\
+  "(moderate-function-pointer-removal)"\
+  "(extreme-function-pointer-removal)"\
   OPT_AGGRESSIVE_SLICER \
   OPT_FLUSH \
   "(splice-call):" \