ThreadEscape: Collect flow-insensitive set of variables reachable from globals

[jerhard]

In #1074 it was discovered that in the analysis it is not communicated to a thread that variable may escape (via a global), after the thread has been created.
Previously, the analysis was adding variables that may become reachable via the argument passed to pthreadcreate. This does not take into account that the escaping after the thread creation may also happen via global variables.
This PR collects variables that are assigned to global variables separately under a flow-insensitive variable global_var.
In the threadenter, the set of variables escaped to globals, that was collected flow-insensitively, is then joined into the local state.

This increases the imprecision of the escape analysis, due to the flow-insensitive nature of the handling of variables escaped via globals. Such variables will be considered escaped even in unique threads before they have actually escaped.

Fixes #1074.

[michael-schwarz]

Two ideas:

• Can we maybe add the thread id of the thread that caused it to escape? Then we would still be able to consider things as not escaped when it is known that that has not happened yet.
• is threadenter ever called for the main thread, i.e., does it also see these things that escaped?

[jerhard]

is threadenter ever called for the main thread, i.e., does it also see these things that escaped?

No, actually not. Another issue with the approach of retrieving the variables escaped via globals and the thread-create-parameter in the threadenter: when the set of escaped variables changes at the threadenter edge, everything happening in the thread has to be recomputed. Instead of variables escaped via globals at the threadenter, one could instead think of checking whether a variable has escaped by looking it up in the flow-insensitive invariant when queried.
A possible advantage of doing this over incorporating the escaped variables at the thread start could be fewer dependencies at the threadenter edge.

Can we maybe add the thread id of the thread that caused it to escape? Then we would still be able to consider things as not escaped when it is known that that has not happened yet.

This should be doable in principle, although I fear it may be quite expensive on larger programs. For sv-comp style code it may be worth doing though.

[jerhard]

Closed in favor of #1078