Refactor bot of threadJoins analysis to mean uncomputed

[Copilot]

The bu solver triggers Lattice.Invalid_widen when threadJoins is active because man.global tid returns bot() before contributions arrive — and MustThreadSet.bot() was {UnknownThread}. Widening then fails because leq doesn't treat UnknownThread as a universal element in the reversed lattice.

Core change

(* before *)
module MustThreadSet = SetDomain.Reverse (ThreadSet)

(* after *)
module MustThreadSet = SetDomain.Reverse (SetDomain.ToppedSet (ThreadIdDomain.FlagConfiguredTID) (struct let topname = "All Threads" end))

• Removes UnknownThread from the element type entirely; elements are now FlagConfiguredTID.t
• bot() becomes the proper Top sentinel (all threads must-joined = unreachable), not the semantically broken {UnknownThread}
• Fixes leq / widening by eliminating the element that had no coherent must-join semantics

[michael-schwarz]

This hopefully fixes all the issues in the forward solver (the AI version did, I just re-structured code from that a little to get less duplication).

[Copilot]

Pull request overview

This PR updates the must-joined threads domain to avoid Lattice.Invalid_widen in the bu solver when threadJoins is enabled by replacing the prior “{UnknownThread} as bot” encoding with a proper reversed topped set over FlagConfiguredTID.

Changes:

• Redefine ConcDomain.MustThreadSet as Reverse (ToppedSet FlagConfiguredTID) to give a coherent bottom/top meaning for must-joined semantics.
• Adapt downstream analyses to pattern-match Thread ft and operate on FlagConfiguredTID.t elements.
• Introduce ThreadSet.diff_mustset to subtract a MustThreadSet from a ThreadSet in call sites that previously used ThreadSet.diff.

Reviewed changes

Copilot reviewed 9 out of 9 changed files in this pull request and generated 3 comments.

Show a summary per file

File	Description
src/cdomain/value/cdomains/concDomain.ml	Redefines MustThreadSet and adds ThreadSet.diff_mustset helper.
src/cdomains/mHP.ml	Switches MHP state to MustThreadSet and updates membership/existence logic accordingly.
src/analyses/threadJoins.ml	Updates join/clean logic to use MustThreadSet element type and reversed lattice semantics.
src/analyses/useAfterFree.ml	Adjusts must-joined membership check to unwrap Thread ft.
src/analyses/threadId.ml	Uses diff_mustset when checking “single-threaded” based on joined threads.
src/analyses/mHPAnalysis.ml	Updates printing predicate to use MustThreadSet.
src/analyses/creationLockset.ml	Uses diff_mustset to remove must-joined tids from possibly-running sets.
src/analyses/basePriv.ml	Uses diff_mustset to avoid re-joining already must-joined threads in forced join path.
src/analyses/apron/relationPriv.apron.ml	Mirrors basePriv.ml change for Apron relation privatization.

---

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

[michael-schwarz]

This is now much more refactoring than I had hoped to do, but it should be a clean solution.

[sim642]

I force pushed a bit of interactive rebase here to clean up the Copilot history a bit but keep the manual parts still separate (instead of squashing everything).