Improved memory handling #639
Merged
Conversation
This file contains 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
Minor refactor in MemoryObject
…sses) - The ProgramEncoder now encodes the memory layout - Renamed MemoryObject.cVar to MemoryObject.name (more general)
- Allocs are not replaced by Local events anymore (they are core events now) - Adapted FieldSensitiveAndersen to understand new Alloc events.
- Allocs are now core events and do not get replaced anymore. - Adapted FieldSensitiveAndersen to understand new Alloc events.
- Removed litmus distinction in MemoryAllocation
…we still use integers in practice) - Removed automatic initialization for static MemoryObjects. Instead, the ProgramBuilder will do so explicitly when building from litmus code.
…ariables. - Use helper method makeZero in ProgramBuilder
dartagnan/src/main/java/com/dat3m/dartagnan/program/event/core/Alloc.java
Outdated
Show resolved
Hide resolved
- Minor improvements in Alloc
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 improves handling all around memory, partially addressing the needs of #136:
MemoryObjectnow has anallocationSite(anAllocevent) which is non-null for dynamic allocations.MemoryObject.addressis gone (theMemoryObjectitself already represents an address).Allocis now a proper core event (also moved to thecorepackage) and does not get replaced byLocalanymore (the alias analysis has been adapted to support this).ProgramEncoder.encodeMemorynow assigns actual addresses to memory objects. For now, it still generates a static memory layout (i.e., fixed addresses) but now it is also possible to encode complex memory layouts (in particular dynamic one's).MemoryObjectdoes not automatically add initial values for static allocations. This is responsibility of the parser frontend:ProgramBuilderwill now explicitly add init values for litmus tests.MemoryAllocationdoes not distinguish between litmus and non-litmus code anymore. It always only generates init events for explicitly initialized events. As above, responsibility of generating initial values is in the parser rather than the allocation pass.--
MemoryObject.cVaris now justMemoryObject.nameto be more general.--
MemoryObject.isAtomicis gone since it was unused.--
MemoryObject.indexis renamed toMemoryObject.id(it was never an index to anything)As far as I see, the only step that is missing to support dynamically-sized allocations is extending
MemoryObject.sizeto be a properExpression(as discussed in #136).The biggest obstacle to this change is the current alias analysis. However, I think the new one in #616 might have an easier time supporting dynamic sizes.