Skip to content

Commit 7e27cb2

Browse files
authored
Merge pull request #5262 from danpoe/feature/restrict-function-pointer-by-name
Restrict function pointers by name
2 parents 094fc97 + 8154f23 commit 7e27cb2

File tree

12 files changed

+594
-178
lines changed

12 files changed

+594
-178
lines changed
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
int f(void)
2+
{
3+
return 1;
4+
}
5+
6+
int g(void)
7+
{
8+
return 2;
9+
}
10+
11+
int h(void)
12+
{
13+
return 3;
14+
}
15+
16+
typedef int (*fp_t)(void);
17+
18+
fp_t fp;
19+
20+
void main()
21+
{
22+
int cond;
23+
fp = cond ? f : g;
24+
int res = fp();
25+
__CPROVER_assert(res == 1, "");
26+
__CPROVER_assert(res == 2, "");
27+
__CPROVER_assert(res == 1 || res == 2, "");
28+
}
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
test.c
3+
--restrict-function-pointer-by-name fp/f,g
4+
\[main\.assertion\.1\] line \d+ dereferenced function pointer at main\.function_pointer_call\.1 must be one of \[(f, g)|(g, f)\]: SUCCESS
5+
\[main.assertion.2\] line \d+ assertion: FAILURE
6+
\[main.assertion.3\] line \d+ assertion: FAILURE
7+
\[main.assertion.4\] line \d+ assertion: SUCCESS
8+
f\(\)
9+
g\(\)
10+
^EXIT=10$
11+
^SIGNAL=0$
12+
--
13+
h\(\)
14+
--
15+
Check that a call to a global function pointer is correctly restricted
Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
#include <assert.h>
2+
3+
int f(void)
4+
{
5+
return 1;
6+
}
7+
8+
int g(void)
9+
{
10+
return 2;
11+
}
12+
13+
typedef int (*fp_t)(void);
14+
15+
void main()
16+
{
17+
fp_t fp = f;
18+
assert(fp() == 1);
19+
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
test.c
3+
--restrict-function-pointer-by-name main::1::fp/f
4+
\[main\.assertion\.1\] line \d+ dereferenced function pointer at main\.function_pointer_call\.1 must be f: SUCCESS
5+
\[main\.assertion\.2\] line \d+ assertion fp\(\) == 1: SUCCESS
6+
f\(\)
7+
^EXIT=0$
8+
^SIGNAL=0$
9+
--
10+
g\(\)
11+
--
12+
Check that a call to a local function pointer is correctly restricted
Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
#include <assert.h>
2+
3+
int f(void)
4+
{
5+
return 1;
6+
}
7+
8+
int g(void)
9+
{
10+
return 2;
11+
}
12+
13+
typedef int (*fp_t)(void);
14+
15+
void use_fp(fp_t fp)
16+
{
17+
assert(fp() == 1);
18+
}
19+
20+
void main()
21+
{
22+
use_fp(f);
23+
}
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
test.c
3+
--restrict-function-pointer-by-name use_fp::fp/f
4+
\[use_fp\.assertion\.1\] line \d+ dereferenced function pointer at use_fp\.function_pointer_call\.1 must be f: SUCCESS
5+
\[use_fp\.assertion\.2\] line \d+ assertion fp\(\) == 1: SUCCESS
6+
f\(\)
7+
^EXIT=0$
8+
^SIGNAL=0$
9+
--
10+
g\(\)
11+
--
12+
Check that a call to a function pointer parameter is correctly restricted

regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.c

Lines changed: 10 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -2,30 +2,14 @@
22

33
typedef int (*fptr_t)(int);
44

5-
fptr_t get_f(void);
6-
75
void use_f(fptr_t fptr)
86
{
9-
assert(fptr(10) >= 10);
10-
}
11-
12-
void select_f(void);
13-
void select_g(void);
14-
void select_h(void);
15-
16-
int main(void)
17-
{
18-
select_f();
19-
use_f(get_f());
20-
select_g();
21-
use_f(get_f());
22-
select_h();
23-
use_f(get_f());
7+
fptr(1);
248
}
259

2610
int f(int x)
2711
{
28-
return x + 1;
12+
return x;
2913
}
3014

3115
int g(int x)
@@ -35,38 +19,19 @@ int g(int x)
3519

3620
int h(int x)
3721
{
38-
return x - 1;
39-
}
40-
41-
int select_function = 0;
42-
43-
void select_f(void)
44-
{
45-
select_function = 0;
22+
return x;
4623
}
4724

48-
void select_g(void)
25+
int other(int x)
4926
{
50-
select_function = 1;
27+
return x;
5128
}
5229

53-
void select_h(void)
30+
int main(void)
5431
{
55-
select_function = 2;
32+
use_f(f);
33+
use_f(g);
34+
use_f(h);
35+
use_f(other);
5636
}
5737

58-
fptr_t get_f(void)
59-
{
60-
if(select_function == 0)
61-
{
62-
return f;
63-
}
64-
else if(select_function == 1)
65-
{
66-
return g;
67-
}
68-
else
69-
{
70-
return h;
71-
}
72-
}

regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,14 @@
11
CORE
22
test.c
3-
--function-pointer-restrictions-file restrictions.json --restrict-function-pointer use_f.function_pointer_call.1/g
4-
\[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
3+
--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
4+
\[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
55
^EXIT=10$
66
^SIGNAL=0$
77
--
88
--
99
This test checks that the restrictions for a function pointer are the union of
10-
the restrictions given in a file and on the command line.
10+
the restrictions given in a file and on the command line (both with functions
11+
pointers being numbered and named)
1112

1213
The test further checks that the correct safety assertions are generated. The
1314
function pointer restriction feature outputs safety assertions for all calls

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1037,13 +1037,17 @@ void goto_instrument_parse_optionst::instrument_goto_program()
10371037
{
10381038
parse_function_pointer_restriction_options_from_cmdline(cmdline, options);
10391039

1040-
const auto function_pointer_restrictions =
1041-
function_pointer_restrictionst::from_options(
1042-
options, log.get_message_handler());
1043-
1044-
if(!function_pointer_restrictions.restrictions.empty())
1040+
if(
1041+
options.is_set(RESTRICT_FUNCTION_POINTER_OPT) ||
1042+
options.is_set(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT) ||
1043+
options.is_set(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT))
10451044
{
10461045
label_function_pointer_call_sites(goto_model);
1046+
1047+
const auto function_pointer_restrictions =
1048+
function_pointer_restrictionst::from_options(
1049+
options, goto_model, log.get_message_handler());
1050+
10471051
restrict_function_pointers(goto_model, function_pointer_restrictions);
10481052
}
10491053
}

0 commit comments

Comments
 (0)