Hoare powerset domain widening doesn't guarantee ascending chain condition and more

Links

In my attempt to understand the Hoare powerset domain (SetDomain.Hoare) used for path-sensitivity I happened upon the following:

• some slides from Miné (slide 20),
• and referred from those: Bagnara et al. Widening Operators for Powerset Domains.

Issue

Our current widening is implemented as follows:
https://github.com/goblint/analyzer/blob/08316c5560b1c1298d8b0b29af4b076f12de0eb5/src/domains/setDomain.ml#L623-L628
This corresponds exactly to Definition 7 from the latter paper. However, it is only called an "extrapolation heuristics" and not "widening" because it doesn't guarantee the ascending chain condition. So we don't do true widening there.

Possible fix

The same paper also presents three different generic proper widening operators for such a domain using the inner domain's widening. Implementing any of them might not be straightforward though because they all require some kind of additional operator.

Merging in Hoare domains

The paper also discusses merging of elements in a Hoare set. Therefore such notion seems closely related but Goblint has multiple different Hoare powerset domains with quite different characteristics:

1. Path-sensitivity lifter (PathSensitive2) domain is defined through SetDomain.Hoare with additional joining of elements wrapped around in join_reduce through should_joins from inner Specs.
2. AddressSet domain is defined through SetDomain.HoarePO but the partitioning of elements into joined sets is deeply encoded into HoarePO through questionable means. It assumes the inner domain's operators (e.g. join) only act on elements which should be joined and raise Lattice.Incomparable on anything else. From what I understand, this just encodes a should_join-like query through exceptions while making no sense as a lattice (two elements can always be joined).
3. EDIT: PartitionDomain.Set and PartitionDomain.Make also use Hoare ordering and seem to use a special collapse function to do joining. This ends up in region analysis domain.
4. EDIT: PartitionDomain.SetSet seems to largely duplicate the behavior of the above partition domains although doesn't explicitly contain a merging function (or it is implicit). This ends up in vareq analysis domain.
5. EDIT: SetDomain.SensitiveConf is some old and unused path-sensitivity domain that also uses Hoare ordering.
6. EDIT: Historically PathSensitive2 was directly implemented as a Hoare-like domain before 5f5d8f88b1c8a08c6fb82ed79032d5f409edf415.

If the should_join-like operator is passed to a hoare powerset domain functor and the merging of elements by equivalence is moved to a single place, a single implementation should do. It would remove the need for exception-based control flow hacks while allowing an optimized bucket-based Hoare domain implementation to still be used.