From d3f9fe76280937d158e74ef095b55784d74dc1af Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Tue, 5 Nov 2019 17:05:23 +0000 Subject: [PATCH 1/7] Add restrict-function-pointer-by-name option This works similar to restrict-function-pointer, but for names of individual function pointer variables (globals, locals, parameters) rather than call sites. This isn't applicable to all situations (for example, calling function pointers in structs or function pointers returned from functions), but is more readily applicable to some common use scenarios (e.g. global function pointers loaded at start time like in OpenGL). --- .../restrict-function-pointer-by-name/test.c | 43 ++++++++++ .../test.desc | 11 +++ .../goto_instrument_parse_options.cpp | 17 ++-- .../restrict_function_pointers.cpp | 79 +++++++++++++++++-- .../restrict_function_pointers.h | 20 ++++- 5 files changed, 154 insertions(+), 16 deletions(-) create mode 100644 regression/goto-instrument/restrict-function-pointer-by-name/test.c create mode 100644 regression/goto-instrument/restrict-function-pointer-by-name/test.desc diff --git a/regression/goto-instrument/restrict-function-pointer-by-name/test.c b/regression/goto-instrument/restrict-function-pointer-by-name/test.c new file mode 100644 index 00000000000..9bbc0bc5d1a --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-by-name/test.c @@ -0,0 +1,43 @@ +#include + +int f(void) +{ + return 1; +} +int g(void) +{ + return 2; +} +int h(void) +{ + return 3; +} + +typedef int (*fptr_t)(void); + +void use_f(fptr_t fptr) +{ + assert(fptr() == 2); +} + +int nondet_int(void); + +fptr_t g_fptr; +int main(void) +{ + int cond = nondet_int(); + if(cond) + { + g_fptr = f; + } + else + { + g_fptr = h; + } + int res = g_fptr(); + assert(res == 1 || res == 3); + use_f(g); + fptr_t fptr = f; + assert(fptr() == 1); + return 0; +} diff --git a/regression/goto-instrument/restrict-function-pointer-by-name/test.desc b/regression/goto-instrument/restrict-function-pointer-by-name/test.desc new file mode 100644 index 00000000000..22d02d0391e --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-by-name/test.desc @@ -0,0 +1,11 @@ +CORE +test.c +--restrict-function-pointer-by-name main::1::fptr/f --restrict-function-pointer-by-name use_f::fptr/g --restrict-function-pointer-by-name g_fptr/f,h +\[use_f.assertion.2\] line \d+ assertion fptr\(\) == 2: SUCCESS +\[use_f.assertion.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be g: SUCCESS +\[main.assertion.1\] line \d+ dereferenced function pointer at main.function_pointer_call.1 must be one of \[(h|f), (h|f)\]: SUCCESS +\[main.assertion.2\] line \d+ assertion res == 1 \|\| res == 3: SUCCESS +\[main.assertion.3\] line \d+ dereferenced function pointer at main.function_pointer_call.2 must be f: SUCCESS +\[main.assertion.4\] line \d+ assertion fptr\(\) == 1: 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 f4aefa1cbb0..1cae103c303 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1037,13 +1037,20 @@ 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.get_list_option(RESTRICT_FUNCTION_POINTER_OPT).empty() || + !options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT).empty() || + !options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT).empty()) { label_function_pointer_call_sites(goto_model); + + auto const by_name_restrictions = + get_function_pointer_by_name_restrictions(goto_model, options); + + const auto function_pointer_restrictions = + by_name_restrictions.merge(function_pointer_restrictionst::from_options( + options, 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..e26b3f47302 100644 --- a/src/goto-programs/restrict_function_pointers.cpp +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -104,12 +104,13 @@ 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); } @@ -220,6 +221,9 @@ void parse_function_pointer_restriction_options_from_cmdline( options.set_option( RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT, cmdline.get_values(RESTRICT_FUNCTION_POINTER_FROM_FILE_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 +248,11 @@ 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_from_command_line( + const std::list &restriction_opts, + const std::string &option_name) { auto function_pointer_restrictions = function_pointer_restrictionst::restrictionst{}; @@ -361,7 +367,8 @@ function_pointer_restrictionst function_pointer_restrictionst::from_options( 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); + parse_function_pointer_restrictions_from_command_line( + restriction_opts, RESTRICT_FUNCTION_POINTER_OPT); auto const file_restrictions = parse_function_pointer_restrictions_from_file( options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT), message_handler); @@ -459,3 +466,61 @@ void function_pointer_restrictionst::write_to_file( function_pointer_restrictions_json.output(outFile); } +function_pointer_restrictionst function_pointer_restrictionst::merge( + const function_pointer_restrictionst &other) const +{ + return function_pointer_restrictionst{ + merge_function_pointer_restrictions(restrictions, other.restrictions)}; +} + +function_pointer_restrictionst get_function_pointer_by_name_restrictions( + const goto_modelt &goto_model, + const optionst &options) +{ + function_pointer_restrictionst::restrictionst by_name_restrictions = + function_pointer_restrictionst:: + parse_function_pointer_restrictions_from_command_line( + options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT), + 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, [&](goto_programt::const_targett location) { + PRECONDITION(location->is_function_call()); + if(can_cast_expr( + location->get_function_call().function())) + { + PRECONDITION(can_cast_expr( + to_dereference_expr(location->get_function_call().function()) + .pointer())); + auto const &function_pointer_call_site = to_symbol_expr( + to_dereference_expr(location->get_function_call().function()) + .pointer()); + auto const &body = goto_function.second.body; + for(auto it = std::prev(location); it != body.instructions.end(); + ++it) + { + if( + it->is_assign() && + it->get_assign().lhs() == function_pointer_call_site && + can_cast_expr(it->get_assign().rhs())) + { + auto const &assign_rhs = to_symbol_expr(it->get_assign().rhs()); + auto const restriction = + by_name_restrictions.find(assign_rhs.get_identifier()); + if( + restriction != by_name_restrictions.end() && + restriction->first == assign_rhs.get_identifier()) + { + restrictions.emplace( + function_pointer_call_site.get_identifier(), + restriction->second); + } + } + } + } + }); + } + return function_pointer_restrictionst{restrictions}; +} diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h index e7681847406..1d22b89c279 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 \ @@ -78,14 +82,18 @@ class function_pointer_restrictionst void write_to_file(const std::string &filename) const; + function_pointer_restrictionst + merge(const function_pointer_restrictionst &other) const; + + static restrictionst parse_function_pointer_restrictions_from_command_line( + const std::list &restriction_opts, + const std::string &option_name); + protected: 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); @@ -94,6 +102,10 @@ class function_pointer_restrictionst parse_function_pointer_restriction(const std::string &restriction_opt); }; +function_pointer_restrictionst get_function_pointer_by_name_restrictions( + const goto_modelt &goto_model, + const optionst &options); + /// Apply function pointer restrictions to a goto_model. Each restriction is a /// mapping from a pointer name to a set of possible targets. Replace calls of /// these "restricted" pointers with a branch on the value of the function From 19040a49dd59a72dcbfed3d5191a6f591d17fa1d Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 16 Mar 2020 16:45:21 +0000 Subject: [PATCH 2/7] Pass command line option to parse_function_pointer_restriction() --- .../restrict_function_pointers.cpp | 15 +++++++------- .../restrict_function_pointers.h | 5 +++-- .../restrict_function_pointers.cpp | 20 +++++++++++-------- 3 files changed, 23 insertions(+), 17 deletions(-) diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp index e26b3f47302..d9ef1c6c674 100644 --- a/src/goto-programs/restrict_function_pointers.cpp +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -260,7 +260,7 @@ parse_function_pointer_restrictions_from_command_line( for(const std::string &restriction_opt : restriction_opts) { const auto restriction = - parse_function_pointer_restriction(restriction_opt); + parse_function_pointer_restriction(restriction_opt, "--" + option_name); const bool inserted = function_pointer_restrictions .emplace(restriction.first, restriction.second) @@ -298,7 +298,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 @@ -311,7 +312,7 @@ function_pointer_restrictionst::parse_function_pointer_restriction( { throw invalid_command_line_argument_exceptiont{ "couldn't find '/' in `" + restriction_opt + "'", - "--" RESTRICT_FUNCTION_POINTER_OPT, + option, restriction_format_message}; } @@ -319,7 +320,7 @@ function_pointer_restrictionst::parse_function_pointer_restriction( { throw invalid_command_line_argument_exceptiont{ "couldn't find names of targets after '/' in `" + restriction_opt + "'", - "--" RESTRICT_FUNCTION_POINTER_OPT, + option, restriction_format_message}; } @@ -327,7 +328,7 @@ function_pointer_restrictionst::parse_function_pointer_restriction( { throw invalid_command_line_argument_exceptiont{ "couldn't find target name before '/' in `" + restriction_opt + "'", - "--" RESTRICT_FUNCTION_POINTER_OPT}; + option}; } auto const pointer_name = restriction_opt.substr(0, pointer_name_end); @@ -339,7 +340,7 @@ function_pointer_restrictionst::parse_function_pointer_restriction( { throw invalid_command_line_argument_exceptiont{ "missing target list for function pointer restriction " + pointer_name, - "--" RESTRICT_FUNCTION_POINTER_OPT, + option, restriction_format_message}; } @@ -352,7 +353,7 @@ function_pointer_restrictionst::parse_function_pointer_restriction( { throw invalid_command_line_argument_exceptiont( "leading or trailing comma in restrictions for `" + pointer_name + "'", - "--" RESTRICT_FUNCTION_POINTER_OPT, + option, restriction_format_message); } } diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h index 1d22b89c279..2a15deba497 100644 --- a/src/goto-programs/restrict_function_pointers.h +++ b/src/goto-programs/restrict_function_pointers.h @@ -98,8 +98,9 @@ class function_pointer_restrictionst const std::list &filenames, message_handlert &message_handler); - static restrictiont - parse_function_pointer_restriction(const std::string &restriction_opt); + static restrictiont parse_function_pointer_restriction( + const std::string &restriction_opt, + const std::string &option); }; function_pointer_restrictionst get_function_pointer_by_name_restrictions( diff --git a/unit/goto-programs/restrict_function_pointers.cpp b/unit/goto-programs/restrict_function_pointers.cpp index 149c04f8898..e400e999d66 100644 --- a/unit/goto-programs/restrict_function_pointers.cpp +++ b/unit/goto-programs/restrict_function_pointers.cpp @@ -23,7 +23,8 @@ void restriction_parsing_test() { { const auto res = - fp_restrictionst::parse_function_pointer_restriction("func1/func2"); + 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()); @@ -31,7 +32,8 @@ void restriction_parsing_test() { const auto res = - fp_restrictionst::parse_function_pointer_restriction("func1/func2,func3"); + 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,27 +41,29 @@ void restriction_parsing_test() } REQUIRE_THROWS_AS( - fp_restrictionst::parse_function_pointer_restriction("func"), + fp_restrictionst::parse_function_pointer_restriction("func", "test"), invalid_command_line_argument_exceptiont); REQUIRE_THROWS_AS( - fp_restrictionst::parse_function_pointer_restriction("/func"), + fp_restrictionst::parse_function_pointer_restriction("/func", "test"), invalid_command_line_argument_exceptiont); REQUIRE_THROWS_AS( - fp_restrictionst::parse_function_pointer_restriction("func/"), + fp_restrictionst::parse_function_pointer_restriction("func/", "test"), invalid_command_line_argument_exceptiont); REQUIRE_THROWS_AS( - fp_restrictionst::parse_function_pointer_restriction("func/,"), + fp_restrictionst::parse_function_pointer_restriction("func/,", "test"), invalid_command_line_argument_exceptiont); REQUIRE_THROWS_AS( - fp_restrictionst::parse_function_pointer_restriction("func1/func2,"), + fp_restrictionst::parse_function_pointer_restriction( + "func1/func2,", "test"), invalid_command_line_argument_exceptiont); REQUIRE_THROWS_AS( - fp_restrictionst::parse_function_pointer_restriction("func1/,func2"), + fp_restrictionst::parse_function_pointer_restriction( + "func1/,func2", "test"), invalid_command_line_argument_exceptiont); } From 84054d5a5f701de00718107c92df3dd4d1a5f9da Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 16 Mar 2020 17:02:50 +0000 Subject: [PATCH 3/7] Refactorings and cleanups for the restrict function pointer by name feature --- .../goto_instrument_parse_options.cpp | 13 +- .../restrict_function_pointers.cpp | 196 +++++++++++------- .../restrict_function_pointers.h | 45 ++-- 3 files changed, 153 insertions(+), 101 deletions(-) diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 1cae103c303..ab5f92079c2 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1038,18 +1038,15 @@ void goto_instrument_parse_optionst::instrument_goto_program() parse_function_pointer_restriction_options_from_cmdline(cmdline, options); if( - !options.get_list_option(RESTRICT_FUNCTION_POINTER_OPT).empty() || - !options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT).empty() || - !options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT).empty()) + 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); - auto const by_name_restrictions = - get_function_pointer_by_name_restrictions(goto_model, options); - const auto function_pointer_restrictions = - by_name_restrictions.merge(function_pointer_restrictionst::from_options( - options, log.get_message_handler())); + 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 d9ef1c6c674..078f6dc9577 100644 --- a/src/goto-programs/restrict_function_pointers.cpp +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -24,6 +24,11 @@ void typecheck_function_pointer_restrictions( const goto_modelt &goto_model, const function_pointer_restrictionst &restrictions) { + const std::string options = + "--" RESTRICT_FUNCTION_POINTER_OPT "/" + "--" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT "/" + "--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT; + for(auto const &restriction : restrictions.restrictions) { auto const function_pointer_sym = @@ -32,14 +37,14 @@ void typecheck_function_pointer_restrictions( { throw invalid_command_line_argument_exceptiont{ id2string(restriction.first) + " not found in the symbol table", - "--restrict-function-pointer"}; + options}; } 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"}; + options}; } auto const &function_type = to_pointer_type(function_pointer_type).subtype(); @@ -47,7 +52,7 @@ void typecheck_function_pointer_restrictions( { throw invalid_command_line_argument_exceptiont{ "not a function pointer: " + id2string(restriction.first), - "--restrict-function-pointer"}; + options}; } auto const &ns = namespacet{goto_model.symbol_table}; for(auto const &function_pointer_target : restriction.second) @@ -58,7 +63,7 @@ void typecheck_function_pointer_restrictions( { throw invalid_command_line_argument_exceptiont{ "symbol not found: " + id2string(function_pointer_target), - "--restrict-function-pointer"}; + options}; } auto const &function_pointer_target_type = function_pointer_target_sym->type; @@ -69,7 +74,7 @@ void typecheck_function_pointer_restrictions( type2c(function_type, ns) + "', but restriction `" + id2string(function_pointer_target) + "' has type `" + type2c(function_pointer_target_type, ns) + "'", - "--restrict-function-pointer"}; + options}; } } } @@ -114,7 +119,7 @@ void for_each_function_call(GotoFunctionT &&goto_function, Handler handler) handler); } -void handle_call( +void restrict_function_pointer( goto_functiont &goto_function, goto_modelt &goto_model, const function_pointer_restrictionst &restrictions, @@ -193,6 +198,51 @@ void handle_call( address_of_exprt{function_pointer_target_symbol_expr}})); } } + +void get_by_name_restriction( + const goto_functiont &goto_function, + const function_pointer_restrictionst::restrictionst &by_name_restrictions, + function_pointer_restrictionst::restrictionst &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; + + auto const &function_pointer_call_site = to_symbol_expr( + to_dereference_expr(function) + .pointer()); + + for(auto it = std::prev(location); + it != goto_function.body.instructions.end(); + ++it) + { + if(!it->is_assign()) + continue; + + if(it->get_assign().lhs() != function_pointer_call_site) + continue; + + if(!can_cast_expr(it->get_assign().rhs())) + continue; + + auto const &rhs = to_symbol_expr(it->get_assign().rhs()); + auto const restriction = + by_name_restrictions.find(rhs.get_identifier()); + + if( + restriction != by_name_restrictions.end() && + restriction->first == rhs.get_identifier()) + { + restrictions.emplace( + function_pointer_call_site.get_identifier(), + restriction->second); + } + } +} } // namespace void restrict_function_pointers( @@ -206,7 +256,7 @@ void restrict_function_pointers( 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); }); } } @@ -215,15 +265,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)); - options.set_option( - RESTRICT_FUNCTION_POINTER_BY_NAME_OPT, - cmdline.get_values(RESTRICT_FUNCTION_POINTER_BY_NAME_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 @@ -249,10 +310,9 @@ function_pointer_restrictionst::merge_function_pointer_restrictions( } function_pointer_restrictionst::restrictionst -function_pointer_restrictionst:: -parse_function_pointer_restrictions_from_command_line( +function_pointer_restrictionst::parse_function_pointer_restrictions( const std::list &restriction_opts, - const std::string &option_name) + const std::string &option) { auto function_pointer_restrictions = function_pointer_restrictionst::restrictionst{}; @@ -260,7 +320,7 @@ parse_function_pointer_restrictions_from_command_line( for(const std::string &restriction_opt : restriction_opts) { const auto restriction = - parse_function_pointer_restriction(restriction_opt, "--" + option_name); + parse_function_pointer_restriction(restriction_opt, option); const bool inserted = function_pointer_restrictions .emplace(restriction.first, restriction.second) @@ -271,23 +331,33 @@ parse_function_pointer_restrictions_from_command_line( throw invalid_command_line_argument_exceptiont{ "function pointer restriction for `" + id2string(restriction.first) + "' was specified twice", - "--" RESTRICT_FUNCTION_POINTER_OPT}; + option}; } } 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); @@ -363,18 +433,27 @@ function_pointer_restrictionst::parse_function_pointer_restriction( 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, RESTRICT_FUNCTION_POINTER_OPT); + parse_function_pointer_restrictions_from_command_line(restriction_opts); + + auto const restriction_file_opts = + options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT); auto const file_restrictions = parse_function_pointer_restrictions_from_file( - options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT), - message_handler); + restriction_file_opts, message_handler); + + auto const restriction_name_opts = + options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT); + auto const name_restrictions = get_function_pointer_by_name_restrictions( + restriction_name_opts, goto_model); + return {merge_function_pointer_restrictions( - std::move(file_restrictions), commandline_restrictions)}; + commandline_restrictions, + merge_function_pointer_restrictions(file_restrictions, name_restrictions))}; } function_pointer_restrictionst @@ -467,61 +546,26 @@ void function_pointer_restrictionst::write_to_file( function_pointer_restrictions_json.output(outFile); } -function_pointer_restrictionst function_pointer_restrictionst::merge( - const function_pointer_restrictionst &other) const -{ - return function_pointer_restrictionst{ - merge_function_pointer_restrictions(restrictions, other.restrictions)}; -} -function_pointer_restrictionst get_function_pointer_by_name_restrictions( - const goto_modelt &goto_model, - const optionst &options) +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 = - function_pointer_restrictionst:: - parse_function_pointer_restrictions_from_command_line( - options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT), - RESTRICT_FUNCTION_POINTER_BY_NAME_OPT); + 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, [&](goto_programt::const_targett location) { - PRECONDITION(location->is_function_call()); - if(can_cast_expr( - location->get_function_call().function())) - { - PRECONDITION(can_cast_expr( - to_dereference_expr(location->get_function_call().function()) - .pointer())); - auto const &function_pointer_call_site = to_symbol_expr( - to_dereference_expr(location->get_function_call().function()) - .pointer()); - auto const &body = goto_function.second.body; - for(auto it = std::prev(location); it != body.instructions.end(); - ++it) - { - if( - it->is_assign() && - it->get_assign().lhs() == function_pointer_call_site && - can_cast_expr(it->get_assign().rhs())) - { - auto const &assign_rhs = to_symbol_expr(it->get_assign().rhs()); - auto const restriction = - by_name_restrictions.find(assign_rhs.get_identifier()); - if( - restriction != by_name_restrictions.end() && - restriction->first == assign_rhs.get_identifier()) - { - restrictions.emplace( - function_pointer_call_site.get_identifier(), - restriction->second); - } - } - } - } + goto_function.second, + [&](const goto_programt::const_targett it) { + get_by_name_restriction( + goto_function.second, by_name_restrictions, restrictions, it); }); } - return function_pointer_restrictionst{restrictions}; + + return restrictions; } diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h index 2a15deba497..48ce0294946 100644 --- a/src/goto-programs/restrict_function_pointers.h +++ b/src/goto-programs/restrict_function_pointers.h @@ -66,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); @@ -82,13 +81,6 @@ class function_pointer_restrictionst void write_to_file(const std::string &filename) const; - function_pointer_restrictionst - merge(const function_pointer_restrictionst &other) const; - - static restrictionst parse_function_pointer_restrictions_from_command_line( - const std::list &restriction_opts, - const std::string &option_name); - protected: static restrictionst merge_function_pointer_restrictions( restrictionst lhs, @@ -98,14 +90,33 @@ class function_pointer_restrictionst const std::list &filenames, message_handlert &message_handler); + 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); -}; -function_pointer_restrictionst get_function_pointer_by_name_restrictions( - const goto_modelt &goto_model, - const optionst &options); + /// 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 /// mapping from a pointer name to a set of possible targets. Replace calls of From 0e659f9bf2f12b9c4f8454b1ff0846e9c8e065d0 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 17 Mar 2020 13:58:06 +0000 Subject: [PATCH 4/7] Update restrict function pointer by name regression tests --- .../test.c | 28 ++++++++++ .../test.desc | 15 +++++ .../test.c | 19 +++++++ .../test.desc | 12 ++++ .../test.c | 23 ++++++++ .../test.desc | 12 ++++ .../restrict-function-pointer-by-name/test.c | 43 --------------- .../test.desc | 11 ---- .../test.c | 55 ++++--------------- .../test.desc | 7 ++- 10 files changed, 123 insertions(+), 102 deletions(-) create mode 100644 regression/goto-instrument/restrict-function-pointer-by-name-global/test.c create mode 100644 regression/goto-instrument/restrict-function-pointer-by-name-global/test.desc create mode 100644 regression/goto-instrument/restrict-function-pointer-by-name-local/test.c create mode 100644 regression/goto-instrument/restrict-function-pointer-by-name-local/test.desc create mode 100644 regression/goto-instrument/restrict-function-pointer-by-name-parameter/test.c create mode 100644 regression/goto-instrument/restrict-function-pointer-by-name-parameter/test.desc delete mode 100644 regression/goto-instrument/restrict-function-pointer-by-name/test.c delete mode 100644 regression/goto-instrument/restrict-function-pointer-by-name/test.desc 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-by-name/test.c b/regression/goto-instrument/restrict-function-pointer-by-name/test.c deleted file mode 100644 index 9bbc0bc5d1a..00000000000 --- a/regression/goto-instrument/restrict-function-pointer-by-name/test.c +++ /dev/null @@ -1,43 +0,0 @@ -#include - -int f(void) -{ - return 1; -} -int g(void) -{ - return 2; -} -int h(void) -{ - return 3; -} - -typedef int (*fptr_t)(void); - -void use_f(fptr_t fptr) -{ - assert(fptr() == 2); -} - -int nondet_int(void); - -fptr_t g_fptr; -int main(void) -{ - int cond = nondet_int(); - if(cond) - { - g_fptr = f; - } - else - { - g_fptr = h; - } - int res = g_fptr(); - assert(res == 1 || res == 3); - use_f(g); - fptr_t fptr = f; - assert(fptr() == 1); - return 0; -} diff --git a/regression/goto-instrument/restrict-function-pointer-by-name/test.desc b/regression/goto-instrument/restrict-function-pointer-by-name/test.desc deleted file mode 100644 index 22d02d0391e..00000000000 --- a/regression/goto-instrument/restrict-function-pointer-by-name/test.desc +++ /dev/null @@ -1,11 +0,0 @@ -CORE -test.c ---restrict-function-pointer-by-name main::1::fptr/f --restrict-function-pointer-by-name use_f::fptr/g --restrict-function-pointer-by-name g_fptr/f,h -\[use_f.assertion.2\] line \d+ assertion fptr\(\) == 2: SUCCESS -\[use_f.assertion.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be g: SUCCESS -\[main.assertion.1\] line \d+ dereferenced function pointer at main.function_pointer_call.1 must be one of \[(h|f), (h|f)\]: SUCCESS -\[main.assertion.2\] line \d+ assertion res == 1 \|\| res == 3: SUCCESS -\[main.assertion.3\] line \d+ dereferenced function pointer at main.function_pointer_call.2 must be f: SUCCESS -\[main.assertion.4\] line \d+ assertion fptr\(\) == 1: SUCCESS -^EXIT=0$ -^SIGNAL=0$ 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 From 07447109a512bfb59a765662e6595e908a4e7978 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 18 Mar 2020 19:03:05 +0000 Subject: [PATCH 5/7] Add unit tests for the restrict function pointers by name feature --- .../restrict_function_pointers.cpp | 151 +++++++++++++++++- 1 file changed, 145 insertions(+), 6 deletions(-) diff --git a/unit/goto-programs/restrict_function_pointers.cpp b/unit/goto-programs/restrict_function_pointers.cpp index e400e999d66..9ff3fc25683 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,23 +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", "test"); + 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", "test"); + 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()); @@ -92,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(); @@ -152,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(); +} From 9917b20c9f75fd1843501c4941319e9d1b4da3fc Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 23 Mar 2020 13:09:30 +0000 Subject: [PATCH 6/7] Refactor get_by_name_restriction() - remove unnecessary loop - make it return the restriction instead of inserting it into the map --- .../restrict_function_pointers.cpp | 100 ++++++++++-------- .../restrict_function_pointers.h | 5 + 2 files changed, 58 insertions(+), 47 deletions(-) diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp index 078f6dc9577..3c375d8e7e9 100644 --- a/src/goto-programs/restrict_function_pointers.cpp +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -198,51 +198,6 @@ void restrict_function_pointer( address_of_exprt{function_pointer_target_symbol_expr}})); } } - -void get_by_name_restriction( - const goto_functiont &goto_function, - const function_pointer_restrictionst::restrictionst &by_name_restrictions, - function_pointer_restrictionst::restrictionst &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; - - auto const &function_pointer_call_site = to_symbol_expr( - to_dereference_expr(function) - .pointer()); - - for(auto it = std::prev(location); - it != goto_function.body.instructions.end(); - ++it) - { - if(!it->is_assign()) - continue; - - if(it->get_assign().lhs() != function_pointer_call_site) - continue; - - if(!can_cast_expr(it->get_assign().rhs())) - continue; - - auto const &rhs = to_symbol_expr(it->get_assign().rhs()); - auto const restriction = - by_name_restrictions.find(rhs.get_identifier()); - - if( - restriction != by_name_restrictions.end() && - restriction->first == rhs.get_identifier()) - { - restrictions.emplace( - function_pointer_call_site.get_identifier(), - restriction->second); - } - } -} } // namespace void restrict_function_pointers( @@ -431,6 +386,52 @@ 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, @@ -562,8 +563,13 @@ function_pointer_restrictionst::get_function_pointer_by_name_restrictions( for_each_function_call( goto_function.second, [&](const goto_programt::const_targett it) { - get_by_name_restriction( - goto_function.second, by_name_restrictions, restrictions, it); + const auto restriction = get_by_name_restriction( + goto_function.second, by_name_restrictions, it); + + if(restriction) + { + restrictions.insert(*restriction); + } }); } diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h index 48ce0294946..b5556afa941 100644 --- a/src/goto-programs/restrict_function_pointers.h +++ b/src/goto-programs/restrict_function_pointers.h @@ -101,6 +101,11 @@ class function_pointer_restrictionst 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 From 8154f236dda8f7f218229d39f971e78aee09a858 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 23 Mar 2020 14:16:24 +0000 Subject: [PATCH 7/7] Refactor error handling of function pointer restriction --- .../restrict_function_pointers.cpp | 226 ++++++++++-------- .../restrict_function_pointers.h | 17 ++ .../restrict_function_pointers.cpp | 12 +- 3 files changed, 152 insertions(+), 103 deletions(-) diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp index 3c375d8e7e9..d42362175cb 100644 --- a/src/goto-programs/restrict_function_pointers.cpp +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -20,66 +20,6 @@ Author: Diffblue Ltd. namespace { -void typecheck_function_pointer_restrictions( - const goto_modelt &goto_model, - const function_pointer_restrictionst &restrictions) -{ - const std::string options = - "--" RESTRICT_FUNCTION_POINTER_OPT "/" - "--" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT "/" - "--" RESTRICT_FUNCTION_POINTER_BY_NAME_OPT; - - 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", - options}; - } - 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), - options}; - } - 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), - options}; - } - 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), - options}; - } - 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) + "'", - options}; - } - } - } -} - source_locationt make_function_pointer_restriction_assertion_source_location( source_locationt source_location, const function_pointer_restrictionst::restrictiont restriction) @@ -200,12 +140,82 @@ void restrict_function_pointer( } } // 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; @@ -283,24 +293,21 @@ function_pointer_restrictionst::parse_function_pointer_restrictions( if(!inserted) { - throw invalid_command_line_argument_exceptiont{ + throw invalid_restriction_exceptiont{ "function pointer restriction for `" + id2string(restriction.first) + - "' was specified twice", - option}; + "' 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) +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); + restriction_opts, "--" RESTRICT_FUNCTION_POINTER_OPT); } function_pointer_restrictionst::restrictionst @@ -335,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 + "'", - option, - 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 + "'", - option, restriction_format_message}; } if(pointer_name_end == 0) { - throw invalid_command_line_argument_exceptiont{ - "couldn't find target name before '/' in `" + restriction_opt + "'", - option}; + throw invalid_restriction_exceptiont{ + "couldn't find target name before '/' in `" + restriction_opt + "'"}; } auto const pointer_name = restriction_opt.substr(0, pointer_name_end); @@ -363,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, - option, restriction_format_message}; } @@ -376,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 + "'", - option, restriction_format_message); } } @@ -426,7 +428,7 @@ function_pointer_restrictionst::get_by_name_restriction( { return optionalt( std::make_pair( - function_pointer_call_site.get_identifier(), restriction->second)); + function_pointer_call_site.get_identifier(), restriction->second)); } return {}; @@ -439,18 +441,49 @@ function_pointer_restrictionst function_pointer_restrictionst::from_options( { 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 restriction_file_opts = - options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT); - auto const file_restrictions = parse_function_pointer_restrictions_from_file( - restriction_file_opts, 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()}; + } - auto const restriction_name_opts = - options.get_list_option(RESTRICT_FUNCTION_POINTER_BY_NAME_OPT); - auto const name_restrictions = get_function_pointer_by_name_restrictions( - restriction_name_opts, goto_model); + 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( commandline_restrictions, @@ -561,8 +594,7 @@ function_pointer_restrictionst::get_function_pointer_by_name_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) { + goto_function.second, [&](const goto_programt::const_targett it) { const auto restriction = get_by_name_restriction( goto_function.second, by_name_restrictions, it); diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h index b5556afa941..bd32fceb7a4 100644 --- a/src/goto-programs/restrict_function_pointers.h +++ b/src/goto-programs/restrict_function_pointers.h @@ -82,6 +82,23 @@ 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); diff --git a/unit/goto-programs/restrict_function_pointers.cpp b/unit/goto-programs/restrict_function_pointers.cpp index 9ff3fc25683..8015b3bcbd6 100644 --- a/unit/goto-programs/restrict_function_pointers.cpp +++ b/unit/goto-programs/restrict_function_pointers.cpp @@ -43,29 +43,29 @@ void restriction_parsing_test() REQUIRE_THROWS_AS( fp_restrictionst::parse_function_pointer_restriction("func", "test"), - invalid_command_line_argument_exceptiont); + fp_restrictionst::invalid_restriction_exceptiont); REQUIRE_THROWS_AS( fp_restrictionst::parse_function_pointer_restriction("/func", "test"), - invalid_command_line_argument_exceptiont); + fp_restrictionst::invalid_restriction_exceptiont); REQUIRE_THROWS_AS( fp_restrictionst::parse_function_pointer_restriction("func/", "test"), - invalid_command_line_argument_exceptiont); + fp_restrictionst::invalid_restriction_exceptiont); REQUIRE_THROWS_AS( fp_restrictionst::parse_function_pointer_restriction("func/,", "test"), - invalid_command_line_argument_exceptiont); + fp_restrictionst::invalid_restriction_exceptiont); REQUIRE_THROWS_AS( fp_restrictionst::parse_function_pointer_restriction( "func1/func2,", "test"), - invalid_command_line_argument_exceptiont); + fp_restrictionst::invalid_restriction_exceptiont); REQUIRE_THROWS_AS( fp_restrictionst::parse_function_pointer_restriction( "func1/,func2", "test"), - invalid_command_line_argument_exceptiont); + fp_restrictionst::invalid_restriction_exceptiont); } void merge_restrictions_test()