UHeapReading composition fixes

[sergeypospelov]

The PR fixes several issues (one of them found by @tochilinak) related to memory regions composition and adds tests for them.

The issue with ITEs

Suppose you have a region reading, stored in a leaf of an ite. Let's assume, that the guard on the path to the leaf discards the case when the key of the reading equals null. Now what if we try to compose the reading onto a model heap? Both true and false branches of the ite will be recursively composed, and one of them will be chosen accordingly to the condition in the ite. Therefore, if the key of the reading maps into mkConcreteHeapRef(0) in the model, we will anyway read from the context heap by this key and get an RE. Example:

reading := inputField<int>[%0]
ite := ite(guard, reading, 0)

model := {guard -> false, %0 -> 0x0}

compose(model, ite) produces RE

Solution:

First, calculate a condition of an ite, then a necessary branch.

NB:

The problem still exists, if we have a guard inside a KAndExpr, KOrExpr, etc. How? Suppose, the first clause verifies the key can't be equal to null and the second one reads by this key from a region. We can't determine which clause to compose firstly, so If a model maps the key into 0x0, we have a problem.

The issue with the predicate on a default value in splittingRead

Suppose you have an allocated array reading, so the defaultValue equals to nullRef. Then in a model, we compose the defaultValue to the 0x0, then if the sort of the region is addressSort, we perform a splitting read, which has the following check:

assert(defaultValue == null || !predicate(defaultValue))

So the reading from the composed region fails.

Solution:

There are two options:

• ❌ Forbid splitting read from the composed region. (I don't know how to implement it now without changing interfaces)
• ✔️ Implement split for a default values. There is still a problem, because even we split out the default value, it still exists in the underlying memory region, so if we try to translate it, we get an RE. Fortunately, we don't translate composed regions now, so it can be omitted.

Anyway, I think, the whole splitting read mechanism should be refactored, because it takes O(n^2) time. Let's wait for containers and revision this again.

PR TODO:

• Description
• Comments