Refactor mutex analyses

[sim642]

Closes #659.

Changes

1. Add mutexEvents analysis to emit events handled by mutex, mayLocks and deadlock analyses.
2. Replace analysis-specific ambiguous lock pointer handling with path splitting via ctx.split. One split is introduced for each possible mutex pointer. Joining of paths automagically takes care of the ambiguity (see table below).
   This also increases the precision of locking an ambiguous lock pointer in the path-sensitive mutex analysis: previously no must locks were added, but now it properly splits into multiple paths with different locksets.
3. Add more complete handling of failing locks (includes try locks) by just having an extra path split via ctx.split if failure is allowed. Again, the joining of paths takes care of everything by considering the extra path where no lock was acquired,
4. Add more complete handling of blob locks via IsMultiple query (see table below). This should additionally account for weakly updated locals too.
5. Add more complete handling of unknown lock pointers using Addr.UnknownPtr (see table below). Previously lockset analyses just dropped these from the MayPointsTo query result conversion.
6. Fix deadlock detection w.r.t. ambiguous, blob and unknown lock pointers.
7. Extract very simple must and may lockset analysis functors and instantiate mutex, maylocks and deadlock analyses using these.

Behavior

The following tables give an overview of all the cases that are now considered.

Must lockset

	Definite pointer	Ambiguous pointer	Blob pointer	Unknown pointer	Failing lock
Lock	Add pointer	Don't add any	Don't add	Don't add	Don't add
Unlock	Remove pointer	Remove all ambiguous pointers	N/A (never added)	Remove all	N/A

May lockset

	Definite pointer	Ambiguous pointer	Blob pointer	Unknown pointer	Failing lock
Lock	Add pointer	Add all ambiguous pointers	Add blob pointer	Add unknown pointer	Add
Unlock	Remove pointer	Don't remove any	Don't remove	Don't remove any	N/A

TODO

• Add unknown mutex pointer handling for both must and may locksets.
• Make failing locks emit all events.
• Fix mayLocks and deadlock unlocking.
• Determine whether MustLock and MustUnlock events are still necessary.
• Merge Reimplement deadlock analysis and extend with MHP #655.

[sim642]

• Determine whether MustLock and MustUnlock events are still necessary.

The only difference that these still provide is that when the general Lock is emitted, MustLock is emitted conditionally:

analyzer/src/analyses/mutexAnalysis.ml

Lines 17 to 19 in d805791

	let nls = D.add l ctx.local in
	if not (D.equal ctx.local nls) then
	ctx.emit (MustLock (fst l));

Removing that relocking condition causes a failure in just one test: 13-privatized/70-mm-reentrant.

At first sight it seems like a reasonable thing to do: only emit MustLock when it's not already locked. But that relocking check is itself based on must locksets. If the mutex isn't already must locked but may locked, then it is treated as if it wasn't locked at all, which doesn't account for the possibility that it might have been already locked. In such scenario we don't know whether it's the first locking or relocking.

Actually emitting MustLock events like this isn't even necessarily right, because in the case of ambiguity or failure, the particular split path still sees the MustLock event, although the following path join might remove it from the must lockset. So this event cannot even guarantee anything. It's similar to the whole branched thread creation and EnterMultithreaded event problem in that a later join would have to account for events that along some path didn't happen.

Therefore I'm unsure whether this is even the right thing to do. Proper handling of recursive locks is a whole other issue #658.

---

EDIT: I managed to get rid of those events by just adding the recursive locking check into mutex-oplus and mutex-meet specifically to make them sound on that test, others were already correct.

[michael-schwarz]

EDIT: I managed to get rid of those events by just adding the recursive locking check into mutex-oplus and mutex-meet specifically to make them sound on that test, others were already correct.

Would the apron mutex meet not also require such special handling then?