goto-symex: expand unknown points-to values to all objects #6442
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
Collaborator
tautschnig
commented
Nov 5, 2021
tautschnig
commented
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- n/a My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.
Structs with sub-byte bit fields demonstrate that big-endian ordering also re-orders the bits within a byte. An executable variant of this unit test was validated on mips (using qemu-mips), demonstrating the same bit ordering. No bug fixes/code changes required, this test just confirms that our endianness interpretation matches actual hardware.
The bits within an object of bv_typet are ordered depending on endianness. This is consistent with typecasts to/from bv_typet of some other bitvector type, which do not alter the sequence of bits.
This commit enables the use of nondeterministic pointers, to allow declarative modeling of states that include pointers.
Byte extract already supports access beyond the bounds of the object being extracted from. Any bits outside bounds are free variables. extractbits now equally supports this case (via free variables).
Non-deterministic pointers should consider all possible objects. goto-symex is aware of all current objects, and can thus expand points-to values of "unknown" to all current objects (leaving the pointer offset unconstrained).
goto-symex now treats empty value sets as dereferences to all current objects. Therefore, there is no need to initialise the value set for pointer-typed objects upon declaration.
This reverts commit 5723e39725bb59bcd55536f8a8c495226de88949.
This reverts commit be0770dbe596d69a134ef08cdaa6a95962e46ee2.
This reverts commit f105968f58e481b29afc82c1f237c0eceef2028d.
Byte operator lowering made several assumptions about array elements being byte aligned, which may be true for ANSI C, but isn't the case for our C front-end (which supports arrays of single bits), and not true for the overall framework in general.
Byte operator lowering made several assumptions about array elements being byte aligned, which may be true for ANSI C, but isn't the case for our C front-end (which supports arrays of single bits), and not true for the overall framework in general.
tautschnig
force-pushed
the
any_object-2
branch
from
ad93441 to
84d6532
Compare
3 tasks
Codecov Report
@@ Coverage Diff @@
## develop #6442 +/- ##
=========================================
Coverage 76.04% 76.04%
=========================================
Files 1546 1546
Lines 165485 165610 +125
=========================================
+ Hits 125836 125932 +96
- Misses 39649 39678 +29
Continue to review full report at Codecov.
|
martin-cs
reviewed
Nov 30, 2021
Not quite, I'm afraid. But ultimately the only interesting commits to remain should be "goto-symex: expand unknown points-to values to all objects" and "goto-symex: initialisation of pointers is no longer necessary". Feel free to look at these and comment! Everything else will go in PRs of its own/has already been PR'ed. |
4 tasks
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.