[depends: #708] Adding tests that check that simplify removes statements generated by FP removal #915
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
… domain operation.
…be picked independently.
The option string --show --intervals is more flexible, --show-intervals is now an alias.
Four additional regression tests are not expected to work at present which are now marked as FUTURE.
This includes skeleton code written by @martin-cs. Added hook for running the variable sensitivity Involved removing messaget inheritance since we require a zero parameter constructor for ai_baset Terminate correctly Made the domain correclty find the fixed point. The merge operation returns whether the merge actually changed any values by implementing a operator== for each of the abstract objects. Further, when merging a map, if a key is absent from one map then we remove it from the other unless the map is bottom. Adding handlers for the special types They are just stubs at the moment, returning top as we need the abstract objects that represent them. Updated interface for ai_domain_baset
Adding ==operator to the constant abstract value
These clasess will represent the basis for complex types with helper methods to read and write to/from them. They however will still be just a 2 element abstraction (top or bottom)
Made so the read returns a bottom element if it is bottom. Made the write return itself if true to faciliate sharing.
added 23 commits
May 16, 2017 13:32
In all cases the copy constructor was doing what the default copy constructor would do. Remove to avoid confusion
To improve readability, the map of lambdas is replaced with a chain of if else statements in both the eval and write methods.
I attempted to change this to generating a abstract object directly from the simplified expression. This caused the tests to fail in what appeared to be a "better" way - that is the constant_propagator tests were reporting more assignment simplifications. Specifically, it was simplifying the return of the function to be a NONDET(int) rather than the return of the function. I've convinced the change is wrong and works by chance, if we could some how have exprt with no children but wasn't a symbol, but also wasn't really a constant, then this would be wrong. The optimisation is also probably wrong since if the return assignment happened earlier, the return value should be the same, not a new non-det.
When we merge, we don't want to create a clone of the object if nothing changes as this reduces the ability of the sharing map to optimize. This simplifies the code for detecting whether a merge has changed anything, as we can compare the pointers, if they are pointing at the same thing, nothing has changed. It complicates the code for the merges as we need to be careful not to leak any abstract objects. We can't use the shared pointer wrapper as we want to be able to use the this pointer (unless we can use std::enable_shared_from_this?)
Modify the merge to return shared pointers by replacing returns of this with returns of `shared_from_this`. This simplifies the code for dealing with when need to modify the result in dervied classes as we are no longer responsible for freeing the pointer returned by the super class.
The base merge should always result in either top or bottom (it is up for dervied classes to clear the top flag if they are not top). Correctly use the base class merge when appropriate in merging constant values.
Refactored the merge maps method to use std::intersection as there was a bug with empty maps caught by the unit tests.
Use the CPROVER_assert as behaviour is consistent across platforms.
Removed some unnecessary debug information from the tests
In release builds, the top/bottom status of the enviroment was undefined. This ensures the enviroment is set to top (i.e. an entry point).
Previously each abstract object that implemented merge had to correctly redirect merging top with anything or merging with a bottom. This is now handled directly in the root merge by checking the three cases where the base merge must be used. If this is bottom must still be handled by derived classes as we must create an abstract object of the same type.
The variable sensitivity domain should be able to simplify the if statements produced by the function pointer removal, even in the cases where the pointer isn't definitely const.
Due to high variation in the number of generated goto statements on different platforms, checking specific number simplified is unreliable. This changes the tests to first simplify then spit out the generated GOTO code. This is then checked to check the if statements generated by function pointer removal is removed by the simplify step
thk123
force-pushed
the
feature/simplify-fp-removal-tests
branch
from
da40aa4 to
211cd21
Compare
tautschnig
changed the title
|
I am going to close this PR as it appears that work on it has been inactive for an extended period of time. This is not any judgement on how worthwhile this work is. This is part of an effort to reduce the number of open PRs which are not being actively worked on. Getting this PR merged would require someone to be willing to put the work into rebasing and addressing any remaining CI failures, assuming that this work has not been merged as part of another PR. If it is worthwhile to get this merged and someone is willing to put in the work, then the branch should be re-based on the latest version of develop and the PR re-opened. |
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 depends on #708
The function pointer removal step replaces calls on function pointers with an if statement on the possible functions it could be (with some improvements in precision introduced by #519). This PR adds tests that ensure that the
--simplifyaction with the variable sensitivity domain removes the if statements where it can.This specifically resolves:
Under the #519 changes, since
fpisn't const, this would be transformed to:However, running
--simplifyon this you get back to:f2();Real diff: https://github.com/diffblue/cbmc/pull/915/files/92a84dc..211cd21