Biosphere memory model optimization

[danieldietsch]

This ticket is a recreation and shortening of a mail conversation between @Heizmann , @alexandernutz , @jhoenicke and @danieldietsch . @Heizmann proposed the following change to our memory model:

Motivation

1. A store is a complex SMT function that causes issues in many places. For example, a store on an interesting array "in the middle" of a trace is always a part of the unsat core, because it not only describes the (usually irrelevant) update but also the connection between in and outvars. A select is comparatively harmless.
2. Our C translation requires many (oh so many) on-heap initializations of global datastructures. Currently, this is done with our alloc implementation and unchecked write procedures.

Naive optimization
Use assume instead of assignment during global initialization (assume becomes select, assignment becomes store). Issue: We cannot (easily) express that non-deterministic addresses are unique.

Biosphere optimization We assign each global data structure a fixed "biosphere". We do not get the pointer-base from alloc anymore, but we just count starting with 1. We have to consider that

• Utimate_alloc and Utimate_alloc_bio are not compatible
• using the biosphere optimization might prevent us from easily modelling the case where malloc returns a previously used and now freed pointer

Ticket #406 is an orthogonal memory model optimization.

[danieldietsch]

An additional benefit of this optimization is that certain abstractions work much better on such a partitioning of the heap.

In particular @franksch94 implementation of an array domain is geared towards this model.

I am currently running some experiments on the speedup-poc03-*.bpl series of programs, e.g. on speedup-poc03-08.bpl

I can modify this program s.t. I get a program with ordered pointers by adding assume statements after the malloc() block like this:

...
call p7 := malloc();
call p8 := malloc();

assume p1 < p2;
assume p2 < p3;
assume p3 < p4;
assume p4 < p5;
assume p5 < p6;
assume p6 < p7;
assume p7 < p8;
...

I have the following timings

    TO              ArrayDomain+Taipan  SmtInterpol+z3+arraydomain(Oct) 
    749487.56 ms.   ArrayDomain+Taipan  SmtInterpol+z3+arraydomain(Oct) (modified)
    TO              Camel 
    OOM             Camel (modified)
    297513.99 ms    SMTInterpol 
    167610.56 ms.   SMTInterpol (modified)
    101637.71 ms    AbsInt +ArrayDomain(Oct) (modified)
    Too weak        AbsInt + VPDomain (modified)

You can see that SMTInterpol alone profits rather much from introducing this order and that Frank's domain alone is strong enough to prove all the asserts in this file.