Fix unknown thread invalidation ordering

[michael-schwarz]

Summary

Fix relational invalidation for unknown spawned functions.

The thread-create result and the unknown thread argument were invalidated in separate thread initialization snapshots. Joining those relational snapshots could introduce a spurious relation between the independently invalidated globals, causing an invalid witness invariant to be confirmed when side widening was disabled.

Apply the unknown function invalidation in threadspawn, where the caller state already contains the invalidated thread-create result. For the first spawn, publish this combined state as the initialization snapshot; later spawns use ordinary privatized writes. threadenter now only initializes the child privatization state.

The regression test disables side widening and independently checks both invalidated globals in addition to the previously spurious relational invariant.

Closes #2098

[sim642]

The thread-create result and the unknown thread argument were invalidated in separate thread initialization snapshots.

What is a "thread-create result"? Is it the resulting abstract state, or is it the lvalue of pthread_create?
EDIT: Or the thread ID assignment?

And what are "thread initialization snapshots"?

Joining those relational snapshots could introduce a spurious relation between the independently invalidated globals, causing an invalid witness invariant to be confirmed when side widening was disabled.

Does "joining" mean something other than join here? There's no join in this code.

[michael-schwarz]

What is a "thread-create result"? Is it the resulting abstract state, or is it the lvalue of pthread_create?

It's the lvalue of the pthread create, so in g = pthread_create(...) it is the g.

[michael-schwarz]

And what are "thread initialization snapshots"?

It's the values published to V.mutex_inits in Priv.enter_multithreaded.

Does "joining" mean something other than join here? There's no join in this code.

It's about the LRD.join that happens for values at V.mutex_init.

The problem is that the invalidations of the things reachable via the argument and the invalidation of the lval happened separately. So in one, you have

A: e ∈ [INT_MIN, INT_MAX], f = 0
B: e = 0,                 f ∈ [INT_MIN, INT_MAX]

The join then gives you f + 2147483648 >= e which holds in both.

[michael-schwarz]

For

e = pthread_create(&t, NULL, b, &f);

the current code works as follows:

1. threadenter constructs the complete child state, including its thread ID.
2. For unknown b, S.special runs on that child state and invalidates memory reachable from &f.
3. The child state is synchronized, publishing the invalidation under the child's thread digest.
4. The call-result lvalue e is passed through man.spawn and stored in the framework's pending-spawn record as result_lval. It is kept separate from the thread-handle lvalue t.
5. S.threadspawn runs for the creator. The thread-flag analysis emits EnterMultiThreaded, which invokes each analysis's normal event handler and therefore its Priv.enter_multithreaded.
6. After S.threadspawn returns, the framework applies an ordinary Events.Assign to the retained result_lval, invalidating e under the creator's digest.

Priv.enter_multithreaded is no longer called explicitly by Base or Apron because the existing EnterMultiThreaded event now occurs at the correct point and performs that transition uniformly for all analyses.

This ensures that f is invalidated using the completed child context, while e is invalidated only after the creator has entered multithreaded mode. The invalidations are ordinary writes attributed to the correct threads, avoiding the separate initialization snapshots whose relational join previously retained the spurious invariant.