From 23d948c1fa576ed5db43fbad9c97ffd10e2341fd Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 11 Nov 2019 16:56:34 +0000 Subject: [PATCH 1/5] Apply miscellaneous refactoring and fixes to goto-harness. Add error checking (check that the entry function is in the symbol table before the code generation, and make sure that it's present correctly) make sure that doc comments are capitalised, change the signatures of functions to make them stricter in the arguments they accept. --- .../function_call_harness_generator.cpp | 19 ++++++++--- src/goto-harness/recursive_initialization.cpp | 34 +++++++++++++------ src/goto-harness/recursive_initialization.h | 18 +++++----- 3 files changed, 48 insertions(+), 23 deletions(-) diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index b7f26a1d649..69727daa648 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -72,10 +72,10 @@ struct function_call_harness_generatort::implt void ensure_harness_does_not_already_exist(); /// Update the goto-model with the new harness function. void add_harness_function_to_goto_model(code_blockt function_body); - /// declare local variables for each of the parameters of the entry function + /// Declare local variables for each of the parameters of the entry function /// and return them code_function_callt::argumentst declare_arguments(code_blockt &function_body); - /// write initialisation code for each of the arguments into function_body, + /// Write initialisation code for each of the arguments into function_body, /// then insert a call to the entry function with the arguments void call_function( const code_function_callt::argumentst &arguments, @@ -269,7 +269,7 @@ void function_call_harness_generatort::implt::generate_initialisation_code_for( void function_call_harness_generatort::validate_options( const goto_modelt &goto_model) { - if(p_impl->function == ID_empty) + if(p_impl->function == ID_empty_string) throw invalid_command_line_argument_exceptiont{ "required parameter entry function not set", "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT}; @@ -283,8 +283,17 @@ void function_call_harness_generatort::validate_options( " --" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT}; } - auto function_to_call = goto_model.symbol_table.lookup_ref(p_impl->function); - auto ftype = to_code_type(function_to_call.type); + const auto function_to_call_pointer = + goto_model.symbol_table.lookup(p_impl->function); + if(function_to_call_pointer == nullptr) + { + throw invalid_command_line_argument_exceptiont{ + "entry function `" + id2string(p_impl->function) + + "' does not exist in the symbol table", + "--" FUNCTION_HARNESS_GENERATOR_FUNCTION_OPT}; + } + const auto &function_to_call = *function_to_call_pointer; + const auto &ftype = to_code_type(function_to_call.type); for(auto const &equal_cluster : p_impl->function_parameters_to_treat_equal) { for(auto const &pointer_id : equal_cluster) diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index 537ba8c8b4d..6de65fb5d39 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -185,7 +185,7 @@ void recursive_initializationt::initialize( code_blockt recursive_initializationt::build_constructor_body( const exprt &depth_symbol, - const exprt &result_symbol, + const symbol_exprt &result_symbol, const optionalt &size_symbol, const optionalt &lhs_name) { @@ -220,7 +220,7 @@ code_blockt recursive_initializationt::build_constructor_body( } } -const irep_idt &recursive_initializationt::build_constructor(const exprt &expr) +irep_idt recursive_initializationt::build_constructor(const exprt &expr) { // for `expr` of type T builds a declaration of a function: // @@ -235,7 +235,9 @@ const irep_idt &recursive_initializationt::build_constructor(const exprt &expr) { expr_name = to_symbol_expr(expr).get_identifier(); if(should_be_treated_as_array(*expr_name)) + { size_var = get_associated_size_variable(*expr_name); + } } const typet &type = expr.type(); if(type_constructor_names.find(type) != type_constructor_names.end()) @@ -554,7 +556,7 @@ symbol_exprt recursive_initializationt::get_free_function() code_blockt recursive_initializationt::build_pointer_constructor( const exprt &depth, - const exprt &result) + const symbol_exprt &result) { PRECONDITION(result.type().id() == ID_pointer); const typet &type = result.type().subtype(); @@ -639,7 +641,7 @@ code_blockt recursive_initializationt::build_pointer_constructor( } code_blockt recursive_initializationt::build_array_string_constructor( - const exprt &result) const + const symbol_exprt &result) const { PRECONDITION(result.type().id() == ID_pointer); const typet &type = result.type().subtype(); @@ -668,7 +670,7 @@ code_blockt recursive_initializationt::build_array_string_constructor( code_blockt recursive_initializationt::build_array_constructor( const exprt &depth, - const exprt &result) + const symbol_exprt &result) { PRECONDITION(result.type().id() == ID_pointer); const typet &type = result.type().subtype(); @@ -690,7 +692,7 @@ code_blockt recursive_initializationt::build_array_constructor( code_blockt recursive_initializationt::build_struct_constructor( const exprt &depth, - const exprt &result) + const symbol_exprt &result) { PRECONDITION(result.type().id() == ID_pointer); const typet &struct_type = result.type().subtype(); @@ -705,8 +707,8 @@ code_blockt recursive_initializationt::build_struct_constructor( return body; } -code_blockt -recursive_initializationt::build_nondet_constructor(const exprt &result) const +code_blockt recursive_initializationt::build_nondet_constructor( + const symbol_exprt &result) const { PRECONDITION(result.type().id() == ID_pointer); code_blockt body{}; @@ -718,7 +720,7 @@ recursive_initializationt::build_nondet_constructor(const exprt &result) const code_blockt recursive_initializationt::build_dynamic_array_constructor( const exprt &depth, - const exprt &result, + const symbol_exprt &result, const exprt &size, const optionalt &lhs_name) { @@ -820,7 +822,19 @@ code_blockt recursive_initializationt::build_dynamic_array_constructor( bool recursive_initializationt::needs_freeing(const exprt &expr) const { - return expr.type().id() == ID_pointer && expr.type().id() != ID_code; + if(expr.type().id() != ID_pointer || expr.type().subtype().id() == ID_code) + return false; + for(auto const &common_arguments_origin : common_arguments_origins) + { + if(common_arguments_origin.has_value() && expr.id() == ID_symbol) + { + auto origin_name = + to_symbol_expr(*common_arguments_origin).get_identifier(); + auto expr_name = to_symbol_expr(expr).get_identifier(); + return origin_name == expr_name; + } + } + return true; } void recursive_initializationt::free_if_possible( diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h index 5b0dfdac37d..ef92643a4c7 100644 --- a/src/goto-harness/recursive_initialization.h +++ b/src/goto-harness/recursive_initialization.h @@ -173,7 +173,7 @@ class recursive_initializationt /// \return the body of the constructor code_blockt build_constructor_body( const exprt &depth_symbol, - const exprt &result_symbol, + const symbol_exprt &result_symbol, const optionalt &size_symbol, const optionalt &lhs_name); @@ -181,7 +181,7 @@ class recursive_initializationt /// it if not. /// \param expr: the expression to be constructed /// \return name of the constructor function - const irep_idt &build_constructor(const exprt &expr); + irep_idt build_constructor(const exprt &expr); /// Generic constructor for all pointers: only builds one pointee (not an /// array) but may recourse in case the pointee contains more pointers, e.g. @@ -190,26 +190,28 @@ class recursive_initializationt /// \param result: symbol of the result parameter /// \return the body of the constructor code_blockt - build_pointer_constructor(const exprt &depth, const exprt &result); + build_pointer_constructor(const exprt &depth, const symbol_exprt &result); /// Constructor for structures: simply iterates over members and initialise /// each one. /// \param depth: symbol of the depth parameter /// \param result: symbol of the result parameter /// \return the body of the constructor - code_blockt build_struct_constructor(const exprt &depth, const exprt &result); + code_blockt + build_struct_constructor(const exprt &depth, const symbol_exprt &result); /// Default constructor: assigns non-deterministic value of the right type. /// \param result: symbol of the result parameter /// \return the body of the constructor - code_blockt build_nondet_constructor(const exprt &result) const; + code_blockt build_nondet_constructor(const symbol_exprt &result) const; /// Constructor for arrays: simply iterates over elements and initialise /// each one. /// \param depth: symbol of the depth parameter /// \param result: symbol of the result parameter /// \return the body of the constructor - code_blockt build_array_constructor(const exprt &depth, const exprt &result); + code_blockt + build_array_constructor(const exprt &depth, const symbol_exprt &result); /// Constructor for dynamic arrays: allocate memory for `n` elements (`n` is /// random but bounded) and initialise each one. @@ -220,14 +222,14 @@ class recursive_initializationt /// \return the body of the constructor code_blockt build_dynamic_array_constructor( const exprt &depth, - const exprt &result, + const symbol_exprt &result, const exprt &size, const optionalt &lhs_name); /// Constructor for strings: as array but the last element is zero. /// \param result: symbol of the result parameter /// \return the body of the constructor - code_blockt build_array_string_constructor(const exprt &result) const; + code_blockt build_array_string_constructor(const symbol_exprt &result) const; }; #endif // CPROVER_GOTO_HARNESS_RECURSIVE_INITIALIZATION_H From 555fcbe8929b0979c907729a502cd9dfbcb0982e Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 11 Nov 2019 16:56:46 +0000 Subject: [PATCH 2/5] Add support for function pointers to goto-harness Also add support for having multiple constructors for the same type with different behaviours and different signatures. We are doing this because we need some types to be sometimes nullable and sometimes not, and for example, for arrays we sometimes need to pass a size parameter and sometimes not. --- .../function_pointer_argument/test.c | 20 +++++ .../function_pointer_argument/test.desc | 9 +++ .../function_pointer_nullable/test.c | 18 +++++ .../function_pointer_nullable/test.desc | 12 +++ .../common_harness_generator_options.h | 6 ++ .../function_call_harness_generator.cpp | 12 +++ src/goto-harness/recursive_initialization.cpp | 79 +++++++++++++++++-- src/goto-harness/recursive_initialization.h | 37 ++++++++- 8 files changed, 185 insertions(+), 8 deletions(-) create mode 100644 regression/goto-harness/function_pointer_argument/test.c create mode 100644 regression/goto-harness/function_pointer_argument/test.desc create mode 100644 regression/goto-harness/function_pointer_nullable/test.c create mode 100644 regression/goto-harness/function_pointer_nullable/test.desc diff --git a/regression/goto-harness/function_pointer_argument/test.c b/regression/goto-harness/function_pointer_argument/test.c new file mode 100644 index 00000000000..6b1fa95af7a --- /dev/null +++ b/regression/goto-harness/function_pointer_argument/test.c @@ -0,0 +1,20 @@ +#include + +typedef int (*fptr)(int a, int b); + +int max_normal(int first, int second) +{ + return first >= second ? first : second; +} + +int max_crazy(int first, int second) +{ + return first >= second ? second : first; +} + +void use_fptr(fptr max, int first, int second) +{ + int m = max(first, second); + assert(m == first || m == second); + assert(m >= first && m >= second); +} diff --git a/regression/goto-harness/function_pointer_argument/test.desc b/regression/goto-harness/function_pointer_argument/test.desc new file mode 100644 index 00000000000..5b596a989b7 --- /dev/null +++ b/regression/goto-harness/function_pointer_argument/test.desc @@ -0,0 +1,9 @@ +CORE +test.c +--harness-type call-function --harness-function-name harness --function use_fptr +^EXIT=10$ +^SIGNAL=0$ +\[use_fptr.assertion.1\] line \d+ assertion m == first \|\| m == second: SUCCESS +\[use_fptr.assertion.2\] line \d+ assertion m >= first && m >= second: FAILURE +-- +^warning: ignoring diff --git a/regression/goto-harness/function_pointer_nullable/test.c b/regression/goto-harness/function_pointer_nullable/test.c new file mode 100644 index 00000000000..13a0c3eec61 --- /dev/null +++ b/regression/goto-harness/function_pointer_nullable/test.c @@ -0,0 +1,18 @@ +#include +#include + +typedef int (*fptr_t)(void); + +void entry_point(fptr_t f, fptr_t f_but_may_be_null) +{ + assert(f != (void *)0); // expected to succeed + assert(f == (void *)0); // expected to fail + assert(f_but_may_be_null != (void *)0); // expected to fail + assert(f_but_may_be_null == (void *)0); // expected to fail + assert(f_but_may_be_null == (void *)0 || f() == f_but_may_be_null()); +} + +int f(void) +{ + return 42; +} diff --git a/regression/goto-harness/function_pointer_nullable/test.desc b/regression/goto-harness/function_pointer_nullable/test.desc new file mode 100644 index 00000000000..f943099b772 --- /dev/null +++ b/regression/goto-harness/function_pointer_nullable/test.desc @@ -0,0 +1,12 @@ +CORE +test.c +--harness-type call-function --function entry_point --function-pointer-can-be-null __goto_harness::f_but_may_be_null +^EXIT=10$ +^SIGNAL=0$ +\[entry_point.assertion.1\] line \d+ assertion f != \(void \*\)0: SUCCESS +\[entry_point.assertion.2\] line \d+ assertion f == \(void \*\)0: FAILURE +\[entry_point.assertion.3\] line \d+ assertion f_but_may_be_null != \(void \*\)0: FAILURE +\[entry_point.assertion.4\] line \d+ assertion f_but_may_be_null == \(void \*\)0: FAILURE +\[entry_point.assertion.5\] line \d+ assertion f_but_may_be_null == \(void \*\)0 || f\(\) == f_but_may_be_null\(\): SUCCESS +-- +^warning: ignoring diff --git a/src/goto-harness/common_harness_generator_options.h b/src/goto-harness/common_harness_generator_options.h index 844309f59b3..9a4c396133d 100644 --- a/src/goto-harness/common_harness_generator_options.h +++ b/src/goto-harness/common_harness_generator_options.h @@ -14,6 +14,8 @@ Author: Diffblue Ltd. "max-nondet-tree-depth" #define COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "min-array-size" #define COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "max-array-size" +#define COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT \ + "function-pointer-can-be-null" // clang-format off #define COMMON_HARNESS_GENERATOR_OPTIONS \ @@ -21,6 +23,7 @@ Author: Diffblue Ltd. "(" COMMON_HARNESS_GENERATOR_MAX_NONDET_TREE_DEPTH_OPT "):" \ "(" COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT "):" \ "(" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT "):" \ + "(" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT "):" \ // COMMON_HARNESS_GENERATOR_OPTIONS // clang-format on @@ -39,6 +42,9 @@ Author: Diffblue Ltd. "--" COMMON_HARNESS_GENERATOR_MAX_ARRAY_SIZE_OPT \ " N maximum size of dynamically created arrays\n" \ " (default: 2)\n" \ + "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT \ + " , name of the function(s) pointer parameters\n" \ + " that can be NULL pointing." // COMMON_HARNESS_GENERATOR_HELP // clang-format on diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index 69727daa648..9b3b54768f1 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -173,6 +173,18 @@ void function_call_harness_generatort::handle_option( { p_impl->recursive_initialization_config.arguments_may_be_equal = true; } + else if(option == COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT) + { + std::transform( + values.begin(), + values.end(), + std::inserter( + p_impl->recursive_initialization_config + .potential_null_function_pointers, + p_impl->recursive_initialization_config.potential_null_function_pointers + .end()), + [](const std::string &opt) -> irep_idt { return irep_idt{opt}; }); + } else { throw invalid_command_line_argument_exceptiont{ diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index 6de65fb5d39..033622a4a35 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -187,7 +187,8 @@ code_blockt recursive_initializationt::build_constructor_body( const exprt &depth_symbol, const symbol_exprt &result_symbol, const optionalt &size_symbol, - const optionalt &lhs_name) + const optionalt &lhs_name, + const bool is_nullable) { PRECONDITION(result_symbol.type().id() == ID_pointer); const typet &type = result_symbol.type().subtype(); @@ -197,6 +198,10 @@ code_blockt recursive_initializationt::build_constructor_body( } else if(type.id() == ID_pointer) { + if(type.subtype().id() == ID_code) + { + return build_function_pointer_constructor(result_symbol, is_nullable); + } if(lhs_name.has_value()) { if(should_be_treated_as_cstring(*lhs_name) && type == char_type()) @@ -231,17 +236,23 @@ irep_idt recursive_initializationt::build_constructor(const exprt &expr) // void type_constructor_T(int depth_T, T *result_T, int *size); optionalt size_var; optionalt expr_name; + bool is_nullable = false; + bool has_size_param = false; if(expr.id() == ID_symbol) { expr_name = to_symbol_expr(expr).get_identifier(); + is_nullable = initialization_config.potential_null_function_pointers.count( + expr_name.value()); if(should_be_treated_as_array(*expr_name)) { size_var = get_associated_size_variable(*expr_name); + has_size_param = true; } } const typet &type = expr.type(); - if(type_constructor_names.find(type) != type_constructor_names.end()) - return type_constructor_names[type]; + const constructor_keyt key{type, is_nullable, has_size_param}; + if(type_constructor_names.find(key) != type_constructor_names.end()) + return type_constructor_names[key]; const std::string &pretty_type = type2id(type); symbolt &depth_symbol = @@ -282,7 +293,7 @@ irep_idt recursive_initializationt::build_constructor(const exprt &expr) } const symbolt &function_symbol = get_fresh_fun_symbol( "type_constructor_" + pretty_type, code_typet{fun_params, empty_typet{}}); - type_constructor_names[type] = function_symbol.name; + type_constructor_names[key] = function_symbol.name; symbolt *mutable_symbol = symbol_table.get_writeable(function_symbol.name); // the body is specific for each type of expression @@ -292,11 +303,12 @@ irep_idt recursive_initializationt::build_constructor(const exprt &expr) size_symbol_expr, // the expression name may be needed to decide if expr should be treated as // a string - expr_name); + expr_name, + is_nullable); goto_model.goto_functions.function_map[function_symbol.name].type = to_code_type(function_symbol.type); - return type_constructor_names[type]; + return type_constructor_names.at(key); } symbol_exprt recursive_initializationt::get_malloc_function() @@ -877,3 +889,58 @@ void recursive_initializationt::free_cluster_origins(code_blockt &body) body.add(code_function_callt{get_free_function(), {*origin}}); } } + +code_blockt recursive_initializationt::build_function_pointer_constructor( + const symbol_exprt &result, + bool is_nullable) +{ + PRECONDITION(can_cast_type(result.type())); + const auto &result_type = to_pointer_type(result.type()); + PRECONDITION(can_cast_type(result_type.subtype())); + const auto &function_pointer_type = to_pointer_type(result_type.subtype()); + PRECONDITION(can_cast_type(function_pointer_type.subtype())); + const auto &function_type = to_code_type(function_pointer_type.subtype()); + + std::vector targets; + + for(const auto &sym : goto_model.get_symbol_table()) + { + if(sym.second.type == function_type) + { + targets.push_back(address_of_exprt{sym.second.symbol_expr()}); + } + } + + if(is_nullable) + targets.push_back(null_pointer_exprt{function_pointer_type}); + + code_blockt body{}; + + const auto function_pointer_selector = + get_fresh_local_symexpr("function_pointer_selector"); + body.add( + code_assignt{function_pointer_selector, + side_effect_expr_nondett{function_pointer_selector.type(), + source_locationt{}}}); + auto function_pointer_index = std::size_t{0}; + + for(const auto &target : targets) + { + auto const assign = code_assignt{dereference_exprt{result}, target}; + if(function_pointer_index != targets.size() - 1) + { + auto const condition = equal_exprt{ + function_pointer_selector, + from_integer(function_pointer_index, function_pointer_selector.type())}; + auto const then = code_blockt{{assign, code_returnt{}}}; + body.add(code_ifthenelset{condition, then}); + } + else + { + body.add(assign); + } + ++function_pointer_index; + } + + return body; +} diff --git a/src/goto-harness/recursive_initialization.h b/src/goto-harness/recursive_initialization.h index ef92643a4c7..725fec9efdf 100644 --- a/src/goto-harness/recursive_initialization.h +++ b/src/goto-harness/recursive_initialization.h @@ -27,6 +27,7 @@ struct recursive_initialization_configt std::size_t min_null_tree_depth = 1; std::size_t max_nondet_tree_depth = 2; irep_idt mode; + std::unordered_set potential_null_function_pointers; // array stuff std::size_t max_dynamic_array_size = 2; @@ -59,8 +60,30 @@ class recursive_initializationt { public: using recursion_sett = std::set; - using type_constructor_namest = std::map; using equal_cluster_idt = std::size_t; + struct constructor_keyt + { + typet constructor_type; + bool is_nullable; + bool has_size_parameter; + bool operator<(const constructor_keyt &other) const + { + return std::tie(constructor_type, is_nullable, has_size_parameter) < + std::tie( + other.constructor_type, + other.is_nullable, + other.has_size_parameter); + }; + bool operator==(const constructor_keyt &other) const + { + return std::tie(constructor_type, is_nullable, has_size_parameter) == + std::tie( + other.constructor_type, + other.is_nullable, + other.has_size_parameter); + }; + }; + using type_constructor_namest = std::map; recursive_initializationt( recursive_initialization_configt initialization_config, @@ -170,12 +193,14 @@ class recursive_initializationt /// \param result_symbol: the symbol for `result` parameter /// \param size_symbol: maybe the symbol for `size` parameter /// \param lhs_name: the name of the original symbol + /// \param is_nullable: flag for setting a function pointer nullable /// \return the body of the constructor code_blockt build_constructor_body( const exprt &depth_symbol, const symbol_exprt &result_symbol, const optionalt &size_symbol, - const optionalt &lhs_name); + const optionalt &lhs_name, + const bool is_nullable); /// Check if a constructor for the type of \p expr already exists and create /// it if not. @@ -183,6 +208,14 @@ class recursive_initializationt /// \return name of the constructor function irep_idt build_constructor(const exprt &expr); + /// Constructor for function pointers. + /// \param result: symbol of the result parameter + /// \param is_nullable: if the function pointer can be null + /// \return the body of the constructor + code_blockt build_function_pointer_constructor( + const symbol_exprt &result, + bool is_nullable); + /// Generic constructor for all pointers: only builds one pointee (not an /// array) but may recourse in case the pointee contains more pointers, e.g. /// a struct. From 8266009f3ad508055242e8756303e2018c219558 Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Mon, 11 Nov 2019 16:56:58 +0000 Subject: [PATCH 3/5] Map function pointer parameter to function pointer argument Add mapping from function pointer argument names to local variable names of the harness so users can specify properties of arguments in terms of the names of the arguments rather than having to rely on internal implementation details of the function harness. --- .../function_pointer_nullable/test.desc | 2 +- .../function_call_harness_generator.cpp | 72 +++++++++++++++++++ 2 files changed, 73 insertions(+), 1 deletion(-) diff --git a/regression/goto-harness/function_pointer_nullable/test.desc b/regression/goto-harness/function_pointer_nullable/test.desc index f943099b772..659a84a28c5 100644 --- a/regression/goto-harness/function_pointer_nullable/test.desc +++ b/regression/goto-harness/function_pointer_nullable/test.desc @@ -1,6 +1,6 @@ CORE test.c ---harness-type call-function --function entry_point --function-pointer-can-be-null __goto_harness::f_but_may_be_null +--harness-type call-function --function entry_point --function-pointer-can-be-null entry_point::f_but_may_be_null ^EXIT=10$ ^SIGNAL=0$ \[entry_point.assertion.1\] line \d+ assertion f != \(void \*\)0: SUCCESS diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index 9b3b54768f1..d07f07c9a7e 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -12,6 +12,7 @@ Author: Diffblue Ltd. #include #include #include +#include #include #include #include @@ -80,6 +81,16 @@ struct function_call_harness_generatort::implt void call_function( const code_function_callt::argumentst &arguments, code_blockt &function_body); + /// For function parameters that are pointers to functions we want to + /// be able to specify whether or not they can be NULL. To disambiguate + /// this specification from that for a global variable of the same name, + /// we prepend the name of the function to the parameter name. However, + /// what is actually being initialised in the implementation is not the + /// parameter itself, but a corresponding function argument (local variable + /// of the harness function). We need a mapping from function parameter + /// name to function argument names, and this is what this function does. + std::unordered_set + map_function_parameters_to_function_argument_names(); }; function_call_harness_generatort::function_call_harness_generatort( @@ -226,6 +237,8 @@ void function_call_harness_generatort::implt::generate( recursive_initialization_config.variables_that_hold_array_sizes.insert( pair.second); } + recursive_initialization_config.potential_null_function_pointers = + map_function_parameters_to_function_argument_names(); recursive_initialization_config.pointers_to_treat_as_cstrings = function_arguments_to_treat_as_cstrings; recursive_initialization = util_make_unique( @@ -346,6 +359,43 @@ void function_call_harness_generatort::validate_options( } } } + + const namespacet ns{goto_model.symbol_table}; + + // Make sure all function pointers that the user asks are nullable are + // present in the symbol table. + for(const auto &nullable : + p_impl->recursive_initialization_config.potential_null_function_pointers) + { + const auto &function_pointer_symbol_pointer = + goto_model.symbol_table.lookup(nullable); + + if(function_pointer_symbol_pointer == nullptr) + { + throw invalid_command_line_argument_exceptiont{ + "nullable function pointer `" + id2string(nullable) + + "' not found in symbol table", + "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT}; + } + + const auto &function_pointer_type = + ns.follow(function_pointer_symbol_pointer->type); + + if(!can_cast_type(function_pointer_type)) + { + throw invalid_command_line_argument_exceptiont{ + "`" + id2string(nullable) + "' is not a pointer", + "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT}; + } + + if(!can_cast_type( + to_pointer_type(function_pointer_type).subtype())) + { + throw invalid_command_line_argument_exceptiont{ + "`" + id2string(nullable) + "' is not pointing to a function", + "--" COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT}; + } + } } const symbolt & @@ -490,3 +540,25 @@ void function_call_harness_generatort::implt::call_function( function_body.add(std::move(function_call)); } + +std::unordered_set function_call_harness_generatort::implt:: + map_function_parameters_to_function_argument_names() +{ + std::unordered_set nullables; + for(const auto &nullable : + recursive_initialization_config.potential_null_function_pointers) + { + const auto &nullable_name = id2string(nullable); + const auto &function_prefix = id2string(function) + "::"; + if(has_prefix(nullable_name, function_prefix)) + { + nullables.insert( + "__goto_harness::" + nullable_name.substr(function_prefix.size())); + } + else + { + nullables.insert(nullable_name); + } + } + return nullables; +} From 6eb59903cd52a4ce0421db6b6faa6a858b10575c Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 12 Nov 2019 15:11:14 +0000 Subject: [PATCH 4/5] Add more tests. Add a test to make sure that we can distinguish between a parameter and a global function pointer variable with the same name and a test to make sure that we get different type constructors for the same type but with extra attributes. --- .../goto-harness/mixed-constructors/test.c | 5 +++++ .../goto-harness/mixed-constructors/test.desc | 8 ++++++++ .../test.c | 18 ++++++++++++++++++ .../test.desc | 10 ++++++++++ 4 files changed, 41 insertions(+) create mode 100644 regression/goto-harness/mixed-constructors/test.c create mode 100644 regression/goto-harness/mixed-constructors/test.desc create mode 100644 regression/goto-harness/parameter_and_global_variable_distinction/test.c create mode 100644 regression/goto-harness/parameter_and_global_variable_distinction/test.desc diff --git a/regression/goto-harness/mixed-constructors/test.c b/regression/goto-harness/mixed-constructors/test.c new file mode 100644 index 00000000000..c820829edc6 --- /dev/null +++ b/regression/goto-harness/mixed-constructors/test.c @@ -0,0 +1,5 @@ +void entry_point(int *array_with_size, int size, int *array_without_size) +{ + assert(array_with_size != (void *)0); + assert(array_with_size != (void *)0); +} diff --git a/regression/goto-harness/mixed-constructors/test.desc b/regression/goto-harness/mixed-constructors/test.desc new file mode 100644 index 00000000000..4c21c51d75e --- /dev/null +++ b/regression/goto-harness/mixed-constructors/test.desc @@ -0,0 +1,8 @@ +CORE +test.c +--function entry_point --harness-type call-function --associated-array-size array_with_size:size +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +call to '\w+': not enough arguments, inserting non-deterministic value diff --git a/regression/goto-harness/parameter_and_global_variable_distinction/test.c b/regression/goto-harness/parameter_and_global_variable_distinction/test.c new file mode 100644 index 00000000000..687549bfcff --- /dev/null +++ b/regression/goto-harness/parameter_and_global_variable_distinction/test.c @@ -0,0 +1,18 @@ +#include + +typedef int (*fptr_t)(void); + +fptr_t f; + +int call_f() +{ + assert(f != ((void *)0)); + return f(); +} + +void function(fptr_t f) +{ + if(f != ((void *)0)) + assert(f() == call_f()); + assert(f != ((void *)0)); +} diff --git a/regression/goto-harness/parameter_and_global_variable_distinction/test.desc b/regression/goto-harness/parameter_and_global_variable_distinction/test.desc new file mode 100644 index 00000000000..f5e5c464a1d --- /dev/null +++ b/regression/goto-harness/parameter_and_global_variable_distinction/test.desc @@ -0,0 +1,10 @@ +CORE +test.c +--harness-type call-function --function function --function-pointer-can-be-null function::f +^EXIT=10$ +^SIGNAL=0$ +\[function.assertion.1\] line \d+ assertion f\(\) == call_f\(\): SUCCESS +\[function.assertion.2\] line \d+ assertion f != \(\(void \*\)0\): FAILURE +\[call_f.assertion.1\] line \d+ assertion f != \(\(void \*\)0\): SUCCESS +-- +^warning: ignoring From 6b684f7866c96c3a17ca3cb3696c5812de22299e Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 12 Nov 2019 16:22:15 +0000 Subject: [PATCH 5/5] Move function-pointer-can-be-null option handling. Move it to recursive_initialization_configt because it's a common option. --- src/goto-harness/function_call_harness_generator.cpp | 12 ++++++++++++ src/goto-harness/recursive_initialization.cpp | 12 ++++++++++++ 2 files changed, 24 insertions(+) diff --git a/src/goto-harness/function_call_harness_generator.cpp b/src/goto-harness/function_call_harness_generator.cpp index d07f07c9a7e..ff8728adcc1 100644 --- a/src/goto-harness/function_call_harness_generator.cpp +++ b/src/goto-harness/function_call_harness_generator.cpp @@ -196,6 +196,18 @@ void function_call_harness_generatort::handle_option( .end()), [](const std::string &opt) -> irep_idt { return irep_idt{opt}; }); } + else if(option == COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT) + { + std::transform( + values.begin(), + values.end(), + std::inserter( + p_impl->recursive_initialization_config + .potential_null_function_pointers, + p_impl->recursive_initialization_config.potential_null_function_pointers + .end()), + [](const std::string &opt) -> irep_idt { return irep_idt{opt}; }); + } else { throw invalid_command_line_argument_exceptiont{ diff --git a/src/goto-harness/recursive_initialization.cpp b/src/goto-harness/recursive_initialization.cpp index 033622a4a35..2ba446def5b 100644 --- a/src/goto-harness/recursive_initialization.cpp +++ b/src/goto-harness/recursive_initialization.cpp @@ -21,6 +21,7 @@ Author: Diffblue Ltd. #include #include +#include bool recursive_initialization_configt::handle_option( const std::string &option, @@ -74,6 +75,17 @@ bool recursive_initialization_configt::handle_option( COMMON_HARNESS_GENERATOR_MIN_ARRAY_SIZE_OPT, values); return true; } + else if(option == COMMON_HARNESS_GENERATOR_FUNCTION_POINTER_CAN_BE_NULL_OPT) + { + std::transform( + values.begin(), + values.end(), + std::inserter( + potential_null_function_pointers, + potential_null_function_pointers.end()), + [](const std::string &opt) -> irep_idt { return irep_idt{opt}; }); + return true; + } return false; }