Extract function pointers using memory analyzer

regression/snapshot-harness/function_pointer_01/main.c

@@ -0,0 +1,28 @@
+#include <assert.h>
+
+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;
+}

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

regression/snapshot-harness/function_pointer_02/main.c

@@ -0,0 +1,37 @@
+#include <assert.h>
+
+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 = &plus;
+  fun_ptr2 = &minus;
+}
+
+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;
+}

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

regression/snapshot-harness/function_pointer_03/main.c

@@ -0,0 +1,42 @@
+#include <assert.h>
+
+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] = &plus;
+  fun_array[1] = &minus;
+  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;
+}

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

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,20 +545,20 @@ 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
     if(target_expr.type() == zero_expr.type())
       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;

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: