From 86b5e6c40d622e733a72d15396ecba70c2a9ad17 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 10 Mar 2020 18:42:30 +0000 Subject: [PATCH 01/18] Introduce get_goto_model_from_c() for use in unit tests The function takes a C program (as a string or an input stream) and converts it to a goto model. --- jbmc/lib/java-models-library | 2 +- unit/Makefile | 1 + unit/get_goto_model_from_c_test.cpp | 40 +++++++++ unit/json_symbol_table.cpp | 61 +------------ unit/testing-utils/Makefile | 1 + unit/testing-utils/get_goto_model_from_c.cpp | 95 ++++++++++++++++++++ unit/testing-utils/get_goto_model_from_c.h | 28 ++++++ unit/testing-utils/module_dependencies.txt | 6 +- 8 files changed, 173 insertions(+), 61 deletions(-) create mode 100644 unit/get_goto_model_from_c_test.cpp create mode 100644 unit/testing-utils/get_goto_model_from_c.cpp create mode 100644 unit/testing-utils/get_goto_model_from_c.h diff --git a/jbmc/lib/java-models-library b/jbmc/lib/java-models-library index 31df88c0bba..242aaff32da 160000 --- a/jbmc/lib/java-models-library +++ b/jbmc/lib/java-models-library @@ -1 +1 @@ -Subproject commit 31df88c0bba7fa5f9c4eeb53a79f8902246f386a +Subproject commit 242aaff32dae81d98bc23479f43640ff03bcd1c6 diff --git a/unit/Makefile b/unit/Makefile index 4f44e33f5ae..876c14b36e1 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -23,6 +23,7 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/last_written_location.cpp \ big-int/big-int.cpp \ compound_block_locations.cpp \ + get_goto_model_from_c_test.cpp \ goto-instrument/cover/cover_only.cpp \ goto-instrument/cover_instrument.cpp \ goto-programs/goto_model_function_type_consistency.cpp \ diff --git a/unit/get_goto_model_from_c_test.cpp b/unit/get_goto_model_from_c_test.cpp new file mode 100644 index 00000000000..1b6f278716e --- /dev/null +++ b/unit/get_goto_model_from_c_test.cpp @@ -0,0 +1,40 @@ +/*******************************************************************\ + +Module: Get goto model test + +Author: Daniel Poetzl + +\*******************************************************************/ + +#include +#include + +TEST_CASE("Get goto model from C test", "[core]") +{ + const std::string code = + "int g;" + "void f(int a) { int b; }" + "void main() {}"; + + const auto goto_model = get_goto_model_from_c(code); + + const auto &function_map = goto_model.goto_functions.function_map; + + REQUIRE(function_map.find("main") != function_map.end()); + REQUIRE(function_map.find(CPROVER_PREFIX "_start") != function_map.end()); + REQUIRE(function_map.find("f") != function_map.end()); + + const auto &main_instructions = function_map.at("main").body.instructions; + REQUIRE(!main_instructions.empty()); + + const auto &f_instructions = function_map.at("f").body.instructions; + REQUIRE(f_instructions.size() >= 2); + + const auto &symbol_table = goto_model.symbol_table; + + REQUIRE(symbol_table.has_symbol("main")); + REQUIRE(symbol_table.has_symbol(CPROVER_PREFIX "_start")); + REQUIRE(symbol_table.has_symbol("g")); + REQUIRE(symbol_table.has_symbol("f::a")); + REQUIRE(symbol_table.has_symbol("f::1::b")); +} diff --git a/unit/json_symbol_table.cpp b/unit/json_symbol_table.cpp index 9a475304323..e35a7e41191 100644 --- a/unit/json_symbol_table.cpp +++ b/unit/json_symbol_table.cpp @@ -23,6 +23,7 @@ #include #include +#include #include #include @@ -49,67 +50,11 @@ class test_ui_message_handlert : public ui_message_handlert json_stream_arrayt json_stream_array; }; -void get_goto_model(std::istream &in, goto_modelt &goto_model) -{ - optionst options; - cbmc_parse_optionst::set_default_options(options); - - messaget null_message(null_message_handler); - - language_filest language_files; - language_files.set_message_handler(null_message_handler); - - std::string filename; - - language_filet &language_file = language_files.add_file(filename); - - language_file.language = get_default_language(); - - languaget &language = *language_file.language; - language.set_message_handler(null_message_handler); - language.set_language_options(options); - - { - bool r = language.parse(in, filename); - REQUIRE(!r); - } - - language_file.get_modules(); - - { - bool r = language_files.typecheck(goto_model.symbol_table); - REQUIRE(!r); - } - - REQUIRE(!goto_model.symbol_table.has_symbol(goto_functionst::entry_point())); - - { - bool r = language_files.generate_support_functions(goto_model.symbol_table); - REQUIRE(!r); - } - - goto_convert( - goto_model.symbol_table, goto_model.goto_functions, null_message_handler); -} - TEST_CASE("json symbol table read/write consistency") { - register_language(new_ansi_c_language); - - cmdlinet cmdline; - config.main = std::string("main"); - config.set(cmdline); - - goto_modelt goto_model; - // Get symbol table associated with goto program - - { - std::string program = "int main() { return 0; }\n"; - - std::istringstream in(program); - get_goto_model(in, goto_model); - } + const std::string program = "int main() { return 0; }\n"; + const auto goto_model = get_goto_model_from_c(program); const symbol_tablet &symbol_table1 = goto_model.symbol_table; diff --git a/unit/testing-utils/Makefile b/unit/testing-utils/Makefile index 72a7f547f0b..df3ef1b5cca 100644 --- a/unit/testing-utils/Makefile +++ b/unit/testing-utils/Makefile @@ -1,6 +1,7 @@ SRC = \ call_graph_test_utils.cpp \ free_form_cmdline.cpp \ + get_goto_model_from_c.cpp \ invariant.cpp \ message.cpp \ require_expr.cpp \ diff --git a/unit/testing-utils/get_goto_model_from_c.cpp b/unit/testing-utils/get_goto_model_from_c.cpp new file mode 100644 index 00000000000..d48c8967f10 --- /dev/null +++ b/unit/testing-utils/get_goto_model_from_c.cpp @@ -0,0 +1,95 @@ +/*******************************************************************\ + +Module: Get goto model + +Author: Daniel Poetzl + +\*******************************************************************/ + +#include "get_goto_model_from_c.h" + +#include + +#include + +#include +#include + +#include +#include +#include +#include +#include +#include +#include + +#include + +goto_modelt get_goto_model_from_c(std::istream &in) +{ + { + const bool has_language = get_language_from_mode(ID_C) != nullptr; + + if(!has_language) + { + register_language(new_ansi_c_language); + } + } + + { + cmdlinet cmdline; + + config = configt{}; + config.main = std::string("main"); + config.set(cmdline); + } + + language_filest language_files; + language_files.set_message_handler(null_message_handler); + + language_filet &language_file = language_files.add_file(""); + + language_file.language = get_language_from_mode(ID_C); + CHECK_RETURN(language_file.language); + + languaget &language = *language_file.language; + language.set_message_handler(null_message_handler); + + { + const bool error = language.parse(in, ""); + + if(error) + throw invalid_source_file_exceptiont("parsing failed"); + } + + language_file.get_modules(); + + goto_modelt goto_model; + + { + const bool error = language_files.typecheck(goto_model.symbol_table); + + if(error) + throw invalid_source_file_exceptiont("typechecking failed"); + } + + { + const bool error = + language_files.generate_support_functions(goto_model.symbol_table); + + if(error) + throw invalid_source_file_exceptiont( + "support function generation failed"); + } + + goto_convert( + goto_model.symbol_table, goto_model.goto_functions, null_message_handler); + + return goto_model; +} + +goto_modelt get_goto_model_from_c(const std::string &code) +{ + std::istringstream in(code); + return get_goto_model_from_c(in); +} diff --git a/unit/testing-utils/get_goto_model_from_c.h b/unit/testing-utils/get_goto_model_from_c.h new file mode 100644 index 00000000000..8b5c3d54057 --- /dev/null +++ b/unit/testing-utils/get_goto_model_from_c.h @@ -0,0 +1,28 @@ +/*******************************************************************\ + +Module: Get goto model + +Author: Daniel Poetzl + +\*******************************************************************/ + +#ifndef CPROVER_TESTING_UTILS_GET_GOTO_MODEL_FROM_C_H +#define CPROVER_TESTING_UTILS_GET_GOTO_MODEL_FROM_C_H + +#include + +#include + +/// Convert C program to a goto model +/// +/// \param code: string giving the C program +/// \return goto model +goto_modelt get_goto_model_from_c(const std::string &code); + +/// Convert C program to a goto model +/// +/// \param in: input stream to read a C program from +/// \return goto model +goto_modelt get_goto_model_from_c(const std::istream &in); + +#endif /* CPROVER_TESTING_UTILS_GET_GOTO_MODEL_FROM_C_H_ */ diff --git a/unit/testing-utils/module_dependencies.txt b/unit/testing-utils/module_dependencies.txt index 636163352dd..eeed80f6cc0 100644 --- a/unit/testing-utils/module_dependencies.txt +++ b/unit/testing-utils/module_dependencies.txt @@ -1,5 +1,7 @@ +analyses ansi-c catch +goto-programs +langapi testing-utils -util -analyses +util \ No newline at end of file From 7fa04c09f8dbbfb2236895b28c1443ce9212a95e Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Fri, 25 Oct 2019 18:37:03 +0100 Subject: [PATCH 02/18] Label function pointer call sites --- src/goto-programs/Makefile | 1 + src/goto-programs/goto_program.h | 24 ++++++++ .../label_function_pointer_call_sites.cpp | 56 +++++++++++++++++++ .../label_function_pointer_call_sites.h | 29 ++++++++++ 4 files changed, 110 insertions(+) create mode 100644 src/goto-programs/label_function_pointer_call_sites.cpp create mode 100644 src/goto-programs/label_function_pointer_call_sites.h diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 9a542a722e2..5fc90a6ce92 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -30,6 +30,7 @@ SRC = adjust_float_expressions.cpp \ json_expr.cpp \ json_goto_trace.cpp \ lazy_goto_model.cpp \ + label_function_pointer_call_sites.cpp \ link_goto_model.cpp \ link_to_library.cpp \ loop_ids.cpp \ diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 0192b0c8cbf..06d1a09935f 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -1169,6 +1169,30 @@ struct pointee_address_equalt } }; +template +void for_each_goto_location_if( + GotoFunctionT &&goto_function, + PredicateT predicate, + HandlerT handle) +{ + auto &&instructions = goto_function.body.instructions; + for(auto it = instructions.begin(); it != instructions.end(); ++it) + { + if(predicate(it)) + { + handle(it); + } + } +} + +template +void for_each_goto_location(GotoFunctionT &&goto_function, HandlerT handle) +{ + using iterator_t = decltype(goto_function.body.instructions.begin()); + for_each_goto_location_if( + goto_function, [](const iterator_t &) { return true; }, handle); +} + #define forall_goto_program_instructions(it, program) \ for(goto_programt::instructionst::const_iterator \ it=(program).instructions.begin(); \ diff --git a/src/goto-programs/label_function_pointer_call_sites.cpp b/src/goto-programs/label_function_pointer_call_sites.cpp new file mode 100644 index 00000000000..6a4a1e51e48 --- /dev/null +++ b/src/goto-programs/label_function_pointer_call_sites.cpp @@ -0,0 +1,56 @@ +/*******************************************************************\ +Module: Label function pointer call sites +Author: Diffblue Ltd. +\*******************************************************************/ + +/// \file +/// Label function pointer call sites across a goto model + +#include "label_function_pointer_call_sites.h" + +#include + +void label_function_pointer_call_sites(goto_modelt &goto_model) +{ + for(auto &goto_function : goto_model.goto_functions.function_map) + { + std::size_t function_pointer_call_counter = 0; + for_each_goto_location_if( + goto_function.second, + [](const goto_programt::targett it) { + return it->is_function_call() && can_cast_expr( + it->get_function_call().function()); + }, + [&](goto_programt::targett it) { + auto const &function_call = it->get_function_call(); + auto const &function_pointer_dereference = + to_dereference_expr(function_call.function()); + auto const &source_location = function_call.source_location(); + auto const &goto_function_symbol_mode = + goto_model.symbol_table.lookup_ref(goto_function.first).mode; + auto const new_symbol_name = + irep_idt{id2string(goto_function.first) + ".function_pointer_call." + + std::to_string(++function_pointer_call_counter)}; + goto_model.symbol_table.insert([&] { + symbolt function_call_site_symbol{}; + function_call_site_symbol.name = function_call_site_symbol.base_name = + function_call_site_symbol.pretty_name = new_symbol_name; + function_call_site_symbol.type = + function_pointer_dereference.pointer().type(); + function_call_site_symbol.location = function_call.source_location(); + function_call_site_symbol.is_lvalue = true; + function_call_site_symbol.mode = goto_function_symbol_mode; + return function_call_site_symbol; + }()); + auto const new_function_pointer = + goto_model.symbol_table.lookup_ref(new_symbol_name).symbol_expr(); + auto const assign_instruction = goto_programt::make_assignment( + code_assignt{new_function_pointer, + function_pointer_dereference.pointer()}, + source_location); + goto_function.second.body.insert_before(it, assign_instruction); + to_code_function_call(it->code).function() = + dereference_exprt{new_function_pointer}; + }); + } +} diff --git a/src/goto-programs/label_function_pointer_call_sites.h b/src/goto-programs/label_function_pointer_call_sites.h new file mode 100644 index 00000000000..a756b1ff6c0 --- /dev/null +++ b/src/goto-programs/label_function_pointer_call_sites.h @@ -0,0 +1,29 @@ +/*******************************************************************\ +Module: Label function pointer call sites +Author: Diffblue Ltd. +\*******************************************************************/ + +/// \file +/// Label function pointer call sites across a goto model +/// \see simplify_function_pointers + +#ifndef CPROVER_GOTO_PROGRAMS_LABEL_FUNCTION_POINTER_CALL_SITES_H +#define CPROVER_GOTO_PROGRAMS_LABEL_FUNCTION_POINTER_CALL_SITES_H + +#include "goto_model.h" + +/// This ensures that call instructions can be only one of two things: +/// +/// 1. A "normal" function call to a concrete function +/// 2. A dereference of a symbol expression of a function pointer type +/// +/// This makes following stages dealing with function calls easier, because they +/// only need to be able to handle these two cases. +/// +/// It does this by replacing all CALL instructions to function pointers with an +/// assignment to a function pointer variable with a name following the pattern +/// [function_name].function_pointer_call.[N], where "N" is the nth call to a +/// function pointer in the function "function_name". +void label_function_pointer_call_sites(goto_modelt &goto_model); + +#endif // CPROVER_GOTO_PROGRAMS_LABEL_FUNCTION_POINTER_CALL_SITES_H From a1347500ed6265ecf52e736bade38794a33ad106 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Fri, 25 Oct 2019 18:37:03 +0100 Subject: [PATCH 03/18] Add function pointer restriction feature This adds a new option, --restrict-function-pointer, to goto-instrument. This lets a user specify a list of possible pointer targets for specific function pointer call sites, rather than have remove_function_pointers guess possible values. The intended purpose behind this is to prevent excessive symex time wasted on exploring paths the user knows the program can never actually take. --- .../goto_instrument_parse_options.cpp | 17 + .../goto_instrument_parse_options.h | 2 + src/goto-programs/Makefile | 1 + .../restrict_function_pointers.cpp | 415 ++++++++++++++++++ .../restrict_function_pointers.h | 87 ++++ src/util/irep.h | 5 + 6 files changed, 527 insertions(+) create mode 100644 src/goto-programs/restrict_function_pointers.cpp create mode 100644 src/goto-programs/restrict_function_pointers.h diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 32553f320c5..43f1c76e81b 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -28,6 +28,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -38,6 +39,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -1032,6 +1034,20 @@ void goto_instrument_parse_optionst::instrument_goto_program() options.set_option("unwind", cmdline.get_value("unwind")); } + { + 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()) + { + label_function_pointer_call_sites(goto_model); + restrict_function_pointers(goto_model, function_pointer_restrictions); + } + } + // skip over selected loops if(cmdline.isset("skip-loops")) { @@ -1765,6 +1781,7 @@ void goto_instrument_parse_optionst::help() " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*) " --log log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*) " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*) + RESTRICT_FUNCTION_POINTER_HELP HELP_REMOVE_CALLS_NO_BODY HELP_REMOVE_CONST_FUNCTION_POINTERS " --add-library add models of C library functions\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h index 964cc045ff1..df69c2ed6b1 100644 --- a/src/goto-instrument/goto_instrument_parse_options.h +++ b/src/goto-instrument/goto_instrument_parse_options.h @@ -24,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -112,6 +113,7 @@ Author: Daniel Kroening, kroening@kroening.com "(validate-goto-binary)" \ OPT_VALIDATE \ OPT_ANSI_C_LANGUAGE \ + OPT_RESTRICT_FUNCTION_POINTER \ "(ensure-one-backedge-per-target)" \ // empty last line diff --git a/src/goto-programs/Makefile b/src/goto-programs/Makefile index 5fc90a6ce92..6eada85fa90 100644 --- a/src/goto-programs/Makefile +++ b/src/goto-programs/Makefile @@ -53,6 +53,7 @@ SRC = adjust_float_expressions.cpp \ remove_unused_functions.cpp \ remove_vector.cpp \ remove_virtual_functions.cpp \ + restrict_function_pointers.cpp \ rewrite_union.cpp \ replace_calls.cpp \ resolve_inherited_component.cpp \ diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp new file mode 100644 index 00000000000..749de44897a --- /dev/null +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -0,0 +1,415 @@ +/*******************************************************************\ + +Module: GOTO Program Utilities + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include "restrict_function_pointers.h" + +#include +#include +#include +#include + +#include +#include +#include + +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::value_type restriction) +{ + std::stringstream comment; + comment << "dereferenced function pointer at " << restriction.first + << " must be "; + if(restriction.second.size() == 1) + { + comment << *restriction.second.begin(); + } + else + { + comment << "one of ["; + bool first = true; + for(auto const &target : restriction.second) + { + if(!first) + { + comment << ", "; + } + else + { + first = false; + } + comment << target; + } + comment << ']'; + } + source_location.set_comment(string2id(comment.str())); + source_location.set_property_class(ID_assertion); + return source_location; +} + +template +void for_each_function_call(goto_functiont &goto_function, Handler handler) +{ + for_each_goto_location_if( + goto_function, + [](goto_programt::targett target) { return target->is_function_call(); }, + handler); +} +} // namespace + +void restrict_function_pointers( + goto_modelt &goto_model, + const function_pointer_restrictionst &restrictions) +{ + typecheck_function_pointer_restrictions(goto_model, restrictions); + + for(auto &goto_function : goto_model.goto_functions.function_map) + { + auto &goto_function_body = goto_function.second.body; + // for each function call, we check if it is using a symbol we have + // restrictions for, and if so branch on its value and insert concrete calls + // to the restriction functions + for_each_function_call( + goto_function.second, [&](const goto_programt::targett location) { + // Check if this is calling a function pointer, and if so if it is one + // we have a restriction for + const auto &original_function_call = location->get_function_call(); + if(can_cast_expr(original_function_call.function())) + { + // because we simplify before this stage a dereference can only + // dereference a symbol expression + auto const &called_function_pointer = + to_dereference_expr(original_function_call.function()).pointer(); + PRECONDITION(can_cast_expr(called_function_pointer)); + auto const &pointer_symbol = to_symbol_expr(called_function_pointer); + auto const restriction_iterator = + restrictions.restrictions.find(pointer_symbol.get_identifier()); + if(restriction_iterator != restrictions.restrictions.end()) + { + auto const &restriction = *restriction_iterator; + // if we can, we will replace uses of it by the + // this is intentionally a copy because we're just about to change + // the instruction this iterator points to + auto const original_function_call_instruction = *location; + *location = goto_programt::make_assertion( + false_exprt{}, + make_function_pointer_restriction_assertion_source_location( + original_function_call_instruction.source_location, + restriction)); + auto const assume_false_location = goto_function_body.insert_after( + location, + goto_programt::make_assumption( + false_exprt{}, + original_function_call_instruction.source_location)); + // this is mutable because we'll update this at the end of each + // loop iteration to always point at the start of the branch + // we created + auto else_location = location; + auto const end_if_location = goto_function_body.insert_after( + assume_false_location, goto_programt::make_skip()); + for(auto const &restriction_target : restriction.second) + { + auto new_instruction = original_function_call_instruction; + // can't use get_function_call because that'll return a const ref + const symbol_exprt &function_pointer_target_symbol_expr = + goto_model.symbol_table.lookup_ref(restriction_target) + .symbol_expr(); + to_code_function_call(new_instruction.code).function() = + function_pointer_target_symbol_expr; + auto const goto_end_if_location = + goto_function_body.insert_before( + else_location, + goto_programt::make_goto( + end_if_location, + original_function_call_instruction.source_location)); + auto const replaced_instruction_location = + goto_function.second.body.insert_before( + goto_end_if_location, new_instruction); + else_location = goto_function.second.body.insert_before( + replaced_instruction_location, + goto_programt::make_goto( + else_location, + notequal_exprt{ + pointer_symbol, + address_of_exprt{function_pointer_target_symbol_expr}})); + } + } + } + }); + } +} + +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)); +} + +namespace +{ +function_pointer_restrictionst::restrictionst +merge_function_pointer_restrictions( + const function_pointer_restrictionst::restrictionst &lhs, + const function_pointer_restrictionst::restrictionst &rhs) +{ + auto result = lhs; + for(auto const &restriction : rhs) + { + auto emplace_result = result.emplace(restriction.first, restriction.second); + if(!emplace_result.second) + { + for(auto const &target : restriction.second) + { + emplace_result.first->second.insert(target); + } + } + } + return result; +} + +function_pointer_restrictionst::restrictionst +parse_function_pointer_restrictions_from_command_line( + const std::list &restriction_opts) +{ + auto function_pointer_restrictions = + function_pointer_restrictionst::restrictionst{}; + for(auto const &restriction_opt : restriction_opts) + { + // the format for restrictions is / + // exactly one pointer and at least one target + auto const pointer_name_end = restriction_opt.find('/'); + auto const restriction_format_message = + "the format for restrictions is " + "/"; + 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}; + } + if(pointer_name_end == restriction_opt.size()) + { + throw invalid_command_line_argument_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}; + } + auto const pointer_name = restriction_opt.substr(0, pointer_name_end); + auto const target_names_substring = + restriction_opt.substr(pointer_name_end + 1); + auto const target_name_strings = split_string(target_names_substring, ','); + if(target_name_strings.size() == 1 && target_name_strings[0].empty()) + { + throw invalid_command_line_argument_exceptiont{ + "missing target list for function pointer restriction " + pointer_name, + "--" RESTRICT_FUNCTION_POINTER_OPT, + restriction_format_message}; + } + auto const target_names = ([&target_name_strings] { + auto target_names = std::unordered_set{}; + std::transform( + target_name_strings.begin(), + target_name_strings.end(), + std::inserter(target_names, target_names.end()), + string2id); + return target_names; + })(); + for(auto const &target_name : target_names) + { + if(target_name == ID_empty_string) + { + throw invalid_command_line_argument_exceptiont( + "leading or trailing comma in restrictions for `" + pointer_name + + "'", + "--" RESTRICT_FUNCTION_POINTER_OPT, + restriction_format_message); + } + } + if(!function_pointer_restrictions + .emplace(irep_idt{pointer_name}, target_names) + .second) + { + throw invalid_command_line_argument_exceptiont{ + "function pointer restriction for `" + pointer_name + + "' was specified twice", + "--" RESTRICT_FUNCTION_POINTER_OPT}; + }; + } + return function_pointer_restrictions; +} + +function_pointer_restrictionst::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); + merged_restrictions = merge_function_pointer_restrictions( + merged_restrictions, restrictions.restrictions); + } + return merged_restrictions; +} +} // namespace + +function_pointer_restrictionst function_pointer_restrictionst::from_options( + const optionst &options, + 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); + return {merge_function_pointer_restrictions( + file_restrictions, commandline_restrictions)}; +} + +function_pointer_restrictionst function_pointer_restrictionst::read_from_file( + const std::string &filename, + message_handlert &message_handler) +{ + auto failed = [](bool failFlag) { return failFlag; }; + function_pointer_restrictionst::restrictionst restrictions; + auto inFile = std::ifstream{filename}; + jsont json; + if(failed(parse_json(inFile, filename, message_handler, json))) + { + throw system_exceptiont{ + "failed to read function pointer restrictions from " + filename}; + } + if(!json.is_object()) + { + throw system_exceptiont{"top level item is not an object"}; + } + for(auto const &kv_pair : to_json_object(json)) + { + restrictions.emplace(irep_idt{kv_pair.first}, [&] { + if(!kv_pair.second.is_array()) + { + throw system_exceptiont{"In " + filename + ", value of " + + kv_pair.first + " is not an array"}; + } + auto possible_targets = std::unordered_set{}; + auto const &array = to_json_array(kv_pair.second); + std::transform( + array.begin(), + array.end(), + std::inserter(possible_targets, possible_targets.end()), + [&](const jsont &array_element) { + if(!array_element.is_string()) + { + throw system_exceptiont{"In " + filename + ", value of " + + kv_pair.first + + "contains a non-string array element"}; + } + return irep_idt{to_json_string(array_element).value}; + }); + return possible_targets; + }()); + } + return function_pointer_restrictionst{restrictions}; +} + +void function_pointer_restrictionst::write_to_file( + const std::string &filename) const +{ + auto function_pointer_restrictions_json = jsont{}; + auto &restrictions_json_object = + function_pointer_restrictions_json.make_object(); + for(auto const &restriction : restrictions) + { + auto &targets_array = + restrictions_json_object[id2string(restriction.first)].make_array(); + for(auto const &target : restriction.second) + { + targets_array.push_back(json_stringt{target}); + } + } + auto outFile = std::ofstream{filename}; + if(!outFile) + { + throw system_exceptiont{"cannot open " + filename + + " for writing function pointer restrictions"}; + } + function_pointer_restrictions_json.output(outFile); +} diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h new file mode 100644 index 00000000000..f7e51d88a34 --- /dev/null +++ b/src/goto-programs/restrict_function_pointers.h @@ -0,0 +1,87 @@ +/*******************************************************************\ + +Module: GOTO Program Utilities + +Author: Diffblue Ltd. + +\*******************************************************************/ + +/// \file +/// Given goto functions and a list of function parameters or globals +/// that are function pointers with lists of possible candidates, replace use of +/// these function pointers with calls to the candidate. +/// The purpose here is to avoid unnecessary branching +/// i.e. "there are 600 functions with this signature, but I know it's +/// always going to be one of these two" + +#ifndef CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H +#define CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H + +#include +#include + +#include +#include + +#include +#include + +#define RESTRICT_FUNCTION_POINTER_OPT "restrict-function-pointer" +#define RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \ + "function-pointer-restrictions-file" + +#define OPT_RESTRICT_FUNCTION_POINTER \ + "(" RESTRICT_FUNCTION_POINTER_OPT \ + "):" \ + "(" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT "):" + +#define RESTRICT_FUNCTION_POINTER_HELP \ + "--" RESTRICT_FUNCTION_POINTER_OPT \ + " /\n" \ + " restrict a function pointer to a set of possible targets\n" \ + " targets must all exist in the symbol table with a matching " \ + "type\n" \ + " works for globals and function parameters right now\n" \ + "--" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \ + " \n" \ + " add from function pointer restrictions from file" + +void parse_function_pointer_restriction_options_from_cmdline( + const cmdlinet &cmdline, + optionst &options); + +class message_handlert; +struct function_pointer_restrictionst +{ + using restrictionst = + std::unordered_map>; + using value_type = restrictionst::value_type; + 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); + + static function_pointer_restrictionst read_from_file( + const std::string &filename, + message_handlert &message_handler); + + void write_to_file(const std::string &filename) const; +}; + +/// Apply a 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 +/// pointer, comparing it to the set of possible targets. This also adds an +/// assertion that the pointer actually has one of the listed values. +/// +/// Note: This requires label_function_pointer_call_sites to be run +/// before +void restrict_function_pointers( + goto_modelt &goto_model, + const function_pointer_restrictionst &restrictions); + +#endif // CPROVER_GOTO_PROGRAMS_RESTRICT_FUNCTION_POINTERS_H diff --git a/src/util/irep.h b/src/util/irep.h index 2e2dacf91c0..0613d1f717c 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -50,6 +50,11 @@ inline const std::string &id2string(const irep_idt &d) #endif } +inline irep_idt string2id(const std::string &id_string) +{ + return irep_idt{id_string}; +} + inline const std::string &name2string(const irep_namet &n) { #ifdef USE_DSTRING From bd52d356f68896d32fabd258f854d8b563a74754 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 13 Mar 2020 12:33:41 +0000 Subject: [PATCH 04/18] Add unit tests for label function pointer call sites --- unit/Makefile | 1 + .../label_function_pointer_call_sites.cpp | 88 +++++++++++++++++++ 2 files changed, 89 insertions(+) create mode 100644 unit/goto-programs/label_function_pointer_call_sites.cpp diff --git a/unit/Makefile b/unit/Makefile index 876c14b36e1..a6d16f1281a 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -37,6 +37,7 @@ SRC += analyses/ai/ai.cpp \ goto-programs/goto_program_validate.cpp \ goto-programs/goto_trace_output.cpp \ goto-programs/is_goto_binary.cpp \ + goto-programs/label_function_pointer_call_sites.cpp \ goto-programs/osx_fat_reader.cpp \ goto-programs/remove_returns.cpp \ goto-programs/xml_expr.cpp \ diff --git a/unit/goto-programs/label_function_pointer_call_sites.cpp b/unit/goto-programs/label_function_pointer_call_sites.cpp new file mode 100644 index 00000000000..4fd17144fb2 --- /dev/null +++ b/unit/goto-programs/label_function_pointer_call_sites.cpp @@ -0,0 +1,88 @@ +/*******************************************************************\ + +Module: Label function pointer call sites unit tests + +Author: Daniel Poetzl + +\*******************************************************************/ + +#include +#include + +#include + +TEST_CASE("Label function pointer call sites", "[core]") +{ + const std::string code = R"( + void f() {} + void g() {} + + void h() + { + f(); + void (*fp)() = f; + fp(); + (1 ? f : g)(); + } + + void main() { h(); } + )"; + + goto_modelt goto_model = get_goto_model_from_c(code); + + label_function_pointer_call_sites(goto_model); + + auto &h = goto_model.goto_functions.function_map.at("h"); + + for_each_instruction_if( + h, + [](goto_programt::const_targett it) { return it->is_function_call(); }, + [](goto_programt::const_targett it) { + static int call_count = 0; + + switch (call_count) + { + case 0: + // first call instruction + REQUIRE(it->get_function_call().function().id() == ID_symbol); + break; + case 1: + { + // second call instruction + const auto &fp_symbol = + to_symbol_expr( + to_dereference_expr(it->get_function_call().function()).pointer()) + .get_identifier(); + REQUIRE(fp_symbol == "h.function_pointer_call.1"); + break; + } + case 2: + { + // third call instruction + const auto &fp_symbol = + to_symbol_expr( + to_dereference_expr(it->get_function_call().function()).pointer()) + .get_identifier(); + REQUIRE(fp_symbol == "h.function_pointer_call.2"); + + auto it_prev = std::prev(it); + const auto &assign = it_prev->get_assign(); + + const auto &lhs = assign.lhs(); + const auto &rhs = assign.rhs(); + + REQUIRE( + to_symbol_expr(lhs).get_identifier() == "h.function_pointer_call.2"); + + REQUIRE(rhs.id() == ID_if); + + break; + } + default: + break; + } + + call_count++; + } + ); +} From 4799bb5ae0dc72f9215ab4a61632ba965a2223a1 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Fri, 25 Oct 2019 18:37:03 +0100 Subject: [PATCH 05/18] Add function pointer restriction regression tests --- .../test.c | 59 ++++++++++++++++ .../test.desc | 7 ++ .../test.json | 3 + .../test.c | 66 ++++++++++++++++++ .../test.desc | 9 +++ .../test.c | 68 +++++++++++++++++++ .../test.desc | 6 ++ .../restrictions.json | 3 + .../test.c | 68 +++++++++++++++++++ .../test.desc | 6 ++ .../restrictions.json | 3 + .../test.c | 68 +++++++++++++++++++ .../test.desc | 6 ++ .../restrictions_1.json | 3 + .../restrictions_2.json | 3 + .../test.c | 68 +++++++++++++++++++ .../test.desc | 6 ++ .../test.c | 66 ++++++++++++++++++ .../test.desc | 6 ++ .../test.c | 39 +++++++++++ .../test.desc | 8 +++ .../test.c | 39 +++++++++++ .../test.desc | 6 ++ .../test.c | 40 +++++++++++ .../test.desc | 6 ++ 25 files changed, 662 insertions(+) create mode 100644 regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.c create mode 100644 regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc create mode 100644 regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.json create mode 100644 regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.c create mode 100644 regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.desc create mode 100644 regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.c create mode 100644 regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc create mode 100644 regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/restrictions.json create mode 100644 regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.c create mode 100644 regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc create mode 100644 regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/restrictions.json create mode 100644 regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.c create mode 100644 regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.desc create mode 100644 regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/restrictions_1.json create mode 100644 regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/restrictions_2.json create mode 100644 regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.c create mode 100644 regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc create mode 100644 regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.c create mode 100644 regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.desc create mode 100644 regression/goto-instrument/restrict-function-pointer-to-single-function-code-check/test.c create mode 100644 regression/goto-instrument/restrict-function-pointer-to-single-function-code-check/test.desc create mode 100644 regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.c create mode 100644 regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.desc create mode 100644 regression/goto-instrument/restrict-function-pointer-to-single-function/test.c create mode 100644 regression/goto-instrument/restrict-function-pointer-to-single-function/test.desc diff --git a/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.c b/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.c new file mode 100644 index 00000000000..3787afa1df6 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.c @@ -0,0 +1,59 @@ +#include + +typedef int (*fptr_t)(int); + +fptr_t get_f(void); +fptr_t get_g(void); + +void use_fg(int choice, fptr_t fptr, fptr_t gptr) +{ + assert((choice ? fptr : gptr)(10) == 10 + choice); +} + +// this is just here to distinguish the behavior from FP removal, which'd include g +int g_always_false_cond = 0; + +int main(void) +{ + use_fg(0, get_f(), get_g()); + use_fg(1, get_f(), get_g()); +} + +int f(int x) +{ + return x + 1; +} + +int g(int x) +{ + return x; +} + +int h(int x) +{ + return x / 2; +} + +fptr_t get_f(void) +{ + if(!g_always_false_cond) + { + return f; + } + else + { + return h; + } +} + +fptr_t get_g(void) +{ + if(!g_always_false_cond) + { + return g; + } + else + { + return h; + } +} diff --git a/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc b/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc new file mode 100644 index 00000000000..03c2e782be9 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc @@ -0,0 +1,7 @@ +CORE +test.c +--restrict-function-pointer "use_fg.function_pointer_call.1/f,g" +\[use_fg.assertion.2\] line \d+ assertion \(choice \? fptr : gptr\)\(10\) == 10 \+ choice: SUCCESS +\[use_fg.assertion.1\] line \d+ dereferenced function pointer at use_fg.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: SUCCESS +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.json b/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.json new file mode 100644 index 00000000000..90f8c5c7cae --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.json @@ -0,0 +1,3 @@ +{ + "use_fg.function_pointer_call.1": ["f"] +} diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.c b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.c new file mode 100644 index 00000000000..eb28bb15684 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.c @@ -0,0 +1,66 @@ +#include + +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()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} +int h(int x) +{ + return x - 1; +} + +int g_select_function = 0; + +void select_f(void) +{ + g_select_function = 0; +} +void select_g(void) +{ + g_select_function = 1; +} +void select_h(void) +{ + g_select_function = 2; +} + +fptr_t get_f(void) +{ + if(g_select_function == 0) + { + return f; + } + else if(g_select_function == 1) + { + return g; + } + else + { + return h; + } +} diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.desc new file mode 100644 index 00000000000..05803cc488c --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.desc @@ -0,0 +1,9 @@ +CORE +test.c +--restrict-function-pointer use_f.function_pointer_call.1/f,g --show-goto-functions +f\(10\) +g\(10\) +^EXIT=0$ +^SIGNAL=0$ +-- +h\(10\) diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.c b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.c new file mode 100644 index 00000000000..ac36b749862 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.c @@ -0,0 +1,68 @@ +#include + +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()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} +int h(int x) +{ + return x - 1; +} + +int g_select_function = 0; + +void select_f(void) +{ + g_select_function = 0; +} +void select_g(void) +{ + g_select_function = 1; +} +void select_h(void) +{ + g_select_function = 2; +} + +fptr_t get_f(void) +{ + if(g_select_function == 0) + { + return f; + } + else if(g_select_function == 1) + { + return g; + } + else + { + return h; + } +} diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc new file mode 100644 index 00000000000..bf6ec38059f --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc @@ -0,0 +1,6 @@ +CORE +test.c +--restrict-function-pointer use_f.function_pointer_call.1/f,g +\[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/restrictions.json b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/restrictions.json new file mode 100644 index 00000000000..e9a374713bf --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/restrictions.json @@ -0,0 +1,3 @@ +{ + "use_f.function_pointer_call.1": ["f"] +} 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 new file mode 100644 index 00000000000..ac36b749862 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.c @@ -0,0 +1,68 @@ +#include + +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()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} +int h(int x) +{ + return x - 1; +} + +int g_select_function = 0; + +void select_f(void) +{ + g_select_function = 0; +} +void select_g(void) +{ + g_select_function = 1; +} +void select_h(void) +{ + g_select_function = 2; +} + +fptr_t get_f(void) +{ + if(g_select_function == 0) + { + return f; + } + else if(g_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 new file mode 100644 index 00000000000..e3a5c3b50c1 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file-and-command-line-options/test.desc @@ -0,0 +1,6 @@ +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 +^EXIT=10$ +^SIGNAL=0$ diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/restrictions.json b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/restrictions.json new file mode 100644 index 00000000000..9538cc31654 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/restrictions.json @@ -0,0 +1,3 @@ +{ + "use_f.function_pointer_call.1": ["f", "g"] +} diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.c b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.c new file mode 100644 index 00000000000..ac36b749862 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.c @@ -0,0 +1,68 @@ +#include + +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()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} +int h(int x) +{ + return x - 1; +} + +int g_select_function = 0; + +void select_f(void) +{ + g_select_function = 0; +} +void select_g(void) +{ + g_select_function = 1; +} +void select_h(void) +{ + g_select_function = 2; +} + +fptr_t get_f(void) +{ + if(g_select_function == 0) + { + return f; + } + else if(g_select_function == 1) + { + return g; + } + else + { + return h; + } +} diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.desc new file mode 100644 index 00000000000..5c9b3816a99 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.desc @@ -0,0 +1,6 @@ +CORE +test.c +--function-pointer-restrictions-file restrictions.json +\[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/restrictions_1.json b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/restrictions_1.json new file mode 100644 index 00000000000..e9a374713bf --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/restrictions_1.json @@ -0,0 +1,3 @@ +{ + "use_f.function_pointer_call.1": ["f"] +} diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/restrictions_2.json b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/restrictions_2.json new file mode 100644 index 00000000000..a0c410ebec7 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/restrictions_2.json @@ -0,0 +1,3 @@ +{ + "use_f.function_pointer_call.1": ["g"] +} diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.c b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.c new file mode 100644 index 00000000000..ac36b749862 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.c @@ -0,0 +1,68 @@ +#include + +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()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} +int h(int x) +{ + return x - 1; +} + +int g_select_function = 0; + +void select_f(void) +{ + g_select_function = 0; +} +void select_g(void) +{ + g_select_function = 1; +} +void select_h(void) +{ + g_select_function = 2; +} + +fptr_t get_f(void) +{ + if(g_select_function == 0) + { + return f; + } + else if(g_select_function == 1) + { + return g; + } + else + { + return h; + } +} diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc new file mode 100644 index 00000000000..b46ff820de6 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc @@ -0,0 +1,6 @@ +CORE +test.c +--function-pointer-restrictions-file restrictions_1.json --function-pointer-restrictions-file restrictions_2.json +\[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.c b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.c new file mode 100644 index 00000000000..eb28bb15684 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.c @@ -0,0 +1,66 @@ +#include + +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()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} +int h(int x) +{ + return x - 1; +} + +int g_select_function = 0; + +void select_f(void) +{ + g_select_function = 0; +} +void select_g(void) +{ + g_select_function = 1; +} +void select_h(void) +{ + g_select_function = 2; +} + +fptr_t get_f(void) +{ + if(g_select_function == 0) + { + return f; + } + else if(g_select_function == 1) + { + return g; + } + else + { + return h; + } +} diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.desc new file mode 100644 index 00000000000..878139b431e --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.desc @@ -0,0 +1,6 @@ +CORE +test.c +--restrict-function-pointer use_f.function_pointer_call.1/f,g +\[use_f\.assertion\.2\] line \d+ assertion fptr\(10\) >= 10: SUCCESS +^EXIT=0$ +^SIGNAL=0$ diff --git a/regression/goto-instrument/restrict-function-pointer-to-single-function-code-check/test.c b/regression/goto-instrument/restrict-function-pointer-to-single-function-code-check/test.c new file mode 100644 index 00000000000..e172f39391c --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-single-function-code-check/test.c @@ -0,0 +1,39 @@ +#include + +typedef int (*fptr_t)(int); + +fptr_t get_f(void); + +void use_f(fptr_t fptr) +{ + assert(fptr(10) == 11); +} + +int main(void) +{ + use_f(get_f()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} + +// this is just here to distinguish the behavior from FP removal, which'd include g +int g_always_false_cond = 0; + +fptr_t get_f(void) +{ + if(!g_always_false_cond) + { + return f; + } + else + { + return g; + } +} diff --git a/regression/goto-instrument/restrict-function-pointer-to-single-function-code-check/test.desc b/regression/goto-instrument/restrict-function-pointer-to-single-function-code-check/test.desc new file mode 100644 index 00000000000..f462acc84c8 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-single-function-code-check/test.desc @@ -0,0 +1,8 @@ +CORE +test.c +--restrict-function-pointer use_f.function_pointer_call.1/f --show-goto-functions +f\(10\) +^EXIT=0$ +^SIGNAL=0$ +-- +g\(10\) diff --git a/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.c b/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.c new file mode 100644 index 00000000000..63370cbd1b1 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.c @@ -0,0 +1,39 @@ +#include + +typedef int (*fptr_t)(int); + +fptr_t get_f(void); + +void use_f(fptr_t fptr) +{ + assert(fptr(10) == 11); +} + +int main(void) +{ + use_f(get_f()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} + +// this is just here to distinguish the behavior from FP removal, which'd include g +int g_always_false_cond = 1; + +fptr_t get_f(void) +{ + if(!g_always_false_cond) + { + return f; + } + else + { + return g; + } +} diff --git a/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.desc b/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.desc new file mode 100644 index 00000000000..fc8b95986c3 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.desc @@ -0,0 +1,6 @@ +CORE +test.c +--restrict-function-pointer use_f.function_pointer_call.1/f +\[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be f: FAILURE +^EXIT=10$ +^SIGNAL=0$ diff --git a/regression/goto-instrument/restrict-function-pointer-to-single-function/test.c b/regression/goto-instrument/restrict-function-pointer-to-single-function/test.c new file mode 100644 index 00000000000..d82c347e8b7 --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-single-function/test.c @@ -0,0 +1,40 @@ +#include + +typedef int (*fptr_t)(int); + +fptr_t get_f(void); + +void use_f(fptr_t fptr) +{ + assert(fptr(10) == 11); +} + +int main(void) +{ + use_f(get_f()); +} + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} + +// this is just here to distinguish the behavior from FP removal, which'd include +// only f if we didn't reference g anywhere. +int g_always_false_cond = 0; + +fptr_t get_f(void) +{ + if(!g_always_false_cond) + { + return f; + } + else + { + return g; + } +} diff --git a/regression/goto-instrument/restrict-function-pointer-to-single-function/test.desc b/regression/goto-instrument/restrict-function-pointer-to-single-function/test.desc new file mode 100644 index 00000000000..13540f25cdd --- /dev/null +++ b/regression/goto-instrument/restrict-function-pointer-to-single-function/test.desc @@ -0,0 +1,6 @@ +CORE +test.c +--restrict-function-pointer use_f.function_pointer_call.1/f +\[use_f\.assertion\.2\] line \d+ assertion fptr\(10\) == 11: SUCCESS +^EXIT=0$ +^SIGNAL=0$ From a77eee803b3deecc7b368d522d06b906d0597e35 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Tue, 5 Nov 2019 15:38:19 +0000 Subject: [PATCH 06/18] Add function pointer restriction documentation --- doc/cprover-manual/index.md | 1 + .../restrict-function-pointer.md | 173 ++++++++++++++++++ 2 files changed, 174 insertions(+) create mode 100644 doc/cprover-manual/restrict-function-pointer.md diff --git a/doc/cprover-manual/index.md b/doc/cprover-manual/index.md index abd028c3b92..9be7116c2a9 100644 --- a/doc/cprover-manual/index.md +++ b/doc/cprover-manual/index.md @@ -9,6 +9,7 @@ [A Short Tutorial](cbmc/tutorial/), [Loop Unwinding](cbmc/unwinding/), [Assertion Checking](cbmc/assertions/), +[Restricting function pointers](cbmc/restrict-function-pointer/), [Memory Analyzer](cbmc/memory-analyzer/), [Program Harness](cbmc/goto-harness/) diff --git a/doc/cprover-manual/restrict-function-pointer.md b/doc/cprover-manual/restrict-function-pointer.md new file mode 100644 index 00000000000..82b5d3d126c --- /dev/null +++ b/doc/cprover-manual/restrict-function-pointer.md @@ -0,0 +1,173 @@ +[CPROVER Manual TOC](../../) + +## Restricting function pointers + +### Motivation + +CBMC comes with a way to resolve calls to function pointers to direct function +calls. This is needed because symbolic execution itself can't handle calls to +function pointers. In practice, this looks something like this: + +Given that there are functions with these signatures available in the program: + +``` +int f(int x); +int g(int x); +int h(int x); +``` + +And we have a call site like this: + +``` +typedef int(*fptr_t)(int x); +void call(fptr_t fptr) { + int r = fptr(10); + assert(r > 0); +} +``` + +Function pointer removal will turn this into code similar to this: + +``` +void call(fptr_t fptr) { + int r; + if(fptr == &f) { + r = f(10); + } else if(fptr == &g) { + r = g(10); + } else if(fptr == &h) { + r = h(10); + } else { + // sanity check + assert(false); + assume(false); + } + return r; +} +``` + +This works well enough for simple cases. However, this is a very simple +replacement only based on the signature of the function (and whether or not they +have their address taken somewhere in the program), so if there are many +functions matching a particular signature, or if some of these functions are +expensive in symex (e.g. functions with lots of loops or recursion), then this +can be a bit cumbersome - especially if we, as a user, already know that a +particular function pointer will only resolve to a single function or a small +set of functions. This is what the `--restrict-function-pointer` option allows. + +### Example + +Take the motivating example. Let us assume that we know for a fact that `call` +will always receive pointers to either `f` or `g` during actual executions of +the program, and symbolic execution for `h` is too expensive to simply ignore +the cost of its branch. For this, we will label the places in each function +where function pointers are being called, to this pattern: + +``` +.function_pointer_call. +``` + +where `N` is referring to which function call it is - so the first call to a +function pointer in a function will have `N=1`, the 5th `N=5` etc. + +We can call `cbmc` with `--restrict-function-pointer +call.function_pointer_call.1/f,g`. This can be read as + +> For the first call to a function pointer in the function `call`, assume that +> it can only be a call to `f` or `g` + +The resulting code looks similar to the original example, except now there will +not be a call to `h`: + +``` +void call(fptr_t fptr) { + int r; + if(fptr == &f) { + r = f(10); + } else if(fptr == &g) { + r = g(10); + } else { + // sanity check + assert(false); + assume(false); + } + return r; +} +``` + +Another example: Imagine we have a simple virtual filesystem API and implementation +like this: + +``` +typedef struct filesystem_t filesystem_t; +struct filesystem_t { + int (*open)(filesystem_t *filesystem, const char* file_name); +}; + +int fs_open(filesystem_t *filesystem, const char* file_name) { + filesystem->open(filesystem, file_name); +} + +int nullfs_open(filesystem_t *filesystem, const char* file_name) { + return -1; +} + +filesystem_t nullfs_val = {.open = nullfs_open}; +filesystem *const nullfs = &nullfs_val; + +filesystem_t *get_fs_impl() { + // some fancy logic to determine + // which filesystem we're getting - + // in-memory, backed by a database, OS file system + // - but in our case, we know that + // it always ends up being nullfs + // for the cases we care about + return nullfs; +} +int main(void) { + filesystem_t *fs = get_fs_impl(); + assert(fs_open(fs, "hello.txt") != -1); +} +``` + +In this case, the assumption is that *we* know that in our `main`, `fs` can be +nothing other than `nullfs`; But perhaps due to the logic being too complicated +symex ends up being unable to figure this out, so in the call to `fs_open()` we +end up branching on all functions matching the signature of +`filesystem_t::open`, which could be quite a few functions within the program. +Worst of all, if it's address is ever taken in the program, as far as the "dumb" +function pointer removal is concerned it could be `fs_open()` itself due to it +having a matching signature, leading to symex being forced to follow a +potentially infinite recursion until its unwind limit. + +In this case we can again restrict the function pointer to the value which we +know it will have: + +``` +--restrict-function-pointer fs_open.function_pointer_call.1/nullfs_open +``` + +### Loading from file + +If you have many places where you want to restrict function pointers, it'd be a +nuisance to have to specify them all on the command line. In these cases, you +can specify a file to load the restrictions from instead, via the +`--function-pointer-restrictions-file` option, which you can give the name of a +JSON file with this format: + +``` +{ + "function_call_site_name": ["function1", "function2", ...], + ... +} +``` + +**Note:** If you pass in multiple files, or a mix of files and command line +restrictions, the final restrictions will be a set union of all specified +restrictions. + +**Note:** as of now, if something goes wrong during type checking (i.e. making +sure that all function pointer replacements refer to functions in the symbol +table that have the correct type), the error message will refer the command line +option `--restrict-function-pointer` regardless of whether the restriction in +question came from the command line or a file. From 2b8556d539d533253bd16e265ec189d0616f6325 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 4 Mar 2020 15:27:48 +0000 Subject: [PATCH 07/18] Refactorings and cleanups for the function pointer restriction feature --- .../restrict-function-pointer.md | 8 +- .../goto_instrument_parse_options.cpp | 2 +- src/goto-programs/goto_program.h | 12 +- .../label_function_pointer_call_sites.cpp | 16 +- .../label_function_pointer_call_sites.h | 7 +- .../restrict_function_pointers.cpp | 420 ++++++++++-------- .../restrict_function_pointers.h | 34 +- src/util/irep.h | 5 - .../label_function_pointer_call_sites.cpp | 5 +- unit/goto-programs/module_dependencies.txt | 1 + 10 files changed, 291 insertions(+), 219 deletions(-) diff --git a/doc/cprover-manual/restrict-function-pointer.md b/doc/cprover-manual/restrict-function-pointer.md index 82b5d3d126c..c8246059e5b 100644 --- a/doc/cprover-manual/restrict-function-pointer.md +++ b/doc/cprover-manual/restrict-function-pointer.md @@ -135,7 +135,7 @@ nothing other than `nullfs`; But perhaps due to the logic being too complicated symex ends up being unable to figure this out, so in the call to `fs_open()` we end up branching on all functions matching the signature of `filesystem_t::open`, which could be quite a few functions within the program. -Worst of all, if it's address is ever taken in the program, as far as the "dumb" +Worst of all, if its address is ever taken in the program, as far as the "dumb" function pointer removal is concerned it could be `fs_open()` itself due to it having a matching signature, leading to symex being forced to follow a potentially infinite recursion until its unwind limit. @@ -168,6 +168,6 @@ restrictions. **Note:** as of now, if something goes wrong during type checking (i.e. making sure that all function pointer replacements refer to functions in the symbol -table that have the correct type), the error message will refer the command line -option `--restrict-function-pointer` regardless of whether the restriction in -question came from the command line or a file. +table that have the correct type), the error message will refer to the command +line option `--restrict-function-pointer` regardless of whether the restriction +in question came from the command line or a file. diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 43f1c76e81b..04b3d443687 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1781,7 +1781,7 @@ void goto_instrument_parse_optionst::help() " --no-caching disable caching of intermediate results during transitive function inlining\n" // NOLINT(*) " --log log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*) " --remove-function-pointers replace function pointers by case statement over function calls\n" // NOLINT(*) - RESTRICT_FUNCTION_POINTER_HELP + HELP_RESTRICT_FUNCTION_POINTER HELP_REMOVE_CALLS_NO_BODY HELP_REMOVE_CONST_FUNCTION_POINTERS " --add-library add models of C library functions\n" diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 06d1a09935f..5d518b53aac 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -1170,27 +1170,27 @@ struct pointee_address_equalt }; template -void for_each_goto_location_if( +void for_each_instruction_if( GotoFunctionT &&goto_function, PredicateT predicate, - HandlerT handle) + HandlerT handler) { auto &&instructions = goto_function.body.instructions; for(auto it = instructions.begin(); it != instructions.end(); ++it) { if(predicate(it)) { - handle(it); + handler(it); } } } template -void for_each_goto_location(GotoFunctionT &&goto_function, HandlerT handle) +void for_each_instruction(GotoFunctionT &&goto_function, HandlerT handler) { using iterator_t = decltype(goto_function.body.instructions.begin()); - for_each_goto_location_if( - goto_function, [](const iterator_t &) { return true; }, handle); + for_each_instruction_if( + goto_function, [](const iterator_t &) { return true; }, handler); } #define forall_goto_program_instructions(it, program) \ diff --git a/src/goto-programs/label_function_pointer_call_sites.cpp b/src/goto-programs/label_function_pointer_call_sites.cpp index 6a4a1e51e48..6c8a050d7e4 100644 --- a/src/goto-programs/label_function_pointer_call_sites.cpp +++ b/src/goto-programs/label_function_pointer_call_sites.cpp @@ -15,7 +15,7 @@ void label_function_pointer_call_sites(goto_modelt &goto_model) for(auto &goto_function : goto_model.goto_functions.function_map) { std::size_t function_pointer_call_counter = 0; - for_each_goto_location_if( + for_each_instruction_if( goto_function.second, [](const goto_programt::targett it) { return it->is_function_call() && can_cast_expr( @@ -28,13 +28,16 @@ void label_function_pointer_call_sites(goto_modelt &goto_model) auto const &source_location = function_call.source_location(); auto const &goto_function_symbol_mode = goto_model.symbol_table.lookup_ref(goto_function.first).mode; - auto const new_symbol_name = + + auto const call_site_symbol_name = irep_idt{id2string(goto_function.first) + ".function_pointer_call." + std::to_string(++function_pointer_call_counter)}; + + // insert new function pointer variable into the symbol table goto_model.symbol_table.insert([&] { symbolt function_call_site_symbol{}; function_call_site_symbol.name = function_call_site_symbol.base_name = - function_call_site_symbol.pretty_name = new_symbol_name; + function_call_site_symbol.pretty_name = call_site_symbol_name; function_call_site_symbol.type = function_pointer_dereference.pointer().type(); function_call_site_symbol.location = function_call.source_location(); @@ -42,8 +45,13 @@ void label_function_pointer_call_sites(goto_modelt &goto_model) function_call_site_symbol.mode = goto_function_symbol_mode; return function_call_site_symbol; }()); + auto const new_function_pointer = - goto_model.symbol_table.lookup_ref(new_symbol_name).symbol_expr(); + goto_model.symbol_table.lookup_ref(call_site_symbol_name) + .symbol_expr(); + + // add assignment to the new function pointer variable, followed by a + // call of the new variable auto const assign_instruction = goto_programt::make_assignment( code_assignt{new_function_pointer, function_pointer_dereference.pointer()}, diff --git a/src/goto-programs/label_function_pointer_call_sites.h b/src/goto-programs/label_function_pointer_call_sites.h index a756b1ff6c0..f9157df333d 100644 --- a/src/goto-programs/label_function_pointer_call_sites.h +++ b/src/goto-programs/label_function_pointer_call_sites.h @@ -21,9 +21,10 @@ Author: Diffblue Ltd. /// only need to be able to handle these two cases. /// /// It does this by replacing all CALL instructions to function pointers with an -/// assignment to a function pointer variable with a name following the pattern -/// [function_name].function_pointer_call.[N], where "N" is the nth call to a -/// function pointer in the function "function_name". +/// assignment to a new function pointer variable followed by a call to that new +/// function pointer. The name of the introduced variable follows the pattern +/// [function_name].function_pointer_call.[N], where N is the nth call to a +/// function pointer in the function function_name. void label_function_pointer_call_sites(goto_modelt &goto_model); #endif // CPROVER_GOTO_PROGRAMS_LABEL_FUNCTION_POINTER_CALL_SITES_H diff --git a/src/goto-programs/restrict_function_pointers.cpp b/src/goto-programs/restrict_function_pointers.cpp index 749de44897a..76b34993e89 100644 --- a/src/goto-programs/restrict_function_pointers.cpp +++ b/src/goto-programs/restrict_function_pointers.cpp @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: GOTO Program Utilities +Module: Restrict function pointers Author: Diffblue Ltd. @@ -15,6 +15,7 @@ Author: Diffblue Ltd. #include #include +#include #include namespace @@ -76,11 +77,13 @@ void typecheck_function_pointer_restrictions( source_locationt make_function_pointer_restriction_assertion_source_location( source_locationt source_location, - const function_pointer_restrictionst::value_type restriction) + const function_pointer_restrictionst::restrictiont restriction) { std::stringstream comment; + comment << "dereferenced function pointer at " << restriction.first << " must be "; + if(restriction.second.size() == 1) { comment << *restriction.second.begin(); @@ -88,34 +91,107 @@ source_locationt make_function_pointer_restriction_assertion_source_location( else { comment << "one of ["; - bool first = true; - for(auto const &target : restriction.second) - { - if(!first) - { - comment << ", "; - } - else - { - first = false; - } - comment << target; - } + + join_strings( + comment, restriction.second.begin(), restriction.second.end(), ", "); + comment << ']'; } - source_location.set_comment(string2id(comment.str())); + + source_location.set_comment(comment.str()); source_location.set_property_class(ID_assertion); + return source_location; } template void for_each_function_call(goto_functiont &goto_function, Handler handler) { - for_each_goto_location_if( + for_each_instruction_if( goto_function, [](goto_programt::targett target) { return target->is_function_call(); }, handler); } + +void handle_call( + goto_functiont &goto_function, + goto_modelt &goto_model, + const function_pointer_restrictionst &restrictions, + const goto_programt::targett &location) +{ + PRECONDITION(location->is_function_call()); + + // for each function call, we check if it is using a symbol we have + // restrictions for, and if so branch on its value and insert concrete calls + // to the restriction functions + + // Check if this is calling a function pointer, and if so if it is one + // we have a restriction for + const auto &original_function_call = location->get_function_call(); + + if(!can_cast_expr(original_function_call.function())) + return; + + // because we run the label function pointer calls transformation pass before + // this stage a dereference can only dereference a symbol expression + auto const &called_function_pointer = + to_dereference_expr(original_function_call.function()).pointer(); + PRECONDITION(can_cast_expr(called_function_pointer)); + auto const &pointer_symbol = to_symbol_expr(called_function_pointer); + auto const restriction_iterator = + restrictions.restrictions.find(pointer_symbol.get_identifier()); + + if(restriction_iterator == restrictions.restrictions.end()) + return; + + auto const &restriction = *restriction_iterator; + + // this is intentionally a copy because we're about to change the + // instruction this iterator points to + // if we can, we will replace uses of it by a case distinction over + // given functions the function pointer can point to + auto const original_function_call_instruction = *location; + + *location = goto_programt::make_assertion( + false_exprt{}, + make_function_pointer_restriction_assertion_source_location( + original_function_call_instruction.source_location, restriction)); + + auto const assume_false_location = goto_function.body.insert_after( + location, + goto_programt::make_assumption( + false_exprt{}, original_function_call_instruction.source_location)); + + // this is mutable because we'll update this at the end of each + // loop iteration to always point at the start of the branch + // we created + auto else_location = location; + + auto const end_if_location = goto_function.body.insert_after( + assume_false_location, goto_programt::make_skip()); + + for(auto const &restriction_target : restriction.second) + { + auto new_instruction = original_function_call_instruction; + // can't use get_function_call because that'll return a const ref + const symbol_exprt &function_pointer_target_symbol_expr = + goto_model.symbol_table.lookup_ref(restriction_target).symbol_expr(); + to_code_function_call(new_instruction.code).function() = + function_pointer_target_symbol_expr; + auto const goto_end_if_location = goto_function.body.insert_before( + else_location, + goto_programt::make_goto( + end_if_location, original_function_call_instruction.source_location)); + auto const replaced_instruction_location = + goto_function.body.insert_before(goto_end_if_location, new_instruction); + else_location = goto_function.body.insert_before( + replaced_instruction_location, + goto_programt::make_goto( + else_location, + notequal_exprt{pointer_symbol, + address_of_exprt{function_pointer_target_symbol_expr}})); + } +} } // namespace void restrict_function_pointers( @@ -124,79 +200,13 @@ void restrict_function_pointers( { typecheck_function_pointer_restrictions(goto_model, restrictions); - for(auto &goto_function : goto_model.goto_functions.function_map) + for(auto &function_item : goto_model.goto_functions.function_map) { - auto &goto_function_body = goto_function.second.body; - // for each function call, we check if it is using a symbol we have - // restrictions for, and if so branch on its value and insert concrete calls - // to the restriction functions - for_each_function_call( - goto_function.second, [&](const goto_programt::targett location) { - // Check if this is calling a function pointer, and if so if it is one - // we have a restriction for - const auto &original_function_call = location->get_function_call(); - if(can_cast_expr(original_function_call.function())) - { - // because we simplify before this stage a dereference can only - // dereference a symbol expression - auto const &called_function_pointer = - to_dereference_expr(original_function_call.function()).pointer(); - PRECONDITION(can_cast_expr(called_function_pointer)); - auto const &pointer_symbol = to_symbol_expr(called_function_pointer); - auto const restriction_iterator = - restrictions.restrictions.find(pointer_symbol.get_identifier()); - if(restriction_iterator != restrictions.restrictions.end()) - { - auto const &restriction = *restriction_iterator; - // if we can, we will replace uses of it by the - // this is intentionally a copy because we're just about to change - // the instruction this iterator points to - auto const original_function_call_instruction = *location; - *location = goto_programt::make_assertion( - false_exprt{}, - make_function_pointer_restriction_assertion_source_location( - original_function_call_instruction.source_location, - restriction)); - auto const assume_false_location = goto_function_body.insert_after( - location, - goto_programt::make_assumption( - false_exprt{}, - original_function_call_instruction.source_location)); - // this is mutable because we'll update this at the end of each - // loop iteration to always point at the start of the branch - // we created - auto else_location = location; - auto const end_if_location = goto_function_body.insert_after( - assume_false_location, goto_programt::make_skip()); - for(auto const &restriction_target : restriction.second) - { - auto new_instruction = original_function_call_instruction; - // can't use get_function_call because that'll return a const ref - const symbol_exprt &function_pointer_target_symbol_expr = - goto_model.symbol_table.lookup_ref(restriction_target) - .symbol_expr(); - to_code_function_call(new_instruction.code).function() = - function_pointer_target_symbol_expr; - auto const goto_end_if_location = - goto_function_body.insert_before( - else_location, - goto_programt::make_goto( - end_if_location, - original_function_call_instruction.source_location)); - auto const replaced_instruction_location = - goto_function.second.body.insert_before( - goto_end_if_location, new_instruction); - else_location = goto_function.second.body.insert_before( - replaced_instruction_location, - goto_programt::make_goto( - else_location, - notequal_exprt{ - pointer_symbol, - address_of_exprt{function_pointer_target_symbol_expr}})); - } - } - } - }); + 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); + }); } } @@ -212,14 +222,13 @@ void parse_function_pointer_restriction_options_from_cmdline( cmdline.get_values(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT)); } -namespace -{ function_pointer_restrictionst::restrictionst -merge_function_pointer_restrictions( - const function_pointer_restrictionst::restrictionst &lhs, +function_pointer_restrictionst::merge_function_pointer_restrictions( + function_pointer_restrictionst::restrictionst lhs, const function_pointer_restrictionst::restrictionst &rhs) { - auto result = lhs; + auto &result = lhs; + for(auto const &restriction : rhs) { auto emplace_result = result.emplace(restriction.first, restriction.second); @@ -231,89 +240,40 @@ merge_function_pointer_restrictions( } } } + return result; } -function_pointer_restrictionst::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) { auto function_pointer_restrictions = function_pointer_restrictionst::restrictionst{}; - for(auto const &restriction_opt : restriction_opts) + + for(const std::string &restriction_opt : restriction_opts) { - // the format for restrictions is / - // exactly one pointer and at least one target - auto const pointer_name_end = restriction_opt.find('/'); - auto const restriction_format_message = - "the format for restrictions is " - "/"; - 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}; - } - if(pointer_name_end == restriction_opt.size()) - { - throw invalid_command_line_argument_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}; - } - auto const pointer_name = restriction_opt.substr(0, pointer_name_end); - auto const target_names_substring = - restriction_opt.substr(pointer_name_end + 1); - auto const target_name_strings = split_string(target_names_substring, ','); - if(target_name_strings.size() == 1 && target_name_strings[0].empty()) - { - throw invalid_command_line_argument_exceptiont{ - "missing target list for function pointer restriction " + pointer_name, - "--" RESTRICT_FUNCTION_POINTER_OPT, - restriction_format_message}; - } - auto const target_names = ([&target_name_strings] { - auto target_names = std::unordered_set{}; - std::transform( - target_name_strings.begin(), - target_name_strings.end(), - std::inserter(target_names, target_names.end()), - string2id); - return target_names; - })(); - for(auto const &target_name : target_names) - { - if(target_name == ID_empty_string) - { - throw invalid_command_line_argument_exceptiont( - "leading or trailing comma in restrictions for `" + pointer_name + - "'", - "--" RESTRICT_FUNCTION_POINTER_OPT, - restriction_format_message); - } - } - if(!function_pointer_restrictions - .emplace(irep_idt{pointer_name}, target_names) - .second) + const auto restriction = + parse_function_pointer_restriction(restriction_opt); + + const bool inserted = function_pointer_restrictions + .emplace(restriction.first, restriction.second) + .second; + + if(!inserted) { throw invalid_command_line_argument_exceptiont{ - "function pointer restriction for `" + pointer_name + + "function pointer restriction for `" + id2string(restriction.first) + "' was specified twice", "--" RESTRICT_FUNCTION_POINTER_OPT}; - }; + } } + return function_pointer_restrictions; } function_pointer_restrictionst::restrictionst -parse_function_pointer_restrictions_from_file( +function_pointer_restrictionst::parse_function_pointer_restrictions_from_file( const std::list &filenames, message_handlert &message_handler) { @@ -322,12 +282,77 @@ parse_function_pointer_restrictions_from_file( { auto const restrictions = function_pointer_restrictionst::read_from_file(filename, message_handler); + merged_restrictions = merge_function_pointer_restrictions( - merged_restrictions, restrictions.restrictions); + std::move(merged_restrictions), restrictions.restrictions); } + return merged_restrictions; } -} // namespace + +function_pointer_restrictionst::restrictiont +function_pointer_restrictionst::parse_function_pointer_restriction( + const std::string &restriction_opt) +{ + // the format for restrictions is / + // exactly one pointer and at least one target + auto const pointer_name_end = restriction_opt.find('/'); + auto const restriction_format_message = + "the format for restrictions is " + "/"; + + 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}; + } + + if(pointer_name_end == restriction_opt.size()) + { + throw invalid_command_line_argument_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}; + } + + auto const pointer_name = restriction_opt.substr(0, pointer_name_end); + auto const target_names_substring = + restriction_opt.substr(pointer_name_end + 1); + auto const target_name_strings = split_string(target_names_substring, ','); + + if(target_name_strings.size() == 1 && target_name_strings[0].empty()) + { + throw invalid_command_line_argument_exceptiont{ + "missing target list for function pointer restriction " + pointer_name, + "--" RESTRICT_FUNCTION_POINTER_OPT, + restriction_format_message}; + } + + std::unordered_set target_names; + target_names.insert(target_name_strings.begin(), target_name_strings.end()); + + for(auto const &target_name : target_names) + { + if(target_name == ID_empty_string) + { + throw invalid_command_line_argument_exceptiont( + "leading or trailing comma in restrictions for `" + pointer_name + "'", + "--" RESTRICT_FUNCTION_POINTER_OPT, + restriction_format_message); + } + } + + return std::make_pair(pointer_name, target_names); +} function_pointer_restrictionst function_pointer_restrictionst::from_options( const optionst &options, @@ -341,36 +366,29 @@ function_pointer_restrictionst function_pointer_restrictionst::from_options( options.get_list_option(RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT), message_handler); return {merge_function_pointer_restrictions( - file_restrictions, commandline_restrictions)}; + std::move(file_restrictions), commandline_restrictions)}; } -function_pointer_restrictionst function_pointer_restrictionst::read_from_file( - const std::string &filename, - message_handlert &message_handler) +function_pointer_restrictionst +function_pointer_restrictionst::from_json(const jsont &json) { - auto failed = [](bool failFlag) { return failFlag; }; function_pointer_restrictionst::restrictionst restrictions; - auto inFile = std::ifstream{filename}; - jsont json; - if(failed(parse_json(inFile, filename, message_handler, json))) - { - throw system_exceptiont{ - "failed to read function pointer restrictions from " + filename}; - } + if(!json.is_object()) { - throw system_exceptiont{"top level item is not an object"}; + throw deserialization_exceptiont{"top level item is not an object"}; } - for(auto const &kv_pair : to_json_object(json)) + + for(auto const &restriction : to_json_object(json)) { - restrictions.emplace(irep_idt{kv_pair.first}, [&] { - if(!kv_pair.second.is_array()) + restrictions.emplace(irep_idt{restriction.first}, [&] { + if(!restriction.second.is_array()) { - throw system_exceptiont{"In " + filename + ", value of " + - kv_pair.first + " is not an array"}; + throw deserialization_exceptiont{"Value of " + restriction.first + + " is not an array"}; } auto possible_targets = std::unordered_set{}; - auto const &array = to_json_array(kv_pair.second); + auto const &array = to_json_array(restriction.second); std::transform( array.begin(), array.end(), @@ -378,24 +396,41 @@ function_pointer_restrictionst function_pointer_restrictionst::read_from_file( [&](const jsont &array_element) { if(!array_element.is_string()) { - throw system_exceptiont{"In " + filename + ", value of " + - kv_pair.first + - "contains a non-string array element"}; + throw deserialization_exceptiont{ + "Value of " + restriction.first + + "contains a non-string array element"}; } return irep_idt{to_json_string(array_element).value}; }); return possible_targets; }()); } + return function_pointer_restrictionst{restrictions}; } -void function_pointer_restrictionst::write_to_file( - const std::string &filename) const +function_pointer_restrictionst function_pointer_restrictionst::read_from_file( + const std::string &filename, + message_handlert &message_handler) +{ + auto inFile = std::ifstream{filename}; + jsont json; + + if(parse_json(inFile, filename, message_handler, json)) + { + throw deserialization_exceptiont{ + "failed to read function pointer restrictions from " + filename}; + } + + return from_json(json); +} + +jsont function_pointer_restrictionst::to_json() const { auto function_pointer_restrictions_json = jsont{}; auto &restrictions_json_object = function_pointer_restrictions_json.make_object(); + for(auto const &restriction : restrictions) { auto &targets_array = @@ -405,11 +440,22 @@ void function_pointer_restrictionst::write_to_file( targets_array.push_back(json_stringt{target}); } } + + return function_pointer_restrictions_json; +} + +void function_pointer_restrictionst::write_to_file( + const std::string &filename) const +{ + auto function_pointer_restrictions_json = to_json(); + auto outFile = std::ofstream{filename}; + if(!outFile) { throw system_exceptiont{"cannot open " + filename + " for writing function pointer restrictions"}; } + function_pointer_restrictions_json.output(outFile); } diff --git a/src/goto-programs/restrict_function_pointers.h b/src/goto-programs/restrict_function_pointers.h index f7e51d88a34..e7681847406 100644 --- a/src/goto-programs/restrict_function_pointers.h +++ b/src/goto-programs/restrict_function_pointers.h @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: GOTO Program Utilities +Module: Restrict function pointers Author: Diffblue Ltd. @@ -35,7 +35,7 @@ Author: Diffblue Ltd. "):" \ "(" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT "):" -#define RESTRICT_FUNCTION_POINTER_HELP \ +#define HELP_RESTRICT_FUNCTION_POINTER \ "--" RESTRICT_FUNCTION_POINTER_OPT \ " /\n" \ " restrict a function pointer to a set of possible targets\n" \ @@ -44,18 +44,22 @@ Author: Diffblue Ltd. " works for globals and function parameters right now\n" \ "--" RESTRICT_FUNCTION_POINTER_FROM_FILE_OPT \ " \n" \ - " add from function pointer restrictions from file" + " add function pointer restrictions from file" void parse_function_pointer_restriction_options_from_cmdline( const cmdlinet &cmdline, optionst &options); +class jsont; class message_handlert; -struct function_pointer_restrictionst + +class function_pointer_restrictionst { +public: using restrictionst = std::unordered_map>; - using value_type = restrictionst::value_type; + using restrictiont = restrictionst::value_type; + const restrictionst restrictions; /// parse function pointer restrictions from command line @@ -65,14 +69,32 @@ struct function_pointer_restrictionst static function_pointer_restrictionst from_options(const optionst &options, message_handlert &message_handler); + jsont to_json() const; + static function_pointer_restrictionst from_json(const jsont &json); + static function_pointer_restrictionst read_from_file( const std::string &filename, message_handlert &message_handler); void write_to_file(const std::string &filename) const; + +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); + + static restrictiont + parse_function_pointer_restriction(const std::string &restriction_opt); }; -/// Apply a function pointer restrictions to a goto_model. Each restriction is a +/// 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 /// pointer, comparing it to the set of possible targets. This also adds an diff --git a/src/util/irep.h b/src/util/irep.h index 0613d1f717c..2e2dacf91c0 100644 --- a/src/util/irep.h +++ b/src/util/irep.h @@ -50,11 +50,6 @@ inline const std::string &id2string(const irep_idt &d) #endif } -inline irep_idt string2id(const std::string &id_string) -{ - return irep_idt{id_string}; -} - inline const std::string &name2string(const irep_namet &n) { #ifdef USE_DSTRING diff --git a/unit/goto-programs/label_function_pointer_call_sites.cpp b/unit/goto-programs/label_function_pointer_call_sites.cpp index 4fd17144fb2..e544a6378d4 100644 --- a/unit/goto-programs/label_function_pointer_call_sites.cpp +++ b/unit/goto-programs/label_function_pointer_call_sites.cpp @@ -40,7 +40,7 @@ TEST_CASE("Label function pointer call sites", "[core]") [](goto_programt::const_targett it) { static int call_count = 0; - switch (call_count) + switch(call_count) { case 0: // first call instruction @@ -83,6 +83,5 @@ TEST_CASE("Label function pointer call sites", "[core]") } call_count++; - } - ); + }); } diff --git a/unit/goto-programs/module_dependencies.txt b/unit/goto-programs/module_dependencies.txt index 070c3bcc8bb..d0aaf35d60d 100644 --- a/unit/goto-programs/module_dependencies.txt +++ b/unit/goto-programs/module_dependencies.txt @@ -1,3 +1,4 @@ goto-programs +json testing-utils util From 966cf3a2abf436b92a5b81157b0a5e38cdc03de8 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 5 Mar 2020 17:44:54 +0000 Subject: [PATCH 08/18] Update restrict function pointer documentation Update to reflect that the feature is now a goto-instrument analysis --- .../restrict-function-pointer.md | 33 +++++++++++-------- 1 file changed, 20 insertions(+), 13 deletions(-) diff --git a/doc/cprover-manual/restrict-function-pointer.md b/doc/cprover-manual/restrict-function-pointer.md index c8246059e5b..5b63b2b0c1a 100644 --- a/doc/cprover-manual/restrict-function-pointer.md +++ b/doc/cprover-manual/restrict-function-pointer.md @@ -2,11 +2,17 @@ ## Restricting function pointers +In this document, we describe the `goto-instrument` feature to replace calls +through function pointers by case distinctions over calls to given sets of +functions. + ### Motivation -CBMC comes with a way to resolve calls to function pointers to direct function -calls. This is needed because symbolic execution itself can't handle calls to -function pointers. In practice, this looks something like this: +The CPROVER framework includes a goto program transformation pass +`remove_function_pointers()` to resolve calls to function pointers to direct +function calls. The pass is needed by `cbmc`, as symbolic execution itself can't +handle calls to function pointers. In practice, the transformation pass works as +follows: Given that there are functions with these signatures available in the program: @@ -53,15 +59,16 @@ functions matching a particular signature, or if some of these functions are expensive in symex (e.g. functions with lots of loops or recursion), then this can be a bit cumbersome - especially if we, as a user, already know that a particular function pointer will only resolve to a single function or a small -set of functions. This is what the `--restrict-function-pointer` option allows. +set of functions. The `goto-instrument` option `--restrict-function-pointer` +allows to manually specify this set of functions. ### Example -Take the motivating example. Let us assume that we know for a fact that `call` -will always receive pointers to either `f` or `g` during actual executions of -the program, and symbolic execution for `h` is too expensive to simply ignore -the cost of its branch. For this, we will label the places in each function -where function pointers are being called, to this pattern: +Take the motivating example above. Let us assume that we know for a fact that +`call` will always receive pointers to either `f` or `g` during actual +executions of the program, and symbolic execution for `h` is too expensive to +simply ignore the cost of its branch. For this, we will label the places in each +function where function pointers are being called, to this pattern: ``` .function_pointer_call. @@ -70,14 +77,14 @@ where function pointers are being called, to this pattern: where `N` is referring to which function call it is - so the first call to a function pointer in a function will have `N=1`, the 5th `N=5` etc. -We can call `cbmc` with `--restrict-function-pointer -call.function_pointer_call.1/f,g`. This can be read as +We can call `goto-instrument --restrict-function-pointer +call.function_pointer_call.1/f,g in.gb out.gb`. This can be read as > For the first call to a function pointer in the function `call`, assume that > it can only be a call to `f` or `g` -The resulting code looks similar to the original example, except now there will -not be a call to `h`: +The resulting output (written to goto binary `out.gb`) looks similar to the +original example, except now there will not be a call to `h`: ``` void call(fptr_t fptr) { From ea8fbcfea0edf14168acc49e71c645b8cf67f463 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 12 Mar 2020 11:32:51 +0000 Subject: [PATCH 09/18] Refactor restrict function pointers regression tests --- .../test.c | 12 ++++---- .../test.desc | 4 +++ .../test.c | 16 +++++++---- .../test.desc | 3 ++ .../test.c | 4 +++ .../test.desc | 12 ++++++++ .../test.c | 16 +++++++---- .../test.desc | 12 ++++++++ .../test.c | 16 +++++++---- .../test.desc | 12 ++++++++ .../test.c | 16 +++++++---- .../test.desc | 14 ++++++++++ .../test.c | 12 ++++---- .../test.c | 27 ++++++------------ .../test.desc | 3 ++ .../test.c | 27 ++++++------------ .../test.desc | 9 ++++++ .../test.c | 28 ++++++------------- .../test.desc | 6 ++++ 19 files changed, 156 insertions(+), 93 deletions(-) diff --git a/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.c b/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.c index 3787afa1df6..97c213b654c 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.c +++ b/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.c @@ -10,9 +10,6 @@ void use_fg(int choice, fptr_t fptr, fptr_t gptr) assert((choice ? fptr : gptr)(10) == 10 + choice); } -// this is just here to distinguish the behavior from FP removal, which'd include g -int g_always_false_cond = 0; - int main(void) { use_fg(0, get_f(), get_g()); @@ -34,9 +31,14 @@ int h(int x) return x / 2; } +// Below we take the address of f, g, and h. Thus remove_function_pointers() +// would create a case distinction involving f, g, and h in the function +// use_fg() above. +int always_false_cond = 0; + fptr_t get_f(void) { - if(!g_always_false_cond) + if(!always_false_cond) { return f; } @@ -48,7 +50,7 @@ fptr_t get_f(void) fptr_t get_g(void) { - if(!g_always_false_cond) + if(!always_false_cond) { return g; } diff --git a/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc b/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc index 03c2e782be9..c6fb8983cc1 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc @@ -5,3 +5,7 @@ test.c \[use_fg.assertion.1\] line \d+ dereferenced function pointer at use_fg.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: SUCCESS ^EXIT=0$ ^SIGNAL=0$ +-- +-- +This test checks that the selected function pointer is replaced by a case +distinction over both functions f and g. diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.c b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.c index eb28bb15684..0acdb6e3495 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.c +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.c @@ -25,37 +25,41 @@ int f(int x) { return x + 1; } + int g(int x) { return x; } + int h(int x) { return x - 1; } -int g_select_function = 0; +int select_function = 0; void select_f(void) { - g_select_function = 0; + select_function = 0; } + void select_g(void) { - g_select_function = 1; + select_function = 1; } + void select_h(void) { - g_select_function = 2; + select_function = 2; } fptr_t get_f(void) { - if(g_select_function == 0) + if(select_function == 0) { return f; } - else if(g_select_function == 1) + else if(select_function == 1) { return g; } diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.desc index 05803cc488c..f18cbd6515f 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-code-check/test.desc @@ -7,3 +7,6 @@ g\(10\) ^SIGNAL=0$ -- h\(10\) +-- +This test checks that no call to g appears in the goto program after the +transformation by the restrict function pointer feature. diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.c b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.c index ac36b749862..2a2840b81e3 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.c +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.c @@ -27,10 +27,12 @@ int f(int x) { return x + 1; } + int g(int x) { return x; } + int h(int x) { return x - 1; @@ -42,10 +44,12 @@ void select_f(void) { g_select_function = 0; } + void select_g(void) { g_select_function = 1; } + void select_h(void) { g_select_function = 2; diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc index bf6ec38059f..18c7fac80e3 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-incorrectly/test.desc @@ -4,3 +4,15 @@ test.c \[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 ^EXIT=10$ ^SIGNAL=0$ +-- +-- +This test checks that multiple restrictions for a given function pointer can be +given. + +The test further checks that the correct safety assertions are generated. The +function pointer restriction feature outputs safety assertions for all calls +that it replaces. That is, when it replaces a call with a case distinction over +a given set of functions, it adds an assertion checking that in the original +program, indeed no other function could have been called at that location. In +this case, the function h could also be called, but the given restrictions only +include f and g, hence the safety assertion fails. 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 ac36b749862..7eeb597247c 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 @@ -27,37 +27,41 @@ int f(int x) { return x + 1; } + int g(int x) { return x; } + int h(int x) { return x - 1; } -int g_select_function = 0; +int select_function = 0; void select_f(void) { - g_select_function = 0; + select_function = 0; } + void select_g(void) { - g_select_function = 1; + select_function = 1; } + void select_h(void) { - g_select_function = 2; + select_function = 2; } fptr_t get_f(void) { - if(g_select_function == 0) + if(select_function == 0) { return f; } - else if(g_select_function == 1) + else if(select_function == 1) { return g; } 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 e3a5c3b50c1..98bb04f6b6a 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 @@ -4,3 +4,15 @@ test.c \[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 ^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 test further checks that the correct safety assertions are generated. The +function pointer restriction feature outputs safety assertions for all calls +that it replaces. That is, when it replaces a call with a case distinction over +a given set of functions, it adds an assertion checking that in the original +program, indeed no other function could have been called at that location. In +this case, the function h could also be called, but the given restrictions only +include f and g, hence the safety assertion fails. diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.c b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.c index ac36b749862..7eeb597247c 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.c +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.c @@ -27,37 +27,41 @@ int f(int x) { return x + 1; } + int g(int x) { return x; } + int h(int x) { return x - 1; } -int g_select_function = 0; +int select_function = 0; void select_f(void) { - g_select_function = 0; + select_function = 0; } + void select_g(void) { - g_select_function = 1; + select_function = 1; } + void select_h(void) { - g_select_function = 2; + select_function = 2; } fptr_t get_f(void) { - if(g_select_function == 0) + if(select_function == 0) { return f; } - else if(g_select_function == 1) + else if(select_function == 1) { return g; } diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.desc index 5c9b3816a99..7f5caa4b0a4 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-file/test.desc @@ -4,3 +4,15 @@ test.c \[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 ^EXIT=10$ ^SIGNAL=0$ +-- +-- +This test checks the reading of function pointer restrictions from a given json +file. + +The test further checks that the correct safety assertions are generated. The +function pointer restriction feature outputs safety assertions for all calls +that it replaces. That is, when it replaces a call with a case distinction over +a given set of functions, it adds an assertion checking that in the original +program, indeed no other function could have been called at that location. In +this case, the function h could also be called, but the given restrictions only +include f and g, hence the safety assertion fails. diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.c b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.c index ac36b749862..7eeb597247c 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.c +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.c @@ -27,37 +27,41 @@ int f(int x) { return x + 1; } + int g(int x) { return x; } + int h(int x) { return x - 1; } -int g_select_function = 0; +int select_function = 0; void select_f(void) { - g_select_function = 0; + select_function = 0; } + void select_g(void) { - g_select_function = 1; + select_function = 1; } + void select_h(void) { - g_select_function = 2; + select_function = 2; } fptr_t get_f(void) { - if(g_select_function == 0) + if(select_function == 0) { return f; } - else if(g_select_function == 1) + else if(select_function == 1) { return g; } diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc index b46ff820de6..b1a1756ad8b 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions-via-multiple-files/test.desc @@ -4,3 +4,17 @@ test.c \[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 ^EXIT=10$ ^SIGNAL=0$ +-- +-- +This test checks that the restrictions for a function pointer are the union of +the restrictions given in multiple files. In this case, the restrictions for the +first function pointer call in use_f are f and g, provided by the files +restrictions_1.json and restrictions_2.json. + +The test further checks that the correct safety assertions are generated. The +function pointer restriction feature outputs safety assertions for all calls +that it replaces. That is, when it replaces a call with a case distinction over +a given set of functions, it adds an assertion checking that in the original +program, indeed no other function could have been called at that location. In +this case, the function h could also be called, but the given restrictions only +include f and g, hence the safety assertion fails. diff --git a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.c b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.c index eb28bb15684..ead7fd6ba9c 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.c +++ b/regression/goto-instrument/restrict-function-pointer-to-multiple-functions/test.c @@ -34,28 +34,28 @@ int h(int x) return x - 1; } -int g_select_function = 0; +int select_function = 0; void select_f(void) { - g_select_function = 0; + select_function = 0; } void select_g(void) { - g_select_function = 1; + select_function = 1; } void select_h(void) { - g_select_function = 2; + select_function = 2; } fptr_t get_f(void) { - if(g_select_function == 0) + if(select_function == 0) { return f; } - else if(g_select_function == 1) + else if(select_function == 1) { return g; } diff --git a/regression/goto-instrument/restrict-function-pointer-to-single-function-code-check/test.c b/regression/goto-instrument/restrict-function-pointer-to-single-function-code-check/test.c index e172f39391c..3b9844dc0dc 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-single-function-code-check/test.c +++ b/regression/goto-instrument/restrict-function-pointer-to-single-function-code-check/test.c @@ -2,38 +2,27 @@ typedef int (*fptr_t)(int); -fptr_t get_f(void); - void use_f(fptr_t fptr) { assert(fptr(10) == 11); } -int main(void) -{ - use_f(get_f()); -} - int f(int x) { return x + 1; } + int g(int x) { return x; } -// this is just here to distinguish the behavior from FP removal, which'd include g -int g_always_false_cond = 0; - -fptr_t get_f(void) +int main(void) { - if(!g_always_false_cond) - { - return f; - } - else - { - return g; - } + int one = 1; + + // We take the address of f and g. In this case remove_function_pointers() + // would create a case distinction involving both f and g in the function + // use_f() above. + use_f(one ? f : g); } diff --git a/regression/goto-instrument/restrict-function-pointer-to-single-function-code-check/test.desc b/regression/goto-instrument/restrict-function-pointer-to-single-function-code-check/test.desc index f462acc84c8..ef4e9827636 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-single-function-code-check/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-to-single-function-code-check/test.desc @@ -6,3 +6,6 @@ f\(10\) ^SIGNAL=0$ -- g\(10\) +-- +This test checks that no call to g appears in the goto program after the +transformation by the restrict function pointer feature. diff --git a/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.c b/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.c index 63370cbd1b1..fff24d46413 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.c +++ b/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.c @@ -2,38 +2,27 @@ typedef int (*fptr_t)(int); -fptr_t get_f(void); - void use_f(fptr_t fptr) { assert(fptr(10) == 11); } -int main(void) -{ - use_f(get_f()); -} - int f(int x) { return x + 1; } + int g(int x) { return x; } -// this is just here to distinguish the behavior from FP removal, which'd include g -int g_always_false_cond = 1; - -fptr_t get_f(void) +int main(void) { - if(!g_always_false_cond) - { - return f; - } - else - { - return g; - } + int one = 1; + + // We take the address of f and g. In this case remove_function_pointers() + // would create a case distinction involving both f and g in the function + // use_f() above. + use_f(!one ? f : g); // selects g } diff --git a/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.desc b/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.desc index fc8b95986c3..8ab6995bf6e 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-to-single-function-incorrectly/test.desc @@ -4,3 +4,12 @@ test.c \[use_f\.assertion\.1\] line \d+ dereferenced function pointer at use_f.function_pointer_call.1 must be f: FAILURE ^EXIT=10$ ^SIGNAL=0$ +-- +-- +The function pointer restriction feature outputs safety assertions for all calls +that it replaces. That is, when it replaces a call with a case distinction over +a given set of functions, it adds an assertion checking that in the original +program, indeed no other function could have been called at that location. This +test verifies this feature, by checking that the safety assertion fails when a +function pointer call is replaced by a call to f, when however g could be called +in the original program. diff --git a/regression/goto-instrument/restrict-function-pointer-to-single-function/test.c b/regression/goto-instrument/restrict-function-pointer-to-single-function/test.c index d82c347e8b7..3b9844dc0dc 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-single-function/test.c +++ b/regression/goto-instrument/restrict-function-pointer-to-single-function/test.c @@ -2,39 +2,27 @@ typedef int (*fptr_t)(int); -fptr_t get_f(void); - void use_f(fptr_t fptr) { assert(fptr(10) == 11); } -int main(void) -{ - use_f(get_f()); -} - int f(int x) { return x + 1; } + int g(int x) { return x; } -// this is just here to distinguish the behavior from FP removal, which'd include -// only f if we didn't reference g anywhere. -int g_always_false_cond = 0; - -fptr_t get_f(void) +int main(void) { - if(!g_always_false_cond) - { - return f; - } - else - { - return g; - } + int one = 1; + + // We take the address of f and g. In this case remove_function_pointers() + // would create a case distinction involving both f and g in the function + // use_f() above. + use_f(one ? f : g); } diff --git a/regression/goto-instrument/restrict-function-pointer-to-single-function/test.desc b/regression/goto-instrument/restrict-function-pointer-to-single-function/test.desc index 13540f25cdd..4108fed725e 100644 --- a/regression/goto-instrument/restrict-function-pointer-to-single-function/test.desc +++ b/regression/goto-instrument/restrict-function-pointer-to-single-function/test.desc @@ -4,3 +4,9 @@ test.c \[use_f\.assertion\.2\] line \d+ assertion fptr\(10\) == 11: SUCCESS ^EXIT=0$ ^SIGNAL=0$ +-- +-- +This test checks that the function f is called for the first function pointer +call in function use_f. Without the restrict function pointer option, the +regular function pointer removal would create a case distinction over both f and +g for the given program (as the address of both is taken). From 6c8a77464dd51eb04c53d69cd253c8b26ed8ebc2 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 11 Mar 2020 17:27:38 +0000 Subject: [PATCH 10/18] Add unit tests for restrict function pointers feature --- unit/Makefile | 1 + .../restrict_function_pointers.cpp | 150 ++++++++++++++++++ 2 files changed, 151 insertions(+) create mode 100644 unit/goto-programs/restrict_function_pointers.cpp diff --git a/unit/Makefile b/unit/Makefile index a6d16f1281a..e324755c1ad 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -39,6 +39,7 @@ SRC += analyses/ai/ai.cpp \ goto-programs/is_goto_binary.cpp \ goto-programs/label_function_pointer_call_sites.cpp \ goto-programs/osx_fat_reader.cpp \ + goto-programs/restrict_function_pointers.cpp \ goto-programs/remove_returns.cpp \ goto-programs/xml_expr.cpp \ goto-symex/apply_condition.cpp \ diff --git a/unit/goto-programs/restrict_function_pointers.cpp b/unit/goto-programs/restrict_function_pointers.cpp new file mode 100644 index 00000000000..149c04f8898 --- /dev/null +++ b/unit/goto-programs/restrict_function_pointers.cpp @@ -0,0 +1,150 @@ +/*******************************************************************\ + +Module: Restrict function pointers unit tests + +Author: Daniel Poetzl + +\*******************************************************************/ + +#include +#include + +#include + +#include + +class fp_restrictionst : public function_pointer_restrictionst +{ + friend void restriction_parsing_test(); + friend void merge_restrictions_test(); +}; + +void restriction_parsing_test() +{ + { + const auto res = + fp_restrictionst::parse_function_pointer_restriction("func1/func2"); + 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"); + REQUIRE(res.first == "func1"); + REQUIRE(res.second.size() == 2); + REQUIRE(res.second.find("func2") != res.second.end()); + REQUIRE(res.second.find("func3") != res.second.end()); + } + + REQUIRE_THROWS_AS( + fp_restrictionst::parse_function_pointer_restriction("func"), + invalid_command_line_argument_exceptiont); + + REQUIRE_THROWS_AS( + fp_restrictionst::parse_function_pointer_restriction("/func"), + invalid_command_line_argument_exceptiont); + + REQUIRE_THROWS_AS( + fp_restrictionst::parse_function_pointer_restriction("func/"), + invalid_command_line_argument_exceptiont); + + REQUIRE_THROWS_AS( + fp_restrictionst::parse_function_pointer_restriction("func/,"), + invalid_command_line_argument_exceptiont); + + REQUIRE_THROWS_AS( + fp_restrictionst::parse_function_pointer_restriction("func1/func2,"), + invalid_command_line_argument_exceptiont); + + REQUIRE_THROWS_AS( + fp_restrictionst::parse_function_pointer_restriction("func1/,func2"), + invalid_command_line_argument_exceptiont); +} + +void merge_restrictions_test() +{ + fp_restrictionst::restrictionst r1; + r1.emplace("fp1", std::unordered_set{"func1", "func2"}); + r1.emplace("fp2", std::unordered_set{"func1"}); + + fp_restrictionst::restrictionst r2; + r2.emplace("fp1", std::unordered_set{"func1", "func3"}); + + fp_restrictionst::restrictionst result = + fp_restrictionst::merge_function_pointer_restrictions(r1, r2); + + REQUIRE(result.size() == 2); + + const auto &fp1_restrictions = result.at("fp1"); + REQUIRE(fp1_restrictions.size() == 3); + REQUIRE(fp1_restrictions.count("func1") == 1); + REQUIRE(fp1_restrictions.count("func2") == 1); + REQUIRE(fp1_restrictions.count("func3") == 1); + + const auto &fp2_restrictions = result.at("fp2"); + REQUIRE(fp2_restrictions.size() == 1); + REQUIRE(fp2_restrictions.count("func1") == 1); +} + +TEST_CASE("Restriction parsing", "[core]") +{ + restriction_parsing_test(); +} + +TEST_CASE("Merge function pointer restrictions", "[core]") +{ + merge_restrictions_test(); +} + +TEST_CASE("Json conversion", "[core]") +{ + // conversion json1 -> restrictions1 -> json2 -> restrictions2 + // then check that restrictions1 == restrictions2 + // + // we use json as a starting point as it is easy to write, and we compare the + // restrictions as it is a canonical representation (in contrast, the json + // representation for the same restrictions can differ, due to the array + // elements appearing in different orders) + + std::istringstream ss( + "{" + " \"use_f.function_pointer_call.1\": [\"f\", \"g\"]," + " \"use_f.function_pointer_call.2\": [\"h\"]" + "}"); + + jsont json1; + + parse_json(ss, "", null_message_handler, json1); + + // json1 -> restrictions1 + const auto function_pointer_restrictions1 = + function_pointer_restrictionst::from_json(json1); + + const auto &restrictions = function_pointer_restrictions1.restrictions; + + REQUIRE(restrictions.size() == 2); + + const auto &fp1_restrictions = + restrictions.at("use_f.function_pointer_call.1"); + REQUIRE(fp1_restrictions.size() == 2); + REQUIRE(fp1_restrictions.count("f") == 1); + REQUIRE(fp1_restrictions.count("g") == 1); + + const auto &fp2_restrictions = + restrictions.at("use_f.function_pointer_call.2"); + REQUIRE(fp2_restrictions.size() == 1); + REQUIRE(fp2_restrictions.count("h") == 1); + + // restrictions1 -> json2 + const auto json2 = function_pointer_restrictions1.to_json(); + + // json2 -> restrictions2 + const auto function_pointer_restrictions2 = + function_pointer_restrictionst::from_json(json2); + + REQUIRE( + function_pointer_restrictions1.restrictions == + function_pointer_restrictions2.restrictions); +} From 7916895fa8e9de35e15cdb779c6f8992849ab593 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Tue, 5 Nov 2019 17:05:23 +0000 Subject: [PATCH 11/18] 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 04b3d443687..3ee127a1e2c 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 7ffdc6d08044b1ab520f9ab05a078315092e2bde Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 16 Mar 2020 16:45:21 +0000 Subject: [PATCH 12/18] 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 da802da95e9adc4b45b7f2e3f37b521d318941ca Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 16 Mar 2020 17:02:50 +0000 Subject: [PATCH 13/18] 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 3ee127a1e2c..930f9b0de2d 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 c252c84b67af23ad33682bcf0f023311e1f27188 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 17 Mar 2020 13:58:06 +0000 Subject: [PATCH 14/18] 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 1b4ad0b21f0b8bd8d86b9d5fbc70de745a8bd45f Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Wed, 18 Mar 2020 19:03:05 +0000 Subject: [PATCH 15/18] 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 bc7c46692a2ddedc0f333153238fc1ce0a265021 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 23 Mar 2020 13:09:30 +0000 Subject: [PATCH 16/18] 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 cedfb0b9b94ec66a846154c05cbd2a1c533f6477 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 23 Mar 2020 14:16:24 +0000 Subject: [PATCH 17/18] 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() From 45d171f138ac7c4e409eb39db97bd11308fac534 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Tue, 17 Mar 2020 13:58:06 +0000 Subject: [PATCH 18/18] Apply clang-format --- .../test.c | 1 - 1 file changed, 1 deletion(-) 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 11ea6388528..1cfea0f8fa5 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 @@ -34,4 +34,3 @@ int main(void) use_f(h); use_f(other); } -