Limit unrolling to specific loops and arrays to make it applicable to larger programs

[michael-schwarz]

With #577 and #563 now merged, we now have the ability to unroll all loops k times and all arrays l times. Often, just unrolling everything will be expensive though and also not be too beneficial when it comes to precision, as it may just add precision in cases we don't care about.

Instead, it would be nice to be able to unroll just some loops and arrays (e.g. by providing an should_be_unrolled predicate).

Possible use cases would be:

• In the case of interactive refinement (i.e. Gobview) the hint to unroll a given loop and a given array could come from a user. The interactive analysis would see the unrolling of loops as a code change and handle it appropriately, one would only need to think about what part of the locals needs to be reset to benefit from unrolling the array.
• For automatic refinement, one could for failing asserts unroll those arrays appearing in the assert (or those that influence the value of variables that are used in the array) and the loops over them. This could use the same mechanism as the first idea.
• We might identify some loops and arrays that we want to unroll based on some heuristic. E.g., if there is an array of pthread_t[20] it would be worth unrolling the array and all loops that use it (potentially even up to a length of 20) if we are interested in race detection to benefit from better MHP information. The same probably goes for malloc(...) in such loops, as having more distinct heap locations may also be helpful here.

The nice thing here that one can not go wrong when deciding what to unroll, the analysis remains sound even if one comically wrong choices.

Changes that would be necessary to achieve this:

• [ ] Mechanism to specify should_be_unrolled predicate (e.g. annotations, heuristics, ...)
• [ ] Support for heterogeneous array abstractions (some may use unrolled, some may use partitioned, ...)
• [ ] ...

[sim642]

Also what wasn't implemented was the path-sensitive analysis based loop unrolling by counting iterations in the domain. Not sure if that deserves a separate issue, but I still think that would be beneficial because the unrolling bound could be completely dynamic and possibly even interactive nearly out of the box.

[michael-schwarz]

Largely completed with #772