forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 0
Vsd cross representation evaluation #4
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
Draft
jezhiggins
wants to merge
53
commits into
vsd-value-set-of-pointers
Choose a base branch
from
vsd-cross-representation-evaluation
base: vsd-value-set-of-pointers
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Draft
Vsd cross representation evaluation #4
jezhiggins
wants to merge
53
commits into
vsd-value-set-of-pointers
from
vsd-cross-representation-evaluation
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
Reduce number of special cases, and generalise expression evaluation. Special case for ID_plus no longer needed, as a+b+c is still evaluated correctly. Previously incorrectly evaluated expressions such as a*b*c now also evaluated properly.
Without this all operations return top, which is unhelpful. With this change, simple arithmetic starts to work, unary operations, etc. Still more to for multi-value sets.
…behaviour was an error
expression_transform correctly creates all combinations of operands, but passed the unmodified expression down for further evaluation. If the expression was something like 2 + p then at the next stage down, we'd look up symbol 'p' and be handed back a value set. The evaluated would then try to convert that value set to a constant which would, naturally, fail. Consequently, the expression would evaluate to top. Now, we rewrite the expression in terms of the evaluated operands. If expression was 2 + p, and p was the set { 2, 3 } the expression is rewritten first as 2 + 2, then as 2 + 3, which we can gather up into our result of { 4, 5 }. The various regression tests in this commit exercise various combinations of constants and value-sets, value-sets of different size, and so on. All the tests use addition, but the operator is immaterial.
Splendid side-effect of the expression_transform work :)
Do this by ensuring new object we return are created though the factory, rather than instantiated directly. Several regression tests need updating as a consequence of this change, generally tweaking the regex to allow the context info in place of a hard line end.
Reduce duplication, separated object create from the context object that may wrap it.
I'm not super thrilled about how I've done this, because ideally all object creation should go through the object factory. However, in this particular case a large value set could be converted to an interval. If we hand off to the factory it'll just create another value-set, so we need to explicitly create the interval. However, when we do that we don't have the context wrapper (write location or data dependency). Consequently, I've added variable_sensitivity_object_factoryt::wrap_with_context and exposed it through abstract_environment so we can add the appropriate context wrapper should we need it.
Tidy up evaluate_conditional and pull out evaluate_unary_expr
…factory Default arguments on a virtual function aren't safe. Even through this function isn't overriden anywhere now, it's a latent bug waiting for the future.
Avoid shadowing member variable, make single-arg constructor explicit
value=-set ordering is unstable in the face of code changes, which made tests fragile. Sorting output fixes that and is also easier on the human eye too. We're sorting string representations, so the output isn't a true numerical sort but it's good enough.
This is going to fail in several different ways, but hopefully not for too long
Pull across functions from value_set_abstract_object and value_set_pointer_abstract_object
Point to a constant, dereference, assert we got the same value out --vsd-pointers value-set fails in this commit
Dereferencing no longer causes an abort. It's still not correct, but it's not as wrong.
Using intervals. Value-sets should work but needs more work on value-set value equality.
Writing through a value-set pointer currently does nothing, so test fails.
a9ded22
to
4a83781
Compare
9be15ad
to
89c91f7
Compare
The index_ranget has, by C++ standards, an unusual interface more akin to something you'd get on a C# enumerator. This is the first step to making it more container-like, with begin()/end() member functions returning iterators. With this commit, the iterators are input-iterator like, in that they can only be traversed once.
89c91f7
to
7605dea
Compare
index_ranget is now only returns its begin and end iterators. It's now returned as a value, rather than through a shared_ptr, as its lifetime will naturally be scope limited and, as described below, polymorphic behaviour is hidden inside. This makes is more natural to use too, as we can just write for (const auto &index : range) rather than having to dereference it. It can now be repeated iterated, rather than the one and done it was in the previous commit. Behind it, the classes that do the actual work of enumerating the ranges have been split out from input_ranget. There is no longer any need to shared these objects, so they are instantiated using unique_ptr rather than shared_ptr.
7605dea
to
ebb341d
Compare
85160cc
to
8342a92
Compare
8342a92
to
df41607
Compare
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.
Work on operations across different value representations.
Initially, work on merging value-sets and constants.