Initial SL Precondition Language

[2over12]

Currently GREASE shapes cannot express logical relationships between values, nor express memory layouts that involve gaps/symbolic offsets to pieces. #492 starts adding a syntax for separation logic specifications and has context for the difficulties therein. We would like to integrate something like this with minimal disruption to the codebase while maintaining the original shapes format. 492 and 535 ran into problems with concretization and printing (post setup phase GREASE operation). If we abstract the precondition entirely after setup, then we end up rewriting more of GREASE than we would wish to. 537 takes a step to removing information the SL specs would not be able to provide after setup, while maintaining concretization and printing. The following steps seem reasonable to implement SL assertions:

1. Merge 537. This removes knowledge about aliases and concrete offsets that an SL precondition will not have from the post-setup shape, while maintaining this information in the pre-setup and concretized shape.
2. Currently a block is a sequence of memshapes. This setup means that if SL preconditions must produce this structure we cannot support symbolic offsets/disjoint blocks. This data-structure should be refactored to become a map/tree from symbolic offset to value (e.g. the expression that defines the offset) with the invariant that blocks are disjoint. This kind of ends up looking like heap treas. Then later these offsets end up concretized, at that point the printer can use the concretized values to lay them out in the continuous syntax (or we could support a sub-block/cell printing syntax).
3. Now we can do roughly 535 and abstract the precondition type as roughly an existential type that supports a setup function. The setup function takes the parsed precond and produces an Args structure that now is sufficiently general for both SL and our original shapes. This allows concretization + printing to now be directly reused.
4. Add the SL syntax itself and parsing 492
5. Write a setup function per internal design, roughly: allocate blocks with symbolic sizes, traverse bounds to bound the size, cells are translated to writes to the block, uninitialized just ensures there is at least enough space for a write by adding a relationship to the symbolic block size

Note: On step 3 there is slight difficulty with

grease/grease-exe/src/Grease/Main.hs

Line 504 in 2f1bb14

interestingConcretizedShapes ::

This function assumes that the precondition type can be translated to the concretized type which is no longer true after this refactor. Intuitively, what this comparison is a proxy to capture is wether concretization took a given argument/shape and translated something from symbolic to concrete. Perhaps we could just have concretization record these directly. (i.e. we want to record where cases like this happen because that makes the parent shape interesting)