diff --git a/regression/goto-instrument/restrict-function-pointer-by-name-global/test.c b/regression/goto-instrument/restrict-function-pointer-by-name-global/test.c new file mode 100644 index 00000000000..965415f75fd --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-by-name-global/test.c @@ -0,0 +1,28 @@ +int f(void) +{ + return 1; +} + +int g(void) +{ + return 2; +} + +int h(void) +{ + return 3; +} + +typedef int (*fp_t)(void); + +fp_t fp; + +void main() +{ + int cond; + fp = cond ? f : g; + int res = fp(); + __CPROVER_assert(res == 1, ""); + __CPROVER_assert(res == 2, ""); + __CPROVER_assert(res == 1 || res == 2, ""); +} 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 new file mode 100644 index 00000000000..6389bbbfbb9 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-by-name-global/test.desc @@ -0,0 +1,15 @@ +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.assertion.2\] line \d+ assertion: FAILURE +\[main.assertion.3\] line \d+ assertion: FAILURE +\[main.assertion.4\] line \d+ assertion: SUCCESS +f\(\) +g\(\) +^EXIT=10$ +^SIGNAL=0$ +-- +h\(\) +-- +Check that a call to a global function pointer is correctly restricted diff --git a/regression/goto-instrument/restrict-function-pointer-by-name-local/test.c b/regression/goto-instrument/restrict-function-pointer-by-name-local/test.c new file mode 100644 index 00000000000..8746d58b66d --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-by-name-local/test.c @@ -0,0 +1,19 @@ +#include + +int f(void) +{ + return 1; +} + +int g(void) +{ + return 2; +} + +typedef int (*fp_t)(void); + +void main() +{ + fp_t fp = f; + assert(fp() == 1); +} 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 new file mode 100644 index 00000000000..b4754a4b5f8 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-by-name-local/test.desc @@ -0,0 +1,12 @@ +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 +f\(\) +^EXIT=0$ +^SIGNAL=0$ +-- +g\(\) +-- +Check that a call to a local function pointer is correctly restricted diff --git a/regression/goto-instrument/restrict-function-pointer-by-name-parameter/test.c b/regression/goto-instrument/restrict-function-pointer-by-name-parameter/test.c new file mode 100644 index 00000000000..f58fb4e6a6b --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-by-name-parameter/test.c @@ -0,0 +1,23 @@ +#include + +int f(void) +{ + return 1; +} + +int g(void) +{ + return 2; +} + +typedef int (*fp_t)(void); + +void use_fp(fp_t fp) +{ + assert(fp() == 1); +} + +void main() +{ + use_fp(f); +} 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 new file mode 100644 index 00000000000..46f11abeb9c --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-by-name-parameter/test.desc @@ -0,0 +1,12 @@ +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 +f\(\) +^EXIT=0$ +^SIGNAL=0$ +-- +g\(\) +-- +Check that a call to a function pointer parameter is correctly restricted diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.c b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.c index 7eeb597247c..11ea6388528 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.c +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.c @@ -2,30 +2,14 @@ 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()); + fptr(1); } int f(int x) { - return x + 1; + return x; } int g(int x) @@ -35,38 +19,19 @@ int g(int x) int h(int x) { - return x - 1; -} - -int select_function = 0; - -void select_f(void) -{ - select_function = 0; + return x; } -void select_g(void) +int other(int x) { - select_function = 1; + return x; } -void select_h(void) +int main(void) { - select_function = 2; + use_f(f); + use_f(g); + use_f(h); + use_f(other); } -fptr_t get_f(void) -{ - if(select_function == 0) - { - return f; - } - else if(select_function == 1) - { - return g; - } - else - { - return h; - } -} 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 98bb04f6b6a..9346da5a265 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,13 +1,14 @@ 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 +--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 ^EXIT=10$ ^SIGNAL=0$ -- -- This test checks that the restrictions for a function pointer are the union of -the restrictions given in a file and on the command line. +the restrictions given in a file and on the command line (both with functions +pointers being numbered and named) The test further checks that the correct safety assertions are generated. The function pointer restriction feature outputs safety assertions for all calls diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index f4aefa1cbb0..ab5f92079c2 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1037,13 +1037,17 @@ void goto_instrument_parse_optionst::instrument_goto_program() { parse_function_pointer_restriction_options_from_cmdline(cmdline, options); - 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); + + const auto function_pointer_restrictions = + function_pointer_restrictionst::from_options( + options, goto_model, log.get_message_handler()); + restrict_function_pointers(goto_model, function_pointer_restrictions); } } diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp index 76b34993e89..d42362175cb 100644 --- a/src/goto-programs/restrict_function_pointers.cpp +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -20,61 +20,6 @@ Author: Diffblue Ltd. 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::restrictiont restriction) @@ -104,16 +49,17 @@ 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_instruction_if( goto_function, - [](goto_programt::targett target) { return target->is_function_call(); }, + [](targett target) { return target->is_function_call(); }, handler); } -void handle_call( +void restrict_function_pointer( goto_functiont &goto_function, goto_modelt &goto_model, const function_pointer_restrictionst &restrictions, @@ -194,18 +140,88 @@ void handle_call( } } // namespace +function_pointer_restrictionst::invalid_restriction_exceptiont:: + invalid_restriction_exceptiont(std::string reason, std::string correct_format) + : reason(std::move(reason)), correct_format(std::move(correct_format)) +{ +} + +std::string +function_pointer_restrictionst::invalid_restriction_exceptiont::what() const +{ + std::string res; + + res += "Invalid restriction"; + res += "\nReason: " + reason; + + if(!correct_format.empty()) + { + res += "\nFormat: " + correct_format; + } + + return res; +} + +void function_pointer_restrictionst::typecheck_function_pointer_restrictions( + const goto_modelt &goto_model, + const function_pointer_restrictionst::restrictionst &restrictions) +{ + for(auto const &restriction : restrictions) + { + auto const function_pointer_sym = + goto_model.symbol_table.lookup(restriction.first); + if(function_pointer_sym == nullptr) + { + throw invalid_restriction_exceptiont{id2string(restriction.first) + + " not found in the symbol table"}; + } + auto const &function_pointer_type = function_pointer_sym->type; + if(function_pointer_type.id() != ID_pointer) + { + throw invalid_restriction_exceptiont{"not a function pointer: " + + id2string(restriction.first)}; + } + auto const &function_type = + to_pointer_type(function_pointer_type).subtype(); + if(function_type.id() != ID_code) + { + throw invalid_restriction_exceptiont{"not a function pointer: " + + id2string(restriction.first)}; + } + 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_restriction_exceptiont{ + "symbol not found: " + id2string(function_pointer_target)}; + } + auto const &function_pointer_target_type = + function_pointer_target_sym->type; + if(function_type != function_pointer_target_type) + { + throw invalid_restriction_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) + "'"}; + } + } + } +} + void restrict_function_pointers( goto_modelt &goto_model, const function_pointer_restrictionst &restrictions) { - typecheck_function_pointer_restrictions(goto_model, restrictions); - for(auto &function_item : goto_model.goto_functions.function_map) { goto_functiont &goto_function = function_item.second; for_each_function_call(goto_function, [&](const goto_programt::targett it) { - handle_call(goto_function, goto_model, restrictions, it); + restrict_function_pointer(goto_function, goto_model, restrictions, it); }); } } @@ -214,12 +230,26 @@ 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)); + if(cmdline.isset(RESTRICT_FUNCTION_POINTER_OPT)) + { + options.set_option( + RESTRICT_FUNCTION_POINTER_OPT, + cmdline.get_values(RESTRICT_FUNCTION_POINTER_OPT)); + } + + if(cmdline.isset(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT)) + { + options.set_option( + RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT, + cmdline.get_values(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT)); + } + + if(cmdline.isset(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT)) + { + options.set_option( + RESTRICT_FUNCTION_POINTER_BY_NAME_OPT, + cmdline.get_values(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT)); + } } function_pointer_restrictionst::restrictionst @@ -244,9 +274,10 @@ function_pointer_restrictionst::merge_function_pointer_restrictions( return result; } -function_pointer_restrictionst::restrictionst function_pointer_restrictionst:: - parse_function_pointer_restrictions_from_command_line( - const std::list &restriction_opts) +function_pointer_restrictionst::restrictionst +function_pointer_restrictionst::parse_function_pointer_restrictions( + const std::list &restriction_opts, + const std::string &option) { auto function_pointer_restrictions = function_pointer_restrictionst::restrictionst{}; @@ -254,7 +285,7 @@ function_pointer_restrictionst::restrictionst function_pointer_restrictionst:: for(const std::string &restriction_opt : restriction_opts) { const auto restriction = - parse_function_pointer_restriction(restriction_opt); + parse_function_pointer_restriction(restriction_opt, option); const bool inserted = function_pointer_restrictions .emplace(restriction.first, restriction.second) @@ -262,26 +293,33 @@ function_pointer_restrictionst::restrictionst function_pointer_restrictionst:: if(!inserted) { - throw invalid_command_line_argument_exceptiont{ + throw invalid_restriction_exceptiont{ "function pointer restriction for `" + id2string(restriction.first) + - "' was specified twice", - "--" RESTRICT_FUNCTION_POINTER_OPT}; + "' was specified twice"}; } } return function_pointer_restrictions; } +function_pointer_restrictionst::restrictionst function_pointer_restrictionst:: + parse_function_pointer_restrictions_from_command_line( + const std::list &restriction_opts) +{ + return parse_function_pointer_restrictions( + restriction_opts, "--" RESTRICT_FUNCTION_POINTER_OPT); +} + function_pointer_restrictionst::restrictionst function_pointer_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); + auto const restrictions = read_from_file(filename, message_handler); merged_restrictions = merge_function_pointer_restrictions( std::move(merged_restrictions), restrictions.restrictions); @@ -292,7 +330,8 @@ function_pointer_restrictionst::parse_function_pointer_restrictions_from_file( function_pointer_restrictionst::restrictiont function_pointer_restrictionst::parse_function_pointer_restriction( - const std::string &restriction_opt) + const std::string &restriction_opt, + const std::string &option) { // the format for restrictions is / // exactly one pointer and at least one target @@ -303,25 +342,22 @@ function_pointer_restrictionst::parse_function_pointer_restriction( 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}; + throw invalid_restriction_exceptiont{"couldn't find '/' in `" + + restriction_opt + "'", + restriction_format_message}; } if(pointer_name_end == restriction_opt.size()) { - throw invalid_command_line_argument_exceptiont{ + throw invalid_restriction_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}; + throw invalid_restriction_exceptiont{ + "couldn't find target name before '/' in `" + restriction_opt + "'"}; } auto const pointer_name = restriction_opt.substr(0, pointer_name_end); @@ -331,9 +367,8 @@ function_pointer_restrictionst::parse_function_pointer_restriction( if(target_name_strings.size() == 1 && target_name_strings[0].empty()) { - throw invalid_command_line_argument_exceptiont{ + throw invalid_restriction_exceptiont{ "missing target list for function pointer restriction " + pointer_name, - "--" RESTRICT_FUNCTION_POINTER_OPT, restriction_format_message}; } @@ -344,9 +379,8 @@ function_pointer_restrictionst::parse_function_pointer_restriction( { if(target_name == ID_empty_string) { - throw invalid_command_line_argument_exceptiont( + throw invalid_restriction_exceptiont( "leading or trailing comma in restrictions for `" + pointer_name + "'", - "--" RESTRICT_FUNCTION_POINTER_OPT, restriction_format_message); } } @@ -354,19 +388,106 @@ function_pointer_restrictionst::parse_function_pointer_restriction( return std::make_pair(pointer_name, target_names); } +optionalt +function_pointer_restrictionst::get_by_name_restriction( + const goto_functiont &goto_function, + const function_pointer_restrictionst::restrictionst &by_name_restrictions, + const goto_programt::const_targett &location) +{ + PRECONDITION(location->is_function_call()); + + const exprt &function = location->get_function_call().function(); + + if(!can_cast_expr(function)) + return {}; + + // the function pointer is guaranteed to be a symbol expression, as the + // label_function_pointer_call_sites() pass (which must be run before the + // function pointer restriction) replaces calls via complex pointer + // expressions by calls to a function pointer variable + auto const &function_pointer_call_site = + to_symbol_expr(to_dereference_expr(function).pointer()); + + const goto_programt::const_targett it = std::prev(location); + + const code_assignt &assign = it->get_assign(); + + INVARIANT( + to_symbol_expr(assign.lhs()).get_identifier() == + function_pointer_call_site.get_identifier(), + "called function pointer must have been assigned at the previous location"); + + if(!can_cast_expr(assign.rhs())) + return {}; + + const auto &rhs = to_symbol_expr(assign.rhs()); + + const auto restriction = by_name_restrictions.find(rhs.get_identifier()); + + if(restriction != by_name_restrictions.end()) + { + return optionalt( + std::make_pair( + function_pointer_call_site.get_identifier(), restriction->second)); + } + + return {}; +} + function_pointer_restrictionst function_pointer_restrictionst::from_options( const optionst &options, + const goto_modelt &goto_model, 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); + + restrictionst commandline_restrictions; + try + { + commandline_restrictions = + parse_function_pointer_restrictions_from_command_line(restriction_opts); + typecheck_function_pointer_restrictions( + goto_model, commandline_restrictions); + } + catch(const invalid_restriction_exceptiont &e) + { + throw invalid_command_line_argument_exceptiont{ + e.reason, "--" RESTRICT_FUNCTION_POINTER_OPT, e.correct_format}; + } + + restrictionst file_restrictions; + try + { + auto const restriction_file_opts = + options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT); + file_restrictions = parse_function_pointer_restrictions_from_file( + restriction_file_opts, message_handler); + typecheck_function_pointer_restrictions(goto_model, file_restrictions); + } + catch(const invalid_restriction_exceptiont &e) + { + throw deserialization_exceptiont{e.what()}; + } + + restrictionst name_restrictions; + try + { + auto const restriction_name_opts = + options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT); + name_restrictions = get_function_pointer_by_name_restrictions( + restriction_name_opts, goto_model); + typecheck_function_pointer_restrictions(goto_model, name_restrictions); + } + catch(const invalid_restriction_exceptiont &e) + { + throw invalid_command_line_argument_exceptiont{ + e.reason, "--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT, e.correct_format}; + } + return {merge_function_pointer_restrictions( - std::move(file_restrictions), commandline_restrictions)}; + commandline_restrictions, + merge_function_pointer_restrictions(file_restrictions, name_restrictions))}; } function_pointer_restrictionst @@ -459,3 +580,30 @@ void function_pointer_restrictionst::write_to_file( function_pointer_restrictions_json.output(outFile); } + +function_pointer_restrictionst::restrictionst +function_pointer_restrictionst::get_function_pointer_by_name_restrictions( + const std::list &restriction_name_opts, + const goto_modelt &goto_model) +{ + function_pointer_restrictionst::restrictionst by_name_restrictions = + parse_function_pointer_restrictions( + restriction_name_opts, "--" 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, [&](const goto_programt::const_targett it) { + const auto restriction = get_by_name_restriction( + goto_function.second, by_name_restrictions, it); + + if(restriction) + { + restrictions.insert(*restriction); + } + }); + } + + return restrictions; +} diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h index e7681847406..bd32fceb7a4 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 HELP_RESTRICT_FUNCTION_POINTER \ "--" RESTRICT_FUNCTION_POINTER_OPT \ @@ -62,12 +66,11 @@ class function_pointer_restrictionst 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); + /// Parse function pointer restrictions from command line + static function_pointer_restrictionst from_options( + const optionst &options, + const goto_modelt &goto_model, + message_handlert &message_handler); jsont to_json() const; static function_pointer_restrictionst from_json(const jsont &json); @@ -79,19 +82,62 @@ class function_pointer_restrictionst void write_to_file(const std::string &filename) const; protected: + class invalid_restriction_exceptiont : public cprover_exception_baset + { + public: + explicit invalid_restriction_exceptiont( + std::string reason, + std::string correct_format = ""); + + std::string what() const override; + + std::string reason; + std::string correct_format; + }; + + static void typecheck_function_pointer_restrictions( + const goto_modelt &goto_model, + const restrictionst &restrictions); + static restrictionst merge_function_pointer_restrictions( restrictionst lhs, const restrictionst &rhs); - static restrictionst parse_function_pointer_restrictions_from_command_line( - const std::list &restriction_opts); - static restrictionst parse_function_pointer_restrictions_from_file( const std::list &filenames, message_handlert &message_handler); - static restrictiont - parse_function_pointer_restriction(const std::string &restriction_opt); + static restrictionst parse_function_pointer_restrictions_from_command_line( + const std::list &restriction_opts); + + static restrictionst parse_function_pointer_restrictions( + const std::list &restriction_opts, + const std::string &option); + + static restrictiont parse_function_pointer_restriction( + const std::string &restriction_opt, + const std::string &option); + + static optionalt get_by_name_restriction( + const goto_functiont &goto_function, + const function_pointer_restrictionst::restrictionst &by_name_restrictions, + const goto_programt::const_targett &location); + + /// Get function pointer restrictions from restrictions with named pointers + /// + /// This takes a list of restrictions, with each restriction consisting of a + /// function pointer name, and the list of target functions. That is, each + /// input restriction is of the form \/\(,\)*. The + /// method then returns a `restrictionst` object constructed from the given + /// list of restrictions + /// + /// \param restriction_name_opts: restrictions + /// \param goto_model: goto model with labelled function pointer calls + /// \return function pointer restrictions in the internal format that is + /// understood by other methods in this class + static restrictionst get_function_pointer_by_name_restrictions( + const std::list &restriction_name_opts, + const goto_modelt &goto_model); }; /// Apply function pointer restrictions to a goto_model. Each restriction is a diff --git a/unit/goto-programs/restrict_function_pointers.cpp b/unit/goto-programs/restrict_function_pointers.cpp index 149c04f8898..8015b3bcbd6 100644 --- a/unit/goto-programs/restrict_function_pointers.cpp +++ b/unit/goto-programs/restrict_function_pointers.cpp @@ -6,9 +6,11 @@ Author: Daniel Poetzl \*******************************************************************/ +#include #include #include +#include #include #include @@ -17,21 +19,22 @@ class fp_restrictionst : public function_pointer_restrictionst { friend void restriction_parsing_test(); friend void merge_restrictions_test(); + friend void get_function_pointer_by_name_restrictions_test(); }; void restriction_parsing_test() { { - const auto res = - fp_restrictionst::parse_function_pointer_restriction("func1/func2"); + const auto res = fp_restrictionst::parse_function_pointer_restriction( + "func1/func2", "test"); REQUIRE(res.first == "func1"); REQUIRE(res.second.size() == 1); REQUIRE(res.second.find("func2") != res.second.end()); } { - const auto res = - fp_restrictionst::parse_function_pointer_restriction("func1/func2,func3"); + const auto res = fp_restrictionst::parse_function_pointer_restriction( + "func1/func2,func3", "test"); REQUIRE(res.first == "func1"); REQUIRE(res.second.size() == 2); REQUIRE(res.second.find("func2") != res.second.end()); @@ -39,28 +42,30 @@ void restriction_parsing_test() } REQUIRE_THROWS_AS( - fp_restrictionst::parse_function_pointer_restriction("func"), - invalid_command_line_argument_exceptiont); + fp_restrictionst::parse_function_pointer_restriction("func", "test"), + fp_restrictionst::invalid_restriction_exceptiont); REQUIRE_THROWS_AS( - fp_restrictionst::parse_function_pointer_restriction("/func"), - invalid_command_line_argument_exceptiont); + fp_restrictionst::parse_function_pointer_restriction("/func", "test"), + fp_restrictionst::invalid_restriction_exceptiont); REQUIRE_THROWS_AS( - fp_restrictionst::parse_function_pointer_restriction("func/"), - invalid_command_line_argument_exceptiont); + fp_restrictionst::parse_function_pointer_restriction("func/", "test"), + fp_restrictionst::invalid_restriction_exceptiont); REQUIRE_THROWS_AS( - fp_restrictionst::parse_function_pointer_restriction("func/,"), - invalid_command_line_argument_exceptiont); + fp_restrictionst::parse_function_pointer_restriction("func/,", "test"), + fp_restrictionst::invalid_restriction_exceptiont); REQUIRE_THROWS_AS( - fp_restrictionst::parse_function_pointer_restriction("func1/func2,"), - invalid_command_line_argument_exceptiont); + fp_restrictionst::parse_function_pointer_restriction( + "func1/func2,", "test"), + fp_restrictionst::invalid_restriction_exceptiont); REQUIRE_THROWS_AS( - fp_restrictionst::parse_function_pointer_restriction("func1/,func2"), - invalid_command_line_argument_exceptiont); + fp_restrictionst::parse_function_pointer_restriction( + "func1/,func2", "test"), + fp_restrictionst::invalid_restriction_exceptiont); } void merge_restrictions_test() @@ -88,6 +93,137 @@ void merge_restrictions_test() REQUIRE(fp2_restrictions.count("func1") == 1); } +void get_function_pointer_by_name_restrictions_test() +{ + SECTION("Translate parameter restriction to indexed restriction") + { + const std::string code = R"( + typedef void (*fp_t)(void); + void f(); + + void func(fp_t fp) + { + f(); // ignored + + fp(); + } + + void main() {} + )"; + + goto_modelt goto_model = get_goto_model_from_c(code); + label_function_pointer_call_sites(goto_model); + + const auto restrictions = + fp_restrictionst::get_function_pointer_by_name_restrictions( + {"func::fp/g"}, goto_model); + + REQUIRE(restrictions.size() == 1); + + const auto set = restrictions.at("func.function_pointer_call.1"); + REQUIRE(set.size() == 1); + REQUIRE(set.count("g") == 1); + } + + SECTION("Translate local nested variable restriction to indexed restriction") + { + const std::string code = R"( + typedef void (*fp_t)(void); + void f(); + + void main() + { + f(); // ignored + + { + fp_t fp; + fp(); + } + } + )"; + + goto_modelt goto_model = get_goto_model_from_c(code); + label_function_pointer_call_sites(goto_model); + + const auto restrictions = + fp_restrictionst::get_function_pointer_by_name_restrictions( + {"main::1::1::fp/g"}, goto_model); + + REQUIRE(restrictions.size() == 1); + + const auto set = restrictions.at("main.function_pointer_call.1"); + REQUIRE(set.size() == 1); + REQUIRE(set.count("g") == 1); + } + + SECTION("Translate global variable restriction to indexed restriction") + { + const std::string code = R"( + typedef void (*fp_t)(void); + void f(); + + fp_t fp; + + void main() + { + f(); // ignored + + fp(); + } + )"; + + goto_modelt goto_model = get_goto_model_from_c(code); + label_function_pointer_call_sites(goto_model); + + const auto restrictions = + fp_restrictionst::get_function_pointer_by_name_restrictions( + {"fp/g"}, goto_model); + + REQUIRE(restrictions.size() == 1); + + const auto set = restrictions.at("main.function_pointer_call.1"); + REQUIRE(set.size() == 1); + REQUIRE(set.count("g") == 1); + } + + SECTION( + "Translate a variable restriction to indexed restrictions, " + "for the case when a function pointer is called more than once") + { + const std::string code = R"( + typedef void (*fp_t)(void); + void f(); + + fp_t fp; + + void main() + { + f(); // ignored + + fp(); + fp(); // second call to same function pointer + } + )"; + + goto_modelt goto_model = get_goto_model_from_c(code); + label_function_pointer_call_sites(goto_model); + + const auto restrictions = + fp_restrictionst::get_function_pointer_by_name_restrictions( + {"fp/g"}, goto_model); + + REQUIRE(restrictions.size() == 2); + + const auto set1 = restrictions.at("main.function_pointer_call.1"); + REQUIRE(set1.size() == 1); + REQUIRE(set1.count("g") == 1); + + const auto set2 = restrictions.at("main.function_pointer_call.2"); + REQUIRE(set2.size() == 1); + REQUIRE(set2.count("g") == 1); + } +} + TEST_CASE("Restriction parsing", "[core]") { restriction_parsing_test(); @@ -148,3 +284,10 @@ TEST_CASE("Json conversion", "[core]") function_pointer_restrictions1.restrictions == function_pointer_restrictions2.restrictions); } + +TEST_CASE( + "Get function pointer by name restrictions", + "[core][goto-programs][restrict-function-pointers]") +{ + get_function_pointer_by_name_restrictions_test(); +}