Optimize and refactor "Hoare" domains

[sim642]

Related to issues #101 and #803.

TODO

• Benchmark on sv-benchmarks.
• Check performance on SQLite.
• Fix termination issue when SetDomain.Joined is used inside AddressDomain?
• Reimplement HoareDomain.MapBot for witness generation?
• Adapt to Limit address sets to include at most one string pointer  #808.
• Rename SensitiveDomain to BucketSetDomain or something?

[michael-schwarz]

I added a few minor comments here and there, but overall I think this is a great step in the right direction. It looks like our various HoareDomains now have a sound footing in theory, so they'll hopefully cause no more issues (or if they do, it is much better understood than what we currently had)

[michael-schwarz]

Does this PR also attempt to fix tests 02/{91, 92, 92} that are also closely related to the address domain?

[sim642]

Does this PR also attempt to fix tests 02/{91, 92, 92} that are also closely related to the address domain?

Not at all. On the contrary, it makes the problem even worse since previously a and a[0] were more-or-less handled equivalently but now they're split into separate buckets. Same with the a and a.fst pairing. So this makes #822 even more obvious and urgent.

[sim642]

On the contrary, it makes the problem even worse since previously a and a[0] were more-or-less handled equivalently but now they're split into separate buckets. Same with the a and a.fst pairing.

I just added the tests for these easier cases as well, which aren't listed in #822. Turns out that the first field one actually accidentally still works due to some of those special cases in lval domain still being present (and thus considering the two buckets, which are represented by themselves, equal). It doesn't work for the zero index since there the index gets turned into top for the bucket representative.