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.

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

Merged
merged 22 commits into from
Jun 12, 2024

Conversation

manud99
Copy link
Contributor

@manud99 manud99 commented May 2, 2024

@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:

field f: Int

method test08a(x: Ref)
    requires acc(x.f)
{
    package acc(x.f) --* acc(x.f)

    x.f := applying (acc(x.f) --* acc(x.f)) in x.f + 1

    apply acc(x.f) --* acc(x.f)

    assert acc(x.f) && x.f == old(x.f) + 1
    assert false
}

The following changes were made:

  • Updated the definition of a MagicWandSnapshot to contain a variable for a wandMap of type MagicWandSnapFunction, short MWSF.
  • Modified the package wand algorithm such that we create a wandMap and add its definition to the path conditions.
  • Modified the apply wand algorithm such that we use the wandMap when producing the wand's RHS.
  • When there are magic wands in a program we add the definitions and axioms for the functions related to 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.

… own function definitions to replace wand maps.
…ginal approach using MagicWandSnapSingleton.
src/main/scala/decider/TermToZ3APIConverter.scala Outdated Show resolved Hide resolved
src/main/scala/rules/MagicWandSupporter.scala Outdated Show resolved Hide resolved
src/main/scala/rules/MagicWandSupporter.scala Outdated Show resolved Hide resolved
src/main/scala/rules/MagicWandSupporter.scala Show resolved Hide resolved
src/main/scala/state/Terms.scala Outdated Show resolved Hide resolved
src/main/scala/state/Terms.scala Outdated Show resolved Hide resolved
src/main/scala/supporters/DefaultMapsContributor.scala Outdated Show resolved Hide resolved
src/main/scala/supporters/DefaultSetsContributor.scala Outdated Show resolved Hide resolved
src/main/scala/verifier/DefaultMainVerifier.scala Outdated Show resolved Hide resolved
@manud99
Copy link
Contributor Author

manud99 commented May 8, 2024

@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 manud99 marked this pull request as ready for review May 8, 2024 08:08
@manud99 manud99 requested a review from marcoeilers May 8, 2024 08:09
@JonasAlaif JonasAlaif enabled auto-merge (squash) June 11, 2024 12:41
@JonasAlaif
Copy link
Contributor

@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)

auto-merge was automatically disabled June 12, 2024 11:30

Head branch was pushed to by a user without write access

@manud99
Copy link
Contributor Author

manud99 commented Jun 12, 2024

@JonasAlaif Done. I updated this branch and the corresponding branch in silver.

@JonasAlaif JonasAlaif dismissed marcoeilers’s stale review June 12, 2024 13:25

Review comments resolved

@JonasAlaif JonasAlaif merged commit f8cc484 into viperproject:master Jun 12, 2024
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants