From 41a7af62caa2947ae6d6ac237704bb6cbc07b8a6 Mon Sep 17 00:00:00 2001 From: xbauch Date: Fri, 7 Jun 2019 11:31:25 +0100 Subject: [PATCH 1/2] Implement extracting function pointers By simply grabbing the pointee name from gdb (which is the function name) and returning the associated symbol expression. --- src/memory-analyzer/analyze_symbol.cpp | 44 ++++++++++++++++++++++---- src/memory-analyzer/analyze_symbol.h | 12 +++++++ 2 files changed, 50 insertions(+), 6 deletions(-) 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: From 8941f724bf7bc5776e4da494e4b66dcf9fe11434 Mon Sep 17 00:00:00 2001 From: xbauch Date: Fri, 7 Jun 2019 11:31:45 +0100 Subject: [PATCH 2/2] Regression tests for function pointers 1. one function one pointer 2. two functions two pointers, check they point to the right ones 3. two functions, array of function pointers, pointers initialised from the array --- .../function_pointer_01/main.c | 28 +++++++++++++ .../function_pointer_01/test.desc | 11 +++++ .../function_pointer_02/main.c | 37 ++++++++++++++++ .../function_pointer_02/test.desc | 13 ++++++ .../function_pointer_03/main.c | 42 +++++++++++++++++++ .../function_pointer_03/test.desc | 13 ++++++ 6 files changed, 144 insertions(+) create mode 100644 regression/snapshot-harness/function_pointer_01/main.c create mode 100644 regression/snapshot-harness/function_pointer_01/test.desc create mode 100644 regression/snapshot-harness/function_pointer_02/main.c create mode 100644 regression/snapshot-harness/function_pointer_02/test.desc create mode 100644 regression/snapshot-harness/function_pointer_03/main.c create mode 100644 regression/snapshot-harness/function_pointer_03/test.desc 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