Use a Map from Snap to Snap to represent a magic wand snapshot.

[manud99]

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

Fixes #307

[manud99]

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

[JonasAlaif]

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

[manud99]

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