Merge pull request #6376 from tautschnig/restrictions

tautschnig · web-flow · commit faaf50ea689c · 2021-12-01T14:40:37.000+01:00
Use remove-function-pointers code for restricted function pointers
diff --git a/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc b/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --function foo --pointer-check
 ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) > 5: SUCCESS$
-^\[foo.pointer_dereference.\d+\] line \d+ invalid function pointer: FAILURE$
+^\[foo.pointer_dereference.\d+\] line \d+ no candidates for dereferenced function pointer: FAILURE$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED
diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc
@@ -5,7 +5,7 @@ main.c
 ^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$
 ^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$
 ^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$
-^\s*ASSERT false // invalid function pointer$
+^\s*ASSERT false // dereferenced function pointer must be one of \[f[2-4], f[2-4], f[2-4]\]$
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc b/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*ASSERT false // invalid function pointer$
+^\s*ASSERT false // no candidates for dereferenced function pointer
 ^EXIT=0$
 ^SIGNAL=0$
 function func: replacing function pointer by 0 possible targets
diff --git a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*ASSERT false // invalid function pointer$
+^\s*ASSERT false // no candidates for dereferenced function pointer
 ^EXIT=0$
 ^SIGNAL=0$
 replacing function pointer by 0 possible targets
diff --git a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*ASSERT false // invalid function pointer$
+^\s*ASSERT false // dereferenced function pointer must be one of \[(f[1-9], ){8}f[1-9]\]$
 replacing function pointer by 9 possible targets
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*ASSERT false // invalid function pointer$
+^\s*ASSERT false // dereferenced function pointer must be one of \[(f[1-9], ){8}f[1-9]\]$
 replacing function pointer by 9 possible targets
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-analyzer/no-match-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-null/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*ASSERT false // invalid function pointer$
+^\s*ASSERT false // no candidates for dereferenced function pointer
 function func: replacing function pointer by 0 possible targets
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --show-goto-functions --pointer-check
 ^Removal of function pointers and virtual functions$
-^\s*ASSERT false // invalid function pointer$
+^\s*ASSERT false // no candidates for dereferenced function pointer
 ^EXIT=0$
 ^SIGNAL=0$
 replacing function pointer by 0 possible targets
diff --git a/regression/goto-instrument/restrict-function-pointer-by-name-global/test.desc b/regression/goto-instrument/restrict-function-pointer-by-name-global/test.desc
@@ -1,10 +1,10 @@
 CORE
 test.c
 --restrict-function-pointer-by-name fp/f,g
