Skip to content

Separate collecting function pointer targets [alternative-to: #4536] #4650

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 35 commits into from

Conversation

xbauch
Copy link
Contributor

@xbauch xbauch commented May 13, 2019

The goal is similar to that of #4536 but here we physically separate the collection from remove-function-pointers into a stand-alone module.

Similarly to #4536: remove returns analysis is no longer depended on remove-function-pointers but the later can produce more efficient GOTO, e.g. in case the remove-const-function-pointer analysis was precise (result was exactly one target).

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

Petr Bauch and others added 30 commits May 13, 2019 13:09
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.
Only the interface, without definition of methods.
That is is_type_compatible and arg_is_type_compatible. Make the later two static
as well.
and make static.
By first initialising the taken-addresses and type-map and then re-using the
get_function_pointer_targets interface.
By re-using the get_function_pointer_targets over goto-model. Also since the
result is now stateful-targets we also merge the intermediate states.
By re-using the origin implementation. The state-flags are renamed:
does_remove_const_success -> code_removes_const
by re-using the original. State flag is renamed here:
only_remove_const_function_pointers_called -> precise_const_removal
that takes the possible-fp-targets-map. The call-operator is also extended.
to take targets-map and call remove_function_pointer with the right
stateful_target.
to take stateful-targets and extract the state from it.
in remove-function-pointers.
in remove-function-pointers implementation.
as a re-name for possible_fp_targetst.
@tautschnig
Copy link
Collaborator

Is there any chance to get this in smaller doses? The overarching idea of this PR seems great to me, but 35 commits and/or +1,379 −398 changed lines is quite scary I have to admit. Or maybe an explanation as to why it has to be this large? And then just the initial look at the overall diff made me wonder why adding message handlers was a necessary part of this change. I'll certainly bite the bullet if it needs to be this big, but if there is a good way to break it up then I'd appreciate this.

@xbauch
Copy link
Contributor Author

xbauch commented May 15, 2019

@tautschnig Splitting in would not be a problem but I think @kroening should first decide if the end-result is something we should aim for in the first place.

@TGWDB
Copy link
Contributor

TGWDB commented Aug 1, 2022

Closing due to age and draft status. 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.

6 participants