Expression splitting analysis prototype

[sim642]

This is a prototype implementation of an analysis which can split the state by arbitrary (integer) expressions and be path-sensitive w.r.t. those split states.

For the purposes of this prototype, I added two special functions __goblint_split_begin(exp) and __goblint_split_end(exp) to start and end the splitting, which correspondingly add and remove the splitting expression in the expsplit analysis domain. See the added tests for usage. I don't know if we want to keep this for annotation (currently the analyzed programs cannot be compiled and especially linked, because there's no runtime no-op stub for them), but these were surprisingly easy to add for fine-grained testing of this feature (to see in HTML where the expressions get added and removed). Also it's neat because the splitting expressions therefore actually correctly refer to the correct varinfos in the scope and CIL itself ensures that the expression only refers to variables in the scope. (I'm saying this because function attributes would not have this property: they would be strings that need to be parsed and the variables associated with those in the scope, which is a lot more trouble).

It was surprisingly easy to implement: there wasn't even need to use ctx.split, but just emit a special event, which allows the analysis to evaluate expressions on the post-state and update its own domain accordingly. Moreover, since there's no splitting by a branching condition and condition values are just integers, this whole thing works for splitting by arbitrary integer expressions for free!

I also had to fix an issue, where the path-sensitive functor did not run should_join after each non-joining transfer function. Otherwise the split didn't actually disappear at all. It might be nicer to implement Dom.add which immediately accounts for should_join when adding instead of doing it in batch.

The added tests show, that this works for the sort of case that @michael-schwarz was worried about, where the expressions must necessarily be evaluated on the states after transfer functions but before the join of incoming edges.

TODO

• [ ] Add UpdateExpSplit emitting to all transfer functions (and add tests).
• [ ] Test if it works when splitting by multiple expressions simultaneously (and add tests).
• [ ] Check for performance overhead of all these extra events, expression evaluations and join_reduces.