Clean up library function spawning in base analysis

[sim642]

Since #1029 is now done, it should be possible to clean up this TODO:

analyzer/src/analyses/base.ml

Lines 2169 to 2173 in 3ad6b39

	| _, _ when get_bool "sem.unknown_function.spawn" ->
	(* TODO: Remove sem.unknown_function.spawn check because it is (and should be) really done in LibraryFunctions.
	But here we consider all non-ThreadCreate functions also unknown, so old-style LibraryFunctions access
	definitions using `Write would still spawn because they are not truly unknown functions (missing from LibraryFunctions).
	Need this to not have memmove spawn in SV-COMP. *)

[michael-schwarz]

The other question is whether it really is the base analysis that should handle spawns and whether it is not better to move this to the same level where also function calls are handled?

[sim642]

That's a good point and would make sense architecturally.
I don't know if there's any technical complication when doing so. Or perhaps there was in the past when the OSEK/ARINC stuff was till around, but perhaps not anymore.

But now I started thinking about how it interacts with path-sensitivity. If it happens at the outermost level, then it's outside of path-sensitivity and queries for the points-to set lose the relation between the path and the possible values of the function pointer.
And it seems like the same could happen with normal function pointer calls, so maybe we already have that issue and never realized it (because function pointer calls are relatively rare?).

[michael-schwarz]

I think this paths as set thing is somehow used to work around this?

[sim642]

I know it's used for some part of it (relating enter and combine perhaps?), but I'm no longer sure if it's used all the way.

In particular, if there are two paths with {fp → {&f}} and {fp → {&g}}, then I think there's a single points-to query for fp, which must return {&f, &g} and then we'd still be trying to call g from the first path.

I could look into these things next week when I'm back from my small vacation. Or is the thread spawning aspect being independent of base relevant for #2012?

[michael-schwarz]

Seems like you are right, and it's really only then enter and combine where this is used. Interesting that we never came across it, it can make quite the difference.

No, it's not really urgent for #2012: I first tried to do the entire thing with base disabled, and was a bit surprised why no new threads were created despite a call to pthread_create. But I have found a way to configure base so it ensures the spawning happens and still doesn't know the property that is to be established. Enjoy your vacation!