Skip to content

Commit cae911c

Browse files
author
thk123
committed
Added flag for goto-instrument to just remove const function pointers
Added a flag --remove-const-function-pointers for goto-instrument that can be used instead of --remove-function-pointers to only remove function pointers where we can resolve to something more precise that all functions with a matching signature.
1 parent 30804d3 commit cae911c

File tree

17 files changed

+361
-15
lines changed

17 files changed

+361
-15
lines changed

‎regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/main.c

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
#include <stdio.h>
2+
3+
void f1 (void) { printf("%i\n", 1); }
4+
void f2 (void) { printf("%i\n", 2); }
5+
void f3 (void) { printf("%i\n", 3); }
6+
void f4 (void) { printf("%i\n", 4); }
7+
void f5 (void) { printf("%i\n", 5); }
8+
void f6 (void) { printf("%i\n", 6); }
9+
void f7 (void) { printf("%i\n", 7); }
10+
void f8 (void) { printf("%i\n", 8); }
11+
void f9 (void) { printf("%i\n", 9); }
12+
13+
typedef void(*void_fp)(void);
14+
15+
const 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(int i)
22+
{
23+
fp_tbl[i]();
24+
}
25+
26+
int main()
27+
{
28+
for(int i=0;i<3;i++)
29+
{
30+
func(i);
31+
}
32+
33+
return 0;
34+
}

‎regression/goto-instrument/approx-array-variable-const-fp-only-remove-const/test.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
--verbosity 10 --pointer-check --remove-const-function-pointers
4+
5+
^\s*IF fp_tbl\[(signed long int)i\] == f2 THEN GOTO [0-9]$
6+
^\s*IF fp_tbl\[(signed long int)i\] == f3 THEN GOTO [0-9]$
7+
^\s*IF fp_tbl\[(signed long int)i\] == f4 THEN GOTO [0-9]$
8+
^SIGNAL=0$
9+
--
10+
^\s*IF fp_tbl\[(signed long int)i\] == f1 THEN GOTO [0-9]$
11+
^\s*IF fp_tbl\[(signed long int)i\] == f5 THEN GOTO [0-9]$
12+
^\s*IF fp_tbl\[(signed long int)i\] == f6 THEN GOTO [0-9]$
13+
^\s*IF fp_tbl\[(signed long int)i\] == f7 THEN GOTO [0-9]$
14+
^\s*IF fp_tbl\[(signed long int)i\] == f8 THEN GOTO [0-9]$
15+
^\s*IF fp_tbl\[(signed long int)i\] == f9 THEN GOTO [0-9]$
16+
^warning: ignoring

‎regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/main.c

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,34 @@
1+
#include <stdio.h>
2+
3+
void f1 (void) { printf("%i\n", 1); }
4+
void f2 (void) { printf("%i\n", 2); }
5+
void f3 (void) { printf("%i\n", 3); }
6+
void f4 (void) { printf("%i\n", 4); }
7+
void f5 (void) { printf("%i\n", 5); }
8+
void f6 (void) { printf("%i\n", 6); }
9+
void f7 (void) { printf("%i\n", 7); }
10+
void f8 (void) { printf("%i\n", 8); }
11+
void f9 (void) { printf("%i\n", 9); }
12+
13+
typedef void(*void_fp)(void);
14+
15+
const 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(int i)
22+
{
23+
fp_tbl[i]();
24+
}
25+
26+
int main()
27+
{
28+
for(int i=0;i<3;i++)
29+
{
30+
func(i);
31+
}
32+
33+
return 0;
34+
}

‎regression/goto-instrument/approx-array-variable-const-fp-remove-all-fp/test.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
--verbosity 10 --pointer-check --remove-function-pointers
4+
5+
^\s*IF fp_tbl\[(signed long int)i\] == f2 THEN GOTO [0-9]$
6+
^\s*IF fp_tbl\[(signed long int)i\] == f3 THEN GOTO [0-9]$
7+
^\s*IF fp_tbl\[(signed long int)i\] == f4 THEN GOTO [0-9]$
8+
^SIGNAL=0$
9+
--
10+
^\s*IF fp_tbl\[(signed long int)i\] == f1 THEN GOTO [0-9]$
11+
^\s*IF fp_tbl\[(signed long int)i\] == f5 THEN GOTO [0-9]$
12+
^\s*IF fp_tbl\[(signed long int)i\] == f6 THEN GOTO [0-9]$
13+
^\s*IF fp_tbl\[(signed long int)i\] == f7 THEN GOTO [0-9]$
14+
^\s*IF fp_tbl\[(signed long int)i\] == f8 THEN GOTO [0-9]$
15+
^\s*IF fp_tbl\[(signed long int)i\] == f9 THEN GOTO [0-9]$
16+
^warning: ignoring