-\[main\.assertion\.1\] line \d+ dereferenced function pointer at main\.function_pointer_call\.1 must be one of \[(f, g)|(g, f)\]: SUCCESS
+\[main\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be one of \[(f, g)|(g, f)\]: SUCCESS
+\[main.assertion.1\] line \d+ assertion: FAILURE
 \[main.assertion.2\] line \d+ assertion: FAILURE
-\[main.assertion.3\] line \d+ assertion: FAILURE
-\[main.assertion.4\] line \d+ assertion: SUCCESS
+\[main.assertion.3\] line \d+ assertion: SUCCESS
 f\(\)
 g\(\)
 ^EXIT=10$
diff --git a/regression/goto-instrument/restrict-function-pointer-by-name-local/test.desc b/regression/goto-instrument/restrict-function-pointer-by-name-local/test.desc
@@ -1,8 +1,8 @@
 CORE
 test.c
 --restrict-function-pointer-by-name main::1::fp/f
-\[main\.assertion\.1\] line \d+ dereferenced function pointer at main\.function_pointer_call\.1 must be f: SUCCESS
-\[main\.assertion\.2\] line \d+ assertion fp\(\) == 1: SUCCESS
+\[main\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be f: SUCCESS
+\[main\.assertion\.1\] line \d+ assertion fp\(\) == 1: SUCCESS
 f\(\)
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/restrict-function-pointer-by-name-parameter/test.desc b/regression/goto-instrument/restrict-function-pointer-by-name-parameter/test.desc
@@ -1,8 +1,8 @@
 CORE
 test.c
 --restrict-function-pointer-by-name use_fp::fp/f
-\[use_fp\.assertion\.1\] line \d+ dereferenced function pointer at use_fp\.function_pointer_call\.1 must be f: SUCCESS
-\[use_fp\.assertion\.2\] line \d+ assertion fp\(\) == 1: SUCCESS
+\[use_fp\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be f: SUCCESS
+\[use_fp\.assertion\.1\] line \d+ assertion fp\(\) == 1: SUCCESS
 f\(\)
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/restrict-function-pointer-goto-target/test.desc b/regression/goto-instrument/restrict-function-pointer-goto-target/test.desc
@@ -3,7 +3,7 @@ test.c
 --restrict-function-pointer main.function_pointer_call.1/f
 ^EXIT=0$
 ^SIGNAL=0$
-\[main.assertion.1\] line \d+ dereferenced function pointer at main.function_pointer_call.1 must be f: SUCCESS
+\[main.pointer_dereference.1\] line \d+ dereferenced function pointer must be f: SUCCESS
 --
 --
 This test checks that a function pointer call that is the target of a goto (in
diff --git a/regression/goto-instrument/restrict-function-pointer-to-compatible-function/test.c b/regression/goto-instrument/restrict-function-pointer-to-compatible-function/test.c
@@ -0,0 +1,28 @@
+#include <assert.h>
+
+typedef int (*fptr_t)(long long);
+
+void use_f(fptr_t fptr)
+{
+  assert(fptr(10) == 11);
+}
+
+int f(int x)
+{
+  return x + 1;
+}
+
+int g(int x)
+{
+  return x;
+}
+
+int main(void)
+{
+  int one = 1;
+
+  // We take the address of f and g. In this case remove_function_pointers()
+  // would create a case distinction involving both f and g in the function
+  // use_f() above.
+  use_f(one ? f : g);
+}
diff --git a/regression/goto-instrument/restrict-function-pointer-to-compatible-function/test.desc b/regression/goto-instrument/restrict-function-pointer-to-compatible-function/test.desc
@@ -0,0 +1,10 @@
+CORE
+test.c
+--restrict-function-pointer use_f.function_pointer_call.1/f
+\[use_f\.assertion\.1\] line \d+ assertion fptr\(10\) == 11: SUCCESS
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test checks that the function f is permitted for the first function pointer
+call in function use_f, despite parameters having different integer types.
diff --git a/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc b/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc
@@ -1,8 +1,8 @@
 CORE
 test.c
 --restrict-function-pointer 'use_fg.function_pointer_call.1/f,g'
-\[use_fg.assertion.2\] line \d+ assertion \(choice \? fptr : gptr\)\(10\) == 10 \+ choice: SUCCESS
-\[use_fg.assertion.1\] line \d+ dereferenced function pointer at use_fg.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: SUCCESS
+\[use_fg.assertion.1\] line \d+ assertion \(choice \? fptr : gptr\)\(10\) == 10 \+ choice: SUCCESS
+\[use_fg.pointer_dereference.1\] line \d+ dereferenced function pointer must be one of \[(f|g), (f|g)\]: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc
@@ -1,7 +1,7 @@
 CORE
 test.c
 --restrict-function-pointer use_f.function_pointer_call.1/f,g
-\[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: FAILURE
+\[use_f\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be one of \[(f|g), (f|g)\]: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc
@@ -1,7 +1,7 @@
 CORE
 test.c
 --function-pointer-restrictions-file restrictions.json --restrict-function-pointer use_f.function_pointer_call.1/g --restrict-function-pointer-by-name use_f::fptr/h
-\[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be one of \[(f|g|h), (f|g|h), (f|g|h)\]: FAILURE
+\[use_f\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be one of \[(f|g|h), (f|g|h), (f|g|h)\]: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.desc
@@ -1,7 +1,7 @@
 CORE
 test.c
 --function-pointer-restrictions-file restrictions.json
-\[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: FAILURE
+\[use_f\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be one of \[(f|g), (f|g)\]: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc
@@ -1,7 +1,7 @@
 CORE
 test.c
 --function-pointer-restrictions-file restrictions_1.json --function-pointer-restrictions-file restrictions_2.json
-\[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: FAILURE
+\[use_f\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be one of \[(f|g), (f|g)\]: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.desc
@@ -1,6 +1,6 @@
 CORE
 test.c
 --restrict-function-pointer use_f.function_pointer_call.1/f,g
-\[use_f\.assertion\.2\] line \d+ assertion fptr\(10\) >= 10: SUCCESS
+\[use_f\.assertion\.1\] line \d+ assertion fptr\(10\) >= 10: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.desc b/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.desc
@@ -1,7 +1,7 @@
 CORE
 test.c
 --restrict-function-pointer use_f.function_pointer_call.1/f
-\[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be f: FAILURE
+\[use_f\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be f: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/regression/goto-instrument/restrict-function-pointer-to-single-function/test.desc b/regression/goto-instrument/restrict-function-pointer-to-single-function/test.desc
@@ -1,7 +1,7 @@
 CORE
 test.c
 --restrict-function-pointer use_f.function_pointer_call.1/f
-\[use_f\.assertion\.2\] line \d+ assertion fptr\(10\) == 11: SUCCESS
+\[use_f\.assertion\.1\] line \d+ assertion fptr\(10\) == 11: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -1034,7 +1034,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
         function_pointer_restrictionst::from_options(
           options, goto_model, log.get_message_handler());
 
-      restrict_function_pointers(goto_model, function_pointer_restrictions);
+      restrict_function_pointers(
+        ui_message_handler, goto_model, function_pointer_restrictions);
     }
   }
 
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
diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp
diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h
