Refactor and fix different lockset analyses

[sim642]

We have at least three lockset analyses:

1. mutex – must locksets,
2. maylocks – may locksets,
3. deadlock – may locking events (locks with location).

These could be combined into a single framework, where Lock and Unlock events work for all of them.

---

We don't have a maintained may lockset analysis. Besides the deadlock analysis keeping its own may locks events, we also have some ancient maylocks analysis, which is very outdated compared to mutex analysis. With path-sensitivity they should almost always coincide.

The case code you linked is just the tip of the ice berg though of a more general issue that we need to refactor our must/may lockset analyses. Ideally the Lock/Unlock events would be emitted the same regardless and the difference is just in whether the local domain is reversed or not. For example, both mutex and maylocks analyses could be just instantiated from a functor with local domains having locksets with differing lattice orderings. And similarly this deadlock analysis would just instantiate it with a may lock events set.

The code you point out isn't just a problem for the deadlock analysis, but probably also some privatizations, where we require mutex path-sensitivity to avoid the may-must distinction. With ambiguous lockings the code avoids any events altogether (which is just appropriate for must locksets), but then we also lack any path-sensitivity accounting for the actual possibilities, which in turn could make such privatizations unsound.

Originally posted by @sim642 in #655 (comment)