Refine Points-to-Sets in Base when Splitting Paths for Mutex Analysis

[michael-schwarz]

As proposed by @hseidl and @sim642 yesterday at Gobcon, we should also refine the pointer information in cases where we perform a state splitting for the mutex analysis.

This would allow us to not produce warnings such as

[Warning][Unknown] unlocking mutex (m1) which may not be held
[Warning][Unknown] unlocking mutex (m2) which may not be held

#include<pthread.h>

pthread_mutex_t m1;
pthread_mutex_t m2;

int main(int argc, char const *argv[])
{
    int top;
    pthread_mutex_t* ptr;
    ptr = &m1;

    if(top) {
        ptr = &m2;
    }

    pthread_mutex_lock(ptr);
    pthread_mutex_unlock(ptr); //NOWARN

    return 0;
}

This will be helpful not just for this category of warnings, but will also allow shrinking may-locksets back down, which may be crucial for the deadlock analysis.

[sim642]

Implementation-wise, this is here:

analyzer/src/analyses/mutexEventsAnalysis.ml

Lines 33 to 35 in 9023dc8

	let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in
	Queries.AD.iter (fun e ->
	ctx.split () [sb; Events.Lock (e, rw)];

In addition to emitting a SplitBranch event about the lock operation return value, another event could be emitted about its argument.