Various XCFA improvements

[csanadtelbisz]

This PR adds proper data race support, a refactored mutex (fence) handling, new error property management, a new complex portfolio, and several minor changes and fixes mainly to the xcfa subprojects.

Data race checking is now preceded by a quick and smart static check that lists the potential racing global variables and memory locations. If none is found, data race is not possible. A reduction of the data race problem to reachability is also added as an xcfa procedure pass: this enables other analyses (such as OC checker or analyses based on the monolithic expression) to analyze data race.

Mutex handling has been refactored: separate XcfaLabels have created for the different fence labels to avoid the string hacking when handling a FenceLabel that we have had previously. The way we handle mutexes has also been generalized by introducing blockingMutexes, acquiredMutexes, and releasedMutexes that give enough room to implement the semantics of different mutex types (such as simple pthread mutexes, read-write locks, etc.). Still, only static mutex handles are supported though it seems fairly easy addition to add full mutex support now (with potential reassignments of mutex handle variables).

The error property is managed by separating the input (immutable) and verified (mutable) property. Algorithms (mostly xcfa frontend passes) that perform a specification transformation modify the verified property to the new property. This way for example, we do not need the obscure and unintuitive state error predicates for all properties (e.g., false for no-overflow): analyses can focus on the properties that they natively support, and it is the responsibility of the transformation steps to properly set the verified property. I tried to refactor all cases correctly (whether they need the input or verified property), but please thoroughly check all changes, especially the ones related to witnesses. Also, as far as I can see, overflow checking is mostly engraved into the frontend xcfa builder rather than a separate pass (though the error/final loc passes also use the information if we check overflow). Thus, I put the verified property update in FrontendXcfaBuilder.

A new portfolio is added which is a slightly refactored form of the previous stable portfolio. Most notable changes include ones related to concurrent program verification. The portfolio is expected to be improved further this month before SV-COMP'26.

Since ReadLabel and WriteLabel in Xcfa were not maintained (practically, it was never supported at all), it is removed. Therefore, the litmus2xcfa tests are commented out, as they need read and write labels for parsing. We should either remove those litmus tests or add proper support for read&write labels in the future.

Atomic blocks are removed from around atomic variable accesses as it is not needed anymore.

[csanadtelbisz]

Apart from the SonarQube analysis failing, this PR is ready to merge on my part. Please review it.

As for the SonarQube analysis:

• coverage not sufficient: I think that Sonar is simply wrong (e.g., it reports 0% coverage on DataRaceUtils.kt, however, its method isDataRacePossible is directly called in the unit test XcfaDataRaceTest, and I expect a very high coverage for this file in fact)
• high duplication is due to adding a new portfolio which naturally contains a lot of duplication: I think we can ignore this condition in this PR (maybe we should exclude the directory of portfolios from duplication check if Sonar allows it)

[sonarqubecloud]

Quality Gate failed

Failed conditions
11.3% Duplication on New Code (required ≤ 5%)

See analysis details on SonarQube Cloud

[leventeBajczi]

Thanks for the updates! Since it doesn't seem to make anything go horribly wrong in the tests, I'm happy to approve.