Add ana.base.strings.domain option and unit string domain

[sim642]

In goblint/bench#62 (comment) I noted:

One possible reason for so many contexts with ana.base.context.non-ptr disabled could be string literals (StrPtr) in address sets, which would be preserved in contexts. ana.base.limit-string-addresses (true by default) doesn't do enough limitation. When true, string literals are handled like a flat lattice (a la constant propagation), which still yields separate contexts for all different calls with string literal arguments. When false, string literals are handled as a set.

It would be possible to do even more limiting: not track any string literals, i.e. use a unit domain for them. I hacked it by making of_string always return StrPtr None. This at least got rid of many contexts for some functions, but not all.

This PR implements that hack more cleanly by extracting a StringDomain module and introducing the option ana.base.strings.domain with three possible values:

1. disjoint corresponds to ana.base.limit-string-addresses false.
2. flat corresponds to ana.base.limit-string-addresses true.
3. unit corresponds to the new even more imprecise domain with no information at all.

[michael-schwarz]

I would strategically propose to delay this until @nathanschmidt can integrate his PR #1076 and potentially also #1118, as these will significantly extend the string domains, and the interface that is needed will hopefully be more clear after this (though I am not sure how significant the overlap is between these two issues here anyway).

@nathanschmidt could you comment with an estimated timeline for addressing the comments on the PRs? Iirc you said no earlier than this week?

[sim642]

Neither of those has to do with the StrPtrs in AddressDomain though: one modifies array domains and the other adds a new relational analysis. So they're orthogonal and there's no conflict.

Right now, the big problem for us analyzing real-world programs is performance, not imprecision. Already given #1126, it's beneficial to have the ability turn off all these new things. We're shooting ourselves in the foot on real-world programs if the analyses keep getting more expensive without a choice.

[nathanschmidt]

@nathanschmidt could you comment with an estimated timeline for addressing the comments on the PRs? Iirc you said no earlier than this week?

@michael-schwarz I currently have quite some time constraints, but I plan to have a look next week.

[michael-schwarz]

As I have been delayed with #1076 and #1118, I think it might make sense to merge this before those. Given that this does not change the behavior for SV-COMP, I'd be open to merging it even before Nov 22.