Partial expression simplification #1020
Closed
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
thk123
assigned NlightNFotis, martin-cs and thk123 and unassigned NlightNFotis and martin-cs
…be picked independently.
The option string --show --intervals is more flexible, --show-intervals is now an alias.
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
added 19 commits
June 15, 2017 17:53
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.
At some point this commit needs backdating as the ai_domain interface has changed under our feet.
|
Looks good to me. The only nit is to make sure to update the call to ai_simplify to the new signature. |
|
Let's see if the merge issues go away once the rebase is done. Other than that I am happy with this change. |
If the ai_simplify is not able to resolve the expression to a constant, it tries to simplify recursively any child operations. For example, given a int i that is know to be 1, and an unknown (top) array a, it would convert a[i] to a[1].
thk123
force-pushed
the
bugfix/partial-expression-simplification
branch
from
9f2198a to
de2f979
Compare
Closed
|
Closing as it's unlike @thk123 is going to pick this up again. Also I believe a version of this was eventually implemented regardless. |
|
Just to close the loop, VSD did get merged and @jezhiggins is currently working on this bit of code, hopefully for a final version. |
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.
Depends on variable sensitivity domain: #708
Fixes part of diffblue/cbmc-toyota#132
When calling
ai_simplify, previously if we couldn't simplify the whole expression we gave up. Now werecurse over the sub-elements to get a partially simplified expression. E.g. if we have an array whose value is top, but the index
iis known to be 1 thenarr[i]will simplify to:Real diff: de2f979