Exclude free-free accesses from racing

[sim642]

We quickly looked at a random NoDataRace false positive from our SV-COMP 2023 results and saw hundreds of race warnings with just free accesses.
Since free is thread-safe and the freed memory is not being even read, we could exclude them from our race check.

[sim642]

That might've been too eager. I think the reason we consider free-free as racing is that, even though free itself is thread-safe, the second free on the same location leads to concurrent double-free, which is also undefined behavior. /cc @vesalvojdani

But that makes me wonder, what does the useAfterFree analysis do to exclude some use-after-free and double-free that our general access framework does no?. And maybe that check could just fit into the framework via an access function and A module to provide exclusions more generally? /cc @mrstanb @michael-schwarz

[michael-schwarz]

But that makes me wonder, what does the useAfterFree analysis do to exclude some use-after-free and double-free that our general access framework does not?

It does not do too much extra, except that it checks that the freeing thread may not run in parallel (disregarding mutexes, as that is not relevant for use-after-free and double-free, as free and access do not need to happen concurrently) or have already run. Additionally, for unique thread ids, we locally keep a set of may freed varinfos, that we check if the memory is also freed by the current thread.
It is not immediately obvious how that would fit into the access framework, as the criteria here are different from the one we apply to checking for race freedom.

[michael-schwarz]

the second free on the same location leads to concurrent double-free, which is also undefined behavior

To me, this seems to be an instance of use-after-free instead of really being a race though? If both frees are protected by a mutex m, there's no race but still undefined behavior?

[sim642]

To me, this seems to be an instance of use-after-free instead of really being a race though? If both frees are protected by a mutex m, there's no race but still undefined behavior?

Indeed, but before we had any sort of multi-threaded use-after-free/double-free, this was the best we could do. It's not a data race, but it's a race condition.

It does not do too much extra, except that it checks that the freeing thread may not run in parallel (disregarding mutexes, as that is not relevant for use-after-free and double-free, as free and access do not need to happen concurrently) or have already run.

Which MHP also does for races, so the same sort of checks are duplicated for these different things.

Additionally, for unique thread ids, we locally keep a set of may freed varinfos, that we check if the memory is also freed by the current thread.

I guess this might be the extra bit of information that doesn't go into the access framework. Although I think it easily could as well.

It is not immediately obvious how that would fit into the access framework, as the criteria here are different from the one we apply to checking for race freedom.

It doesn't immediately fit indeed, but it should be possible to generalize a bit to make it fit. Precisely because use-after-free duplicates a lot of the logic already there for accesses in general: including iterating over all memory accesses at every expression and this MHP stuff.
Now having use-after-free analysis, it's easy to exclude the earlier attempts at this from the access/race analysis. In light of #1194, it might turn out to be overly expensive to have two analyses iterating over all the subexpressions of all the expressions in all the statements to collect the accesses.
This is why I'm wondering of use-after-free could piggyback on the existing access framework. Obviously may_race isn't sufficient for that, but may_happen_before might be. It would allow use-after-free to also benefit from other analyses like region/mallocFresh for free.

[sim642]

I cherry-picked the refactoring 23863e5 onto master.
Since #1207 disables free races in SV-COMP anyway, I'm removing this from the milestone.

[sim642]

Closing as unneeded after all. The still-relevant discussion is delegated to #1351.