Relational: Use same invalidation strategy as base #1646
Conversation
michael-schwarz
added
bug
precision
relational
|
|
| (* TODO: HACK: Simulate enter_multithreaded for first entering thread to publish global inits before analyzing thread. | ||
| Otherwise thread is analyzed with no global inits, reading globals gives bot, which turns into top, which might get published... | ||
| sync `Thread doesn't help us here, it's not specific to entering multithreaded mode. | ||
| EnterMultithreaded events only execute after threadenter and threadspawn. *) | ||
| if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man)) then | ||
| ignore (Priv.enter_multithreaded (Analyses.ask_of_man man) man.global man.sideg st); |
There was a problem hiding this comment.
Why is this moved out? Base only does it for non-unknown thread functions.
There was a problem hiding this comment.
The logic of why it is needed is the same here as it is for the case where a known thread is created: One should not go into multi-threaded mode without notifying the privatization that this switch happened to ensure everything that should be published is published.
Maybe base has some reason this can be avoided, but I'm not really sure why that should be the case. We may want to make an issue to investigate this.
There was a problem hiding this comment.
Also see the last few comments in #1551
There was a problem hiding this comment.
The one test in this PR doesn't cover this, does it?
I tried the very simple thing of creating a thread from unknown function pointer and that seems to work with base. That's because threadflag analysis emits the EnterMultiThreaded event which is handled by base (and relational).
The comment for this hack is about the globals values that get used when analyzing the created thread. For an unknown function pointer, there's no thread body to analyze anyway, so it's not clear to me when it would make a difference.
There was a problem hiding this comment.
The test covers it in some sense. We mean to invalidate e and output
[Info][Imprecise] Invalidating expressions: & e (1.c:11:3-11:35)
But this invalidation does not take and we still claim to be able to prove things about e.
There was a problem hiding this comment.
Edit: That case is listed in the linked issue.
Co-authored-by: Simmo Saan <[email protected]>
Closes #1535