diff --git a/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc b/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc index fd055d8d613..01bd38d3647 100644 --- a/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc +++ b/regression/cbmc/Function_Pointer_Init_No_Candidate/test.desc @@ -2,7 +2,7 @@ CORE main.c --function foo --pointer-check ^\[foo.assertion.\d+\] line \d+ assertion other_function\(4\) > 5: SUCCESS$ -^\[foo.pointer_dereference.\d+\] line \d+ invalid function pointer: FAILURE$ +^\[foo.pointer_dereference.\d+\] line \d+ no candidates for dereferenced function pointer: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED diff --git a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc index 5d052a3dd17..0195ef93083 100644 --- a/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc +++ b/regression/goto-analyzer/approx-const-fp-array-variable-struct-const-fp-with-zero/test.desc @@ -5,7 +5,7 @@ main.c ^\s*IF .*::fp = address_of\(f2\) THEN GOTO [0-9]$ ^\s*IF .*::fp = address_of\(f3\) THEN GOTO [0-9]$ ^\s*IF .*::fp = address_of\(f4\) THEN GOTO [0-9]$ -^\s*ASSERT false // invalid function pointer$ +^\s*ASSERT false // dereferenced function pointer must be one of \[f[2-4], f[2-4], f[2-4]\]$ ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc b/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc index d42046c6e62..ef4794c6913 100644 --- a/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-array-literal-const-fp-null/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*ASSERT false // invalid function pointer$ +^\s*ASSERT false // no candidates for dereferenced function pointer ^EXIT=0$ ^SIGNAL=0$ function func: replacing function pointer by 0 possible targets diff --git a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc index 6072f5b10f4..027977038b9 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-fp-null/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*ASSERT false // invalid function pointer$ +^\s*ASSERT false // no candidates for dereferenced function pointer ^EXIT=0$ ^SIGNAL=0$ replacing function pointer by 0 possible targets diff --git a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc index 35d7e0bfdc0..a376a6fb940 100644 --- a/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-const-pointer-const-struct-const-fp-null/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*ASSERT false // invalid function pointer$ +^\s*ASSERT false // dereferenced function pointer must be one of \[(f[1-9], ){8}f[1-9]\]$ replacing function pointer by 9 possible targets ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc index 35d7e0bfdc0..a376a6fb940 100644 --- a/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-dereference-const-pointer-null/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*ASSERT false // invalid function pointer$ +^\s*ASSERT false // dereferenced function pointer must be one of \[(f[1-9], ){8}f[1-9]\]$ replacing function pointer by 9 possible targets ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/no-match-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-fp-null/test.desc index 9fdf5e55158..65e2f401b56 100644 --- a/regression/goto-analyzer/no-match-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-fp-null/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*ASSERT false // invalid function pointer$ +^\s*ASSERT false // no candidates for dereferenced function pointer function func: replacing function pointer by 0 possible targets ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc b/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc index 6072f5b10f4..027977038b9 100644 --- a/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc +++ b/regression/goto-analyzer/no-match-const-struct-non-const-fp-null/test.desc @@ -2,7 +2,7 @@ CORE main.c --show-goto-functions --pointer-check ^Removal of function pointers and virtual functions$ -^\s*ASSERT false // invalid function pointer$ +^\s*ASSERT false // no candidates for dereferenced function pointer ^EXIT=0$ ^SIGNAL=0$ replacing function pointer by 0 possible targets diff --git a/regression/goto-instrument/restrict-function-pointer-by-name-global/test.desc b/regression/goto-instrument/restrict-function-pointer-by-name-global/test.desc index 6389bbbfbb9..58c33f52c09 100644 --- a/regression/goto-instrument/restrict-function-pointer-by-name-global/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-by-name-global/test.desc @@ -1,10 +1,10 @@ CORE test.c --restrict-function-pointer-by-name fp/f,g -\[main\.assertion\.1\] line \d+ dereferenced function pointer at main\.function_pointer_call\.1 must be one of \[(f, g)|(g, f)\]: SUCCESS +\[main\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be one of \[(f, g)|(g, f)\]: SUCCESS +\[main.assertion.1\] line \d+ assertion: FAILURE \[main.assertion.2\] line \d+ assertion: FAILURE -\[main.assertion.3\] line \d+ assertion: FAILURE -\[main.assertion.4\] line \d+ assertion: SUCCESS +\[main.assertion.3\] line \d+ assertion: SUCCESS f\(\) g\(\) ^EXIT=10$ diff --git a/regression/goto-instrument/restrict-function-pointer-by-name-local/test.desc b/regression/goto-instrument/restrict-function-pointer-by-name-local/test.desc index b4754a4b5f8..30e0263ff8a 100644 --- a/regression/goto-instrument/restrict-function-pointer-by-name-local/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-by-name-local/test.desc @@ -1,8 +1,8 @@ CORE test.c --restrict-function-pointer-by-name main::1::fp/f -\[main\.assertion\.1\] line \d+ dereferenced function pointer at main\.function_pointer_call\.1 must be f: SUCCESS -\[main\.assertion\.2\] line \d+ assertion fp\(\) == 1: SUCCESS +\[main\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be f: SUCCESS +\[main\.assertion\.1\] line \d+ assertion fp\(\) == 1: SUCCESS f\(\) ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/restrict-function-pointer-by-name-parameter/test.desc b/regression/goto-instrument/restrict-function-pointer-by-name-parameter/test.desc index 46f11abeb9c..83e5af94c54 100644 --- a/regression/goto-instrument/restrict-function-pointer-by-name-parameter/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-by-name-parameter/test.desc @@ -1,8 +1,8 @@ CORE test.c --restrict-function-pointer-by-name use_fp::fp/f -\[use_fp\.assertion\.1\] line \d+ dereferenced function pointer at use_fp\.function_pointer_call\.1 must be f: SUCCESS -\[use_fp\.assertion\.2\] line \d+ assertion fp\(\) == 1: SUCCESS +\[use_fp\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be f: SUCCESS +\[use_fp\.assertion\.1\] line \d+ assertion fp\(\) == 1: SUCCESS f\(\) ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/restrict-function-pointer-goto-target/test.desc b/regression/goto-instrument/restrict-function-pointer-goto-target/test.desc index 57f430fea9a..ea332cd23c0 100644 --- a/regression/goto-instrument/restrict-function-pointer-goto-target/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-goto-target/test.desc @@ -3,7 +3,7 @@ test.c --restrict-function-pointer main.function_pointer_call.1/f ^EXIT=0$ ^SIGNAL=0$ -\[main.assertion.1\] line \d+ dereferenced function pointer at main.function_pointer_call.1 must be f: SUCCESS +\[main.pointer_dereference.1\] line \d+ dereferenced function pointer must be f: SUCCESS -- -- This test checks that a function pointer call that is the target of a goto (in diff --git a/regression/goto-instrument/restrict-function-pointer-to-compatible-function/test.c b/regression/goto-instrument/restrict-function-pointer-to-compatible-function/test.c new file mode 100644 index 00000000000..cf1adda65d0 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-compatible-function/test.c @@ -0,0 +1,28 @@ +#include + +typedef int (*fptr_t)(long long); + +void use_f(fptr_t fptr) +{ + assert(fptr(10) == 11); +} + +int f(int x) +{ + return x + 1; +} + +int g(int x) +{ + return x; +} + +int main(void) +{ + int one = 1; + + // We take the address of f and g. In this case remove_function_pointers() + // would create a case distinction involving both f and g in the function + // use_f() above. + use_f(one ? f : g); +} diff --git a/regression/goto-instrument/restrict-function-pointer-to-compatible-function/test.desc b/regression/goto-instrument/restrict-function-pointer-to-compatible-function/test.desc new file mode 100644 index 00000000000..70fcf31af06 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-compatible-function/test.desc @@ -0,0 +1,10 @@ +CORE +test.c +--restrict-function-pointer use_f.function_pointer_call.1/f +\[use_f\.assertion\.1\] line \d+ assertion fptr\(10\) == 11: SUCCESS +^EXIT=0$ +^SIGNAL=0$ +-- +-- +This test checks that the function f is permitted for the first function pointer +call in function use_f, despite parameters having different integer types. diff --git a/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc b/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc index f073eea9512..1e97e2783ba 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc @@ -1,8 +1,8 @@ CORE test.c --restrict-function-pointer 'use_fg.function_pointer_call.1/f,g' -\[use_fg.assertion.2\] line \d+ assertion \(choice \? fptr : gptr\)\(10\) == 10 \+ choice: SUCCESS -\[use_fg.assertion.1\] line \d+ dereferenced function pointer at use_fg.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: SUCCESS +\[use_fg.assertion.1\] line \d+ assertion \(choice \? fptr : gptr\)\(10\) == 10 \+ choice: SUCCESS +\[use_fg.pointer_dereference.1\] line \d+ dereferenced function pointer must be one of \[(f|g), (f|g)\]: SUCCESS ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc index 18c7fac80e3..4d1c9dcb977 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc @@ -1,7 +1,7 @@ CORE test.c --restrict-function-pointer use_f.function_pointer_call.1/f,g -\[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: FAILURE +\[use_f\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be one of \[(f|g), (f|g)\]: FAILURE ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc index 9346da5a265..3d49fd80182 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc @@ -1,7 +1,7 @@ CORE test.c --function-pointer-restrictions-file restrictions.json --restrict-function-pointer use_f.function_pointer_call.1/g --restrict-function-pointer-by-name use_f::fptr/h -\[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be one of \[(f|g|h), (f|g|h), (f|g|h)\]: FAILURE +\[use_f\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be one of \[(f|g|h), (f|g|h), (f|g|h)\]: FAILURE ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.desc index 7f5caa4b0a4..6e38e05e2bc 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.desc @@ -1,7 +1,7 @@ CORE test.c --function-pointer-restrictions-file restrictions.json -\[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: FAILURE +\[use_f\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be one of \[(f|g), (f|g)\]: FAILURE ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc index b1a1756ad8b..2bdeb52bd3b 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc @@ -1,7 +1,7 @@ CORE test.c --function-pointer-restrictions-file restrictions_1.json --function-pointer-restrictions-file restrictions_2.json -\[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: FAILURE +\[use_f\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be one of \[(f|g), (f|g)\]: FAILURE ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.desc index 878139b431e..287a1f3ea7a 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.desc @@ -1,6 +1,6 @@ CORE test.c --restrict-function-pointer use_f.function_pointer_call.1/f,g -\[use_f\.assertion\.2\] line \d+ assertion fptr\(10\) >= 10: SUCCESS +\[use_f\.assertion\.1\] line \d+ assertion fptr\(10\) >= 10: SUCCESS ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.desc b/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.desc index 8ab6995bf6e..4df0a73ca28 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.desc @@ -1,7 +1,7 @@ CORE test.c --restrict-function-pointer use_f.function_pointer_call.1/f -\[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be f: FAILURE +\[use_f\.pointer_dereference\.1\] line \d+ dereferenced function pointer must be f: FAILURE ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/goto-instrument/restrict-function-pointer-to-single-function/test.desc b/regression/goto-instrument/restrict-function-pointer-to-single-function/test.desc index 4108fed725e..f6d227f46f6 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-single-function/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-to-single-function/test.desc @@ -1,7 +1,7 @@ CORE test.c --restrict-function-pointer use_f.function_pointer_call.1/f -\[use_f\.assertion\.2\] line \d+ assertion fptr\(10\) == 11: SUCCESS +\[use_f\.assertion\.1\] line \d+ assertion fptr\(10\) == 11: SUCCESS ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 8bc4ff2b7a7..b0c50776e94 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1034,7 +1034,8 @@ void goto_instrument_parse_optionst::instrument_goto_program() function_pointer_restrictionst::from_options( options, goto_model, log.get_message_handler()); - restrict_function_pointers(goto_model, function_pointer_restrictions); + restrict_function_pointers( + ui_message_handler, goto_model, function_pointer_restrictions); } } diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index e4903f8d9ee..a0bcdd80db9 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include @@ -44,24 +45,8 @@ class remove_function_pointerst goto_programt &goto_program, const irep_idt &function_id); - // a set of function symbols - using functionst = remove_const_function_pointerst::functionst; - - /// Replace a call to a dynamic function at location - /// target in the given goto-program by a case-split - /// over a given set of functions - /// \param goto_program: The goto program that contains target - /// \param function_id: Name of function containing the target - /// \param target: location with function call with function pointer - /// \param functions: The set of functions to consider - void remove_function_pointer( - goto_programt &goto_program, - const irep_idt &function_id, - goto_programt::targett target, - const functionst &functions); - protected: - messaget log; + message_handlert &message_handler; const namespacet ns; symbol_tablet &symbol_table; bool add_safety_assertion; @@ -89,21 +74,6 @@ class remove_function_pointerst typedef std::map type_mapt; type_mapt type_map; - - bool is_type_compatible( - bool return_value_used, - const code_typet &call_type, - const code_typet &function_type); - - bool arg_is_type_compatible( - const typet &call_type, - const typet &function_type); - - void fix_argument_types(code_function_callt &function_call); - void fix_return_type( - const irep_idt &in_function_id, - code_function_callt &function_call, - goto_programt &dest); }; remove_function_pointerst::remove_function_pointerst( @@ -112,7 +82,7 @@ remove_function_pointerst::remove_function_pointerst( bool _add_safety_assertion, bool only_resolve_const_fps, const goto_functionst &goto_functions) - : log(_message_handler), + : message_handler(_message_handler), ns(_symbol_table), symbol_table(_symbol_table), add_safety_assertion(_add_safety_assertion), @@ -131,9 +101,10 @@ remove_function_pointerst::remove_function_pointerst( } } -bool remove_function_pointerst::arg_is_type_compatible( +static bool arg_is_type_compatible( const typet &call_type, - const typet &function_type) + const typet &function_type, + const namespacet &ns) { if(call_type == function_type) return true; @@ -157,10 +128,11 @@ bool remove_function_pointerst::arg_is_type_compatible( pointer_offset_bits(function_type, ns); } -bool remove_function_pointerst::is_type_compatible( +bool function_is_type_compatible( bool return_value_used, const code_typet &call_type, - const code_typet &function_type) + const code_typet &function_type, + const namespacet &ns) { // we are willing to ignore anything that's returned // if we call with 'void' @@ -173,8 +145,8 @@ bool remove_function_pointerst::is_type_compatible( } else { - if(!arg_is_type_compatible(call_type.return_type(), - function_type.return_type())) + if(!arg_is_type_compatible( + call_type.return_type(), function_type.return_type(), ns)) return false; } @@ -199,16 +171,15 @@ bool remove_function_pointerst::is_type_compatible( return false; for(std::size_t i=0; i &candidates) +{ + std::stringstream comment; + + comment << "dereferenced function pointer must be "; + + if(candidates.size() == 1) + { + comment << candidates.begin()->get_identifier(); + } + else if(candidates.empty()) + { + comment.str("no candidates for dereferenced function pointer"); + } + else + { + comment << "one of ["; + + join_strings( + comment, + candidates.begin(), + candidates.end(), + ", ", + [](const symbol_exprt &s) { return s.get_identifier(); }); + + comment << ']'; + } + + return comment.str(); +} + +void remove_function_pointer( + message_handlert &message_handler, + symbol_tablet &symbol_table, goto_programt &goto_program, const irep_idt &function_id, goto_programt::targett target, - const functionst &functions) + const std::unordered_set &functions, + const bool add_safety_assertion) { const exprt &function = target->call_function(); const exprt &pointer = to_dereference_expr(function).pointer(); @@ -388,7 +405,7 @@ void remove_function_pointerst::remove_function_pointer( fix_argument_types(new_call); goto_programt tmp; - fix_return_type(function_id, new_call, tmp); + fix_return_type(function_id, new_call, symbol_table, tmp); auto call = new_code_calls.add(goto_programt::make_function_call(new_call)); new_code_calls.destructive_append(tmp); @@ -412,7 +429,8 @@ void remove_function_pointerst::remove_function_pointer( goto_programt::targett t = new_code_gotos.add(goto_programt::make_assertion(false_exprt())); t->source_location_nonconst().set_property_class("pointer dereference"); - t->source_location_nonconst().set_comment("invalid function pointer"); + t->source_location_nonconst().set_comment( + function_pointer_assertion_comment(functions)); } new_code_gotos.add(goto_programt::make_assumption(false_exprt())); @@ -450,6 +468,7 @@ void remove_function_pointerst::remove_function_pointer( goto_programt::make_other(code_expression, target->source_location()); // report statistics + messaget log{message_handler}; log.statistics().source_location = target->source_location(); log.statistics() << "replacing function pointer by " << functions.size() << " possible targets" << messaget::eom; diff --git a/src/goto-programs/remove_function_pointers.h b/src/goto-programs/remove_function_pointers.h index bff989e1cea..ccbfd308847 100644 --- a/src/goto-programs/remove_function_pointers.h +++ b/src/goto-programs/remove_function_pointers.h @@ -14,10 +14,11 @@ Date: June 2003 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H #define CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H -#include +#include "goto_program.h" + +#include class goto_functionst; -class goto_programt; class goto_modelt; class message_handlert; class symbol_tablet; @@ -46,4 +47,32 @@ bool remove_function_pointers( bool add_safety_assertion, bool only_remove_const_fps = false); +/// Replace a call to a dynamic function at location +/// target in the given goto-program by a case-split +/// over a given set of functions +/// \param message_handler: Message handler to print warnings +/// \param symbol_table: Symbol table +/// \param goto_program: The goto program that contains target +/// \param function_id: Name of function containing the target +/// \param target: location with function call with function pointer +/// \param functions: The set of functions to consider +/// \param add_safety_assertion: Iff true, include an assertion that the +// pointer matches one of the candidate functions +void remove_function_pointer( + message_handlert &message_handler, + symbol_tablet &symbol_table, + goto_programt &goto_program, + const irep_idt &function_id, + goto_programt::targett target, + const std::unordered_set &functions, + const bool add_safety_assertion); + +/// Returns true iff \p call_type can be converted to produce a function call of +/// the same type as \p function_type. +bool function_is_type_compatible( + bool return_value_used, + const code_typet &call_type, + const code_typet &function_type, + const namespacet &ns); + #endif // CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp index 37f6a2c40d0..93de4bf8ea7 100644 --- a/src/goto-programs/restrict_function_pointers.cpp +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -18,41 +18,13 @@ Author: Diffblue Ltd. #include #include "goto_model.h" +#include "remove_function_pointers.h" #include #include namespace { -source_locationt make_function_pointer_restriction_assertion_source_location( - source_locationt source_location, - const function_pointer_restrictionst::restrictiont 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 ["; - - join_strings( - comment, restriction.second.begin(), restriction.second.end(), ", "); - - comment << ']'; - } - - source_location.set_comment(comment.str()); - source_location.set_property_class(ID_assertion); - - return source_location; -} - template void for_each_function_call(GotoFunctionT &&goto_function, Handler handler) { @@ -63,9 +35,11 @@ void for_each_function_call(GotoFunctionT &&goto_function, Handler handler) handler); } -void restrict_function_pointer( - goto_functiont &goto_function, - goto_modelt &goto_model, +static void restrict_function_pointer( + message_handlert &message_handler, + symbol_tablet &symbol_table, + goto_programt &goto_program, + const irep_idt &function_id, const function_pointer_restrictionst &restrictions, const goto_programt::targett &location) { @@ -94,53 +68,19 @@ void restrict_function_pointer( if(restriction_iterator == restrictions.restrictions.end()) return; - auto const &restriction = *restriction_iterator; - - // this is intentionally a copy because we're about to change the - // instruction this iterator points to - // if we can, we will replace uses of it by a case distinction over - // given functions the function pointer can point 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)); + const namespacet ns(symbol_table); + std::unordered_set candidates; + for(const auto &candidate : restriction_iterator->second) + candidates.insert(ns.lookup(candidate).symbol_expr()); - auto const assume_false_location = goto_function.body.insert_after( + remove_function_pointer( + message_handler, + symbol_table, + goto_program, + function_id, 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_nonconst()).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.body.insert_before(goto_end_if_location, new_instruction); - else_location = goto_function.body.insert_before( - replaced_instruction_location, - goto_programt::make_goto( - else_location, - notequal_exprt{pointer_symbol, - address_of_exprt{function_pointer_target_symbol_expr}})); - } + candidates, + true); } } // namespace @@ -204,7 +144,17 @@ void function_pointer_restrictionst::typecheck_function_pointer_restrictions( } auto const &function_pointer_target_type = function_pointer_target_sym->type; - if(function_type != function_pointer_target_type) + if(function_pointer_target_type.id() != ID_code) + { + throw invalid_restriction_exceptiont{ + "not a function: " + id2string(function_pointer_target)}; + } + + if(!function_is_type_compatible( + true, + to_code_type(function_type), + to_code_type(function_pointer_target_type), + ns)) { throw invalid_restriction_exceptiont{ "type mismatch: `" + id2string(restriction.first) + "' points to `" + @@ -217,6 +167,7 @@ void function_pointer_restrictionst::typecheck_function_pointer_restrictions( } void restrict_function_pointers( + message_handlert &message_handler, goto_modelt &goto_model, const function_pointer_restrictionst &restrictions) { @@ -225,7 +176,13 @@ void restrict_function_pointers( goto_functiont &goto_function = function_item.second; for_each_function_call(goto_function, [&](const goto_programt::targett it) { - restrict_function_pointer(goto_function, goto_model, restrictions, it); + restrict_function_pointer( + message_handler, + goto_model.symbol_table, + goto_function.body, + function_item.first, + restrictions, + it); }); } } diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h index d7ea6a262f3..5a44a96b9f6 100644 --- a/src/goto-programs/restrict_function_pointers.h +++ b/src/goto-programs/restrict_function_pointers.h @@ -156,6 +156,7 @@ class function_pointer_restrictionst /// Note: This requires label_function_pointer_call_sites to be run /// before void restrict_function_pointers( + message_handlert &message_handler, goto_modelt &goto_model, const function_pointer_restrictionst &restrictions);