From e90edca43bf1fa93253ead349f7e93f159a8d937 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Fri, 25 Oct 2019 18:37:03 +0100 Subject: [PATCH 1/5] Add function pointer restriction option This adds a new option, --restrict-function-pointer, to cbmc. This lets a user specify a list of possible pointer targets for specific function pointer call sites, rather than have remove_function_pointers guess possible values. The intended purpose behind this is to prevent excessive symex time wasted on exploring paths the user knows the program can never actually take. --- doc/cprover-manual/index.md | 1 + .../restrict-function-pointer.md | 148 +++++++ .../test.c | 59 +++ .../test.desc | 7 + .../test.json | 3 + .../test.c | 66 +++ .../test.desc | 9 + .../test.c | 68 +++ .../test.desc | 6 + .../restrictions.json | 3 + .../test.c | 68 +++ .../test.desc | 6 + .../restrictions.json | 3 + .../test.c | 68 +++ .../test.desc | 6 + .../restrictions_1.json | 3 + .../restrictions_2.json | 3 + .../test.c | 68 +++ .../test.desc | 6 + .../test.c | 66 +++ .../test.desc | 6 + .../test.c | 39 ++ .../test.desc | 8 + .../test.c | 39 ++ .../test.desc | 6 + .../test.c | 40 ++ .../test.desc | 6 + src/cbmc/cbmc_parse_options.cpp | 15 +- src/cbmc/cbmc_parse_options.h | 2 + src/goto-programs/Makefile | 2 + src/goto-programs/goto_program.h | 24 + .../label_function_pointer_call_sites.cpp | 56 +++ .../label_function_pointer_call_sites.h | 29 ++ .../restrict_function_pointers.cpp | 415 ++++++++++++++++++ .../restrict_function_pointers.h | 87 ++++ src/util/irep.h | 5 + 36 files changed, 1445 insertions(+), 1 deletion(-) create mode 100644 doc/cprover-manual/restrict-function-pointer.md create mode 100644 regression/cbmc/restrict-function-pointer-to-complex-expression/test.c create mode 100644 regression/cbmc/restrict-function-pointer-to-complex-expression/test.desc create mode 100644 regression/cbmc/restrict-function-pointer-to-complex-expression/test.json create mode 100644 regression/cbmc/restrict-function-pointer-to-multiple-functions-code-check/test.c create mode 100644 regression/cbmc/restrict-function-pointer-to-multiple-functions-code-check/test.desc create mode 100644 regression/cbmc/restrict-function-pointer-to-multiple-functions-incorrectly/test.c create mode 100644 regression/cbmc/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc create mode 100644 regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/restrictions.json create mode 100644 regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.c create mode 100644 regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc create mode 100644 regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file/restrictions.json create mode 100644 regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file/test.c create mode 100644 regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file/test.desc create mode 100644 regression/cbmc/restrict-function-pointer-to-multiple-functions-via-multiple-files/restrictions_1.json create mode 100644 regression/cbmc/restrict-function-pointer-to-multiple-functions-via-multiple-files/restrictions_2.json create mode 100644 regression/cbmc/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.c create mode 100644 regression/cbmc/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc create mode 100644 regression/cbmc/restrict-function-pointer-to-multiple-functions/test.c create mode 100644 regression/cbmc/restrict-function-pointer-to-multiple-functions/test.desc create mode 100644 regression/cbmc/restrict-function-pointer-to-single-function-code-check/test.c create mode 100644 regression/cbmc/restrict-function-pointer-to-single-function-code-check/test.desc create mode 100644 regression/cbmc/restrict-function-pointer-to-single-function-incorrectly/test.c create mode 100644 regression/cbmc/restrict-function-pointer-to-single-function-incorrectly/test.desc create mode 100644 regression/cbmc/restrict-function-pointer-to-single-function/test.c create mode 100644 regression/cbmc/restrict-function-pointer-to-single-function/test.desc create mode 100644 src/goto-programs/label_function_pointer_call_sites.cpp create mode 100644 src/goto-programs/label_function_pointer_call_sites.h create mode 100644 src/goto-programs/restrict_function_pointers.cpp create mode 100644 src/goto-programs/restrict_function_pointers.h diff --git a/doc/cprover-manual/index.md b/doc/cprover-manual/index.md index abd028c3b92..9be7116c2a9 100644 --- a/doc/cprover-manual/index.md +++ b/doc/cprover-manual/index.md @@ -9,6 +9,7 @@ [A Short Tutorial](cbmc/tutorial/), [Loop Unwinding](cbmc/unwinding/), [Assertion Checking](cbmc/assertions/), +[Restricting function pointers](cbmc/restrict-function-pointer/), [Memory Analyzer](cbmc/memory-analyzer/), [Program Harness](cbmc/goto-harness/) diff --git a/doc/cprover-manual/restrict-function-pointer.md b/doc/cprover-manual/restrict-function-pointer.md new file mode 100644 index 00000000000..7b402b1e40c --- /dev/null +++ b/doc/cprover-manual/restrict-function-pointer.md @@ -0,0 +1,148 @@ +[CPROVER Manual TOC](../../) + +## Restricting function pointers + +### Motivation + +CBMC comes with a way to resolve calls to function pointers to direct function +calls. This is needed because symbolic execution itself can't handle calls to +function pointers. In practice, this looks something like this: + +Given that there are functions with these signatures available in the program: + +``` +int f(int x); +int g(int x); +int h(int x); +``` + +And we have a call site like this: + +``` +typedef int(*fptr_t)(int x); +void call(fptr_t fptr) { + int r = fptr(10); + assert(r > 0); +} +``` + +Function pointer removal will turn this into code similar to this: + +``` +void call(fptr_t fptr) { + int r; + if(fptr == &f) { + r = f(10); + } else if(fptr == &g) { + r = g(10); + } else if(fptr == &h) { + r = h(10); + } else { + // sanity check + assert(false); + assume(false); + } + return r; +} +``` + +This works well enough for simple cases. However, this is a very simple +replacement only based on the signature of the function (and whether or not they +have their address taken somewhere in the program), so if there are many +functions matching a particular signature, or if some of these functions are +expensive in symex (e.g. functions with lots of loops or recursion), then this +can be a bit cumbersome - especially if we, as a user, already know that a +particular function pointer will only resolve to a single function or a small +set of functions. This is what the `--restrict-function-pointer` option allows. + +### Example + +Take the motivating example. Let us assume that we know for a fact that `call` +will always receive pointers to either `f` or `g` during actual executions of +the program, and symbolic execution for `h` is too expensive to simply ignore +the cost of its branch. For this, we will label the places in each function +where function pointers are being called, to this pattern: + +``` +.function_pointer_call. +``` + +where `N` is referring to which function call it is - so the first call to a +function pointer in a function will have `N=1`, the 5th `N=5` etc. + +We can call `cbmc` with `--restrict-function-pointer +call.function_pointer_call.1/f,g`. This can be read as + +> For the first call to a function pointer in the function `call`, assume that +> it can only be a call to `f` or `g` + +The resulting code looks similar to the original example, except now there will +not be a call to `h`: + +``` +void call(fptr_t fptr) { + int r; + if(fptr == &f) { + r = f(10); + } else if(fptr == &g) { + r = g(10); + } else { + // sanity check + assert(false); + assume(false); + } + return r; +} +``` + +Another example: Imagine we have a simple virtual filesystem API and implementation +like this: + +``` +typedef struct filesystem_t filesystem_t; +struct filesystem_t { + int (*open)(filesystem_t *filesystem, const char* file_name); +}; + +int fs_open(filesystem_t *filesystem, const char* file_name) { + filesystem->open(filesystem, file_name); +} + +int nullfs_open(filesystem_t *filesystem, const char* file_name) { + return -1; +} + +filesystem_t nullfs_val = {.open = nullfs_open}; +filesystem *const nullfs = &nullfs_val; + +filesystem_t *get_fs_impl() { + // some fancy logic to determine + // which filesystem we're getting - + // in-memory, backed by a database, OS file system + // - but in our case, we know that + // it always ends up being nullfs + // for the cases we care about + return nullfs; +} +int main(void) { + filesystem_t *fs = get_fs_impl(); + assert(fs_open(fs, "hello.txt") != -1); +} +``` + +In this case, the assumption is that *we* know that in our `main`, `fs` can be +nothing other than `nullfs`; But perhaps due to the logic being too complicated +symex ends up being unable to figure this out, so in the call to `fs_open()` we +end up branching on all functions matching the signature of +`filesystem_t::open`, which could be quite a few functions within the program. +Worst of all, if it's address is ever taken in the program, as far as the "dumb" +function pointer removal is concerned it could be `fs_open()` itself due to it +having a matching signature, leading to symex being forced to follow a +potentially infinite recursion until its unwind limit. + +In this case we can again restrict the function pointer to the value which we +know it will have: + +``` +--restrict-function-pointer fs_open.function_pointer_call.1/nullfs_open +``` diff --git a/regression/cbmc/restrict-function-pointer-to-complex-expression/test.c b/regression/cbmc/restrict-function-pointer-to-complex-expression/test.c new file mode 100644 index 00000000000..3787afa1df6 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-complex-expression/test.c @@ -0,0 +1,59 @@ +#include + +typedef int (*fptr_t)(int); + +fptr_t get_f(void); +fptr_t get_g(void); + +void use_fg(int choice, fptr_t fptr, fptr_t gptr) +{ + assert((choice ? fptr : gptr)(10) == 10 + choice); +} + +// this is just here to distinguish the behavior from FP removal, which'd include g +int g_always_false_cond = 0; + +int main(void) +{ + use_fg(0, get_f(), get_g()); + use_fg(1, get_f(), get_g()); +} + +int f(int x) +{ + return x + 1; +} + +int g(int x) +{ + return x; +} + +int h(int x) +{ + return x / 2; +} + +fptr_t get_f(void) +{ + if(!g_always_false_cond) + { + return f; + } + else + { + return h; + } +} + +fptr_t get_g(void) +{ + if(!g_always_false_cond) + { + return g; + } + else + { + return h; + } +} diff --git a/regression/cbmc/restrict-function-pointer-to-complex-expression/test.desc b/regression/cbmc/restrict-function-pointer-to-complex-expression/test.desc new file mode 100644 index 00000000000..03c2e782be9 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-complex-expression/test.desc @@ -0,0 +1,7 @@ +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 +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/cbmc/restrict-function-pointer-to-complex-expression/test.json b/regression/cbmc/restrict-function-pointer-to-complex-expression/test.json new file mode 100644 index 00000000000..90f8c5c7cae --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-complex-expression/test.json @@ -0,0 +1,3 @@ +{ + "use_fg.function_pointer_call.1": ["f"] +} diff --git a/regression/cbmc/restrict-function-pointer-to-multiple-functions-code-check/test.c b/regression/cbmc/restrict-function-pointer-to-multiple-functions-code-check/test.c new file mode 100644 index 00000000000..eb28bb15684 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-multiple-functions-code-check/test.c @@ -0,0 +1,66 @@ +#include + +typedef int (*fptr_t)(int); + +fptr_t get_f(void); + +void use_f(fptr_t fptr) +{ + assert(fptr(10) >= 10); +} + +void select_f(void); +void select_g(void); +void select_h(void); + +int main(void) +{ + select_f(); + use_f(get_f()); + select_g(); + use_f(get_f()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} +int h(int x) +{ + return x - 1; +} + +int g_select_function = 0; + +void select_f(void) +{ + g_select_function = 0; +} +void select_g(void) +{ + g_select_function = 1; +} +void select_h(void) +{ + g_select_function = 2; +} + +fptr_t get_f(void) +{ + if(g_select_function == 0) + { + return f; + } + else if(g_select_function == 1) + { + return g; + } + else + { + return h; + } +} diff --git a/regression/cbmc/restrict-function-pointer-to-multiple-functions-code-check/test.desc b/regression/cbmc/restrict-function-pointer-to-multiple-functions-code-check/test.desc new file mode 100644 index 00000000000..05803cc488c --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-multiple-functions-code-check/test.desc @@ -0,0 +1,9 @@ +CORE +test.c +--restrict-function-pointer use_f.function_pointer_call.1/f,g --show-goto-functions +f\(10\) +g\(10\) +^EXIT=0$ +^SIGNAL=0$ +-- +h\(10\) diff --git a/regression/cbmc/restrict-function-pointer-to-multiple-functions-incorrectly/test.c b/regression/cbmc/restrict-function-pointer-to-multiple-functions-incorrectly/test.c new file mode 100644 index 00000000000..ac36b749862 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-multiple-functions-incorrectly/test.c @@ -0,0 +1,68 @@ +#include + +typedef int (*fptr_t)(int); + +fptr_t get_f(void); + +void use_f(fptr_t fptr) +{ + assert(fptr(10) >= 10); +} + +void select_f(void); +void select_g(void); +void select_h(void); + +int main(void) +{ + select_f(); + use_f(get_f()); + select_g(); + use_f(get_f()); + select_h(); + use_f(get_f()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} +int h(int x) +{ + return x - 1; +} + +int g_select_function = 0; + +void select_f(void) +{ + g_select_function = 0; +} +void select_g(void) +{ + g_select_function = 1; +} +void select_h(void) +{ + g_select_function = 2; +} + +fptr_t get_f(void) +{ + if(g_select_function == 0) + { + return f; + } + else if(g_select_function == 1) + { + return g; + } + else + { + return h; + } +} diff --git a/regression/cbmc/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc b/regression/cbmc/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc new file mode 100644 index 00000000000..bf6ec38059f --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc @@ -0,0 +1,6 @@ +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 +^EXIT=10$ +^SIGNAL=0$ diff --git a/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/restrictions.json b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/restrictions.json new file mode 100644 index 00000000000..e9a374713bf --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/restrictions.json @@ -0,0 +1,3 @@ +{ + "use_f.function_pointer_call.1": ["f"] +} diff --git a/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.c b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.c new file mode 100644 index 00000000000..ac36b749862 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.c @@ -0,0 +1,68 @@ +#include + +typedef int (*fptr_t)(int); + +fptr_t get_f(void); + +void use_f(fptr_t fptr) +{ + assert(fptr(10) >= 10); +} + +void select_f(void); +void select_g(void); +void select_h(void); + +int main(void) +{ + select_f(); + use_f(get_f()); + select_g(); + use_f(get_f()); + select_h(); + use_f(get_f()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} +int h(int x) +{ + return x - 1; +} + +int g_select_function = 0; + +void select_f(void) +{ + g_select_function = 0; +} +void select_g(void) +{ + g_select_function = 1; +} +void select_h(void) +{ + g_select_function = 2; +} + +fptr_t get_f(void) +{ + if(g_select_function == 0) + { + return f; + } + else if(g_select_function == 1) + { + return g; + } + else + { + return h; + } +} diff --git a/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc new file mode 100644 index 00000000000..e3a5c3b50c1 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc @@ -0,0 +1,6 @@ +CORE +test.c +--function-pointer-restrictions-file restrictions.json --restrict-function-pointer use_f.function_pointer_call.1/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 +^EXIT=10$ +^SIGNAL=0$ diff --git a/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file/restrictions.json b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file/restrictions.json new file mode 100644 index 00000000000..9538cc31654 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file/restrictions.json @@ -0,0 +1,3 @@ +{ + "use_f.function_pointer_call.1": ["f", "g"] +} diff --git a/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file/test.c b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file/test.c new file mode 100644 index 00000000000..ac36b749862 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file/test.c @@ -0,0 +1,68 @@ +#include + +typedef int (*fptr_t)(int); + +fptr_t get_f(void); + +void use_f(fptr_t fptr) +{ + assert(fptr(10) >= 10); +} + +void select_f(void); +void select_g(void); +void select_h(void); + +int main(void) +{ + select_f(); + use_f(get_f()); + select_g(); + use_f(get_f()); + select_h(); + use_f(get_f()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} +int h(int x) +{ + return x - 1; +} + +int g_select_function = 0; + +void select_f(void) +{ + g_select_function = 0; +} +void select_g(void) +{ + g_select_function = 1; +} +void select_h(void) +{ + g_select_function = 2; +} + +fptr_t get_f(void) +{ + if(g_select_function == 0) + { + return f; + } + else if(g_select_function == 1) + { + return g; + } + else + { + return h; + } +} diff --git a/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file/test.desc b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file/test.desc new file mode 100644 index 00000000000..5c9b3816a99 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-file/test.desc @@ -0,0 +1,6 @@ +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 +^EXIT=10$ +^SIGNAL=0$ diff --git a/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-multiple-files/restrictions_1.json b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-multiple-files/restrictions_1.json new file mode 100644 index 00000000000..e9a374713bf --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-multiple-files/restrictions_1.json @@ -0,0 +1,3 @@ +{ + "use_f.function_pointer_call.1": ["f"] +} diff --git a/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-multiple-files/restrictions_2.json b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-multiple-files/restrictions_2.json new file mode 100644 index 00000000000..a0c410ebec7 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-multiple-files/restrictions_2.json @@ -0,0 +1,3 @@ +{ + "use_f.function_pointer_call.1": ["g"] +} diff --git a/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.c b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.c new file mode 100644 index 00000000000..ac36b749862 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.c @@ -0,0 +1,68 @@ +#include + +typedef int (*fptr_t)(int); + +fptr_t get_f(void); + +void use_f(fptr_t fptr) +{ + assert(fptr(10) >= 10); +} + +void select_f(void); +void select_g(void); +void select_h(void); + +int main(void) +{ + select_f(); + use_f(get_f()); + select_g(); + use_f(get_f()); + select_h(); + use_f(get_f()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} +int h(int x) +{ + return x - 1; +} + +int g_select_function = 0; + +void select_f(void) +{ + g_select_function = 0; +} +void select_g(void) +{ + g_select_function = 1; +} +void select_h(void) +{ + g_select_function = 2; +} + +fptr_t get_f(void) +{ + if(g_select_function == 0) + { + return f; + } + else if(g_select_function == 1) + { + return g; + } + else + { + return h; + } +} diff --git a/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc new file mode 100644 index 00000000000..b46ff820de6 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc @@ -0,0 +1,6 @@ +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 +^EXIT=10$ +^SIGNAL=0$ diff --git a/regression/cbmc/restrict-function-pointer-to-multiple-functions/test.c b/regression/cbmc/restrict-function-pointer-to-multiple-functions/test.c new file mode 100644 index 00000000000..eb28bb15684 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-multiple-functions/test.c @@ -0,0 +1,66 @@ +#include + +typedef int (*fptr_t)(int); + +fptr_t get_f(void); + +void use_f(fptr_t fptr) +{ + assert(fptr(10) >= 10); +} + +void select_f(void); +void select_g(void); +void select_h(void); + +int main(void) +{ + select_f(); + use_f(get_f()); + select_g(); + use_f(get_f()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} +int h(int x) +{ + return x - 1; +} + +int g_select_function = 0; + +void select_f(void) +{ + g_select_function = 0; +} +void select_g(void) +{ + g_select_function = 1; +} +void select_h(void) +{ + g_select_function = 2; +} + +fptr_t get_f(void) +{ + if(g_select_function == 0) + { + return f; + } + else if(g_select_function == 1) + { + return g; + } + else + { + return h; + } +} diff --git a/regression/cbmc/restrict-function-pointer-to-multiple-functions/test.desc b/regression/cbmc/restrict-function-pointer-to-multiple-functions/test.desc new file mode 100644 index 00000000000..878139b431e --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-multiple-functions/test.desc @@ -0,0 +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 +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/cbmc/restrict-function-pointer-to-single-function-code-check/test.c b/regression/cbmc/restrict-function-pointer-to-single-function-code-check/test.c new file mode 100644 index 00000000000..e172f39391c --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-single-function-code-check/test.c @@ -0,0 +1,39 @@ +#include + +typedef int (*fptr_t)(int); + +fptr_t get_f(void); + +void use_f(fptr_t fptr) +{ + assert(fptr(10) == 11); +} + +int main(void) +{ + use_f(get_f()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} + +// this is just here to distinguish the behavior from FP removal, which'd include g +int g_always_false_cond = 0; + +fptr_t get_f(void) +{ + if(!g_always_false_cond) + { + return f; + } + else + { + return g; + } +} diff --git a/regression/cbmc/restrict-function-pointer-to-single-function-code-check/test.desc b/regression/cbmc/restrict-function-pointer-to-single-function-code-check/test.desc new file mode 100644 index 00000000000..f462acc84c8 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-single-function-code-check/test.desc @@ -0,0 +1,8 @@ +CORE +test.c +--restrict-function-pointer use_f.function_pointer_call.1/f --show-goto-functions +f\(10\) +^EXIT=0$ +^SIGNAL=0$ +-- +g\(10\) diff --git a/regression/cbmc/restrict-function-pointer-to-single-function-incorrectly/test.c b/regression/cbmc/restrict-function-pointer-to-single-function-incorrectly/test.c new file mode 100644 index 00000000000..63370cbd1b1 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-single-function-incorrectly/test.c @@ -0,0 +1,39 @@ +#include + +typedef int (*fptr_t)(int); + +fptr_t get_f(void); + +void use_f(fptr_t fptr) +{ + assert(fptr(10) == 11); +} + +int main(void) +{ + use_f(get_f()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} + +// this is just here to distinguish the behavior from FP removal, which'd include g +int g_always_false_cond = 1; + +fptr_t get_f(void) +{ + if(!g_always_false_cond) + { + return f; + } + else + { + return g; + } +} diff --git a/regression/cbmc/restrict-function-pointer-to-single-function-incorrectly/test.desc b/regression/cbmc/restrict-function-pointer-to-single-function-incorrectly/test.desc new file mode 100644 index 00000000000..fc8b95986c3 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-single-function-incorrectly/test.desc @@ -0,0 +1,6 @@ +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 +^EXIT=10$ +^SIGNAL=0$ diff --git a/regression/cbmc/restrict-function-pointer-to-single-function/test.c b/regression/cbmc/restrict-function-pointer-to-single-function/test.c new file mode 100644 index 00000000000..d82c347e8b7 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-single-function/test.c @@ -0,0 +1,40 @@ +#include + +typedef int (*fptr_t)(int); + +fptr_t get_f(void); + +void use_f(fptr_t fptr) +{ + assert(fptr(10) == 11); +} + +int main(void) +{ + use_f(get_f()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} + +// this is just here to distinguish the behavior from FP removal, which'd include +// only f if we didn't reference g anywhere. +int g_always_false_cond = 0; + +fptr_t get_f(void) +{ + if(!g_always_false_cond) + { + return f; + } + else + { + return g; + } +} diff --git a/regression/cbmc/restrict-function-pointer-to-single-function/test.desc b/regression/cbmc/restrict-function-pointer-to-single-function/test.desc new file mode 100644 index 00000000000..13540f25cdd --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-to-single-function/test.desc @@ -0,0 +1,6 @@ +CORE +test.c +--restrict-function-pointer use_f.function_pointer_call.1/f +\[use_f\.assertion\.2\] line \d+ assertion fptr\(10\) == 11: SUCCESS +^EXIT=0$ +^SIGNAL=0$ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index a5404457dbb..8748f50950c 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -60,6 +60,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -78,6 +79,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include #include #include "c_test_input_generator.h" @@ -136,6 +138,8 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) cbmc_parse_optionst::set_default_options(options); parse_c_object_factory_options(cmdline, options); + parse_function_pointer_restriction_options_from_cmdline(cmdline, options); + if(cmdline.isset("function")) options.set_option("function", cmdline.get_value("function")); @@ -749,7 +753,6 @@ int cbmc_parse_optionst::get_goto_program( show_symbol_table(goto_model, ui_message_handler); return CPROVER_EXIT_SUCCESS; } - if(cbmc_parse_optionst::process_goto_program(goto_model, options, log)) return CPROVER_EXIT_INTERNAL_ERROR; @@ -836,6 +839,15 @@ bool cbmc_parse_optionst::process_goto_program( // remove function pointers log.status() << "Removal of function pointers and virtual functions" << messaget::eom; + + const auto function_pointer_restrictions = + function_pointer_restrictionst::from_options( + options, log.get_message_handler()); + if(!function_pointer_restrictions.restrictions.empty()) + { + label_function_pointer_call_sites(goto_model); + restrict_function_pointers(goto_model, function_pointer_restrictions); + } remove_function_pointers( log.get_message_handler(), goto_model, @@ -1066,6 +1078,7 @@ void cbmc_parse_optionst::help() HELP_FLUSH " --verbosity # verbosity level\n" HELP_TIMESTAMP + RESTRICT_FUNCTION_POINTER_HELP "\n"; // clang-format on } diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h index 8d5fba3737f..9b4d1bfd42e 100644 --- a/src/cbmc/cbmc_parse_options.h +++ b/src/cbmc/cbmc_parse_options.h @@ -28,6 +28,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include @@ -81,6 +82,7 @@ class optionst; OPT_GOTO_TRACE \ OPT_VALIDATE \ OPT_ANSI_C_LANGUAGE \ + OPT_RESTRICT_FUNCTION_POINTER \ "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length) // clang-format on diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 09dbe6d802a..cf4b9bf3a31 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -28,6 +28,7 @@ SRC = adjust_float_expressions.cpp \ interpreter_evaluate.cpp \ json_expr.cpp \ json_goto_trace.cpp \ + label_function_pointer_call_sites.cpp \ lazy_goto_model.cpp \ link_goto_model.cpp \ link_to_library.cpp \ @@ -51,6 +52,7 @@ SRC = adjust_float_expressions.cpp \ remove_unused_functions.cpp \ remove_vector.cpp \ remove_virtual_functions.cpp \ + restrict_function_pointers.cpp \ rewrite_union.cpp \ replace_calls.cpp \ resolve_inherited_component.cpp \ diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 0192b0c8cbf..06d1a09935f 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -1169,6 +1169,30 @@ struct pointee_address_equalt } }; +template +void for_each_goto_location_if( + GotoFunctionT &&goto_function, + PredicateT predicate, + HandlerT handle) +{ + auto &&instructions = goto_function.body.instructions; + for(auto it = instructions.begin(); it != instructions.end(); ++it) + { + if(predicate(it)) + { + handle(it); + } + } +} + +template +void for_each_goto_location(GotoFunctionT &&goto_function, HandlerT handle) +{ + using iterator_t = decltype(goto_function.body.instructions.begin()); + for_each_goto_location_if( + goto_function, [](const iterator_t &) { return true; }, handle); +} + #define forall_goto_program_instructions(it, program) \ for(goto_programt::instructionst::const_iterator \ it=(program).instructions.begin(); \ diff --git a/src/goto-programs/label_function_pointer_call_sites.cpp b/src/goto-programs/label_function_pointer_call_sites.cpp new file mode 100644 index 00000000000..6a4a1e51e48 --- /dev/null +++ b/src/goto-programs/label_function_pointer_call_sites.cpp @@ -0,0 +1,56 @@ +/*******************************************************************\ +Module: Label function pointer call sites +Author: Diffblue Ltd. +\*******************************************************************/ + +/// \file +/// Label function pointer call sites across a goto model + +#include "label_function_pointer_call_sites.h" + +#include + +void label_function_pointer_call_sites(goto_modelt &goto_model) +{ + for(auto &goto_function : goto_model.goto_functions.function_map) + { + std::size_t function_pointer_call_counter = 0; + for_each_goto_location_if( + goto_function.second, + [](const goto_programt::targett it) { + return it->is_function_call() && can_cast_expr( + it->get_function_call().function()); + }, + [&](goto_programt::targett it) { + auto const &function_call = it->get_function_call(); + auto const &function_pointer_dereference = + to_dereference_expr(function_call.function()); + auto const &source_location = function_call.source_location(); + auto const &goto_function_symbol_mode = + goto_model.symbol_table.lookup_ref(goto_function.first).mode; + auto const new_symbol_name = + irep_idt{id2string(goto_function.first) + ".function_pointer_call." + + std::to_string(++function_pointer_call_counter)}; + goto_model.symbol_table.insert([&] { + symbolt function_call_site_symbol{}; + function_call_site_symbol.name = function_call_site_symbol.base_name = + function_call_site_symbol.pretty_name = new_symbol_name; + function_call_site_symbol.type = + function_pointer_dereference.pointer().type(); + function_call_site_symbol.location = function_call.source_location(); + function_call_site_symbol.is_lvalue = true; + function_call_site_symbol.mode = goto_function_symbol_mode; + return function_call_site_symbol; + }()); + auto const new_function_pointer = + goto_model.symbol_table.lookup_ref(new_symbol_name).symbol_expr(); + auto const assign_instruction = goto_programt::make_assignment( + code_assignt{new_function_pointer, + function_pointer_dereference.pointer()}, + source_location); + goto_function.second.body.insert_before(it, assign_instruction); + to_code_function_call(it->code).function() = + dereference_exprt{new_function_pointer}; + }); + } +} diff --git a/src/goto-programs/label_function_pointer_call_sites.h b/src/goto-programs/label_function_pointer_call_sites.h new file mode 100644 index 00000000000..a756b1ff6c0 --- /dev/null +++ b/src/goto-programs/label_function_pointer_call_sites.h @@ -0,0 +1,29 @@ +/*******************************************************************\ +Module: Label function pointer call sites +Author: Diffblue Ltd. +\*******************************************************************/ + +/// \file +/// Label function pointer call sites across a goto model +/// \see simplify_function_pointers + +#ifndef CPROVER_GOTO_PROGRAMS_LABEL_FUNCTION_POINTER_CALL_SITES_H +#define CPROVER_GOTO_PROGRAMS_LABEL_FUNCTION_POINTER_CALL_SITES_H + +#include "goto_model.h" + +/// This ensures that call instructions can be only one of two things: +/// +/// 1. A "normal" function call to a concrete function +/// 2. A dereference of a symbol expression of a function pointer type +/// +/// This makes following stages dealing with function calls easier, because they +/// only need to be able to handle these two cases. +/// +/// It does this by replacing all CALL instructions to function pointers with an +/// assignment to a function pointer variable with a name following the pattern +/// [function_name].function_pointer_call.[N], where "N" is the nth call to a +/// function pointer in the function "function_name". +void label_function_pointer_call_sites(goto_modelt &goto_model); + +#endif // CPROVER_GOTO_PROGRAMS_LABEL_FUNCTION_POINTER_CALL_SITES_H diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp new file mode 100644 index 00000000000..749de44897a --- /dev/null +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -0,0 +1,415 @@ +/*******************************************************************\ + +Module: GOTO Program Utilities + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include "restrict_function_pointers.h" + +#include +#include +#include +#include + +#include +#include +#include + +namespace +{ +void typecheck_function_pointer_restrictions( + const goto_modelt &goto_model, + const function_pointer_restrictionst &restrictions) +{ + for(auto const &restriction : restrictions.restrictions) + { + auto const function_pointer_sym = + goto_model.symbol_table.lookup(restriction.first); + if(function_pointer_sym == nullptr) + { + throw invalid_command_line_argument_exceptiont{ + id2string(restriction.first) + " not found in the symbol table", + "--restrict-function-pointer"}; + } + auto const &function_pointer_type = function_pointer_sym->type; + if(function_pointer_type.id() != ID_pointer) + { + throw invalid_command_line_argument_exceptiont{ + "not a function pointer: " + id2string(restriction.first), + "--restrict-function-pointer"}; + } + auto const &function_type = + to_pointer_type(function_pointer_type).subtype(); + if(function_type.id() != ID_code) + { + throw invalid_command_line_argument_exceptiont{ + "not a function pointer: " + id2string(restriction.first), + "--restrict-function-pointer"}; + } + auto const &ns = namespacet{goto_model.symbol_table}; + for(auto const &function_pointer_target : restriction.second) + { + auto const function_pointer_target_sym = + goto_model.symbol_table.lookup(function_pointer_target); + if(function_pointer_target_sym == nullptr) + { + throw invalid_command_line_argument_exceptiont{ + "symbol not found: " + id2string(function_pointer_target), + "--restrict-function-pointer"}; + } + auto const &function_pointer_target_type = + function_pointer_target_sym->type; + if(function_type != function_pointer_target_type) + { + throw invalid_command_line_argument_exceptiont{ + "type mismatch: `" + id2string(restriction.first) + "' points to `" + + type2c(function_type, ns) + "', but restriction `" + + id2string(function_pointer_target) + "' has type `" + + type2c(function_pointer_target_type, ns) + "'", + "--restrict-function-pointer"}; + } + } + } +} + +source_locationt make_function_pointer_restriction_assertion_source_location( + source_locationt source_location, + const function_pointer_restrictionst::value_type restriction) +{ + std::stringstream comment; + comment << "dereferenced function pointer at " << restriction.first + << " must be "; + if(restriction.second.size() == 1) + { + comment << *restriction.second.begin(); + } + else + { + comment << "one of ["; + bool first = true; + for(auto const &target : restriction.second) + { + if(!first) + { + comment << ", "; + } + else + { + first = false; + } + comment << target; + } + comment << ']'; + } + source_location.set_comment(string2id(comment.str())); + source_location.set_property_class(ID_assertion); + return source_location; +} + +template +void for_each_function_call(goto_functiont &goto_function, Handler handler) +{ + for_each_goto_location_if( + goto_function, + [](goto_programt::targett target) { return target->is_function_call(); }, + handler); +} +} // namespace + +void restrict_function_pointers( + goto_modelt &goto_model, + const function_pointer_restrictionst &restrictions) +{ + typecheck_function_pointer_restrictions(goto_model, restrictions); + + for(auto &goto_function : goto_model.goto_functions.function_map) + { + auto &goto_function_body = goto_function.second.body; + // for each function call, we check if it is using a symbol we have + // restrictions for, and if so branch on its value and insert concrete calls + // to the restriction functions + for_each_function_call( + goto_function.second, [&](const goto_programt::targett location) { + // Check if this is calling a function pointer, and if so if it is one + // we have a restriction for + const auto &original_function_call = location->get_function_call(); + if(can_cast_expr(original_function_call.function())) + { + // because we simplify before this stage a dereference can only + // dereference a symbol expression + auto const &called_function_pointer = + to_dereference_expr(original_function_call.function()).pointer(); + PRECONDITION(can_cast_expr(called_function_pointer)); + auto const &pointer_symbol = to_symbol_expr(called_function_pointer); + auto const restriction_iterator = + restrictions.restrictions.find(pointer_symbol.get_identifier()); + if(restriction_iterator != restrictions.restrictions.end()) + { + auto const &restriction = *restriction_iterator; + // if we can, we will replace uses of it by the + // this is intentionally a copy because we're just about to change + // the instruction this iterator points to + auto const original_function_call_instruction = *location; + *location = goto_programt::make_assertion( + false_exprt{}, + make_function_pointer_restriction_assertion_source_location( + original_function_call_instruction.source_location, + restriction)); + auto const assume_false_location = goto_function_body.insert_after( + location, + goto_programt::make_assumption( + false_exprt{}, + original_function_call_instruction.source_location)); + // this is mutable because we'll update this at the end of each + // loop iteration to always point at the start of the branch + // we created + auto else_location = location; + auto const end_if_location = goto_function_body.insert_after( + assume_false_location, goto_programt::make_skip()); + for(auto const &restriction_target : restriction.second) + { + auto new_instruction = original_function_call_instruction; + // can't use get_function_call because that'll return a const ref + const symbol_exprt &function_pointer_target_symbol_expr = + goto_model.symbol_table.lookup_ref(restriction_target) + .symbol_expr(); + to_code_function_call(new_instruction.code).function() = + function_pointer_target_symbol_expr; + auto const goto_end_if_location = + goto_function_body.insert_before( + else_location, + goto_programt::make_goto( + end_if_location, + original_function_call_instruction.source_location)); + auto const replaced_instruction_location = + goto_function.second.body.insert_before( + goto_end_if_location, new_instruction); + else_location = goto_function.second.body.insert_before( + replaced_instruction_location, + goto_programt::make_goto( + else_location, + notequal_exprt{ + pointer_symbol, + address_of_exprt{function_pointer_target_symbol_expr}})); + } + } + } + }); + } +} + +void parse_function_pointer_restriction_options_from_cmdline( + const cmdlinet &cmdline, + optionst &options) +{ + options.set_option( + RESTRICT_FUNCTION_POINTER_OPT, + cmdline.get_values(RESTRICT_FUNCTION_POINTER_OPT)); + options.set_option( + RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT, + cmdline.get_values(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT)); +} + +namespace +{ +function_pointer_restrictionst::restrictionst +merge_function_pointer_restrictions( + const function_pointer_restrictionst::restrictionst &lhs, + const function_pointer_restrictionst::restrictionst &rhs) +{ + auto result = lhs; + for(auto const &restriction : rhs) + { + auto emplace_result = result.emplace(restriction.first, restriction.second); + if(!emplace_result.second) + { + for(auto const &target : restriction.second) + { + emplace_result.first->second.insert(target); + } + } + } + return result; +} + +function_pointer_restrictionst::restrictionst +parse_function_pointer_restrictions_from_command_line( + const std::list &restriction_opts) +{ + auto function_pointer_restrictions = + function_pointer_restrictionst::restrictionst{}; + for(auto const &restriction_opt : restriction_opts) + { + // the format for restrictions is / + // exactly one pointer and at least one target + auto const pointer_name_end = restriction_opt.find('/'); + auto const restriction_format_message = + "the format for restrictions is " + "/"; + if(pointer_name_end == std::string::npos) + { + throw invalid_command_line_argument_exceptiont{ + "couldn't find '/' in `" + restriction_opt + "'", + "--" RESTRICT_FUNCTION_POINTER_OPT, + restriction_format_message}; + } + if(pointer_name_end == restriction_opt.size()) + { + throw invalid_command_line_argument_exceptiont{ + "couldn't find names of targets after '/' in `" + restriction_opt + "'", + "--" RESTRICT_FUNCTION_POINTER_OPT, + restriction_format_message}; + } + if(pointer_name_end == 0) + { + throw invalid_command_line_argument_exceptiont{ + "couldn't find target name before '/' in `" + restriction_opt + "'", + "--" RESTRICT_FUNCTION_POINTER_OPT}; + } + auto const pointer_name = restriction_opt.substr(0, pointer_name_end); + auto const target_names_substring = + restriction_opt.substr(pointer_name_end + 1); + auto const target_name_strings = split_string(target_names_substring, ','); + if(target_name_strings.size() == 1 && target_name_strings[0].empty()) + { + throw invalid_command_line_argument_exceptiont{ + "missing target list for function pointer restriction " + pointer_name, + "--" RESTRICT_FUNCTION_POINTER_OPT, + restriction_format_message}; + } + auto const target_names = ([&target_name_strings] { + auto target_names = std::unordered_set{}; + std::transform( + target_name_strings.begin(), + target_name_strings.end(), + std::inserter(target_names, target_names.end()), + string2id); + return target_names; + })(); + for(auto const &target_name : target_names) + { + if(target_name == ID_empty_string) + { + throw invalid_command_line_argument_exceptiont( + "leading or trailing comma in restrictions for `" + pointer_name + + "'", + "--" RESTRICT_FUNCTION_POINTER_OPT, + restriction_format_message); + } + } + if(!function_pointer_restrictions + .emplace(irep_idt{pointer_name}, target_names) + .second) + { + throw invalid_command_line_argument_exceptiont{ + "function pointer restriction for `" + pointer_name + + "' was specified twice", + "--" RESTRICT_FUNCTION_POINTER_OPT}; + }; + } + return function_pointer_restrictions; +} + +function_pointer_restrictionst::restrictionst +parse_function_pointer_restrictions_from_file( + const std::list &filenames, + message_handlert &message_handler) +{ + auto merged_restrictions = function_pointer_restrictionst::restrictionst{}; + for(auto const &filename : filenames) + { + auto const restrictions = + function_pointer_restrictionst::read_from_file(filename, message_handler); + merged_restrictions = merge_function_pointer_restrictions( + merged_restrictions, restrictions.restrictions); + } + return merged_restrictions; +} +} // namespace + +function_pointer_restrictionst function_pointer_restrictionst::from_options( + const optionst &options, + message_handlert &message_handler) +{ + auto const restriction_opts = + options.get_list_option(RESTRICT_FUNCTION_POINTER_OPT); + auto const commandline_restrictions = + parse_function_pointer_restrictions_from_command_line(restriction_opts); + auto const file_restrictions = parse_function_pointer_restrictions_from_file( + options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT), + message_handler); + return {merge_function_pointer_restrictions( + file_restrictions, commandline_restrictions)}; +} + +function_pointer_restrictionst function_pointer_restrictionst::read_from_file( + const std::string &filename, + message_handlert &message_handler) +{ + auto failed = [](bool failFlag) { return failFlag; }; + function_pointer_restrictionst::restrictionst restrictions; + auto inFile = std::ifstream{filename}; + jsont json; + if(failed(parse_json(inFile, filename, message_handler, json))) + { + throw system_exceptiont{ + "failed to read function pointer restrictions from " + filename}; + } + if(!json.is_object()) + { + throw system_exceptiont{"top level item is not an object"}; + } + for(auto const &kv_pair : to_json_object(json)) + { + restrictions.emplace(irep_idt{kv_pair.first}, [&] { + if(!kv_pair.second.is_array()) + { + throw system_exceptiont{"In " + filename + ", value of " + + kv_pair.first + " is not an array"}; + } + auto possible_targets = std::unordered_set{}; + auto const &array = to_json_array(kv_pair.second); + std::transform( + array.begin(), + array.end(), + std::inserter(possible_targets, possible_targets.end()), + [&](const jsont &array_element) { + if(!array_element.is_string()) + { + throw system_exceptiont{"In " + filename + ", value of " + + kv_pair.first + + "contains a non-string array element"}; + } + return irep_idt{to_json_string(array_element).value}; + }); + return possible_targets; + }()); + } + return function_pointer_restrictionst{restrictions}; +} + +void function_pointer_restrictionst::write_to_file( + const std::string &filename) const +{ + auto function_pointer_restrictions_json = jsont{}; + auto &restrictions_json_object = + function_pointer_restrictions_json.make_object(); + for(auto const &restriction : restrictions) + { + auto &targets_array = + restrictions_json_object[id2string(restriction.first)].make_array(); + for(auto const &target : restriction.second) + { + targets_array.push_back(json_stringt{target}); + } + } + auto outFile = std::ofstream{filename}; + if(!outFile) + { + throw system_exceptiont{"cannot open " + filename + + " for writing function pointer restrictions"}; + } + function_pointer_restrictions_json.output(outFile); +} diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h new file mode 100644 index 00000000000..f7e51d88a34 --- /dev/null +++ b/src/goto-programs/restrict_function_pointers.h @@ -0,0 +1,87 @@ +/*******************************************************************\ + +Module: GOTO Program Utilities + +Author: Diffblue Ltd. + +\*******************************************************************/ + +/// \file +/// Given goto functions and a list of function parameters or globals +/// that are function pointers with lists of possible candidates, replace use of +/// these function pointers with calls to the candidate. +/// The purpose here is to avoid unnecessary branching +/// i.e. "there are 600 functions with this signature, but I know it's +/// always going to be one of these two" + +#ifndef CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H +#define CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H + +#include +#include + +#include +#include + +#include +#include + +#define RESTRICT_FUNCTION_POINTER_OPT "restrict-function-pointer" +#define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \ + "function-pointer-restrictions-file" + +#define OPT_RESTRICT_FUNCTION_POINTER \ + "(" RESTRICT_FUNCTION_POINTER_OPT \ + "):" \ + "(" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT "):" + +#define RESTRICT_FUNCTION_POINTER_HELP \ + "--" RESTRICT_FUNCTION_POINTER_OPT \ + " /\n" \ + " restrict a function pointer to a set of possible targets\n" \ + " targets must all exist in the symbol table with a matching " \ + "type\n" \ + " works for globals and function parameters right now\n" \ + "--" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \ + " \n" \ + " add from function pointer restrictions from file" + +void parse_function_pointer_restriction_options_from_cmdline( + const cmdlinet &cmdline, + optionst &options); + +class message_handlert; +struct function_pointer_restrictionst +{ + using restrictionst = + std::unordered_map>; + using value_type = restrictionst::value_type; + const restrictionst restrictions; + + /// parse function pointer restrictions from command line + /// + /// Note: These are are only syntactically checked at this stage, + /// because type checking them requires a goto_modelt + static function_pointer_restrictionst + from_options(const optionst &options, message_handlert &message_handler); + + static function_pointer_restrictionst read_from_file( + const std::string &filename, + message_handlert &message_handler); + + void write_to_file(const std::string &filename) const; +}; + +/// Apply a function pointer restrictions to a goto_model. Each restriction is a +/// mapping from a pointer name to a set of possible targets. Replace calls of +/// these "restricted" pointers with a branch on the value of the function +/// pointer, comparing it to the set of possible targets. This also adds an +/// assertion that the pointer actually has one of the listed values. +/// +/// Note: This requires label_function_pointer_call_sites to be run +/// before +void restrict_function_pointers( + goto_modelt &goto_model, + const function_pointer_restrictionst &restrictions); + +#endif // CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H diff --git a/src/util/irep.h b/src/util/irep.h index 2e2dacf91c0..0613d1f717c 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -50,6 +50,11 @@ inline const std::string &id2string(const irep_idt &d) #endif } +inline irep_idt string2id(const std::string &id_string) +{ + return irep_idt{id_string}; +} + inline const std::string &name2string(const irep_namet &n) { #ifdef USE_DSTRING From 860117dfcbfe08d6d397620211a6817b4d781cc2 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Tue, 5 Nov 2019 15:38:19 +0000 Subject: [PATCH 2/5] Add more documentation --- .../restrict-function-pointer.md | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/doc/cprover-manual/restrict-function-pointer.md b/doc/cprover-manual/restrict-function-pointer.md index 7b402b1e40c..82b5d3d126c 100644 --- a/doc/cprover-manual/restrict-function-pointer.md +++ b/doc/cprover-manual/restrict-function-pointer.md @@ -146,3 +146,28 @@ know it will have: ``` --restrict-function-pointer fs_open.function_pointer_call.1/nullfs_open ``` + +### Loading from file + +If you have many places where you want to restrict function pointers, it'd be a +nuisance to have to specify them all on the command line. In these cases, you +can specify a file to load the restrictions from instead, via the +`--function-pointer-restrictions-file` option, which you can give the name of a +JSON file with this format: + +``` +{ + "function_call_site_name": ["function1", "function2", ...], + ... +} +``` + +**Note:** If you pass in multiple files, or a mix of files and command line +restrictions, the final restrictions will be a set union of all specified +restrictions. + +**Note:** as of now, if something goes wrong during type checking (i.e. making +sure that all function pointer replacements refer to functions in the symbol +table that have the correct type), the error message will refer the command line +option `--restrict-function-pointer` regardless of whether the restriction in +question came from the command line or a file. From bb617bb2a2a3e08e20a2a62c94158e16d139ec6c Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Tue, 5 Nov 2019 17:05:23 +0000 Subject: [PATCH 3/5] Add restrict-function-pointer-by-name option This works similar to restrict-function-pointer, but for names of individual function pointer variables (globals, locals, parameters) rather than call sites. This isn't applicable to all situations (for example, calling function pointers in structs or function pointers returned from functions), but is more readily applicable to some common use scenarios (e.g. global function pointers loaded at start time like in OpenGL). --- .../restrict-function-pointer-by-name/test.c | 43 +++++++++++ .../test.desc | 11 +++ src/cbmc/cbmc_parse_options.cpp | 68 +++++++++-------- .../restrict_function_pointers.cpp | 73 +++++++++++++++++-- .../restrict_function_pointers.h | 11 ++- 5 files changed, 168 insertions(+), 38 deletions(-) create mode 100644 regression/cbmc/restrict-function-pointer-by-name/test.c create mode 100644 regression/cbmc/restrict-function-pointer-by-name/test.desc diff --git a/regression/cbmc/restrict-function-pointer-by-name/test.c b/regression/cbmc/restrict-function-pointer-by-name/test.c new file mode 100644 index 00000000000..9bbc0bc5d1a --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-by-name/test.c @@ -0,0 +1,43 @@ +#include + +int f(void) +{ + return 1; +} +int g(void) +{ + return 2; +} +int h(void) +{ + return 3; +} + +typedef int (*fptr_t)(void); + +void use_f(fptr_t fptr) +{ + assert(fptr() == 2); +} + +int nondet_int(void); + +fptr_t g_fptr; +int main(void) +{ + int cond = nondet_int(); + if(cond) + { + g_fptr = f; + } + else + { + g_fptr = h; + } + int res = g_fptr(); + assert(res == 1 || res == 3); + use_f(g); + fptr_t fptr = f; + assert(fptr() == 1); + return 0; +} diff --git a/regression/cbmc/restrict-function-pointer-by-name/test.desc b/regression/cbmc/restrict-function-pointer-by-name/test.desc new file mode 100644 index 00000000000..7f0dc87e1d1 --- /dev/null +++ b/regression/cbmc/restrict-function-pointer-by-name/test.desc @@ -0,0 +1,11 @@ +CORE +test.c +--restrict-function-pointer-by-name main::1::fptr/f --restrict-function-pointer-by-name use_f::fptr/g --restrict-function-pointer-by-name g_fptr/f,h +\[use_f.assertion.2\] line \d+ assertion fptr\(\) == 2: SUCCESS +\[use_f.assertion.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be g: SUCCESS +\[main.assertion.1\] line \d+ dereferenced function pointer at main.function_pointer_call.1 must be one of \[h, f\]: SUCCESS +\[main.assertion.2\] line \d+ assertion res == 1 || res == 3: SUCCESS +\[main.assertion.3\] line \d+ dereferenced function pointer at main.function_pointer_call.2 must be f: SUCCESS +\[main.assertion.4\] line \d+ assertion fptr\(\) == 1: SUCCESS +^EXIT=0$ +^SIGNAL=0$ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 8748f50950c..4d5349534ea 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -11,8 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "cbmc_parse_options.h" -#include #include // exit() +#include #include #include @@ -178,8 +178,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) exit(CPROVER_EXIT_USAGE_ERROR); } - if(cmdline.isset("reachability-slice") && - cmdline.isset("reachability-slice-fb")) + if( + cmdline.isset("reachability-slice") && + cmdline.isset("reachability-slice-fb")) { log.error() << "--reachability-slice and --reachability-slice-fb must not be " @@ -258,9 +259,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("no-simplify")) options.set_option("simplify", false); - if(cmdline.isset("stop-on-fail") || - cmdline.isset("dimacs") || - cmdline.isset("outfile")) + if( + cmdline.isset("stop-on-fail") || cmdline.isset("dimacs") || + cmdline.isset("outfile")) options.set_option("stop-on-fail", true); if( @@ -370,8 +371,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("max-node-refinement")) options.set_option( - "max-node-refinement", - cmdline.get_value("max-node-refinement")); + "max-node-refinement", cmdline.get_value("max-node-refinement")); // SMT Options @@ -387,11 +387,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("fpa")) options.set_option("fpa", true); - bool solver_set=false; + bool solver_set = false; if(cmdline.isset("boolector")) { - options.set_option("boolector", true), solver_set=true; + options.set_option("boolector", true), solver_set = true; options.set_option("smt2", true); } @@ -403,25 +403,25 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("mathsat")) { - options.set_option("mathsat", true), solver_set=true; + options.set_option("mathsat", true), solver_set = true; options.set_option("smt2", true); } if(cmdline.isset("cvc4")) { - options.set_option("cvc4", true), solver_set=true; + options.set_option("cvc4", true), solver_set = true; options.set_option("smt2", true); } if(cmdline.isset("yices")) { - options.set_option("yices", true), solver_set=true; + options.set_option("yices", true), solver_set = true; options.set_option("smt2", true); } if(cmdline.isset("z3")) { - options.set_option("z3", true), solver_set=true; + options.set_option("z3", true), solver_set = true; options.set_option("smt2", true); } @@ -461,8 +461,7 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("symex-coverage-report")) { options.set_option( - "symex-coverage-report", - cmdline.get_value("symex-coverage-report")); + "symex-coverage-report", cmdline.get_value("symex-coverage-report")); options.set_option("paths-symex-explore-all", true); } @@ -512,8 +511,7 @@ int cbmc_parse_optionst::doit() // Unwinding of transition systems is done by hw-cbmc. // - if(cmdline.isset("module") || - cmdline.isset("gen-interface")) + if(cmdline.isset("module") || cmdline.isset("gen-interface")) { log.error() << "This version of CBMC has no support for " " hardware modules. Please use hw-cbmc." @@ -552,13 +550,13 @@ int cbmc_parse_optionst::doit() return CPROVER_EXIT_INCORRECT_TASK; } - std::string filename=cmdline.args[0]; + std::string filename = cmdline.args[0]; - #ifdef _MSC_VER +#ifdef _MSC_VER std::ifstream infile(widen(filename)); - #else +#else std::ifstream infile(filename); - #endif +#endif if(!infile) { @@ -567,10 +565,9 @@ int cbmc_parse_optionst::doit() return CPROVER_EXIT_INCORRECT_TASK; } - std::unique_ptr language= - get_language_from_filename(filename); + std::unique_ptr language = get_language_from_filename(filename); - if(language==nullptr) + if(language == nullptr) { log.error() << "failed to figure out type of file '" << filename << "'" << messaget::eom; @@ -595,11 +592,12 @@ int cbmc_parse_optionst::doit() int get_goto_program_ret = get_goto_program(goto_model, options, cmdline, ui_message_handler); - if(get_goto_program_ret!=-1) + if(get_goto_program_ret != -1) return get_goto_program_ret; - if(cmdline.isset("show-claims") || // will go away - cmdline.isset("show-properties")) // use this one + if( + cmdline.isset("show-claims") || // will go away + cmdline.isset("show-properties")) // use this one { show_properties(goto_model, ui_message_handler); return CPROVER_EXIT_SUCCESS; @@ -840,14 +838,20 @@ bool cbmc_parse_optionst::process_goto_program( log.status() << "Removal of function pointers and virtual functions" << messaget::eom; - const auto function_pointer_restrictions = - function_pointer_restrictionst::from_options( - options, log.get_message_handler()); - if(!function_pointer_restrictions.restrictions.empty()) + if( + options.is_set(RESTRICT_FUNCTION_POINTER_OPT) || + options.is_set(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT) || + options.is_set(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT)) { label_function_pointer_call_sites(goto_model); + auto const by_name_restrictions = + get_function_pointer_by_name_restrictions(goto_model, options); + const auto function_pointer_restrictions = + by_name_restrictions.merge(function_pointer_restrictionst::from_options( + options, log.get_message_handler())); restrict_function_pointers(goto_model, function_pointer_restrictions); } + remove_function_pointers( log.get_message_handler(), goto_model, diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp index 749de44897a..8d4fd0732b5 100644 --- a/src/goto-programs/restrict_function_pointers.cpp +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -108,12 +108,13 @@ source_locationt make_function_pointer_restriction_assertion_source_location( return source_location; } -template -void for_each_function_call(goto_functiont &goto_function, Handler handler) +template +void for_each_function_call(GotoFunctionT &&goto_function, Handler handler) { + using targett = decltype(goto_function.body.instructions.begin()); for_each_goto_location_if( goto_function, - [](goto_programt::targett target) { return target->is_function_call(); }, + [](targett target) { return target->is_function_call(); }, handler); } } // namespace @@ -210,6 +211,9 @@ void parse_function_pointer_restriction_options_from_cmdline( options.set_option( RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT, cmdline.get_values(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT)); + options.set_option( + RESTRICT_FUNCTION_POINTER_BY_NAME_OPT, + cmdline.get_values(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT)); } namespace @@ -236,7 +240,8 @@ merge_function_pointer_restrictions( function_pointer_restrictionst::restrictionst parse_function_pointer_restrictions_from_command_line( - const std::list &restriction_opts) + const std::list &restriction_opts, + const std::string &option_name) { auto function_pointer_restrictions = function_pointer_restrictionst::restrictionst{}; @@ -336,7 +341,8 @@ function_pointer_restrictionst function_pointer_restrictionst::from_options( auto const restriction_opts = options.get_list_option(RESTRICT_FUNCTION_POINTER_OPT); auto const commandline_restrictions = - parse_function_pointer_restrictions_from_command_line(restriction_opts); + parse_function_pointer_restrictions_from_command_line( + restriction_opts, RESTRICT_FUNCTION_POINTER_OPT); auto const file_restrictions = parse_function_pointer_restrictions_from_file( options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT), message_handler); @@ -413,3 +419,60 @@ void function_pointer_restrictionst::write_to_file( } function_pointer_restrictions_json.output(outFile); } +function_pointer_restrictionst function_pointer_restrictionst::merge( + const function_pointer_restrictionst &other) const +{ + return function_pointer_restrictionst{ + merge_function_pointer_restrictions(restrictions, other.restrictions)}; +} + +function_pointer_restrictionst get_function_pointer_by_name_restrictions( + const goto_modelt &goto_model, + const optionst &options) +{ + function_pointer_restrictionst::restrictionst by_name_restrictions = + parse_function_pointer_restrictions_from_command_line( + options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT), + RESTRICT_FUNCTION_POINTER_BY_NAME_OPT); + function_pointer_restrictionst::restrictionst restrictions; + for(auto const &goto_function : goto_model.goto_functions.function_map) + { + for_each_function_call( + goto_function.second, [&](goto_programt::const_targett location) { + PRECONDITION(location->is_function_call()); + if(can_cast_expr( + location->get_function_call().function())) + { + PRECONDITION(can_cast_expr( + to_dereference_expr(location->get_function_call().function()) + .pointer())); + auto const &function_pointer_call_site = to_symbol_expr( + to_dereference_expr(location->get_function_call().function()) + .pointer()); + auto const &body = goto_function.second.body; + for(auto it = std::prev(location); it != body.instructions.end(); + ++it) + { + if( + it->is_assign() && + it->get_assign().lhs() == function_pointer_call_site && + can_cast_expr(it->get_assign().rhs())) + { + auto const &assign_rhs = to_symbol_expr(it->get_assign().rhs()); + auto const restriction = + by_name_restrictions.find(assign_rhs.get_identifier()); + if( + restriction != by_name_restrictions.end() && + restriction->first == assign_rhs.get_identifier()) + { + restrictions.emplace( + function_pointer_call_site.get_identifier(), + restriction->second); + } + } + } + } + }); + } + return function_pointer_restrictionst{restrictions}; +} diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h index f7e51d88a34..7bcdfc79852 100644 --- a/src/goto-programs/restrict_function_pointers.h +++ b/src/goto-programs/restrict_function_pointers.h @@ -29,11 +29,15 @@ Author: Diffblue Ltd. #define RESTRICT_FUNCTION_POINTER_OPT "restrict-function-pointer" #define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \ "function-pointer-restrictions-file" +#define RESTRICT_FUNCTION_POINTER_BY_NAME_OPT \ + "restrict-function-pointer-by-name" #define OPT_RESTRICT_FUNCTION_POINTER \ "(" RESTRICT_FUNCTION_POINTER_OPT \ "):" \ - "(" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT "):" + "(" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \ + "):" \ + "(" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT "):" #define RESTRICT_FUNCTION_POINTER_HELP \ "--" RESTRICT_FUNCTION_POINTER_OPT \ @@ -70,8 +74,13 @@ struct function_pointer_restrictionst message_handlert &message_handler); void write_to_file(const std::string &filename) const; + function_pointer_restrictionst + merge(const function_pointer_restrictionst &other) const; }; +function_pointer_restrictionst get_function_pointer_by_name_restrictions( + const goto_modelt &goto_model, + const optionst &options); /// Apply a function pointer restrictions to a goto_model. Each restriction is a /// mapping from a pointer name to a set of possible targets. Replace calls of /// these "restricted" pointers with a branch on the value of the function From 7d2be6a30bc3351a09b9cefc6438817e8eab9a9e Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Wed, 6 Nov 2019 17:07:08 +0000 Subject: [PATCH 4/5] Don't change stuff unless asked --- src/cbmc/cbmc_parse_options.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 4d5349534ea..f0273cc6f77 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -839,9 +839,9 @@ bool cbmc_parse_optionst::process_goto_program( << messaget::eom; if( - options.is_set(RESTRICT_FUNCTION_POINTER_OPT) || - options.is_set(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT) || - options.is_set(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT)) + !options.get_list_option(RESTRICT_FUNCTION_POINTER_OPT).empty() || + !options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT).empty() || + !options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT).empty()) { label_function_pointer_call_sites(goto_model); auto const by_name_restrictions = From ee5b42b6f7266c8c8aec38e52bea7379bc00ceac Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Thu, 7 Nov 2019 09:28:21 +0000 Subject: [PATCH 5/5] Remove order dependency from regression test --- regression/cbmc/restrict-function-pointer-by-name/test.desc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/cbmc/restrict-function-pointer-by-name/test.desc b/regression/cbmc/restrict-function-pointer-by-name/test.desc index 7f0dc87e1d1..22d02d0391e 100644 --- a/regression/cbmc/restrict-function-pointer-by-name/test.desc +++ b/regression/cbmc/restrict-function-pointer-by-name/test.desc @@ -3,8 +3,8 @@ test.c --restrict-function-pointer-by-name main::1::fptr/f --restrict-function-pointer-by-name use_f::fptr/g --restrict-function-pointer-by-name g_fptr/f,h \[use_f.assertion.2\] line \d+ assertion fptr\(\) == 2: SUCCESS \[use_f.assertion.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be g: SUCCESS -\[main.assertion.1\] line \d+ dereferenced function pointer at main.function_pointer_call.1 must be one of \[h, f\]: SUCCESS -\[main.assertion.2\] line \d+ assertion res == 1 || res == 3: SUCCESS +\[main.assertion.1\] line \d+ dereferenced function pointer at main.function_pointer_call.1 must be one of \[(h|f), (h|f)\]: SUCCESS +\[main.assertion.2\] line \d+ assertion res == 1 \|\| res == 3: SUCCESS \[main.assertion.3\] line \d+ dereferenced function pointer at main.function_pointer_call.2 must be f: SUCCESS \[main.assertion.4\] line \d+ assertion fptr\(\) == 1: SUCCESS ^EXIT=0$