[Civl] Combine linear heaps and maps into a single abstraction #830
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 PR unifies Lmap and Lheap into a single abstraction with the latter being defined in terms of the former.
The type
Ref T
is explained below.The implementation of Lmap primitives is done by modeling them directly as pure procedures in Boogie syntax. Thus a lot of rewriting code in LinearRewriter.cs is eliminated. However, inlining of atomic actions had to be adjusted to allow for calling and inlining pure procedures from atomic actions. It is possible that these changes can be reverted by modeling these primitives as pure actions (which are already callable from both yield procedures and actions).
An important innovation is separating the Lmap primitives from the dynamic allocation of keys for which two separate types are provided.
The type
Loc
models a dynamically-allocated location. The allocation itself is performed by theLoc_New
primitive:The caller gets a fresh location (notice the
Lval
wrapper) every timeLoc_New
is called. An instance ofLoc T
may be wrapped into an instance ofRef T
via theRef
constructor.Two separate types
Loc
andRef
are needed because we want the domains of differentLheap T
values to be disjoint. At the same time, we want to provide the capability to have unique references to locations. If we unifiedLoc
andRef
, then we cannot have both capabilities.This PR appears to be a step in the right direction due to the unification of Lmap and Lheap. However, there is still room for improvement. To avoid the need to write collector functions, we introduced types Lval, Lset, and Lheap that have built-in collector functions. But we have introduced drawbacks.
My current assessment is that the wrapper Lval for wrapping a value to convert it into a possibly linear value is fundamental because it influences the definition of the collector function for the value. But the wrappers Lmap and Lset can be eliminated by going back to the original Civl approach.