-
Notifications
You must be signed in to change notification settings - Fork 32
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.
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
Use a Map from Snap to Snap to represent a magic wand snapshot. #836
Conversation
… own function definitions to replace wand maps.
…ginal approach using MagicWandSnapSingleton.
… the original approach using MagicWandSnapSingleton." This reverts commit fd87482.
@marcoeilers Thanks for your code review. I updated my branch accordingly. After performing some benchmarking, Jonas and I decided to revert the second optimization. We compared the mean execution time of all test files that contain a magic wand. In average this version took 2.2% longer than the initial version. The second optimization took slightly longer (+2.72%). |
@manud99 could you update the PR from the main branch so that I can merge it (don't have access to a pc right now) |
# Conflicts: # silver
Head branch was pushed to by a user without write access
@JonasAlaif Done. I updated this branch and the corresponding branch in silver. |
@JonasAlaif and I are working on a different method to generate snapshots for magic wands. The problem with the current approach is that it is potentially unsound when we apply the same magic wand multiple times. This problem has been illustrated in issue #307 and occurs when using
applying
expressions.To solve that issue we introduce wand maps. These are functions that map a snapshot of the wand's LHS to a corresponding snapshot for the RHS. They make sure that values in the state are preserved when applying a magic wand. In comparison to the initial version they also work when applying a magic wand multiple times in different states. One example for that can be found in the file attached in issue #307 or in this example:
The following changes were made:
MagicWandSnapshot
to contain a variable for awandMap
of typeMagicWandSnapFunction
, short MWSF.wandMap
and add its definition to the path conditions.wandMap
when producing the wand's RHS.MagicWandSnapFunction
.Requires viperproject/silver#788 to fully pass the test suite.
Additionally, there is a test suite consisting of 12 files that check the behavior of this PR in viperproject/silver#796.