Refactor race warnings (accesses) to use global invariant on master

[michael-schwarz]

This is merging #397 into master, such that conflicts with #518 can be resolved there instead of having to be resolved together with all the changes originating from the interactive analysis.

I think we're not yet at the point to merge #391 entirely, but I suppose I could merge #397 also to master now to allow those conflicts to be solved already here instead of leaving more conflicts to be merged for #391.

Originally posted by @sim642 in #518 (comment)

[sim642]

@michael-schwarz Since you opened this PR, it seems like GitHub doesn't let me request a review from you, but I think I managed to get this ready for master. I also cherry-picked a bunch of other commits and changes from interactive surrounding this, hopefully didn't miss anything important, because this also now contains the change of using non-varinfo global constraint variables for the access analysis. That wasn't part of #397 originally.

[sim642]

Hmm, 00-basic/06-threadid from the interactive tests does fail now with the incremental run detecting a race:

[Warning][Race] Memory location [email protected]:4:5-4:13 (race with conf. 110):
  write with {thread:([t_fun@./tests/incremental/00-basic/06-threadid.c:21:3-21:40, main], {})} (conf. 110)  (exp: & myglobal) (./tests/incremental/00-basic/06-threadid.c:7:3-7:14)
  write with {thread:([t_fun@./tests/incremental/00-basic/06-threadid.c:24:3-24:40, main], {})} (conf. 110)  (exp: & myglobal) (./tests/incremental/00-basic/06-threadid.c:7:3-7:14)

I think the problem with that is that without restarting globals (which is done on interactive), the set of accesses that's now in the global invariant doesn't get cleared and thus the access with the old thread ID remains in the set and appears to race with the new one.

Not sure if anything can be done about it before #391 itself is merged, so maybe this just needs to be skipped for the time being?

EDIT: Although... On interactive it isn't actually restarting anything either, because only whitespace is changed by the patch and no function is changed. So somehow it subtly does pass there.

[michael-schwarz]

Yes, let's just mark the failing test as //SKIP and then I'd say we're good to merge (after addressing my two questions above).

[sim642]

I didn't investigate it further, but I suspect this failure might be just due to not having incremental warnings here, so even without any changes, postsolving reevaluates everything once and side-effects something spurious (which isn't a verification error because of the G.leq hack of the access analysis) that the incremental warnings do not.