Malloc uniqueness

[TDacik]

This PR tries to increase the precision of the representation of heap-allocated variables.

• 83e413c Each malloc can now allocate up to n unique heap variables, where n is given as the command-line parameter (by default n is 0, which means that only one non-unique heap variable is allocated for each malloc node -- this is for backward compatibility). Heap variables now also contain a thread identifier of a thread where the allocation happened to distinguish memory allocated in different threads. A heap variable is considered unique if its thread identifier is unique and the number of its alocation is lesser than n.

• 8e68873 Heap variables that are unique can be strongly (destructively) updated if the size of a written value matches the size of a blob that represents a memory allocated for the variable.

[sim642]

The two issues this at least partially relates to are #186 and #702.

[sim642]

I guess for me the big question is whether this works for the example in #186 and possibly the first solution steps for #702.

[sim642]

How about with mallocFresh analysis also enabled? These alloc variables are created thread-local and never escape, so theoretically they should be strongly updateable.

[michael-schwarz]

The corresponding variables are still created as globals here, so freshness does not help here.

[sim642]

Oh right, mallocFresh analysis only affects race checking, but not anything value-based, which I suppose it also could. Actually the freshness stuff could become part of escape analysis, but there was some issue at the time which prevented that (considering everything non-escaped to be fresh in general).

[michael-schwarz]

Yes, in the future, we should definitely make that change. I'd suggest doing it in a different PR though.

[michael-schwarz]

I started an sv-comp run to see what sort of impact this has.

[michael-schwarz]

As it stands, the PR is unsound for calloc, as the size is not properly calculated there.

[michael-schwarz]

As it stands, the PR is unsound for calloc, as the size is not properly calculated there.

This was some ancient bug where when we modified the Calloc variant in LibraryFunctions to take two arguments, but did not appropriately pull in the multiplication.

[michael-schwarz]

Before we can merge this, I am still waiting on the results of the sv-comp run: I seem to encounter the issue with benchexec freezing up again, so I need to babysit it.

[michael-schwarz]

For sv-comp the result once again is a resounding it does not matter, but probably it is one of those things where when used selectively may form the key ingredient somewhere.

Interestingly, performance is also not too bad: the x axis is with setting 0, the y axis is with setting 3

[sim642]

the y axis is with setting 3

I tried to find what Frama-C used in SV-COMP for the equivalent limit. According to their manual -eva-mlevel sounds to be the option for that, but Frama-C's SV-COMP logs don't indicate anything about that (whereas they indicate a bunch of other precision levels, e.g. loop unrolling being much higher). I suppose in it was the default 0 in SV-COMP then.

Given that the Frama-C manual describes this being useful up to certain loop bounds, it probably won't make a real difference with 3, since most loops aren't that short and thus would end up with one weak alloc variable for all the rest anyway.

This doesn't block this PR, but it might be interesting to take a closer look at ReachSafety-Heap with a much higher limit (based on loops actually occurring in those benchmarks) to see if it gets us further. It's probably a matter for #772 to bump the limit based on mallocs in loops.

[michael-schwarz]

I think to really benefit in loops, we would have to enable some sort of path-sensitivity, which we currently don't do here.
Yes, may be interesting to run it on the heap benchmarks with a higher limit.

I'll merge this for now though, such that it doesn't become stale.