Skip to content

Interface for collecting function pointer targets #4536

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 18 commits into from

Conversation

xbauch
Copy link
Contributor

@xbauch xbauch commented Apr 15, 2019

Motivation: we want remove_returns to work even if not preceded by remove_function_pointers. For example:

int (* const fptbl2[])(void) = {g1, g2};

int func(int id1)
{
  t = fptbl2[id1];  // for this instruction the set is {"g1", "g2"}
  return t;
}

This PR exposes the function-pointer-target-collecting part of remove_function_pointers to be used in other analyses and the does so in remove_returns.

In remove_returns use the possible_fp_targets_map to be able to remove returns for calls to function pointers. CALL x=*fp() should become CALL *fp(); ASSIGN x = (fp == &f00) ? return_value_f00 : (fp == &f01) ? ....

The first 3 commits are refactoring/preparation. The fourth introduces the interface. The fifth implements the new do_function_call for function pointers.

Then we refactor the remove_function_pointers to extract the collect-candidate-functions part and separate the modify-function-call part.

Finally -- now that the file is open -- we also refactor the internal remove_function_pointers without any functional change.

  • 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.

@xbauch xbauch force-pushed the feature/remove-return-fp-mod branch from 4bebc52 to 240fcda Compare April 15, 2019 16:34
@xbauch xbauch force-pushed the feature/remove-return-fp-mod branch 5 times, most recently from 434e869 to 715ee95 Compare April 16, 2019 08:58
@xbauch xbauch force-pushed the feature/remove-return-fp-mod branch 2 times, most recently from 7853563 to d9c92a0 Compare April 16, 2019 13:09
@xbauch xbauch marked this pull request as ready for review April 16, 2019 13:28
@xbauch xbauch force-pushed the feature/remove-return-fp-mod branch from f54b052 to 6a410e5 Compare April 16, 2019 14:11
@xbauch xbauch force-pushed the feature/remove-return-fp-mod branch 3 times, most recently from 101bf06 to e0f1172 Compare April 17, 2019 09:14
Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 101bf06).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108667731
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

Copy link
Contributor

@allredj allredj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: e0f1172).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/108669241
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

@xbauch xbauch force-pushed the feature/remove-return-fp-mod branch from e0f1172 to 327099a Compare April 29, 2019 09:52
@xbauch xbauch force-pushed the feature/remove-return-fp-mod branch 2 times, most recently from 74584f8 to 81b2a4c Compare May 11, 2019 09:52
@tautschnig
Copy link
Collaborator

@kroening @xbauch Is there an ongoing conversation to align the changes the two of you are working on?

@xbauch
Copy link
Contributor Author

xbauch commented May 11, 2019

@tautschnig Well, there is a conversation. @kroening raised the issue that with this PR's changes remove_return will effectively subsume remove_function_pointers.

@xbauch xbauch force-pushed the feature/remove-return-fp-mod branch from 81b2a4c to abedd92 Compare May 12, 2019 08:35
Petr Bauch and others added 17 commits May 12, 2019 09:42
Move the checks for is_function_call and does-return-anything outside; and
pre-compute the is_stub. do_function_call now always does something.
Also extract the common behaviour to do_function_calls.
The type and the function to return the map.
In case the function id is dereference we grab the set of possible targets (via
the possible_fp_targets_map) and pass it to the new do_function_call method.

There we build a cond_expr by iterating over the possible targets and adding a
case: (f==target ? target_return_value) to it. This cond_expr then becomes the
right-hand-side of the new assignment. We also have to dead all the return
values that were created, see https://github.com/martin-cs/ASVAT/issues/46.

Also building remove_function_pointerst requires messaget

And now so does remove_returnst, hence extending the call sites as well.
From remove_function_pointers to a separate function split into three:
1. get_funtion_pointer_targets .. the wrapper (for model/program)
2. refine_call_type .. for incomplete function types
3. try_remove_const_fp .. call remove_const_function_pointer

Then implement a wrapper that returns a map: function-name -> list-of-candidates
Using the new candidate-collecting function.
Introducing two new member function:
1. build_new_code .. wraps the collection of function calls and gotos
2. remove_function_pointer_log .. wraps the logging and statistics

Setting the location now takes place inside the loop over candidate functions:
there is no second loop over newly introduced gotos.
And correctly report the case when there are no targets.
so that message handler is not the first.
matching variant function pointer to a complete function.
from a function call expression.
on a per-callee basis. To prevent the state for one callee to be used when
removing pointers for another callee.
that takes the target map as argument.

To avoid duplication we also refactor the existing functions a bit.
will be squashed.
@xbauch xbauch force-pushed the feature/remove-return-fp-mod branch from abedd92 to 576b7ca Compare May 12, 2019 08:50
@xbauch
Copy link
Contributor Author

xbauch commented May 12, 2019

@martin-cs It was a good thing that you suggested a new interface taking the possible_function_targetst map because it turned out I wasn't collecting the function ids to index that map with correctly. I'm extracting them here: c048b5d. I also had to start keeping track of the state of the rfp on per-callee basis: 759b7f3.

will be squashed.
@xbauch
Copy link
Contributor Author

xbauch commented May 13, 2019

@martin-cs and @kroening I've put together an alternative implementation in #4650. It does the same thing but the collection of function pointers is completely separate from remove-function-pointers. I also describe there how remove-returns will differ from remove-function-pointers there. It share some commits to this PR so if you want to read it, I recommend starting here: 5a39535.

@martin-cs
Copy link
Collaborator

Perhaps it would be useful for me to say why this functionality was desirable. I would like to be able to run ait before function pointer removal. This seems doable and may even help us get down to just the one abstract interpretation framework. It will also allow more stateful analysis to produce more compact sets of possible function pointer candidates. However it would be good to keep function removal as a precondition for ait as otherwise we have to mimic the same effect in ait and that would be kind of daft.

@TGWDB
Copy link
Contributor

TGWDB commented Aug 1, 2022

Closing due to age. If you believe this is erroneous please reopen and update the PR.

@TGWDB TGWDB closed this Aug 1, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

8 participants