Multiset domain for recursive must-locksets

[sim642]

#1073 introduced multiplicity counters for recursive mutexes in must-locksets. As hinted in #1073 (comment), this is simply a multiset domain. However, the implementation keeps a map of multiplicities in addition to the existing must-lockset..

During #1430, which enforces additional correctness via type-safety, numerous unsoundness issues have already been revealed:

1. pthread_mutex_lock(&m[i]); // may lock m[1]
   pthread_mutex_lock(&m[j]); // may lock m[1] recursively
   pthread_mutex_lock(&m[0]); // must lock m[0]
   pthread_mutex_unlock(&m[k]); // may unlock m[0]
   // m[0] should not be in must-lockset here!

2. pthread_mutex_lock(&m[0]); // must lock m[0]
   pthread_mutex_unlock(&m[i]); // may unlock m[0]
   pthread_mutex_lock(&m[0]); // must lock m[0]
   pthread_mutex_unlock(&m[0]); // must unlock m[0]
   // m[0] should not be in must-lockset here!

(Full regression tests on the mutex-recursive-unsound branch.)

I will fix these in #1430, but a clean multiset-based solution is needed to avoid futher/future instances of unsoundness. The key reason for unsoundness in these cases is that must-locksets have special add and remove behavior:

analyzer/src/cdomains/lockDomain.ml

Lines 42 to 56 in 3eee39f

	let add ((addr, _) as lock) set =
	match addr with
	| Addr.Addr mv when Addr.Mval.is_definite mv -> (* avoids NULL *)
	add lock set
	| _ ->
	set
	let remove ((addr, _) as lock) set =
	match addr with
	| Addr.Addr mv when Addr.Mval.is_definite mv -> (* avoids NULL *)
	remove lock set
	| _ ->
	filter (fun (addr', _) ->
	Addr.semantic_equal addr addr' = Some false
	) set

The Multiplicity map does not, but should. However, duplicating the same logic and keeping it in sync in two data structures is error-prone. A multiset domain would avoid that.

The overhead of storing multiplicity 1 for each non-recursive must-lock is negligible, because it's just one int for each must-lock and our must-locksets are very small.