Fix longjmp crash on Uninitialized

[sim642]

On concrat/pigz the longjmp analysis crashes because it takes a jmp_buf out from a pthread_getspecific which currently gives top results.
This PR replaces the crash with a message and a top value.

[sim642]

The crash on longjmp is fixed but apparently this doesn't still become reachable?

[michael-schwarz]

Returning top here doesn't make code that is otherwise unreachable reachable iirc... I think this is a fundamental limitation that I am not sure how to address best.

[sim642]

I thought a top jmpbuf would just jump back to every setjmp without filtering by node/context, but apparently all we do is warn:

analyzer/src/framework/constraints.ml

Lines 1664 to 1666 in 5cc4811

	let handle_target target = match target with
	| JmpBufDomain.BufferEntryOrTop.AllTargets ->
	M.warn ~category:Imprecise "Longjmp to potentially invalid target, as contents of buffer %a may be unknown! (imprecision due to heap?)" d_exp env

Maybe we should have an option to do that?

[michael-schwarz]

The problem is a bit where one wants to propagate things to... Just up the call stack, assuming the invocation was not UB? Also down the callstack because someone might be trying to implement co-routines? Also to completely unrelated places?
The other problem is that quite often the local state propagated somewhere because of an unknown longjmp will not be suitable for incorporation by join, as it is incorporated into an unsuitable function. This might lead to a huge precision loss.
My idea would be to leave this as is, but make this type of warning one of the severe top-level warnings that is reported separately at the end of the analysis (in the sense of #1190 ).

[sim642]

The problem is a bit where one wants to propagate things to... Just up the call stack, assuming the invocation was not UB? Also down the callstack because someone might be trying to implement co-routines? Also to completely unrelated places?

To the same places we normally do: in the same function and up the call stack. It could just be that all setjmps incorporate the unknown jump target instead of the same node and context check that normally happens. So unknown jump buffer would mean "all jumpbuffers that we normally could jump to".

The other problem is that quite often the local state propagated somewhere because of an unknown longjmp will not be suitable for incorporation by join, as it is incorporated into an unsuitable function. This might lead to a huge precision loss.

Of course it would be very imprecise, but I'm not sure if it'd cause anything incompatible per se. Ambiguous longjmps to multiple possible targets should be similar. The compatibility is ensured by each upwards propagation of the jumps doing the appropriate returns and combine_envs.

My idea would be to leave this as is, but make this type of warning one of the severe top-level warnings that is reported separately at the end of the analysis (in the sense of #1190 ).

I added that, so let's leave it at that.

[michael-schwarz]

To the same places we normally do: in the same function and up the call stack.

In this case, the clean solution would be to warn and then replace the top set of possible targets with the set of legal jumptargets (which we have at hand anyway), which indeed seems reasonable and also prevents any issues with propagation to ill-suited locations.