Add 1-Dimensional memory model for memory safe tasks - #756
Merged
Conversation
jankoerner
requested review from
Heizmann,
bahnwaerter,
maul-esel and
schuessf
November 6, 2025 19:17
Member
|
@jankoerner Thanks for your work! I will try to review this PR tomorrow. I just quickly fixed the compilation, as some settings were changed in #752 and started the Jenkins nightly for this PR. |
Member
|
Many thanks also for your extensive work, @jankoerner!
Thanks @schuessf for fixing the issue. It looked like the Git rebase didn't include all the other changes. |
bahnwaerter
requested changes
Nov 7, 2025
jankoerner
force-pushed
the
wip/jk/simplified-memory-model-post
branch
2 times, most recently
from
November 8, 2025 21:25
17dd19a to
3cb57aa
Compare
Member
schuessf
reviewed
Nov 10, 2025
schuessf
left a comment
schuessf
left a comment
Member
There was a problem hiding this comment.
Thank you for your work! I briefly looked over the structure of your new code and it looks good to me -- if it works, we can merge it in principal.
I left a few more general comments. In addition: Please make sure for all the files you added that they the have at least a header, an author and a description such that we know what the class is supposed to do.
Member
|
I just checked the latest nightly and a lot of tests failed, but (probably) only because the new setting "memory neutrality" did not parse an empty string to an empty set and therefore the check in |
Member
|
@jankoerner The nightly tests run now in principle. There is however one issue left, where the existing implementation still only works with 2D pointers, see here Edit: I just fixed that myself. |
schuessf
changed the title
schuessf
approved these changes
Nov 19, 2025
Renamed memory model to memory structure because it only covers the memory representation. The full memory model alos features a memory addressing and this commit is a preparation for this step.
Added the interfaces for structure and addressing. Added 1D and 2D memory addressing as well as a common base class. Added a utils class.
The ExpressionTranslation was neither used in the abstract base class nor in the subclasses. Also removed unnecessary cast of TypeHandler.
This factory is used to create concrete instances implementing interfaces that are used in the memory model. All validity checks are also part of the factory.
Use the memory structure from the new memory model instead of the using the structure that was part of the memory handler. From time to time, more parts will move to the memory model.
The malloc now depent on the settings. Moved things out of the MemoryHandler to access them there and in the model. Renamed things.
The statements in Ultimate.Init depent on the current memory model.
Removed introduced Supresswarning to allow external tools to notice them.
Also renamed some classes to match the naming scheme.
This method was deleted because it is unused but restored again such that it can be deleted in a dedicated commit / pull-request.
…ettings/toolchains
schuessf
force-pushed
the
wip/jk/simplified-memory-model-post
branch
from
November 19, 2025 17:01
7ffa30c to
2bc755f
Compare
schuessf
added a commit
that referenced
this pull request
Nov 21, 2025
#756 added more tests (~1000), therefore the latest nightly was aborted just before it finished.
32 tasks
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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
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 pull request introduces a 1-dimensional memory model which can be used for ReachSafety tasks.
The 1-dimensional memory model comes with some major refactorings of the source code.
These refactoring can be seen in the attached image and allow an easy extension for new Addressings, Structures, ManagementStrategies and Metadatas (not visible in the image).