Refactor must-locksets to use definite mvals instead of addresses

[sim642]

Currently must-locksets are (reversed) sets of addresses, which can be the usual addresses (as mvals), but the type also allows UnknownPtr, NullPtr and StrPtr. None of these should be in must-locksets, but currently this is enforced by the combination of three different checks in three different files.

The goal of this PR is to refine the type of must-lockset elements from addresses to mvals with definite indices, whereby this correctness property is enforced by the type system.
This immediately paid off: it revealed two cases of unsoundness in recursive mutex handling because definite indices were only checked for the must-lockset, but not for the recursive locking counter map (which must duplicate all the set logic to avoid becoming unsound). See #1432.

Hopefully this also allows some Addr wrapping and unwrapping to be avoided, which should be less verbose.

TODO

• Enforce definite indices in must-locks by type.
• Rename Simple.
• Add all and is_all operations to Simple.
• Fix NULL warning in cram test.

[sim642]

This goes quite a long way to clean things up, but not as far as I would've liked. The oddity is that privatizations get the mutex as an AddressDomain address, which can still be any of the odd things (UnknownPtr, NullPtr or ambiguous index).

@michael-schwarz What are privatizations supposed to do with those? It seems to me that we completely forgot about the non-definite possibilities, which might make things even unsound. Privatizations may have to be adapted to behave more like the must-lockset analysis: only lock definite addresses and unlock should unlock all semantic_equal addresses in case of non-definite.

[michael-schwarz]

What are privatizations supposed to do with those? It seems to me that we completely forgot about the non-definite possibilities, which might make things even unsound.

I think I considered this issue when designing the privatizations. They should still be sound for the original setting according to the following arguments:

• For lock & mine-W: Incorporating too many values early makes the analysis imprecise, not unsound; All other operations are based on must-locksets, and for background locksets and minimal locksets only definite elements are kept
• For write: lock is a no-op, other actions are based on must-lockset
• For per-mutex flavors incl. relational & protection-based: Protection by one of these indefinite addresses means they are always held when the global is accessed, so that is not harmful either

However, these are indeed a bit shaky in some places and may easily be subject to breakage. So in the long run, it does make sense to refactor this as well.

Also, with the new additions such as atomic and invariants about unprotected globals, I'm not sure if this still all holds.