Introduce UExprTranslator, UModelBase and revise regions composition

[sergeypospelov]

This PR adds translation and decoding mechanisms. They now encapsulated in USolverBase via a translator and a decoder. USolverBase::check returns a USolverSat with a UModelBase in case of satisfiable path constraints. To successfully evaluate any UHeapReadings via UModelBase::eval, memory regions composition was revised and partly reimplemented.

Details

UExprTranslator

Translates custom UExpr to a KExpr. Region readings are translated via URegionTranslators. Base version caches everything, but doesn't track translated expressions. UExprCachingTranslator tracks translated symbols (e.g. register readings, mock symbols, translated region ids, etc.). This information is used in ULazyModelDecoder.

The translator can be safely reused inside a single UContext.

ULazyModelDecoder

Performs decoding of a KModel to a UModelBase. Initialized with tracked information from UExprTranslator. Actually, it is updated on the fly: when new expressions are translated, they automatically leak to passed caches in ULazyModelDecoder, so the decoder sees them. This is the only semantic connection between the decoder and the translator. Syntactically, they don't know about each other, and all the configuration happens in buildDefaultTranslatorAndDecoder function.

Internally, the decoder splits KModel into 4 components: stack, heap, types and mocks and initiaizes them with KModel. It has to be detached, due to lazy way of decoding.

UModelBase

Consists of decoded components and allows to evaluate any expression. Evaluation is done via generic composition. Evaluated expressions are cached within UModelBase instance. If a symbol from an expression not found inside the model, components return the default value of the correct sort.

URegionId

URegionIds holds an instantiate function, which is called for reading a value from a region by a key after fast checks (take default value or a top-most update) in UMemoryRegions fail. This allows us to substitute this behavior when composing onto context heap.

ULazyHeapModel

A lazy immutable heap model. Declared as a mutable heap for using in regions composition in [UComposer]. Any call to modifying operation throws an exception.

Any UHeapReading possibly writing to this heap in its URegionId.instantiate call actually has empty updates,
because localization happened, so this heap isn't mutated. It significantly relies on simplification and localization in memory regions!

Heap readings composition

1. We map every single expression in the underlying memory regions. regionIds mapped as well and we put a context heap there.
2. Then we perform reading from a mapped region by a mapped key.
3. Whenever we call the underlying instantiate function, we firstly recursively apply this region to the context heap, then read from the context heap by a passed key. In case of a UModelHeap, region.updates will be empty due to localization, so no mutation occurs. Therefore, we only read a value from the UModelHeap by the passed key.

Minor:

• Add new tests for composition, a few tests on decoding and evaluating in UModelBase.
• Introduce UMemoryRegion interface and renamed previous one to USymbolicMemoryRegion.
• Remove UEmptyUpdates.
• Make UFlatUpdates simplify reads.
• Add UMemoryUpdates visitor.
• Refactor URegionIds, add a visitor for them.
• Small renamings.
• Fix mkHeapRefEq to pass tests.
• Fix tests.
• Advance KSMT version to 0.5.0.
• Other minor refactorings.

TODO:

• Push a commit about caching UMemoryUpdates
• Split UExprTranslator into several parts or fix the SRP for it in a different way
• Fix URangedUpdateNode for 2D arrays
• Fix other TODOs in the code
• Fix internal/private functions
• Carefully review possible extension points for user translations
• Add more tests: register readings, interleaved writings, readings, observer tests, etc.
• Add comments on everything
• Add description to PR