‎regression/goto-instrument/no-match-non-const-fp-only-remove-const/main.c

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\n", 1); }
4+
void f2 (void) { printf("%i\n", 2); }
5+
void f3 (void) { printf("%i\n", 3); }
6+
void f4 (void) { printf("%i\n", 4); }
7+
void f5 (void) { printf("%i\n", 5); }
8+
void f6 (void) { printf("%i\n", 6); }
9+
void f7 (void) { printf("%i\n", 7); }
10+
void f8 (void) { printf("%i\n", 8); }
11+
void f9 (void) { printf("%i\n", 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+
int main()
27+
{
28+
func();
29+
30+
return 0;
31+
}

‎regression/goto-instrument/no-match-non-const-fp-only-remove-const/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--verbosity 10 --pointer-check --remove-const-function-pointers
4+
5+
^\s*fp();$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring

‎regression/goto-instrument/no-match-non-const-fp-remove-all-fp/main.c

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\n", 1); }
4+
void f2 (void) { printf("%i\n", 2); }
5+
void f3 (void) { printf("%i\n", 3); }
6+
void f4 (void) { printf("%i\n", 4); }
7+
void f5 (void) { printf("%i\n", 5); }
8+
void f6 (void) { printf("%i\n", 6); }
9+
void f7 (void) { printf("%i\n", 7); }
10+
void f8 (void) { printf("%i\n", 8); }
11+
void f9 (void) { printf("%i\n", 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+
int main()
27+
{
28+
func();
29+
30+
return 0;
31+
}

‎regression/goto-instrument/no-match-non-const-fp-remove-all-fp/test.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
main.c
3+
--verbosity 10 --pointer-check --remove-function-pointers
4+
5+
^\s*IF fp == f1 THEN GOTO [0-9]$
6+
^\s*IF fp == f2 THEN GOTO [0-9]$
7+
^\s*IF fp == f3 THEN GOTO [0-9]$
8+
^\s*IF fp == f4 THEN GOTO [0-9]$
9+
^\s*IF fp == f5 THEN GOTO [0-9]$
10+
^\s*IF fp == f6 THEN GOTO [0-9]$
11+
^\s*IF fp == f7 THEN GOTO [0-9]$
12+
^\s*IF fp == f8 THEN GOTO [0-9]$
13+
^\s*IF fp == f9 THEN GOTO [0-9]$
14+
^SIGNAL=0$
15+
--
16+
^warning: ignoring

‎regression/goto-instrument/precise-const-fp-only-remove-const/main.c

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
#include <stdio.h>
2+
3+
void f1 (void) { printf("%i\n", 1); }
4+
void f2 (void) { printf("%i\n", 2); }
5+
void f3 (void) { printf("%i\n", 3); }
6+
void f4 (void) { printf("%i\n", 4); }
7+
void f5 (void) { printf("%i\n", 5); }
8+
void f6 (void) { printf("%i\n", 6); }
9+
void f7 (void) { printf("%i\n", 7); }
10+
void f8 (void) { printf("%i\n", 8); }
11+
void f9 (void) { printf("%i\n", 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+
int main()
26+
{
27+
func();
28+
29+
return 0;
30+
}

‎regression/goto-instrument/precise-const-fp-only-remove-const/test.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--verbosity 10 --pointer-check --remove-const-function-pointers
4+
5+
^\s*f2();
6+
--
7+
^warning: ignoring

‎regression/goto-instrument/precise-const-fp-remove-all-fp/main.c

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
#include <stdio.h>
2+
3+
void f1 (void) { printf("%i\n", 1); }
4+
void f2 (void) { printf("%i\n", 2); }
5+
void f3 (void) { printf("%i\n", 3); }
6+
void f4 (void) { printf("%i\n", 4); }
7+
void f5 (void) { printf("%i\n", 5); }
8+
void f6 (void) { printf("%i\n", 6); }
9+
void f7 (void) { printf("%i\n", 7); }
10+
void f8 (void) { printf("%i\n", 8); }
11+
void f9 (void) { printf("%i\n", 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+
int main()
26+
{
27+
func();
28+
29+
return 0;
30+
}

‎regression/goto-instrument/precise-const-fp-remove-all-fp/test.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--verbosity 10 --pointer-check --remove-function-pointers
4+
5+
^\s*f2();
6+
--
7+
^warning: ignoring

‎src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -791,6 +791,39 @@ void goto_instrument_parse_optionst::do_indirect_call_and_rtti_removal(
791791

792792
/*******************************************************************\
793793
794+
Function: goto_instrument_parse_optionst::do_remove_const_function_pointers_only
795+
796+
Inputs:
797+
798+
Outputs:
799+
800+
Purpose: Remove function pointers that can be resolved by analysing
801+
const variables (i.e. can be resolved using
802+
remove_const_function_pointers). Function pointers that cannot
803+
be resolved will be left as function pointers.
804+
805+
\*******************************************************************/
806+
807+
void goto_instrument_parse_optionst::do_remove_const_function_pointers_only()
808+
{
809+
// Don't bother if we've already done a full function pointer
810+
// removal.
811+
if(function_pointer_removal_done)
812+
{
813+
return;
814+
}
815+
816+
status() << "Removing const function pointers only" << eom;
817+
remove_function_pointers(
818+
*message_handler,
819+
symbol_table,
820+
goto_functions,
821+
cmdline.isset("pointer-check"),
822+
true); // abort if we can't resolve via const pointers
823+
}
824+
825+
/*******************************************************************\
826+
794827
Function: goto_instrument_parse_optionst::do_partial_inlining
795828
796829
Inputs:
@@ -1017,7 +1050,13 @@ void goto_instrument_parse_optionst::instrument_goto_program()
10171050

10181051
// replace function pointers, if explicitly requested
10191052
if(cmdline.isset("remove-function-pointers"))
1053+
{
10201054
do_indirect_call_and_rtti_removal();
1055+
}
1056+
else if(cmdline.isset("remove-const-function-pointers"))
1057+
{
1058+
do_remove_const_function_pointers_only();
1059+
}
10211060

10221061
if(cmdline.isset("function-inline"))
10231062
{
@@ -1520,6 +1559,7 @@ void goto_instrument_parse_optionst::help()
15201559
" --function-inline <function> transitively inline all calls <function> makes\n" // NOLINT(*)
15211560
" --log <file> log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
15221561
" --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*)
1562+
HELP_REMOVE_CONST_FUNCTION_POINTERS
15231563
" --add-library add models of C library functions\n"
15241564
" --model-argc-argv <n> model up to <n> command line arguments\n"
15251565
"\n"

‎src/goto-instrument/goto_instrument_parse_options.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
1515
#include <langapi/language_ui.h>
1616
#include <goto-programs/goto_functions.h>
1717
#include <goto-programs/show_goto_functions.h>
18+
#include <goto-programs/remove_const_function_pointers.h>
1819

1920
#include <analyses/goto_check.h>
2021

@@ -54,6 +55,7 @@ Author: Daniel Kroening, kroening@kroening.com
5455
"(show-uninitialized)(show-locations)" \
5556
"(full-slice)(reachability-slice)(slice-global-inits)" \
5657
"(inline)(partial-inline)(function-inline):(log):" \
58+
OPT_REMOVE_CONST_FUNCTION_POINTERS \
5759
"(remove-function-pointers)" \
5860
"(show-claims)(show-properties)(property):" \
5961
"(show-symbol-table)(show-points-to)(show-rw-set)" \
@@ -97,6 +99,7 @@ class goto_instrument_parse_optionst:
9799
void eval_verbosity();
98100

99101
void do_indirect_call_and_rtti_removal(bool force=false);
102+
void do_remove_const_function_pointers_only();
100103
void do_partial_inlining();
101104
void do_remove_returns();
102105

‎src/goto-programs/remove_const_function_pointers.h

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -95,4 +95,11 @@ class remove_const_function_pointerst:public messaget
9595
const symbol_tablet &symbol_table;
9696
};
9797

98+
#define OPT_REMOVE_CONST_FUNCTION_POINTERS \
99+
"(remove-const-function-pointers)"
100+
101+
#define HELP_REMOVE_CONST_FUNCTION_POINTERS \
102+
" --remove-const-function-pointers Remove function pointers that are constant or constant part of an array\n" // NOLINT(*)
103+
104+
98105
#endif // CPROVER_GOTO_PROGRAMS_REMOVE_CONST_FUNCTION_POINTERS_H

0 commit comments

Comments
 (0)