Add unknown thread ID #1224
Add unknown thread ID #1224
Conversation
It is not an analysis we currently have, but e.g. for an analysis trying to detect the case where thread may be joined multiple times by the same thread, one could imagine tracking may-joined threads - in this case if I find that a specific thread id is in that set in could issue a warning with a higher confidence as opposed to the case where only the unknown thread id is there. |
It's a slippery slope to do things for hypothetical analyses because it has a performance impact right now. A set of known threads in addition to unknown can increase, creating even more contexts that we all analyze identically with existing analyses. We already have issues with contexts exploding on real-world programs (including on not-so-large Concrat ones), so we're just shooting ourselves in the foot performance-wise with absolutely no benefit right now. The soundness fixes here also work with the current |
Yes, this is certainly true. However, I think having a clean solution, that, e.g., coincides with the solution we have for pointers is preferable to these potential gains here. Also, if we encounter such contexts being problematic in the future, we could still always opt to construct contexts in a different way that do not admit this blowup. This is the beauty of having completely decoupled contexts from local values by giving up on simulating the side-effect free formulation of function-calls. |
|
As soon as the conflict with master is resolved, I think we can merge this. |
| @@ -2372,6 +2372,7 @@ struct | |||
| | Int n when GobOption.exists (BI.equal BI.zero) (ID.to_int n) -> st | |||
| | Address ret_a -> | |||
| begin match eval_rv (Analyses.ask_of_ctx ctx) gs st id with | |||
| | Thread a when ValueDomain.Threads.is_top a -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var] | |||
There was a problem hiding this comment.
In light of #1264, this and the other invalidates for ThreadJoin should also be shallow I think. pthread_join writes the return value, but doesn't dereference its previous value for writing (it even can't because it's void*).
|
CI failure is unrelated. |
Relates to #392.
ThreadIdDomain.ThreadSetDomainwithUnknownThreadelement as top instead ofToppedSetforThreadSetinconcDomainUnknownThreadelement toThreadSetwhen invalidating. Fixes an unsoundness issue and adds a test case.However, I am not too sure what having an
UnknownThreadelement and preserving other thread IDs in the set is good for. I could not find a case where this would improve our precision. Maybe others have ideas?