Skip to content

Commit 89562ca

Browse files
author
thk123
committed
Adding tests for function pointer removal
These tests demonstrate the different ways in which we could easily do better in function pointer resolution. At the moment, each example thinks the function pointer could be any of the 9 functions but in all cases can do much better (either know exactly the function or subset of functions) Added const to arrays that aren't modified which will then be used to determine arrays whose contents can be known. Added test for arrays that are not constant and are in fact modified. Adding test for when FP array declared as a pointer The function pointer optimsation can be further improved by dealing with things like structs and pointers to function pointers. More detail is outlined in diffblue#476 Added test for nullptr terminated arrays Adding const struct regression tests FPs may not always be assigned into a const FP and instead may be called in place (e.g. directly from the array). This modifies the exprt structure that must be unpacked. These tests demonstrate the different ways that can be done. Adding and correcting tests for pointers to FPs
1 parent 5ecb15e commit 89562ca

File tree

78 files changed

+1840
-0
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

78 files changed

+1840
-0
lines changed
Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
#include <stdio.h>
2+
3+
void f1 (void) { printf("%i", 1); }
4+
void f2 (void) { printf("%i", 2); }
5+
void f3 (void) { printf("%i", 3); }
6+
void f4 (void) { printf("%i", 4); }
7+
void f5 (void) { printf("%i", 5); }
8+
void f6 (void) { printf("%i", 6); }
9+
void f7 (void) { printf("%i", 7); }
10+
void f8 (void) { printf("%i", 8); }
11+
void f9 (void) { printf("%i", 9); }
12+
13+
typedef void(*void_fp)(void);
14+
15+
// There is a basic check that excludes all functions that aren't used anywhere
16+
// This ensures that check can't work in this example
17+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
18+
19+
void func()
20+
{
21+
const void_fp fp = f2;
22+
fp();
23+
}
24+
25+
void main(){
26+
func();
27+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--show-goto-functions
4+
5+
^Removing function pointers and virtual functions$
6+
^\s*f2();
7+
--
8+
^warning: ignoring
Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
#include <stdio.h>
2+
3+
void f1 (void) { printf("%i", 1); }
4+
void f2 (void) { printf("%i", 2); }
5+
void f3 (void) { printf("%i", 3); }
6+
void f4 (void) { printf("%i", 4); }
7+
void f5 (void) { printf("%i", 5); }
8+
void f6 (void) { printf("%i", 6); }
9+
void f7 (void) { printf("%i", 7); }
10+
void f8 (void) { printf("%i", 8); }
11+
void f9 (void) { printf("%i", 9); }
12+
13+
typedef void(*void_fp)(void);
14+
15+
void_fp fp_tbl[] = {f2, f3, f4};
16+
17+
// There is a basic check that excludes all functions that aren't used anywhere
18+
// This ensures that check can't work in this example
19+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
20+
21+
void func(void_fp fp, int i){
22+
fp_tbl[2] = fp;
23+
const void_fp fp2 = fp_tbl[2];
24+
fp2();
25+
}
26+
27+
void main(){
28+
for(int i=0;i<3;i++){
29+
func(fp_all[i+3], i);
30+
}
31+
}
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
main.c
3+
--show-goto-functions
4+
5+
^Removing function pointers and virtual functions$
6+
^\s*IF fp2 == f1 THEN GOTO 1$
7+
^\s*IF fp2 == f2 THEN GOTO 2$
8+
^\s*IF fp2 == f3 THEN GOTO 3$
9+
^\s*IF fp2 == f4 THEN GOTO 4$
10+
^\s*IF fp2 == f5 THEN GOTO 5$
11+
^\s*IF fp2 == f6 THEN GOTO 6$
12+
^\s*IF fp2 == f7 THEN GOTO 7$
13+
^\s*IF fp2 == f8 THEN GOTO 8$
14+
^\s*IF fp2 == f9 THEN GOTO 9$
15+
^SIGNAL=0$
16+
--
17+
^warning: ignoring
Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
#include <stdio.h>
2+
#include <stdlib.h>
3+
4+
void f1 (void) { printf("%i", 1); }
5+
void f2 (void) { printf("%i", 2); }
6+
void f3 (void) { printf("%i", 3); }
7+
void f4 (void) { printf("%i", 4); }
8+
void f5 (void) { printf("%i", 5); }
9+
void f6 (void) { printf("%i", 6); }
10+
void f7 (void) { printf("%i", 7); }
11+
void f8 (void) { printf("%i", 8); }
12+
void f9 (void) { printf("%i", 9); }
13+
14+
typedef void(*void_fp)(void);
15+
16+
// There is a basic check that excludes all functions that aren't used anywhere
17+
// This ensures that check can't work in this example
18+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
19+
20+
void func(){
21+
void_fp * const fp_tbl= malloc(sizeof(void_fp) * 3);
22+
fp_tbl[0]=f2;
23+
fp_tbl[1]=f3;
24+
fp_tbl[2]=f4;
25+
const void_fp fp = fp_tbl[1];
26+
fp();
27+
}
28+
29+
void main(){
30+
func();
31+
}
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
main.c
3+
--show-goto-functions
4+
5+
^Removing function pointers and virtual functions$
6+
^\s*IF fp == f1 THEN GOTO 1$
7+
^\s*IF fp == f2 THEN GOTO 2$
8+
^\s*IF fp == f3 THEN GOTO 3$
9+
^\s*IF fp == f4 THEN GOTO 4$
10+
^\s*IF fp == f5 THEN GOTO 5$
11+
^\s*IF fp == f6 THEN GOTO 6$
12+
^\s*IF fp == f7 THEN GOTO 7$
13+
^\s*IF fp == f8 THEN GOTO 8$
14+
^\s*IF fp == f9 THEN GOTO 9$
15+
^SIGNAL=0$
16+
--
17+
^warning: ignoring
Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
#include <stdio.h>
2+
#include <stdlib.h>
3+
4+
void f1 (void) { printf("%i", 1); }
5+
void f2 (void) { printf("%i", 2); }
6+
void f3 (void) { printf("%i", 3); }
7+
void f4 (void) { printf("%i", 4); }
8+
void f5 (void) { printf("%i", 5); }
9+
void f6 (void) { printf("%i", 6); }
10+
void f7 (void) { printf("%i", 7); }
11+
void f8 (void) { printf("%i", 8); }
12+
void f9 (void) { printf("%i", 9); }
13+
14+
typedef void(*void_fp)(void);
15+
16+
// There is a basic check that excludes all functions that aren't used anywhere
17+
// This ensures that check can't work in this example
18+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
19+
20+
typedef struct fp_container
21+
{
22+
const void_fp fp_tbl[3];
23+
} fp_container;
24+
25+
26+
27+
void func(){
28+
fp_container container = { .fp_tbl = {f2 ,f3, f4} };
29+
fp_container container2 = { .fp_tbl = {f5 ,f6, f7} };
30+
// Illegal:
31+
// container = container2;
32+
const void_fp fp = container.fp_tbl[1];
33+
fp();
34+
}
35+
36+
void main(){
37+
func();
38+
}
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
KNOWNBUG
2+
main.c
3+
--show-goto-functions
4+
5+
^Removing function pointers and virtual functions$
6+
^\s*f3();$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--
11+
This test is marked as a KNOWNBUG as it is possible for the function
12+
pointer to be optimized away. Currently goto-analyzer falls back to
13+
assuming it could be any type compatible function.
14+
15+
Issue: https://github.com/diffblue/cbmc/issues/476
Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
#include <stdio.h>
2+
#include <stdlib.h>
3+
4+
void f1 (void) { printf("%i", 1); }
5+
void f2 (void) { printf("%i", 2); }
6+
void f3 (void) { printf("%i", 3); }
7+
void f4 (void) { printf("%i", 4); }
8+
void f5 (void) { printf("%i", 5); }
9+
void f6 (void) { printf("%i", 6); }
10+
void f7 (void) { printf("%i", 7); }
11+
void f8 (void) { printf("%i", 8); }
12+
void f9 (void) { printf("%i", 9); }
13+
14+
typedef void(*void_fp)(void);
15+
16+
// There is a basic check that excludes all functions that aren't used anywhere
17+
// This ensures that check can't work in this example
18+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
19+
20+
typedef struct fp_container
21+
{
22+
void_fp fp_tbl[3];
23+
} fp_container;
24+
25+
26+
27+
void func(){
28+
const fp_container container = { .fp_tbl = {f2 ,f3, f4} };
29+
fp_container container2 = { .fp_tbl = {f5 ,f6, f7} };
30+
const void_fp alternatate_fp_tbl[] = {f5 ,f6, f7};
31+
// Illegal:
32+
// container = container2;
33+
// container.fp_tbl = alternatate_fp_tbl;
34+
// container.fp_tbl[1] = f4;
35+
const void_fp fp = container.fp_tbl[1];
36+
fp();
37+
}
38+
39+
void main(){
40+
func();
41+
}
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
main.c
3+
--show-goto-functions --verbosity 10
4+
5+
^Removing function pointers and virtual functions$
6+
^\s*f3();$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--
11+
This test is marked as a KNOWNBUG as it is possible for the function
12+
pointer to be optimized away. Currently goto-analyzer falls back to
13+
assuming it could be any type compatible function.
14+
15+
Issue: https://github.com/diffblue/cbmc/issues/476
Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
#include <stdio.h>
2+
#include <stdlib.h>
3+
4+
void f1 (void) { printf("%i", 1); }
5+
void f2 (void) { printf("%i", 2); }
6+
void f3 (void) { printf("%i", 3); }
7+
void f4 (void) { printf("%i", 4); }
8+
void f5 (void) { printf("%i", 5); }
9+
void f6 (void) { printf("%i", 6); }
10+
void f7 (void) { printf("%i", 7); }
11+
void f8 (void) { printf("%i", 8); }
12+
void f9 (void) { printf("%i", 9); }
13+
14+
typedef void(*void_fp)(void);
15+
16+
// There is a basic check that excludes all functions that aren't used anywhere
17+
// This ensures that check can't work in this example
18+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
19+
20+
void func(){
21+
const void_fp fp = f3;
22+
const void_fp fp2 = f4;
23+
const void_fp* const p2fp = &fp;
24+
// Illegal:
25+
//p2fp = &fp2;
26+
//fp = f5;
27+
(*p2fp)();
28+
}
29+
30+
void main(){
31+
func();
32+
}
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
KNOWNBUG
2+
main.c
3+
--show-goto-functions
4+
5+
^Removing function pointers and virtual functions$
6+
^\s*f3();$
7+
^SIGNAL=0$
8+
--
9+
^warning: ignoring
10+
--
11+
This test is marked as a KNOWNBUG as it is possible for the function
12+
pointer to be optimized away. Currently goto-analyzer falls back to
13+
assuming it could be any type compatible function.
14+
15+
Issue: https://github.com/diffblue/cbmc/issues/476
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
#include <stdio.h>
2+
3+
void f1 (void) { printf("%i", 1); }
4+
void f2 (void) { printf("%i", 2); }
5+
void f3 (void) { printf("%i", 3); }
6+
void f4 (void) { printf("%i", 4); }
7+
void f5 (void) { printf("%i", 5); }
8+
void f6 (void) { printf("%i", 6); }
9+
void f7 (void) { printf("%i", 7); }
10+
void f8 (void) { printf("%i", 8); }
11+
void f9 (void) { printf("%i", 9); }
12+
13+
typedef void(*void_fp)(void);
14+
15+
// There is a basic check that excludes all functions that aren't used anywhere
16+
// This ensures that check can't work in this example
17+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
18+
19+
void func()
20+
{
21+
void_fp fp = f2;
22+
fp = f3;
23+
fp();
24+
}
25+
26+
void main(){
27+
func();
28+
}
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
main.c
3+
--show-goto-functions
4+
5+
^Removing function pointers and virtual functions$
6+
^\s*IF fp == f1 THEN GOTO 1$
7+
^\s*IF fp == f2 THEN GOTO 2$
8+
^\s*IF fp == f3 THEN GOTO 3$
9+
^\s*IF fp == f4 THEN GOTO 4$
10+
^\s*IF fp == f5 THEN GOTO 5$
11+
^\s*IF fp == f6 THEN GOTO 6$
12+
^\s*IF fp == f7 THEN GOTO 7$
13+
^\s*IF fp == f8 THEN GOTO 8$
14+
^\s*IF fp == f9 THEN GOTO 9$
15+
^SIGNAL=0$
16+
--
17+
^warning: ignoring
Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
#include <stdio.h>
2+
3+
void f1 (void) { printf("%i", 1); }
4+
void f2 (void) { printf("%i", 2); }
5+
void f3 (void) { printf("%i", 3); }
6+
void f4 (void) { printf("%i", 4); }
7+
void f5 (void) { printf("%i", 5); }
8+
void f6 (void) { printf("%i", 6); }
9+
void f7 (void) { printf("%i", 7); }
10+
void f8 (void) { printf("%i", 8); }
11+
void f9 (void) { printf("%i", 9); }
12+
13+
typedef void(*void_fp)(void);
14+
15+
// There is a basic check that excludes all functions that aren't used anywhere
16+
// This ensures that check can't work in this example
17+
const void_fp fp_all[] = {f1, f2 ,f3, f4, f5 ,f6, f7, f8, f9};
18+
19+
void func()
20+
{
21+
const void_fp fp = f2;
22+
const void_fp fp3 = f4;
23+
void_fp fp2 = fp;
24+
fp2 = fp3;
25+
fp2();
26+
}
27+
28+
void main()
29+
{
30+
func();
31+
}
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
--show-goto-functions
4+
^Removing function pointers and virtual functions$
5+
^\s*IF fp2 == f1 THEN GOTO 1$
6+
^\s*IF fp2 == f2 THEN GOTO 2$
7+
^\s*IF fp2 == f3 THEN GOTO 3$
8+
^\s*IF fp2 == f4 THEN GOTO 4$
9+
^\s*IF fp2 == f5 THEN GOTO 5$
10+
^\s*IF fp2 == f6 THEN GOTO 6$
11+
^\s*IF fp2 == f7 THEN GOTO 7$
12+
^\s*IF fp2 == f8 THEN GOTO 8$
13+
^\s*IF fp2 == f9 THEN GOTO 9$
14+
^SIGNAL=0$
15+
--
16+
^warning: ignoring

0 commit comments

Comments
 (0)