diff --git a/regression/snapshot-harness/function_pointer_01/main.c b/regression/snapshot-harness/function_pointer_01/main.c new file mode 100644 index 00000000000..c09357b1b3f --- /dev/null +++ b/regression/snapshot-harness/function_pointer_01/main.c @@ -0,0 +1,28 @@ +#include + +int foo(int i) +{ + return i + 1; +} + +int (*fun_ptr)(int); + +void initialize() +{ + fun_ptr = &foo; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(fun_ptr == &foo); + assert((*fun_ptr)(5) == 6); + assert((*fun_ptr)(5) == foo(5)); + return 0; +} diff --git a/regression/snapshot-harness/function_pointer_01/test.desc b/regression/snapshot-harness/function_pointer_01/test.desc new file mode 100644 index 00000000000..025c9ef29b1 --- /dev/null +++ b/regression/snapshot-harness/function_pointer_01/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +fun_ptr --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion fun_ptr == \&foo: SUCCESS +\[main.assertion.2\] line [0-9]+ assertion \(\*fun_ptr\)\(5\) == 6: SUCCESS +\[main.assertion.3\] line [0-9]+ assertion \(\*fun_ptr\)\(5\) == foo\(5\): SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/snapshot-harness/function_pointer_02/main.c b/regression/snapshot-harness/function_pointer_02/main.c new file mode 100644 index 00000000000..28a6fdd2b6b --- /dev/null +++ b/regression/snapshot-harness/function_pointer_02/main.c @@ -0,0 +1,37 @@ +#include + +int plus(int i) +{ + return i + 1; +} + +int minus(int i) +{ + return i - 1; +} + +int (*fun_ptr1)(int); +int (*fun_ptr2)(int); + +void initialize() +{ + fun_ptr1 = + + fun_ptr2 = − +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(fun_ptr1 == &plus); + assert((*fun_ptr1)(5) == 6); + assert((*fun_ptr1)(5) == plus(5)); + assert(fun_ptr2 != fun_ptr1); + assert((*fun_ptr2)(5) == 4); + return 0; +} diff --git a/regression/snapshot-harness/function_pointer_02/test.desc b/regression/snapshot-harness/function_pointer_02/test.desc new file mode 100644 index 00000000000..7fd5bdee7cc --- /dev/null +++ b/regression/snapshot-harness/function_pointer_02/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion fun_ptr1 == \&plus: SUCCESS +\[main.assertion.2\] line [0-9]+ assertion \(\*fun_ptr1\)\(5\) == 6: SUCCESS +\[main.assertion.3\] line [0-9]+ assertion \(\*fun_ptr1\)\(5\) == plus\(5\): SUCCESS +\[main.assertion.4\] line [0-9]+ assertion fun_ptr2 \!= fun_ptr1: SUCCESS +\[main.assertion.5\] line [0-9]+ assertion \(\*fun_ptr2\)\(5\) == 4: SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/regression/snapshot-harness/function_pointer_03/main.c b/regression/snapshot-harness/function_pointer_03/main.c new file mode 100644 index 00000000000..968a768ebf8 --- /dev/null +++ b/regression/snapshot-harness/function_pointer_03/main.c @@ -0,0 +1,42 @@ +#include + +int plus(int i) +{ + return i + 1; +} + +int minus(int i) +{ + return i - 1; +} + +typedef int (*fun_ptrt)(int); +fun_ptrt fun_array[2]; + +fun_ptrt fun_ptr1; +fun_ptrt fun_ptr2; + +void initialize() +{ + fun_array[0] = + + fun_array[1] = − + fun_ptr1 = *fun_array; + fun_ptr2 = fun_array[1]; +} + +void checkpoint() +{ +} + +int main() +{ + initialize(); + checkpoint(); + + assert(fun_ptr1 == &plus); + assert((*fun_ptr1)(5) == 6); + assert((*fun_ptr1)(5) == plus(5)); + assert(fun_ptr2 != fun_ptr1); + assert((*fun_ptr2)(5) == 4); + return 0; +} diff --git a/regression/snapshot-harness/function_pointer_03/test.desc b/regression/snapshot-harness/function_pointer_03/test.desc new file mode 100644 index 00000000000..cd66bd09c6d --- /dev/null +++ b/regression/snapshot-harness/function_pointer_03/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +fun_array,fun_ptr1,fun_ptr2 --harness-type initialise-with-memory-snapshot --initial-goto-location main:4 +^EXIT=0$ +^SIGNAL=0$ +\[main.assertion.1\] line [0-9]+ assertion fun_ptr1 == \&plus: SUCCESS +\[main.assertion.2\] line [0-9]+ assertion \(\*fun_ptr1\)\(5\) == 6: SUCCESS +\[main.assertion.3\] line [0-9]+ assertion \(\*fun_ptr1\)\(5\) == plus\(5\): SUCCESS +\[main.assertion.4\] line [0-9]+ assertion fun_ptr2 \!= fun_ptr1: SUCCESS +\[main.assertion.5\] line [0-9]+ assertion \(\*fun_ptr2\)\(5\) == 4: SUCCESS +VERIFICATION SUCCESSFUL +-- +^warning: ignoring diff --git a/src/memory-analyzer/analyze_symbol.cpp b/src/memory-analyzer/analyze_symbol.cpp index 3e874b28219..bb3fa1e830c 100644 --- a/src/memory-analyzer/analyze_symbol.cpp +++ b/src/memory-analyzer/analyze_symbol.cpp @@ -324,6 +324,27 @@ exprt gdb_value_extractort::get_pointer_to_member_value( return *maybe_member_expr; } +exprt gdb_value_extractort::get_pointer_to_function_value( + const exprt &expr, + const pointer_valuet &pointer_value, + const source_locationt &location) +{ + PRECONDITION(expr.type().id() == ID_pointer); + PRECONDITION(expr.type().subtype().id() == ID_code); + PRECONDITION(!pointer_value.address.is_null()); + + const auto &function_name = pointer_value.pointee; + CHECK_RETURN(!function_name.empty()); + const auto function_symbol = symbol_table.lookup(function_name); + if(function_symbol == nullptr) + { + throw invalid_source_file_exceptiont{ + "input source code does not contain function: " + function_name}; + } + CHECK_RETURN(function_symbol->type.id() == ID_code); + return function_symbol->symbol_expr(); +} + exprt gdb_value_extractort::get_non_char_pointer_value( const exprt &expr, const pointer_valuet &value, @@ -484,9 +505,20 @@ exprt gdb_value_extractort::get_pointer_value( const auto target_expr = get_pointer_to_member_value(expr, value, location); CHECK_RETURN(target_expr.is_not_nil()); - const auto result_expr = address_of_exprt(target_expr); + const address_of_exprt result_expr{target_expr}; + CHECK_RETURN(result_expr.type() == zero_expr.type()); + return std::move(result_expr); + } + + // pointer to function + if(expr.type().subtype().id() == ID_code) + { + const auto target_expr = + get_pointer_to_function_value(expr, value, location); + CHECK_RETURN(target_expr.is_not_nil()); + const address_of_exprt result_expr{target_expr}; CHECK_RETURN(result_expr.type() == zero_expr.type()); - return result_expr; + return std::move(result_expr); } // non-member: split for char/non-char @@ -513,9 +545,9 @@ exprt gdb_value_extractort::get_pointer_value( CHECK_RETURN(result_indexed_expr.has_value()); if(result_indexed_expr->type() == zero_expr.type()) return *result_indexed_expr; - const auto result_expr = address_of_exprt{*result_indexed_expr}; + const address_of_exprt result_expr{*result_indexed_expr}; CHECK_RETURN(result_expr.type() == zero_expr.type()); - return result_expr; + return std::move(result_expr); } // if the types match return right away @@ -523,10 +555,10 @@ exprt gdb_value_extractort::get_pointer_value( return target_expr; // otherwise the address of target should type-match - const auto result_expr = address_of_exprt(target_expr); + const address_of_exprt result_expr{target_expr}; if(result_expr.type() != zero_expr.type()) return typecast_exprt{result_expr, zero_expr.type()}; - return result_expr; + return std::move(result_expr); } return zero_expr; diff --git a/src/memory-analyzer/analyze_symbol.h b/src/memory-analyzer/analyze_symbol.h index d622d15fc72..15d4cb52796 100644 --- a/src/memory-analyzer/analyze_symbol.h +++ b/src/memory-analyzer/analyze_symbol.h @@ -286,6 +286,18 @@ class gdb_value_extractort const pointer_valuet &value, const source_locationt &location); + /// Extract the function name from \p pointer_value, check it has a symbol and + /// return the associated symbol expression + /// \param expr: the pointer-to-function expression + /// \param pointer_value: pointer value with the function name as the pointee + /// member + /// \param location: the source location + /// \return symbol expression for the function pointed at by \p pointer_value + exprt get_pointer_to_function_value( + const exprt &expr, + const pointer_valuet &pointer_value, + const source_locationt &location); + /// If \p memory_location is found among \ref values then return the symbol /// expression associated with it. /// Otherwise we add the appropriate \ref values mapping: