Split memLeak paths with sem.malloc.fail

[sim642]

Closes #2093.

TODO

• sv-benchmarks.

[michael-schwarz]

Could you explain why path-sensitivity is the right tool here?

[sim642]

Sure, it wasn't my first idea either.

Initially I thought I'd just replace the handling of free here:

analyzer/src/analyses/memLeak.ml

Lines 207 to 217 in 3062271

	| Free ptr ->
	begin match man.ask (Queries.MayPointTo ptr) with
	| ad when (not (Queries.AD.is_top ad)) && Queries.AD.cardinal ad = 1 ->
	(* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *)
	begin match Queries.AD.choose ad with
	| Queries.AD.Addr.Addr (v,_) when man.ask (Queries.IsAllocVar v) && man.ask (Queries.IsHeapVar v) && not @@ man.ask (Queries.IsMultiple v) ->
	ToppedVarInfoSet.remove v man.local
	| _ -> man.local
	end
	| _ -> man.local
	end

In particular, to do the natural thing of joining states over all points-to targets. But the sound thing to do in the NullPtr case is to remove nothing, so that wouldn't help in such a case.

And matching 2-element points-to sets which contain such a removable pointer and NullPtr to remove the variable also wouldn't be sound. The NullPtr in the points-to set might've come from somewhere else, not the failing allocation. So NullPtr might still be in there if the allocation succeeded and there's memory that still needs to be cleaned up.

The memLeak analysis is already path-sensitive w.r.t. its whole local state of allocated variables that still need to be freed, so this additional splitting seems to be the right way. Hopefully, the additional paths with NULLs are very short-lived: existing and adapted sv-benchmarks do an abort() close to the failed allocation.