VSD pointer arithmetic, differencing, and comparisons #5678
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
jezhiggins
force-pushed
the
vsd-pointer-arithmetic
branch
2 times, most recently
from
314828d to
fdea979
Compare
Codecov Report
@@ Coverage Diff @@
## develop #5678 +/- ##
=========================================
Coverage 76.16% 76.17%
=========================================
Files 1484 1484
Lines 162164 162317 +153
=========================================
+ Hits 123516 123646 +130
- Misses 38648 38671 +23
Continue to review full report at Codecov.
|
jezhiggins
force-pushed
the
vsd-pointer-arithmetic
branch
5 times, most recently
from
0fac00e to
c844d94
Compare
|
Build Xen with CPROVER tools / CompileXen (pull_request) is failing for unrelated reasons. |
jezhiggins
changed the title
jezhiggins
requested review from
chrisr-diffblue,
kroening,
martin-cs,
peterschrammel,
smowton and
tautschnig
as code owners
martin-cs
requested changes
Jan 4, 2021
There was a problem hiding this comment.
I like what this is doing, there are a few places where I feel how it is doing it could be better. I suspect "better" here means deeper and more intrusive changes to the write_stack parts and constant_pointer_abstract_objectt which are only obviously "better" when taking into account a load of other things so why don't we have a chat and see what can be done?
regression/goto-analyzer/pointer-difference-after-decrement/test.desc
Outdated
Show resolved
Hide resolved
| offset = (q - p); | ||
| assert(offset == 0); | ||
| assert(q == p); | ||
| } |
| @@ -97,6 +97,15 @@ class pointer_abstract_objectt : public abstract_objectt | |||
| protected: | |||
| CLONE | |||
|
|
|||
| virtual bool same_target(abstract_object_pointert other) const | |||
There was a problem hiding this comment.
I am not entirely opposed to adding to the interface for pointers if it is necessary. However there is a general move towards making the interface of abstract_objectt and children more uniform so I wonder if there is another way.
jezhiggins
force-pushed
the
vsd-pointer-arithmetic
branch
10 times, most recently
from
d93594a to
5fedaf1
Compare
jezhiggins
force-pushed
the
vsd-pointer-arithmetic
branch
from
5fedaf1 to
e092e9f
Compare
If a pointer addition simplifies to p+a, if we continue to simplify we risk incorrectly eliminating zeros from the expression, erroneously going to TOP when we would otherwise have a correct pointer to the base object.
Detect case by checking expr has ID_minus and the operands are both pointers
It implements some of what should be two_value_pointer_abstract_object, so moved that out.
Representation specific implementations in derived classes. value_set_pointer currently a stub.
jezhiggins
force-pushed
the
vsd-pointer-arithmetic
branch
2 times, most recently
from
483f564 to
11880d1
Compare
jezhiggins
force-pushed
the
vsd-pointer-arithmetic
branch
from
11880d1 to
6f2f117
Compare
jezhiggins
force-pushed
the
vsd-pointer-arithmetic
branch
4 times, most recently
from
617a5b5 to
908e599
Compare
We can pick up the special case for pointer addition in abstract_object::expression_transform.
jezhiggins
force-pushed
the
vsd-pointer-arithmetic
branch
from
908e599 to
4844d22
Compare
martin-cs
approved these changes
Aug 3, 2021
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.
Pointer arithmetic fixes
(p - q)correctly, whenpandqpoint to the same base objectAssertion is now SUCCESS, when previously it was UNKNOWN.
A pointer difference or comparison expression is slightly unusual - the type of the expression is a number (or boolean), but the two operands are pointer types. Generally, the expression type is the same as the first operand (if not all of them). Because of this type mismatch, the abstract environment was dispatching the expression to the wrong abstract type for evaluation, so the result was TOP and therefore unhelpful.
The changes to evaluate pointer differences are small - an additional case in
abstract_environmentt::evalto pick up a pointer difference and dispatch it toabstract_pointer_object, and then the corresponding changes inabstract_pointer_objectto calculate the difference.Pointer comparisons are a little more involved. Again, we have an additional case in
abstract_environmentt::evalto dispatch the expression toabstract_pointer_object. If the two pointers point to the same base object we can rewrite the comparison in terms of the pointer offset and evaluate that. If the two pointers point to different objects, we can evaluate == and !=, but other comparisons go top.