Make signal handler threads unique

[sim642]

While thinking about the signal handler analysis for AnalyzeThat, I realized that we spawn the signal handlers as non-unique threads.
This PR currently adds separate handling for signal handlers to spawn them as unique. Intuitively this seems right but I haven't thought too much about it.

It makes very little difference though: it prevents signal handlers from racing with themselves. Maybe it can also help some privatizations with TIDs.

This might also allow joining the signal handler threads with some extra work: if a new signal handler is installed, then the previous one could be joined.

TODO

• sigaction?

[Copilot]

Pull request overview

This PR updates Goblint’s library modeling of signal() so that installed signal handlers are spawned as unique threads (instead of non-unique), improving precision for analyses where non-unique handler threads caused self-race noise.

Changes:

• Add a new LibraryDesc.special variant (SignalHandler) and use it to model signal(signum, handler).
• Update Base analysis thread-spawn detection to treat SignalHandler as a unique thread spawn (multiple:false).
• Add regression tests covering (1) soundness of asynchronous handler effects and (2) absence of self-races within a handler.

Reviewed changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
src/util/library/libraryDesc.ml	Introduces SignalHandler as a new library “special” classification.
src/util/library/libraryFunctions.ml	Switches signal to a special returning SignalHandler (and notes sigaction TODO).
src/analyses/base.ml	Spawns signal handlers as unique threads in forkfun.
tests/regression/03-practical/37-signal-sound.c	Regression test asserting handler effects make post-signal() checks unknown.
tests/regression/03-practical/38-signal-unique.c	Regression test ensuring no self-race is reported within a handler.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

sigaction still uses the generic unknown descriptor, so installing a handler via sigaction will continue to be treated as spawning a non-unique thread through Spawn accesses. If the intent of this PR is to make signal-handler threads unique in general, consider introducing a SignalHandler-style special for sigaction as well (extracting the handler from struct sigaction), or otherwise documenting why sigaction is intentionally left imprecise/unsound for now.

Suggested change

	("sigaction", unknown [drop "signum" []; drop "act" [r_deep; s_deep]; drop "oldact" [w_deep]]); (* TODO: SignalHandler special *)
	("sigaction", unknown [drop "signum" []; drop "act" [r_deep; s_deep]; drop "oldact" [w_deep]]); (* Intentionally modeled as unknown: signal-handler threads installed via sigaction are treated as non-unique (like generic Spawn). A more precise SignalHandler-style special may be added in the future. *)