Add state transformers!

[N1ark]

Add state model transformers!

finally..

Interface

This is possible by defining MyMonadicSMemory, a similar but smaller and strongly typed version of Gillian's MonadicSMemory. All state model transformers are then defined to fit that interface, and a functor is provided to then convert it into a Gillian compatible module.

"Atomic" state models:

• Exclusive: exclusively owned value
• Agreement: shared, immutable value
• Fractional: exclusively owned value with fractional permissions

State model transformers:

• Product: product of two state models
• Sum: sum of two state models
• Freeable: state model that can be freed
• PMap: maps indices to sub state models (more detailed further down)
• MList: represents a bounded list of substates

"Utility" state model transformers:

• ActionAdder: allows adding new actions to a state model, without worrying about implementing consume, produce, etc.
• Filter: allows filtering out actions and core predicates
• Injector: adds hooks before and after actions, consume, produce and instantiation, to allow customising specific behaviour without having to mess with functors (eg. re-order or manipulate arguments, return values...)
• Logger: logs actions, consume and produce when called
• Mapper: allows renaming core predicates and actions

Instantiations

Three state model instantiations are provided, and are shown to be equivalent (to our knowledge) to the existing Gillian-C, Gillian-JS and WISL implementations. They're all in the prebuilt/ folder. In particular, the JS and WISL instantiations are "pure" -- the C instantiation uses a modified BlockTree, taken from Gillian-C and adapted (see prebuilt/c_states/).

PMaps?

To make customisation easier, PMaps are a bit more convoluted than the others.

tl;dr: one functor (Make/MakeOpen) for the state model, one module for the data structure implementation (PMapImpl), one module for the PMap's domain handling (PMapIndex).

In particular there are a few variations to this; first, two functors:

• Make: creates a PMap state model with a domain set, to allow distinguishing misses from out of bounds accesses.
• MakeOpen, creates a PMap with no domain set -- simpler implementation, but doesn't support dynamic indexing, and always misses.

These functors take in a module of type PMapImpl, which is the implementation of a PMap's data structure, allowing to easily swap out optimisations. There are currently three such modules:

• BaseImplSat/BaseImplEnt: a naive implementation using a Map over Expr.t, and always checking for equality over keys. There is a variant for SAT checks, and a variant for ENT checks (though the latter doesn't seem significantly faster).
• SplitImplSat/SplitImplEnt: splits the heap into a concrete and symbolic part, avoiding checking for substitutions on the concrete side.
• ALocImpl: indexes by abstract locations only; doesn't check for equality if possible.

While ALocImpl is restricted to abstract locations, BaseImpl--- and SplitImpl--- can accept several indexing domains, implemented as a PMapIndex module. These modules are responsible for checking if a given Expr.t is valid according to the domain, as well as specifying the mode of the domain. It either is Static, in which case the PMap uses allocation -- it then must implement the make_fresh function. Otherwise it is Dynamic -- there is no allocation, and substates are instantiated on access, in which case it must provide the default_instantiation list containing the default argument to instantiate the substate.
There currently exist three such indices:

• LocationIndex: static, only accepts locations, abstract locations -- uses Gillian's abstract location mechanism (e.g. C uses location indexing)
• StringIndex: dynamic, accepts strings (e.g. JavaScript objects use string indexing)
• IntegerIndex: static, uses increasing integers (e.g. used in a simple linear heap)

An example of PMap is then: PMap.Make (BaseImplSat (IntegerIndex)) (Exclusive)

[N1ark]

ping @NatKarmios @giltho -- sorry about the huge PR I guess
Also I don't know if eventually we'll want to remove the state models in WISL/Gillian-C/Gillian-JS as a result?

[AndreasLoow]

Also I don't know if eventually we'll want to remove the state models in WISL/Gillian-C/Gillian-JS as a result?

Heh, maybe eventually but for now we probably want to keep them around to do e.g. behaviour/perf comparisons.