Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Memory rework #51

Merged
merged 27 commits into from
Aug 29, 2023
Merged

Memory rework #51

merged 27 commits into from
Aug 29, 2023

Conversation

Saloed
Copy link
Collaborator

@Saloed Saloed commented Aug 24, 2023 •
edited
Loading

Memory refactoring

  • Memory is now consists of symbolic collections, e.g. fields or arrays
  • Each collection is accessible through the corresponding Value
  • Each collection encapsulates input/allocated splitting
  • Each collection defines its own translation rules and model representation

Composition refactoring

  • Composition is defined via filterMap operation
  • All collection updates are filtered during composition wrt collection reading key

API

  • All collection specific operations are provided via the API, not memory
  • API also provides utils for efficient java collections modeling, e.g. ObjectMapCollectionApi

sergeypospelov
sergeypospelov requested changes Aug 28, 2023
View reviewed changes
usvm-core/src/main/kotlin/org/usvm/collection/map/ref/Expressions.kt Outdated Show resolved Hide resolved
usvm-core/src/main/kotlin/org/usvm/memory/Memory.kt Show resolved Hide resolved
usvm-core/src/main/kotlin/org/usvm/collection/array/ArrayRegion.kt Outdated Show resolved Hide resolved
usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionId.kt Outdated Show resolved Hide resolved
usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionId.kt Outdated Show resolved Hide resolved
usvm-core/src/main/kotlin/org/usvm/solver/RegionTranslator.kt Outdated Show resolved Hide resolved
usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegionTranslator.kt Outdated Show resolved Hide resolved
usvm-core/src/main/kotlin/org/usvm/collection/array/length/ArrayLengthRegionTranslator.kt Outdated Show resolved Hide resolved
usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionId.kt Show resolved Hide resolved
usvm-core/src/main/kotlin/org/usvm/memory/USymbolicCollectionId.kt Show resolved Hide resolved
@Saloed Saloed merged commit 29a3340 into main Aug 29, 2023
1 check passed
@Saloed Saloed deleted the saloed/memory-rework branch August 29, 2023 12:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@sergeypospelov sergeypospelov sergeypospelov approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@Saloed @sergeypospelov