Extract function pointers using memory analyzer #4730

xbauch · 2019-05-30T07:33:16Z

This PR adds the facilities to query GDB via memory-analyzer to obtain information about function pointers. The values of function pointers can then be extracted into a symbol table and reused, e.g. by goto-harness.

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

hannes-steffenhagen-diffblue

Seems reasonable to me (modulo note on error handling) (probably needs a rebase due to changes in cbmc that broke/fixed/broke/fixed again CI.

hannes-steffenhagen-diffblue · 2019-06-05T14:55:28Z

src/memory-analyzer/analyze_symbol.cpp

+  const auto &function_name = pointer_value.pointee;
+  CHECK_RETURN(!function_name.empty());
+  const auto function_symbol = symbol_table.lookup(function_name);
+  CHECK_RETURN(function_symbol != nullptr);


this should be causing a runtime error instead of us asserting this is true; In practical programs it's very possible for this to happen.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 64e9fdb).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/114620019

codecov-io · 2019-06-06T16:47:34Z

Codecov Report

❗ No coverage uploaded for pull request base (develop@891f04e). Click here to learn what that means.
The diff coverage is 94.44%.

@@            Coverage Diff             @@
##             develop    #4730   +/-   ##
==========================================
  Coverage           ?   68.51%           
==========================================
  Files              ?     1275           
  Lines              ?   105032           
  Branches           ?        0           
==========================================
  Hits               ?    71958           
  Misses             ?    33074           
  Partials           ?        0

Impacted Files	Coverage Δ
src/memory-analyzer/analyze_symbol.h	`90% <ø> (ø)`
src/memory-analyzer/analyze_symbol.cpp	`90.93% <94.44%> (ø)`

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 891f04e...8941f72. Read the comment docs.

tautschnig · 2019-06-07T10:03:47Z

src/memory-analyzer/analyze_symbol.cpp

+    {
+      const auto target_expr =
+        get_pointer_to_function_value(expr, value, location);
+      CHECK_RETURN(target_expr.id() != ID_nil);


Although equivalent, I'd prefer target_expr.is_not_nil()

tautschnig · 2019-06-07T10:05:09Z

src/memory-analyzer/analyze_symbol.cpp

+      const auto target_expr =
+        get_pointer_to_function_value(expr, value, location);
+      CHECK_RETURN(target_expr.id() != ID_nil);
+      const auto result_expr = address_of_exprt(target_expr);


I'd use either exprt result_expr = ... or address_of_exprt result_expr{target_expr}; (see below for more).

I went for the address_of_exprt and then std::move.

tautschnig · 2019-06-07T10:06:13Z

src/memory-analyzer/analyze_symbol.cpp

+      CHECK_RETURN(target_expr.id() != ID_nil);
+      const auto result_expr = address_of_exprt(target_expr);
+      CHECK_RETURN(result_expr.type() == zero_expr.type());
+      return result_expr;


This needs to be return std::move(result_expr); if you use address_of_exprt above, or can stay as-is if using exprt result_expr = .... I'd say this is a case where auto above really hurts you, because it hides a lot of this.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: a71e426).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/114723581

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 420e334).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/114734689

By simply grabbing the pointee name from gdb (which is the function name) and returning the associated symbol expression.

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

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 8941f72).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/114902696

xbauch changed the title ~~Extract function pointers using memory analyzer~~ Extract function pointers using memory analyzer [depends-on: #4578] May 30, 2019

xbauch added the dependent - do not merge label May 30, 2019

xbauch force-pushed the feature/gdb-function-pointers branch from ab9c7be to ac5dee2 Compare May 30, 2019 11:17

xbauch changed the title ~~Extract function pointers using memory analyzer [depends-on: #4578]~~ Extract function pointers using memory analyzer May 30, 2019

xbauch removed the dependent - do not merge label May 30, 2019

hannes-steffenhagen-diffblue approved these changes Jun 5, 2019

View reviewed changes

xbauch force-pushed the feature/gdb-function-pointers branch from ac5dee2 to de53ece Compare June 6, 2019 15:39

xbauch marked this pull request as ready for review June 6, 2019 15:39

xbauch requested review from chrisr-diffblue, kroening, peterschrammel, smowton and tautschnig as code owners June 6, 2019 15:39

xbauch force-pushed the feature/gdb-function-pointers branch from de53ece to 64e9fdb Compare June 6, 2019 15:56

allredj reviewed Jun 6, 2019

View reviewed changes

peterschrammel assigned xbauch Jun 7, 2019

tautschnig approved these changes Jun 7, 2019

View reviewed changes

xbauch force-pushed the feature/gdb-function-pointers branch from 64e9fdb to a71e426 Compare June 7, 2019 10:32

allredj reviewed Jun 7, 2019

View reviewed changes

xbauch force-pushed the feature/gdb-function-pointers branch from a71e426 to 420e334 Compare June 7, 2019 12:18

allredj reviewed Jun 7, 2019

View reviewed changes

petr-bauch added 2 commits June 10, 2019 08:04

Implement extracting function pointers

41a7af6

By simply grabbing the pointee name from gdb (which is the function name) and returning the associated symbol expression.

Regression tests for function pointers

8941f72

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

xbauch force-pushed the feature/gdb-function-pointers branch from 420e334 to 8941f72 Compare June 10, 2019 07:04

allredj reviewed Jun 10, 2019

View reviewed changes

xbauch merged commit 09cf08d into diffblue:develop Jun 10, 2019

xbauch deleted the feature/gdb-function-pointers branch June 10, 2019 12:29

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Extract function pointers using memory analyzer #4730

Extract function pointers using memory analyzer #4730

xbauch commented May 30, 2019 •

edited

Loading

hannes-steffenhagen-diffblue left a comment •

edited

Loading

hannes-steffenhagen-diffblue Jun 5, 2019

xbauch Jun 6, 2019

allredj left a comment

codecov-io commented Jun 6, 2019 •

edited

Loading

tautschnig Jun 7, 2019

xbauch Jun 7, 2019

tautschnig Jun 7, 2019

xbauch Jun 7, 2019

tautschnig Jun 7, 2019

allredj left a comment

allredj left a comment

allredj left a comment

Extract function pointers using memory analyzer #4730

Extract function pointers using memory analyzer #4730

Conversation

xbauch commented May 30, 2019 • edited Loading

hannes-steffenhagen-diffblue left a comment • edited Loading

Choose a reason for hiding this comment

hannes-steffenhagen-diffblue Jun 5, 2019

Choose a reason for hiding this comment

xbauch Jun 6, 2019

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

codecov-io commented Jun 6, 2019 • edited Loading

Codecov Report

tautschnig Jun 7, 2019

Choose a reason for hiding this comment

xbauch Jun 7, 2019

Choose a reason for hiding this comment

tautschnig Jun 7, 2019

Choose a reason for hiding this comment

xbauch Jun 7, 2019

Choose a reason for hiding this comment

tautschnig Jun 7, 2019

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

xbauch commented May 30, 2019 •

edited

Loading

hannes-steffenhagen-diffblue left a comment •

edited

Loading

codecov-io commented Jun 6, 2019 •

edited

Loading