Added flag for goto-instrument to just remove const function pointers

thk123 · thk123 · commit cae911c3d6f2 · 2017-02-14T11:32:48.000Z
Added a flag --remove-const-function-pointers for goto-instrument that
can be used
instead of --remove-function-pointers to only remove function pointers
where we can resolve to something more precise that all functions with a
matching signature.
diff --git a/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/main.c b/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/main.c
@@ -0,0 +1,34 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i\n", 1); }
+void f2 (void) { printf("%i\n", 2); }
+void f3 (void) { printf("%i\n", 3); }
+void f4 (void) { printf("%i\n", 4); }
+void f5 (void) { printf("%i\n", 5); }
+void f6 (void) { printf("%i\n", 6); }
+void f7 (void) { printf("%i\n", 7); }
+void f8 (void) { printf("%i\n", 8); }
+void f9 (void) { printf("%i\n", 9); }
+
+typedef void(*void_fp)(void);
+
+const void_fp fp_tbl[] = {f2, f3 ,f4};
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func(int i)
+{
+  fp_tbl[i]();
+}
+
+int main()
+{
+  for(int i=0;i<3;i++)
+  {
+    func(i);
+  }
+
+  return 0;
+}
diff --git a/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc b/regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc
@@ -0,0 +1,16 @@
+CORE
+main.c
+--verbosity 10 --pointer-check --remove-const-function-pointers
+
+^\s*IF fp_tbl\[(signed long int)i\] == f2 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[(signed long int)i\] == f3 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[(signed long int)i\] == f4 THEN GOTO [0-9]$
+^SIGNAL=0$
+--
+^\s*IF fp_tbl\[(signed long int)i\] == f1 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[(signed long int)i\] == f5 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[(signed long int)i\] == f6 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[(signed long int)i\] == f7 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[(signed long int)i\] == f8 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[(signed long int)i\] == f9 THEN GOTO [0-9]$
+^warning: ignoring
diff --git a/regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/main.c b/regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/main.c
@@ -0,0 +1,34 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i\n", 1); }
+void f2 (void) { printf("%i\n", 2); }
+void f3 (void) { printf("%i\n", 3); }
+void f4 (void) { printf("%i\n", 4); }
+void f5 (void) { printf("%i\n", 5); }
+void f6 (void) { printf("%i\n", 6); }
+void f7 (void) { printf("%i\n", 7); }
+void f8 (void) { printf("%i\n", 8); }
+void f9 (void) { printf("%i\n", 9); }
+
+typedef void(*void_fp)(void);
+
+const void_fp fp_tbl[] = {f2, f3 ,f4};
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func(int i)
+{
+  fp_tbl[i]();
+}
+
+int main()
+{
+  for(int i=0;i<3;i++)
+  {
+    func(i);
+  }
+
+  return 0;
+}
diff --git a/regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/test.desc b/regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/test.desc
@@ -0,0 +1,16 @@
+CORE
+main.c
+--verbosity 10 --pointer-check --remove-function-pointers
+
+^\s*IF fp_tbl\[(signed long int)i\] == f2 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[(signed long int)i\] == f3 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[(signed long int)i\] == f4 THEN GOTO [0-9]$
+^SIGNAL=0$
+--
+^\s*IF fp_tbl\[(signed long int)i\] == f1 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[(signed long int)i\] == f5 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[(signed long int)i\] == f6 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[(signed long int)i\] == f7 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[(signed long int)i\] == f8 THEN GOTO [0-9]$
+^\s*IF fp_tbl\[(signed long int)i\] == f9 THEN GOTO [0-9]$
+^warning: ignoring
diff --git a/regression/goto-instrument/no-match-non-const-fp-only-remove-const/main.c b/regression/goto-instrument/no-match-non-const-fp-only-remove-const/main.c
@@ -0,0 +1,31 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i\n", 1); }
+void f2 (void) { printf("%i\n", 2); }
+void f3 (void) { printf("%i\n", 3); }
+void f4 (void) { printf("%i\n", 4); }
+void f5 (void) { printf("%i\n", 5); }
+void f6 (void) { printf("%i\n", 6); }
+void f7 (void) { printf("%i\n", 7); }
+void f8 (void) { printf("%i\n", 8); }
+void f9 (void) { printf("%i\n", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func()
+{
+  void_fp fp = f2;
+  fp = f3;
+  fp();
+}
+
+int main()
+{
+  func();
+
+  return 0;
+}
diff --git a/regression/goto-instrument/no-match-non-const-fp-only-remove-const/test.desc b/regression/goto-instrument/no-match-non-const-fp-only-remove-const/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--verbosity 10 --pointer-check --remove-const-function-pointers
+
+^\s*fp();$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/no-match-non-const-fp-remove-all-fp/main.c b/regression/goto-instrument/no-match-non-const-fp-remove-all-fp/main.c
@@ -0,0 +1,31 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i\n", 1); }
+void f2 (void) { printf("%i\n", 2); }
+void f3 (void) { printf("%i\n", 3); }
+void f4 (void) { printf("%i\n", 4); }
+void f5 (void) { printf("%i\n", 5); }
+void f6 (void) { printf("%i\n", 6); }
+void f7 (void) { printf("%i\n", 7); }
+void f8 (void) { printf("%i\n", 8); }
+void f9 (void) { printf("%i\n", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func()
+{
+  void_fp fp = f2;
+  fp = f3;
+  fp();
+}
+
+int main()
+{
+  func();
+
+  return 0;
+}
diff --git a/regression/goto-instrument/no-match-non-const-fp-remove-all-fp/test.desc b/regression/goto-instrument/no-match-non-const-fp-remove-all-fp/test.desc
@@ -0,0 +1,16 @@
+CORE
+main.c
+--verbosity 10 --pointer-check --remove-function-pointers
+
+^\s*IF fp == f1 THEN GOTO [0-9]$
+^\s*IF fp == f2 THEN GOTO [0-9]$
+^\s*IF fp == f3 THEN GOTO [0-9]$
+^\s*IF fp == f4 THEN GOTO [0-9]$
+^\s*IF fp == f5 THEN GOTO [0-9]$
+^\s*IF fp == f6 THEN GOTO [0-9]$
+^\s*IF fp == f7 THEN GOTO [0-9]$
+^\s*IF fp == f8 THEN GOTO [0-9]$
+^\s*IF fp == f9 THEN GOTO [0-9]$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/precise-const-fp-only-remove-const/main.c b/regression/goto-instrument/precise-const-fp-only-remove-const/main.c
@@ -0,0 +1,30 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i\n", 1); }
+void f2 (void) { printf("%i\n", 2); }
+void f3 (void) { printf("%i\n", 3); }
+void f4 (void) { printf("%i\n", 4); }
+void f5 (void) { printf("%i\n", 5); }
+void f6 (void) { printf("%i\n", 6); }
+void f7 (void) { printf("%i\n", 7); }
+void f8 (void) { printf("%i\n", 8); }
+void f9 (void) { printf("%i\n", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func()
+{
+  const void_fp fp = f2;
+  fp();
+}
+
+int main()
+{
+  func();
+
+  return 0;
+}
diff --git a/regression/goto-instrument/precise-const-fp-only-remove-const/test.desc b/regression/goto-instrument/precise-const-fp-only-remove-const/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--verbosity 10 --pointer-check --remove-const-function-pointers
+
+^\s*f2();
+--
+^warning: ignoring
diff --git a/regression/goto-instrument/precise-const-fp-remove-all-fp/main.c b/regression/goto-instrument/precise-const-fp-remove-all-fp/main.c
@@ -0,0 +1,30 @@
+#include <stdio.h>
+
+void f1 (void) { printf("%i\n", 1); }
+void f2 (void) { printf("%i\n", 2); }
+void f3 (void) { printf("%i\n", 3); }
+void f4 (void) { printf("%i\n", 4); }
+void f5 (void) { printf("%i\n", 5); }
+void f6 (void) { printf("%i\n", 6); }
+void f7 (void) { printf("%i\n", 7); }
+void f8 (void) { printf("%i\n", 8); }
+void f9 (void) { printf("%i\n", 9); }
+
+typedef void(*void_fp)(void);
+
+// There is a basic check that excludes all functions that aren't used anywhere
+// This ensures that check can't work in this example
+const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
+
+void func()
+{
+  const void_fp fp = f2;
+  fp();
+}
+
+int main()
+{
+  func();
+
+  return 0;
+}
diff --git a/regression/goto-instrument/precise-const-fp-remove-all-fp/test.desc b/regression/goto-instrument/precise-const-fp-remove-all-fp/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--verbosity 10 --pointer-check --remove-function-pointers
+
+^\s*f2();
+--
+^warning: ignoring
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -791,6 +791,39 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(
 
 /*******************************************************************\
 
+Function: goto_instrument_parse_optionst::do_remove_const_function_pointers_only
+
+  Inputs:
+
+ Outputs:
+
+ Purpose: Remove function pointers that can be resolved by analysing
+          const variables (i.e. can be resolved using
+          remove_const_function_pointers). Function pointers that cannot
+          be resolved will be left as function pointers.
+
+\*******************************************************************/
+
+void goto_instrument_parse_optionst::do_remove_const_function_pointers_only()
+{
+  // Don't bother if we've already done a full function pointer
+  // removal.
+  if(function_pointer_removal_done)
+  {
+    return;
+  }
+
+  status() << "Removing const function pointers only" << eom;
+  remove_function_pointers(
+    *message_handler,
+    symbol_table,
+    goto_functions,
+    cmdline.isset("pointer-check"),
+    true); // abort if we can't resolve via const pointers
+}
+
+/*******************************************************************\
+
 Function: goto_instrument_parse_optionst::do_partial_inlining
 
   Inputs:
@@ -1017,7 +1050,13 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
   // replace function pointers, if explicitly requested
   if(cmdline.isset("remove-function-pointers"))
+  {
     do_indirect_call_and_rtti_removal();
+  }
+  else if(cmdline.isset("remove-const-function-pointers"))
+  {
+    do_remove_const_function_pointers_only();
+  }
 
   if(cmdline.isset("function-inline"))
   {
@@ -1520,6 +1559,7 @@ void goto_instrument_parse_optionst::help()
     " --function-inline <function> transitively inline all calls <function> makes\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(*)
+    HELP_REMOVE_CONST_FUNCTION_POINTERS
     " --add-library                add models of C library functions\n"
     " --model-argc-argv <n>        model up to <n> command line arguments\n"
     "\n"
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/language_ui.h>
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/show_goto_functions.h>
+#include <goto-programs/remove_const_function_pointers.h>
 
 #include <analyses/goto_check.h>
 
@@ -54,6 +55,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(show-uninitialized)(show-locations)" \
   "(full-slice)(reachability-slice)(slice-global-inits)" \
   "(inline)(partial-inline)(function-inline):(log):" \
+  OPT_REMOVE_CONST_FUNCTION_POINTERS \
   "(remove-function-pointers)" \
   "(show-claims)(show-properties)(property):" \
   "(show-symbol-table)(show-points-to)(show-rw-set)" \
@@ -97,6 +99,7 @@ class goto_instrument_parse_optionst:
   void eval_verbosity();
 
   void do_indirect_call_and_rtti_removal(bool force=false);
+  void do_remove_const_function_pointers_only();
   void do_partial_inlining();
   void do_remove_returns();
 
diff --git a/src/goto-programs/remove_const_function_pointers.h b/src/goto-programs/remove_const_function_pointers.h
@@ -95,4 +95,11 @@ class remove_const_function_pointerst:public messaget
   const symbol_tablet &symbol_table;
 };
 
+#define OPT_REMOVE_CONST_FUNCTION_POINTERS \
+  "(remove-const-function-pointers)"
+
+#define HELP_REMOVE_CONST_FUNCTION_POINTERS \
+  " --remove-const-function-pointers    Remove function pointers that are constant or constant part of an array\n" // NOLINT(*)
+
+
 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_CONST_FUNCTION_POINTERS_H
diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp
diff --git a/src/goto-programs/remove_function_pointers.h b/src/goto-programs/remove_function_pointers.h
