Refactor and add documentation for mmio goto-program pass
#7553
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
In order to make the naming pattern easier to spot.
To make it clear that they are not mutated.
This ensures that the variable is only in scope when it is non-null.
To reduce indentation and make it clear that this check filters which instructions the loop operates on.
This removes the need for an excessively vebose type, matches C++11 style and is suggested by clang-tidy.
So that there is an overview of the algorithm used and so that the relevant markdown file about the related feature is more easily discoverable.
This helps make it clearer that the dereference writes operation considers only a single write per assignment, rather than a set of writes.
This allows for `deref_expr_r` to be made constant, which makes it clear that the set is rebuilt for each assign instruction and is built in one place only. This also makes it clear that the result of the `collect_deref_expr` function is its return value. There is no performance cost to this refactor as Return Value Optimization (RVO) applies in this case.
This makes it clear from reading the `.cpp` file only that this function is not part of the external API and is used within this file only.
thomasspriggs
requested review from
kroening,
tautschnig and
peterschrammel
as code owners
peterschrammel
approved these changes
Feb 22, 2023
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR refactors and documents the
mmiogoto-program pass. I found it to be non-trivial to get an overview of what this transformation pass was doing to the goto-program. The refactoring and documentation in this PR is that which I carried out in order to further my own understanding. This PR is not intended to include any bugfixes or additional functionality, nor am I planning to carry out such work in the near future.The functionality implemented in the
mmiopass is tested by theregression/cbmc/mm_io1test. I suggest that reviewers review commit by commit as every step-wise refactor is in its own commit, with justification in the commit body. So it should be easier to see that there are no functional changes based on the individual commits rather than reading the change set of PR as a whole.