Slicing unused addresses and their init events

[ThomasHaas]

Context: Malloc operations create an address for every byte that was malloced.
Most of the time, accesses are not byte-granular and, e.g., an allocation malloc(8) is only accessed with offsets 0 and 4.

Problem: This causes us to create a large number of unused addresses, which in turn result in an unnecessary large amount of Init events that initialize never-accessed addresses. We could slice all these Init events from the program.

Typically, dead init events are no issue in the encoding, because the relation analysis will identify that there are no possible relationships to these events that need to be encoded. Therefore, we cannot improve solving times with this.
However, dead events can unnecessarily increase analysis times!

Example: The SVCOMP benchmark stack_longest-1 allocates around 3200 addresses (meaning at least 3200init events and hence also threads!) of which only around 800 are even accessible.
The ext relation of the benchmark has around 10,000,000 tuples which could be reduced to less than a million.
This is relevant, because of the total verification time of this benchmark, 93% is spent in the relation analysis and 66% just in computing ext.
In general, this might be useful for benchmarks that allocate large arrays as those create a huge number of dead addresses.

LFDS benchmarks like dglm can also be reduced from 160 to just 12 addresses, but that should not impact performance much.

[hernanponcedeleon]

Is this still an issue after #641?

[ThomasHaas]

I guess the issue is outdated and can be closed.